QuotientSectionMeasure.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Product measure in quotient-section coordinates

theorem OAI.PolycyclicRecognition.quotientSection_skew_measurePreserving line 24
Source documentation
Conjugation invariance of the kernel measure and right invariance of its translations make the coordinate skew action preserve product measure.
```
theorem quotientSection_skew_measurePreserving
    (hconj : ∀ n : N, MeasurePreserving (quotientKernelConjugate π n) μI μI) (n : N) :
    MeasurePreserving (fun p : Q × π.ker =>
      (π n * p.1, quotientKernelConjugate π n p.2 * quotientSectionCocycle π s hs n p.1))
      (μQ.prod μI) (μQ.prod μI) := by
…
```
Mentions: OAI.PolycyclicRecognition.quotientKernelConjugate, OAI.PolycyclicRecognition.quotientSectionCocycle

theorem OAI.PolycyclicRecognition.quotientSection_product_left_invariant line 45

Source documentation

Pushing product measure through the actual global section coordinates gives a left-invariant measure on the original group.

theorem quotientSection_product_left_invariant
    (hconj : ∀ n : N, MeasurePreserving (quotientKernelConjugate π n) μI μI) (n : N) :
    MeasurePreserving (fun x : N => n * x)
      (Measure.map (quotientSectionHomeomorph π hπ s hs).symm (μQ.prod μI))
      (Measure.map (quotientSectionHomeomorph π hπ s hs).symm (μQ.prod μI)) := by
…

Mentions: OAI.PolycyclicRecognition.quotientKernelConjugate, OAI.PolycyclicRecognition.quotientSectionHomeomorph