BoundaryTranslateMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform translated masses from the nilpotent leaf bound

theorem OAI.PolycyclicRecognition.leftTranslate_eq_mul_image line 16
Source documentation
The preimage description of a translate agrees with its multiplication image, including for nonmeasurable sets.
```
theorem leftTranslate_eq_mul_image
    {S : Type*} [Group S] [MeasurableSpace S] [MeasurableMul₂ S] [MeasurableInv S]
    (E : Set S) (z : S) : leftTranslate E z = (fun x => z * x) '' E := by
…
```
Mentions: OAI.PolycyclicRecognition.leftTranslate

theorem OAI.PolycyclicRecognition.boundary_pullback_measure_apply line 28

Source documentation

Pulling Haar measure back by a boundary homeomorphism measures precisely its image sets; absolute continuity is unnecessary.

theorem boundary_pullback_measure_apply
    {S T : Type*} [TopologicalSpace S] [TopologicalSpace T]
    [MeasurableSpace S] [MeasurableSpace T] [BorelSpace S] [BorelSpace T]
    (B : S ≃ₜ T) (μ : Measure T) (E : Set S) :
    Measure.map B.symm μ E = μ (B '' E) := by
…

theorem OAI.PolycyclicRecognition.boundary_translated_mass_bounds line 38

Source documentation

Every source quotient translation lifts to a nilpotent element. The leaf bound then makes all translates of a fixed Cartan image have comparable mass. The comparison constant is uniform in both the map and the Cartan parameter.

theorem boundary_translated_mass_bounds
    {P G N S T D : Type*} [Group G] [Group N] [Group S]
    [TopologicalSpace S] [TopologicalSpace T]
    [MeasurableSpace S] [MeasurableSpace T] [BorelSpace S] [BorelSpace T]
    [MeasurableMul₂ S] [MeasurableInv S]
    (act : G →* Equiv.Perm S) (ι : N →* G) (π : N →* S)
    (hπ : Function.Surjective π) (hact : ∀ n x, act (ι n) x = π n * x)
    (B : P → S ≃ₜ T) (μ : Measure T) (f : P → G → G) (height : G → ℝ)
    (d : D → G) (U : Set S) {K C : ℝ} (hK : 0 < K)
    (hmass : ∀ p x,
      ENNReal.ofReal (Real.exp (height (f p x))) ≤
        ENNReal.ofReal K * μ (B p '' (act x '' U)) ∧
…