HaarProduct.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Factoring a measure along Haar fibers

A measure finite on compact subsets of a compact section times a group, and invariant under translations of the group coordinate, is a product. The section measure is obtained by averaging over a set of positive finite Haar measure, never by restricting to a single fiber.

def OAI.PolycyclicRecognition.haarFiberSlice line 25
Source documentation
The group measure cut out by a measurable subset of the compact section.
```
def haarFiberSlice (E : Set X) : Measure G :=
…
```
theorem OAI.PolycyclicRecognition.haarFiberSlice_apply line 28
def OAI.PolycyclicRecognition.haarSectionMeasure line 40
Source documentation
Average the coupling over a fixed finite Haar region to define its section measure.
```
def haarSectionMeasure (m : Measure G) (B : Set G) : Measure X :=
…
```
theorem OAI.PolycyclicRecognition.haarSectionMeasure_apply line 43
theorem OAI.PolycyclicRecognition.haarFiberSlice_rightInvariant line 55

theorem OAI.PolycyclicRecognition.rightInvariant_eq_div_smul line 69

Source documentation

Right-invariant uniqueness, deduced from left-invariant uniqueness by inverting both measures.

theorem rightInvariant_eq_div_smul (μ m : Measure G)
    [SigmaFinite μ] [SigmaFinite m] [μ.IsMulRightInvariant] [m.IsMulRightInvariant]
    {B : Set G} (hB0 : m B ≠ 0) (hBtop : m B ≠ ∞) :
    μ = (μ B / m B) • m := by
…

theorem OAI.PolycyclicRecognition.measurePreserving_base_of_left_skew line 83

Source documentation

A measure-preserving skew translation over a map of the section forces that section map to preserve the marginal Haar factor.

theorem measurePreserving_base_of_left_skew (ν : Measure X) (m : Measure G)
    [SFinite ν] [SFinite m] [m.IsMulLeftInvariant]
    {T : X → X} (hT : Measurable T) {a : X → G} (ha : Measurable a)
    (hskew : MeasurePreserving (fun q : X × G => (T q.1, a q.1 * q.2))
      (ν.prod m) (ν.prod m))
    {B : Set G} (hB : MeasurableSet B) (hB0 : m B ≠ 0) (hBtop : m B ≠ ∞) :
    MeasurePreserving T ν ν := by
…

theorem OAI.PolycyclicRecognition.haarFiberSlice_finiteOnCompacts line 113

theorem OAI.PolycyclicRecognition.haarProduct_rectangle line 122

Source documentation

Translation invariance forces all measurable rectangles to have the product measure predicted by a single Haar normalization.

theorem haarProduct_rectangle (m : Measure G) [SigmaFinite m] [m.IsMulRightInvariant]
    (hM : ∀ g : G, MeasurePreserving (fun q : X × G => (q.1, q.2 * g)) M M)
    {B : Set G} (hB : MeasurableSet B) (hB0 : m B ≠ 0) (hBtop : m B ≠ ∞)
    {E : Set X} (hE : MeasurableSet E) {C : Set G} (hC : MeasurableSet C) :
    M (E ×ˢ C) = haarSectionMeasure M m B E * m C := by
…

Mentions: OAI.PolycyclicRecognition.haarSectionMeasure

theorem OAI.PolycyclicRecognition.haarSectionMeasure_finite line 137
Source documentation
The section measure has finite mass if the averaging region is compact.
```
theorem haarSectionMeasure_finite (m : Measure G) {B : Set G}
    (hB : IsCompact B) (hB0 : m B ≠ 0) :
    IsFiniteMeasure (haarSectionMeasure M m B) := by
…
```
Mentions: OAI.PolycyclicRecognition.haarSectionMeasure

theorem OAI.PolycyclicRecognition.haarProduct_factorization line 146

Source documentation

Haar uniqueness on each section slice yields equality on the whole product sigma algebra.

theorem haarProduct_factorization (m : Measure G) [SigmaFinite m] [m.IsMulRightInvariant]
    (hM : ∀ g : G, MeasurePreserving (fun q : X × G => (q.1, q.2 * g)) M M)
    {B : Set G} (hB : IsCompact B) (hB0 : m B ≠ 0) (hBtop : m B ≠ ∞) :
    M = (haarSectionMeasure M m B).prod m := by
…

Mentions: OAI.PolycyclicRecognition.haarSectionMeasure

theorem OAI.PolycyclicRecognition.haarSectionMeasure_ne_zero line 157

Source documentation

A nonzero invariant coupling has a finite nonzero section measure.

theorem haarSectionMeasure_ne_zero (m : Measure G) [SigmaFinite m] [m.IsMulRightInvariant]
    (hM : ∀ g : G, MeasurePreserving (fun q : X × G => (q.1, q.2 * g)) M M)
    (hM0 : M ≠ 0) {B : Set G} (hB : IsCompact B)
    (hB0 : m B ≠ 0) (hBtop : m B ≠ ∞) :
    haarSectionMeasure M m B ≠ 0 := by
…

Mentions: OAI.PolycyclicRecognition.haarSectionMeasure