OAI/GroupTheory/PolycyclicRecognition/Analysis/TranslatedCellDomination.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.translated_cell_domination line 14

   Source documentation

   A measure-preserving change of the target cell is dominated by the independent starting-cell and suffix law. The inverse-cover inclusion supplies the required geometric hypothesis.

   theorem translated_cell_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 ≠ ∞)
       (ψ : Y → Y) (hψ : Measurable ψ) (τ : X → Y → Y) (m : 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)))
       (hmatch : ∀ a k, ψ (τ a k) = m a k)
       (S : Set Y) (hS : MeasurableSet S) :
   …