OAI/GroupTheory/PolycyclicRecognition/Analysis/BasepointAffineSeparation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.affine_labels_offsets_of_chart_transport line 16

   Source documentation

   Comparing transported affine profiles identifies their finite linear labels and measures the exact remaining center error.

   theorem affine_labels_offsets_of_chart_transport
       {V W L : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [ProperSpace V]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [Fintype L] [Nonempty L]
       (q : V →L[ℝ] W) (hq : Function.Surjective q)
       (A : L → W →L[ℝ] W) (hA : Function.Injective A)
       {R S : ℝ} (hR : 0 < R) (_hS : 0 < S)
       (a a' : ℕ → L) (b b' c : ℕ → W) (v : ℕ → W) (t : ℕ → ℝ)
       (ψ : ℕ → C(closedBall (0 : V) R, closedBall (0 : V) S))
       (hheight : ∀ᶠ n in atTop, ∀ z, t n • q (ψ n z) = q z - v n)
       (hd : Tendsto (fun n => dist
         (linearBallProfile q (A (a n)) R + ContinuousMap.const _ (b n))
         (transportCompactProfile (t n) (ψ n) (c n)
   …

   Mentions: OAI.PolycyclicRecognition.linearBallProfile, OAI.PolycyclicRecognition.transportCompactProfile

2. theorem OAI.PolycyclicRecognition.center_error_tendsto_zero_of_offsets line 55

   Source documentation

   Vanishing mean offsets remove the affine constants from the comparison, leaving precisely the normalized error in the two center heights.

   theorem center_error_tendsto_zero_of_offsets
       {W L : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
       (A : L → W →L[ℝ] W) (a : ℕ → L) (b b' c v : ℕ → W) (t : ℝ)
       (hb : Tendsto b atTop (𝓝 0)) (hb' : Tendsto b' atTop (𝓝 0))
       (hoff : Tendsto (fun n => dist (b n) (t • b' n + c n - A (a n) (v n)))
         atTop (𝓝 0)) :
       Tendsto (fun n => c n - A (a n) (v n)) atTop (𝓝 0) := by
   …