OAI/GroupTheory/PolycyclicRecognition/Analysis/DifferentCellDomination.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.different_cell_pair_domination line 15

   Source documentation

   The starting law is arbitrary. Only the target-to-suffix volume ratio enters the domination constant, including when the two scales differ.

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

   Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure