CartanHaarConjugation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A common Haar measure for Cartan boxes and conjugation

The determinant computation gives exact invariance under the actual Cartan adjoint automorphisms. The same measure retains the explicit weighted-box volume, so the lower packing argument and box rates use compatible measures.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_haar_adjoint_invariant_weighted_boxes line 38

Source documentation

One Haar measure has both the exact word-box formula and invariance under every Cartan adjoint action.

theorem exists_haar_adjoint_invariant_weighted_boxes
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ μ : Measure N, μ.IsHaarMeasure ∧
      (∀ h : H, MeasurePreserving (M.adjointGroupAutomorphism T eN Exp hExp hbij dynkin h) μ μ) ∧
      ∀ (cost : M.wordList → ℝ) (β : M.Bases) (r R : ℝ), 0 ≤ R →
        μ (exponentialCoordinateBox (Exp ∘ eN)
          (exponentialRescaleBasis (WordBasisSelections.basis M.letter M.wordList β)
            (fun i => cost (β.val i)) r) R) =
          ENNReal.ofReal |(columnBasisMatrix (wordListCoordinates M.letter M.wordList b₀) β.val).det| *
            ENNReal.ofReal (Real.exp (r * columnBasisWeight cost β.val)) *
              ENNReal.ofReal (2 * R) ^ finrank ℝ (cartanRootIdeal H) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.exponentialCoordinateBox, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.columnBasisMatrix, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.columnBasisWeight

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_haar_adjoint_invariant_box_bounds line 72

Source documentation

The conjugation-invariant Haar measure has the same exponential lower and upper rates as all maximizing Cartan boxes.

theorem exists_haar_adjoint_invariant_box_bounds
    {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (eW : HeightSpace T.character ≃ₗ[ℝ] W)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ (μ : Measure N) (c C : ℝ), μ.IsHaarMeasure ∧ 0 < c ∧ 0 < C ∧
      (∀ h : H, MeasurePreserving (M.adjointGroupAutomorphism T eN Exp hExp hbij dynkin h) μ μ) ∧
      ∀ (E : Set W) (β : M.Bases),
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val →
      ∀ (r R : ℝ), 0 ≤ R →
        ENNReal.ofReal c * ENNReal.ofReal (Real.exp (r * (M.supportIn T hunimod eW).templateSupport E)) *
          ENNReal.ofReal (2 * R) ^ finrank ℝ (cartanRootIdeal H) ≤
…

Mentions: OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates