CartanSourceDilation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The same Cartan dilation in tiling, concentration, and source measure

def OAI.PolycyclicRecognition.CartanWordModel.sourceDilation line 31
Source documentation
The continuous source dilation integrates the same Lie automorphism as the algebraic dilation used by the stored linked chains.
```
def sourceDilation (h : H) : F.N.carrier ≃ₜ* F.N.carrier :=
…
```
theorem OAI.PolycyclicRecognition.CartanWordModel.sourceDilation_toMulEquiv line 35
theorem OAI.PolycyclicRecognition.CartanWordModel.sourceDilation_apply_exp line 40

theorem OAI.PolycyclicRecognition.CartanWordModel.sourceDilation_normalized_step line 48

Source documentation

The normalized original step is the one used by this continuous dilation, so the tiling identity requires no independent group action.

theorem sourceDilation_normalized_step (h : H) (i : Fin M.letterCount)
    (time : ℝ) (step : F.N.carrier)
    (hstep : F.inclusionN step = Exp (time •
      (M.letter i : GroupLieAlgebra (𝓘(ℝ, EG)) G))) :
    (M.sourceDilation T F hbij chartN hchartN dynkinN h).symm step =
      F.ExpN (F.N.equiv ((Real.exp (-M.weight i h) * time) • M.letter i)) := by
…

theorem OAI.PolycyclicRecognition.CartanWordModel.sourceDilation_inward_contact line 60

Source documentation

Translating the polar templates to the inward contact point gives the same dilation parameter as normalizing the neighboring letter.

theorem sourceDilation_inward_contact
    (eW : HeightSpace T.character ≃ₗ[ℝ] W) (w : W) (c δ r : ℝ) :
    (M.sourceDilation T F hbij chartN hchartN dynkinN
      ((r * (1 - c * δ)) • cartanHeightSection T H (eW.symm w))).toMulEquiv =
      integrateNilpotentLieEquiv F.N.equiv F.ExpN hbij dynkinN F.isExpN
        M.bound_zero (cartanIdealWeightDilation T H
          (r • cartanHeightSection T H (eW.symm ((1 - c * δ) • w)))) := by
…

Mentions: OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.cartanHeightSection, OAI.PolycyclicRecognition.integrateNilpotentLieEquiv, OAI.PolycyclicRecognition.cartanIdealWeightDilation

theorem OAI.PolycyclicRecognition.CartanWordModel.sourceDilation_preserves_sectionMeasure line 72

Source documentation

The canonical dilation preserves the product Haar measure for the section selected by the source partition.

theorem sourceDilation_preserves_sectionMeasure
    (hunimod : ∀ x : GroupLieAlgebra (𝓘(ℝ, EG)) G,
      LinearMap.trace ℝ _ (ad ℝ _ x) = 0)
    (C : Set (H →ₗ[ℝ] ℝ)) (D : M.MeasuredCone F C)
    (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
    (σ : ContinuousMap D.Q.carrier F.N.carrier)
    (hσ : ∀ q, D.maps.quotient (σ q) = q) (h : H) :
    MeasureTheory.MeasurePreserving
      (M.sourceDilation T F hbij chartN hchartN dynkinN h)
      (D.sectionMeasure M F C σ hσ) (D.sectionMeasure M F C σ hσ) := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput