OAI/GroupTheory/PolycyclicRecognition/Analysis/IndependentCellConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.independent_cell_concentration line 16

   Source documentation

   A uniformly bounded volume ratio turns deterministic suffix concentration into concentration of independent ordinary samples.

   theorem independent_cell_concentration
       {G : Type*} [Group G] [MeasurableSpace G] [MeasurableMul₂ G]
       (μ : Measure G) [μ.IsMulLeftInvariant]
       (C D : ℕ → Set G) (hC : ∀ n, MeasurableSet (C n))
       (hD : ∀ n, MeasurableSet (D n))
       (hC0 : ∀ n, μ (C n) ≠ 0) (hCfin : ∀ n, μ (C n) ≠ ∞)
       (hD0 : ∀ n, μ (D n) ≠ 0) (hDfin : ∀ n, μ (D n) ≠ ∞)
       (hcover : ∀ n a, a ∈ C n → ∀ b ∈ C n, a⁻¹ * b ∈ D n)
       {K : ℝ≥0∞} (hK : K ≠ ∞) (hratio : ∀ n, μ (D n) / μ (C n) ≤ K)
       (B : ℕ → Set (G × G)) (hB : ∀ n, MeasurableSet (B n))
       (hp : ∀ k : ℕ → G, (∀ n, k n ∈ D n) →
         Tendsto (fun n => (cellProbabilityMeasure μ (C n) (hC0 n) (hCfin n) : Measure G)
   …

   Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure