OAI/GroupTheory/PolycyclicRecognition/Analysis/IndependentCellDomination.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.independent_cell_pair_domination line 16

   Source documentation

   Integrate the conditional normalized-cell comparison in the starting point. The cost is the exact larger-to-smaller Haar-volume ratio.

   theorem independent_cell_pair_domination
       {X : Type*} [MeasurableSpace X] (μ : Measure X)
       (C D : Set X) (hC : MeasurableSet C)
       (hC0 : μ C ≠ 0) (hCfin : μ C ≠ ∞)
       (hD0 : μ D ≠ 0) (hDfin : μ D ≠ ∞)
       (τ : X → X → X)
       (hτ : ∀ a ∈ C, MeasurePreserving (τ a) μ μ)
       (hcover : ∀ a ∈ C, (τ a) ⁻¹' C ⊆ D)
       (hpair : Measurable (fun p : X × X => (p.1, τ p.1 p.2)))
       (B : Set (X × X)) (hB : MeasurableSet B) :
       (cellProbabilityMeasure μ C hC0 hCfin : Measure X).prod
           (cellProbabilityMeasure μ C hC0 hCfin : Measure X) B ≤
   …

   Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure