OAI/GroupTheory/PolycyclicRecognition/Geometry/GoodProfileFlow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.good_profile_along_flow line 17

   Source documentation

   Uniform approximation on the fixed profile compact extends to the actual varying flow. The only additional error tends to zero with that flow.

   theorem good_profile_along_flow
       {U V W A ι : Type*} {l : Filter ι} [TopologicalSpace U] [LocallyCompactSpace U]
       [TopologicalSpace V] [LocallyCompactSpace V] [NormedAddCommGroup W]
       (f : C(V, W)) (Ψ : ι → C(U, V)) (Ψ₀ : C(U, V))
       (hΨ : Tendsto Ψ l (𝓝 Ψ₀)) (K : Set U) (hK : IsCompact K)
       (Z : Set V) (hZ : ∀ᶠ r in l, ∀ u ∈ K, Ψ r u ∈ Z)
       (profile : ι → A → V → W) (good : ι → Set A) (ζ : ι → ℝ)
       (hgood : ∀ r a, a ∈ good r → ∀ z ∈ Z, ‖profile r a z - f z‖ ≤ ζ r)
       {η : ℝ} (hη : 0 < η) :
       ∀ᶠ r in l, ∀ a ∈ good r, ∀ u ∈ K,
         ‖profile r a (Ψ r u) - f (Ψ₀ u)‖ ≤ ζ r + η := by
   …

2. theorem OAI.PolycyclicRecognition.height_bound_of_rescaled_profile line 43

   Source documentation

   Recover the physical-scale image height from the actual normalized profile, with its prescribed common center.

   theorem height_bound_of_rescaled_profile
       {G W Z : Type*} [Group G] [NormedAddCommGroup W] [NormedSpace ℝ W]
       (J : G → W) (x n : G) (s : ℝ) (φ : Z → G) (z : Z) (w : W) {ε : ℝ}
       (h : ‖rescaledMapProfile J x n s φ z - w‖ ≤ ε) :
       ‖J (x * n * φ z) - J x - Real.exp s • w‖ ≤ Real.exp s * ε := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile