OAI/GroupTheory/PolycyclicRecognition/Analysis/GoodSheetProfileAgreement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.good_sheet_profile_values_eq line 16

   Source documentation

   A good set may have vanishing relative probability. Its nonemptiness, vanishing profile errors, and the actual short source bridge still identify the two limiting profile values.

   theorem good_sheet_profile_values_eq
       {G W Z A : Type*} [Group G] [PseudoMetricSpace G]
       [NormedAddCommGroup W] [NormedSpace ℝ W]
       {K : ℝ≥0} (J : ℕ → G → W) (hJ : ∀ n, LipschitzWith K (J n))
       (scale : ℕ → ℝ) (hscale : ∀ n, 0 < scale n)
       (x : ℕ → G) (k l : ℕ → A → G) (chart : ℕ → Z → G) (z : Z)
       (Good : ℕ → Set A) (hne : ∀ n, (Good n).Nonempty)
       (ε : ℕ → ℝ) (hε : Tendsto ε atTop (𝓝 0)) (f g : W)
       (happrox : ∀ᶠ n in atTop, ∀ a ∈ Good n,
         ‖rescaledMapProfile (J n) (x n) (k n a) (Real.log (scale n)) (chart n) z - f‖ ≤ ε n ∧
         ‖rescaledMapProfile (J n) (x n) (l n a) (Real.log (scale n)) (chart n) z - g‖ ≤ ε n)
       (hnear : ∀ η : ℝ, 0 < η → ∀ᶠ n in atTop, ∀ a ∈ Good n,
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile