InverseSection.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The invariant measure on the inverse section

For the actual compact space of quasi-inverse pairs, the Haar coupling in inverse coordinates factors as a finite nonzero invariant section measure times Haar measure. No absolute continuity of the section measure is used.

instance OAI.PolycyclicRecognition.inversePairCoupling_finiteOnCompacts line 25
theorem OAI.PolycyclicRecognition.inversePairCoupling_ne_zero line 32
Source documentation
The product measure remains nonzero under the change of charts.
```
theorem inversePairCoupling_ne_zero
    (m : Measure G) [SFinite m] (hm : m ≠ 0)
    (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ] :
    inversePairCoupling m μ ≠ 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.inversePairCoupling

theorem OAI.PolycyclicRecognition.exists_inverseSection_measure line 46

Source documentation

The inverse section has a finite nonzero stationary measure, and its product with Haar measure is exactly the coupling in inverse coordinates.

theorem exists_inverseSection_measure
    (m : Measure G) [m.IsHaarMeasure] [m.IsMulRightInvariant]
    (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ]
    [SMulInvariantMeasure G (NormalizedPair G Λ) μ] :
    ∃ ν : Measure (NormalizedPair G Λ), IsFiniteMeasure ν ∧ ν ≠ 0 ∧
      SMulInvariantMeasure G (NormalizedPair G Λ) ν ∧
      inversePairCoupling m μ = ν.prod m := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.inversePairCoupling