BasepointCellDomination.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual changed-center sampling law

The deterministic inclusion is isolated from its measure-theoretic use. The conclusion concerns the translated and conjugated ordinary Haar cell, with the exact volume ratio of the suffix cell.

theorem OAI.PolycyclicRecognition.basepoint_cell_domination line 22

Source documentation

Independent smaller-cell and suffix sampling dominates the actual nilpotent factor after changing the ambient basepoint.

theorem basepoint_cell_domination
    {N D : Type*} [Group N] [Group D] [MeasurableSpace N] [MeasurableMul₂ N]
    (φ : D →* MulAut N) (μ : Measure N) [μ.IsMulLeftInvariant]
    (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
    (ν : ProbabilityMeasure N) (A : Set N)
    (hA : ∀ᵐ a ∂(ν : Measure N), a ∈ A)
    (C B : Set N) (hC : MeasurableSet C) (hB : MeasurableSet B)
    (hC0 : μ C ≠ 0) (hCfin : μ C ≠ ∞) (hB0 : μ B ≠ 0) (hBfin : μ B ≠ ∞)
    (u : N) (d : D)
    (hcover : ∀ a₀ ∈ A, ∀ a ∈ C, (φ d a₀)⁻¹ * u⁻¹ * a ∈ B)
    (S : Set N) (hS : MeasurableSet S) :
    let K := (φ d) ⁻¹' B
…

theorem OAI.PolycyclicRecognition.exists_basepoint_cell_domination line 70

Source documentation

The conjugated suffix cell can be packaged as a probability law, with any established upper bound for its exact Haar-volume ratio.

theorem exists_basepoint_cell_domination
    {N D : Type*} [Group N] [Group D] [MeasurableSpace N] [MeasurableMul₂ N]
    (φ : D →* MulAut N) (μ : Measure N) [μ.IsMulLeftInvariant]
    (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
    (νA : ProbabilityMeasure N) (A : Set N)
    (hA : ∀ᵐ a ∂(νA : Measure N), a ∈ A)
    (C B : Set N) (hC : MeasurableSet C) (hB : MeasurableSet B)
    (hC0 : μ C ≠ 0) (hCfin : μ C ≠ ∞) (hB0 : μ B ≠ 0) (hBfin : μ B ≠ ∞)
    (u : N) (d : D)
    (hcover : ∀ a₀ ∈ A, ∀ a ∈ C, (φ d a₀)⁻¹ * u⁻¹ * a ∈ B)
    {K : ℝ≥0∞} (hratio : μ B / μ C ≤ K) :
    ∃ ν : ProbabilityMeasure N,
…