ConeQuotientHaar.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The exact positive character of quotient Haar measure

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cone_haar_multiplier line 21

Source documentation

A single Haar measure has the quotient Jacobian character for every Cartan parameter. The character coefficients are positive exactly on the retained generators.

theorem exists_cone_haar_multiplier
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
    (ExpQ : GroupLieAlgebra (𝓘(ℝ, Q.modelSpace)) Q.carrier → Q.carrier)
    (hExpQ : IsGroupExponential ExpQ) (hbij : Function.Bijective ExpQ)
    (haar : NilpotentExponentialHaarInput Q.modelSpace Q.carrier) :
    ∃ (μ : Measure Q.carrier) (c : Fin M.letterCount → ℕ), μ.IsHaarMeasure ∧
      (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∉ C → c i = 0) ∧
      (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C → 0 < c i) ∧
      (∀ h : H, Measure.map
        (exponentialConjugate Q.equiv ExpQ hbij (M.coneAdjointAutomorphism T C hadd h)) μ =
        ENNReal.ofReal (Real.exp (-(∑ i, (c i : ℝ) * M.weight i h))) • μ) ∧
…

Mentions: OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.exponentialConjugate