CartanBoundaryHaarAction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual boundary Haar action in ambient height coordinates

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_boundary_haar_height_multiplier line 43

Source documentation

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

theorem exists_boundary_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 →ₗ[ℝ] ℝ) ∉ positiveWeightRay α₀ → c i = 0) ∧
      (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ positiveWeightRay α₀ → 0 < c i) ∧
…

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