CartanConeHaarAction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual cone Haar action for the offset trace tests

theorem OAI.PolycyclicRecognition.CartanWordModel.factor_cone_quotient_action_eq_exponential line 44
Source documentation
The quotient action of each actual Cartan factor is the exponential of its induced Lie action, with the actual Cartan logarithm.
```
theorem factor_cone_quotient_action_eq_exponential (d : F.D.carrier) (q : Q.carrier) :
    α d q = exponentialConjugate Q.equiv ExpQ hbijQ
      (M.coneAdjointAutomorphism T C hadd
        (cartanLog H F.D.equiv F.ExpD hbijD d)) q := by
…
```
Mentions: OAI.PolycyclicRecognition.exponentialConjugate, OAI.PolycyclicRecognition.cartanLog

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cone_action_haar_height_multiplier line 79

Source documentation

The quotient Haar character is the actual ambient height character. The nilpotent factor contributes only a Haar-preserving translation.

theorem exists_cone_action_haar_height_multiplier
    {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (eW : HeightSpace T.character ≃ₗ[ℝ] W) (height : G →* Multiplicative W)
    (hheight : ∀ x, (height (ExpG x)).toAdd = eW (heightProjection T.character x))
    (hExpQ : IsGroupExponential ExpQ)
    (haar : NilpotentExponentialHaarInput Q.modelSpace Q.carrier)
    (act : G →* Equiv.Perm Q.carrier)
    (hact : ∀ u d q, act (F.inclusionN u * F.inclusionD d) q = π u * α d q) :
    ∃ (μ : Measure Q.carrier) (ell : W →ₗ[ℝ] ℝ) (c : Fin M.letterCount → ℕ),
      μ.IsHaarMeasure ∧
      (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∉ C → c i = 0) ∧
      (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C → 0 < c i) ∧
…

Mentions: OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput