CartanMeasuredConeHaar.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Haar measure for the actual section used by the probe chains

def OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone.kernelMeasure line 24
Source documentation
The intrinsic ideal Haar measure transported to the exact kernel.
```
def MeasuredCone.kernelMeasure : Measure D.maps.quotient.ker :=
…
```
def OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone.sectionMeasure line 29
Source documentation
The original product measure for any prescribed continuous section.
```
def MeasuredCone.sectionMeasure
    (σ : ContinuousMap D.Q.carrier F.N.carrier) (hσ : ∀ q, D.maps.quotient (σ q) = q) :
    Measure F.N.carrier := by
…
```
theorem OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone.sectionMeasure_isHaar line 41
Source documentation
The pure-word section chosen by the tile construction can replace the initial quotient section without changing the Haar property.
```
theorem MeasuredCone.sectionMeasure_isHaar
    (σ : ContinuousMap D.Q.carrier F.N.carrier) (hσ : ∀ q, D.maps.quotient (σ q) = q) :
    (D.sectionMeasure M F C σ hσ).IsHaarMeasure := by
…
```
theorem OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone.action_preserves_sectionMeasure line 73
Source documentation
The actual Cartan factor preserves the product measure of the chosen source section. This is the same measure used by source packing.
```
theorem MeasuredCone.action_preserves_sectionMeasure
    (hExp : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput

theorem OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone.dilation_preserves_sectionMeasure line 89

Source documentation

The sampler's prescribed scalar dilation preserves this same source measure; no comparison of arbitrary Haar normalizations is required later.

theorem MeasuredCone.dilation_preserves_sectionMeasure
    (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
    (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
    (hbijN : Function.Bijective F.ExpN)
    (σ : ContinuousMap D.Q.carrier F.N.carrier) (hσ : ∀ q, D.maps.quotient (σ q) = q)
    (h : H) (S : F.N.carrier → F.N.carrier)
    (hS : ∀ v, S (F.ExpN (F.N.equiv v)) =
      F.ExpN (F.N.equiv (cartanIdealWeightDilation T H h v))) :
    MeasurePreserving S (D.sectionMeasure M F C σ hσ) (D.sectionMeasure M F C σ hσ) := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.cartanIdealWeightDilation