OAI/GroupTheory/PolycyclicRecognition/Analysis/DominatedAffineComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.deterministic_distance_tendsto_zero_of_dominated_transport line 17

   Source documentation

   The proved density domination and suffix concentration transport the target affine approximant to the source law, where the exact chart identity compares the two deterministic approximants.

   theorem deterministic_distance_tendsto_zero_of_dominated_transport
       {X Y Z : Type*} [MeasurableSpace X] [PseudoMetricSpace Y] [PseudoMetricSpace Z]
       (ξ μ ν : ℕ → ProbabilityMeasure X) (a : ℕ → Y) (b : ℕ → Z)
       (f : ℕ → X → Y) (g : ℕ → X → Z) (ψ : ℕ → X → X)
       (m : ℕ → X → X → X) (H : ℕ → Z → Y)
       {K : ℝ} (hK : 0 < K)
       (hH : ∀ n u v, dist (H n u) (H n v) ≤ K * dist u v)
       (hmatch : ∀ᶠ n in atTop, ∀ x, f n x = H n (g n (ψ n x)))
       {D : ℝ≥0∞} (hD : D ≠ ∞)
       (hmeas : ∀ n ε, MeasurableSet {x | ε ≤ dist (g n x) (b n)})
       (hdom : ∀ᶠ n in atTop, ∀ S : Set X, MeasurableSet S →
         (ξ n : Measure X) (ψ n ⁻¹' S) ≤ D * (μ n : Measure X).prod (ν n : Measure X)
   …