OAI/GroupTheory/PolycyclicRecognition/Analysis/SegmentProfileLegs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.absorb_vanishing_profile_error line 16

   Source documentation

   The slowly vanishing good-profile error can be absorbed into any fixed positive multiple of the physical scale, uniformly over the retained sheets.

   theorem absorb_vanishing_profile_error
       {A : Type*} (B : ℝ → Set A) (err : ℝ → A → ℝ) (ζ : ℝ → ℝ)
       (hζ : Tendsto ζ atTop (𝓝 0))
       (hbound : ∀ η : ℝ, 0 < η → ∀ᶠ r in atTop, ∀ a ∈ B r, err r a ≤ r * (ζ r + η)) :
       ∀ η : ℝ, 0 < η → ∀ᶠ r in atTop, ∀ a ∈ B r, err r a ≤ η * r := by
   …

2. theorem OAI.PolycyclicRecognition.segment_profile_support_legs line 32

   Source documentation

   Every shortened support leg lies in the same original horizontal segment. In particular, one good profile controls all the chosen support endpoints and the common pivot, without separate good sets for the letters.

   theorem segment_profile_support_legs
       {L D N G W I : Type*} [AddCommGroup L] [Module ℝ L]
       [Group D] [Group N] [Group G] [NormedAddCommGroup W] [NormedSpace ℝ W]
       (ExpD : L → D) (hzero : ExpD 0 = 1) (ι : N →* G) (κ : D →* G)
       (J : G → W) (x d₀ : G) (center : W) (A : Set N) (r T ε : ℝ)
       (hT : 0 ≤ T) (v : L) (θ : I → ℝ) (hθ : ∀ i, θ i ∈ Icc 0 T)
       (g : ℝ → W)
       (hgood : ∀ u ∈ A, ∀ t ∈ Icc (0 : ℝ) T,
         ‖J ((x * ι u * d₀) * κ (ExpD ((r * t) • v))) - center - r • g t‖ ≤ ε) :
       (∀ u ∈ A, ‖J (x * ι u * d₀) - center - r • g 0‖ ≤ ε) ∧
       ∀ u ∈ A, ∀ i, ∀ t : unitInterval,
         ∃ w ∈ g '' Icc (0 : ℝ) T,
   …