KernelHaarTransport.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Haar measure on the actual quotient kernel

A closed realization of a Lie ideal identifies its intrinsic group with the kernel. Equivariance transports conjugation invariance, and hence also right invariance, to the measure used in section coordinates.

def OAI.PolycyclicRecognition.kernelRealization line 26
Source documentation
The intrinsic ideal group and the actual kernel have the same topology and multiplication.
```
def kernelRealization : I ≃ₜ* π.ker := by
…
```
theorem OAI.PolycyclicRecognition.kernelRealization_coe line 35

theorem OAI.PolycyclicRecognition.kernelRealization_conjugation_preserving line 44

Source documentation

A concrete equivariant automorphism preserving intrinsic Haar measure also preserves its image on the kernel.

theorem kernelRealization_conjugation_preserving (n : N) (F : I → I)
    (hF : MeasurePreserving F μ μ)
    (hequiv : ∀ x, ι (F x) = n * ι x * n⁻¹) :
    MeasurePreserving (quotientKernelConjugate π n)
      (Measure.map (kernelRealization π ι hι hrange) μ)
      (Measure.map (kernelRealization π ι hι hrange) μ) := by
…

Mentions: OAI.PolycyclicRecognition.quotientKernelConjugate, OAI.PolycyclicRecognition.kernelRealization

theorem OAI.PolycyclicRecognition.kernel_measure_right_invariant line 61
Source documentation
Left invariance together with the ambient conjugation invariance gives the right invariance needed by the section cocycle.
```
theorem kernel_measure_right_invariant (ν : Measure π.ker) [ν.IsMulLeftInvariant]
    (hconj : ∀ n : N, MeasurePreserving (quotientKernelConjugate π n) ν ν) :
    ν.IsMulRightInvariant := by
…
```
Mentions: OAI.PolycyclicRecognition.quotientKernelConjugate