OAI/GroupTheory/PolycyclicRecognition/Analysis/DominatedProfileConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.dominated_profile_concentration line 15

   Source documentation

   Ordinary affine approximation and suffix concentration give the same approximation for a changed sampling law dominated by the independent starting-point and suffix distribution.

   theorem dominated_profile_concentration
       {X Y : Type*} [MeasurableSpace X] [PseudoMetricSpace Y]
       (μ ν : ℕ → ProbabilityMeasure X) (ξ : ℕ → Measure X)
       (ψ : ℕ → X → X) (m : ℕ → X → X → X)
       (f : ℕ → X → Y) (a : ℕ → Y)
       {K : ℝ≥0∞} (hK : K ≠ ∞)
       (hmeas : ∀ n ε, MeasurableSet {x | ε ≤ dist (f n x) (a n)})
       (hdom : ∀ᶠ n in atTop, ∀ S : Set X, MeasurableSet S →
         ξ n (ψ n ⁻¹' S) ≤ K * (μ n : Measure X).prod (ν n : Measure X)
           {p | m n p.1 p.2 ∈ S})
       (hordinary : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure X) {x | ε ≤ dist (f n x) (a n)}) atTop (𝓝 0))
   …