OAI/GroupTheory/PolycyclicRecognition/Analysis/MixedCellConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.mixed_cell_concentration line 17

   Source documentation

   A difference cover with bounded target volume ratio passes suffix concentration to independent samples from two possibly different cells.

   theorem mixed_cell_concentration
       {G : Type*} [Group G] [MeasurableSpace G] [MeasurableMul₂ G]
       (μ : Measure G) [μ.IsMulLeftInvariant]
       (A C D : ℕ → Set G) (hA : ∀ n, MeasurableSet (A n))
       (hC : ∀ n, MeasurableSet (C n)) (hD : ∀ n, MeasurableSet (D n))
       (hA0 : ∀ n, μ (A n) ≠ 0) (hAfin : ∀ n, μ (A n) ≠ ∞)
       (hC0 : ∀ n, μ (C n) ≠ 0) (hCfin : ∀ n, μ (C n) ≠ ∞)
       (hD0 : ∀ n, μ (D n) ≠ 0) (hDfin : ∀ n, μ (D n) ≠ ∞)
       (hcover : ∀ n a, a ∈ A 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) →
   …