OAI/GroupTheory/PolycyclicRecognition/Analysis/ProfilePointwiseBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.rescaledMapProfile_norm_le line 19

   Source documentation

   A bound at the identity extends to a pointwise bound by the actual scaled chart distance.

   theorem rescaledMapProfile_norm_le
       {K : ℝ≥0} {J : G → W} (hJ : LipschitzWith K J)
       (x k : G) (r : ℝ) (φ : Z → G) (hφ : φ 0 = 1) (z : Z) :
       ‖rescaledMapProfile J x k r φ z‖ ≤
         (K : ℝ) * (dist 1 (φ z) / Real.exp r) + ‖rescaledMapProfile J x k r φ 0‖ := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile

2. theorem OAI.PolycyclicRecognition.rescaledMapProfile_zero_norm_le line 35

   Source documentation

   The profile value at the identity is controlled by the suffix length.

   theorem rescaledMapProfile_zero_norm_le
       {K : ℝ≥0} {J : G → W} (hJ : LipschitzWith K J)
       (x k : G) (r : ℝ) (φ : Z → G) (hφ : φ 0 = 1) :
       ‖rescaledMapProfile J x k r φ 0‖ ≤ (K : ℝ) * (dist 1 k / Real.exp r) := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile

3. theorem OAI.PolycyclicRecognition.exists_compact_containing_rescaled_profiles line 55

   Source documentation

   Once equicontinuity is proved, only the anchor and pointwise chart radius bounds are needed to contain all sampled profiles in one compact set for locally uniform convergence.

   theorem exists_compact_containing_rescaled_profiles
       {A : Type*} {K : ℝ≥0} (J : ℕ → A → G → W)
       (hJ : ∀ i u, LipschitzWith K (J i u)) (x k : ℕ → A → G)
       (scale : ℕ → ℝ) (φ : ℕ → Z → G) (hφ : ∀ i, Continuous (φ i))
       (hzero : ∀ i, φ i 0 = 1)
       (hequi : Equicontinuous (fun p : ℕ × A =>
         rescaledMapProfile (J p.1 p.2) (x p.1 p.2) (k p.1 p.2) (scale p.1) (φ p.1)))
       (B : ℝ) (hanchor : ∀ i u,
         ‖rescaledMapProfile (J i u) (x i u) (k i u) (scale i) (φ i) 0‖ ≤ B)
       (hradius : ∀ z, ∃ D : ℝ, ∀ i, dist 1 (φ i z) / Real.exp (scale i) ≤ D) :
       ∃ S : Set C(Z, W), IsCompact S ∧ ∀ i u,
         (⟨rescaledMapProfile (J i u) (x i u) (k i u) (scale i) (φ i),
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile