CartanDirectionalVisits.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Visits along the prescribed horizontal directions

The direction of each leg is retained, so its profile is evaluated along the original horizontal flow. Polynomial pivot coordinates give logarithmic switch diameter at the chosen supporting endpoint.

def OAI.PolycyclicRecognition.CartanWordModel.directionalVisitPath line 32

Source documentation

The outward-switch-return path using an explicitly prescribed Cartan direction.

def directionalVisitPath (v : H) (i : Fin M.letterCount)
    (n : G) (h₀ : H) (r b : ℝ) :
    Path (n * Exp h₀) (n * Exp (b • (M.letter i : GroupLieAlgebra (𝓘(ℝ, EG)) G)) * Exp h₀) := by
…

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_directional_visit_bound line 46

Source documentation

Uniform path and switch bounds for any fixed finite list of prescribed horizontal directions. The support condition is only an equality of heights.

theorem exists_directional_visit_bound
    (haarD : NilpotentExponentialHaarInput F.D.modelSpace F.D.carrier)
    (dynkinD : NilpotentDynkinExpansionInput F.D.modelSpace F.D.carrier)
    {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (eW : HeightSpace T.character ≃ₗ[ℝ] W) (π : G →* Multiplicative W)
    (hπ : ∀ x, (π (Exp x)).toAdd = eW (heightProjection T.character x))
    (v : Fin M.letterCount → H) (w₀ : W) (s : Fin M.letterCount → ℝ)
    (hs : ∀ i, cartanHeightWeight T H (M.weight i)
      (eW.symm (w₀ + eW (heightProjection T.character (v i)))) = s i)
    {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (p : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ r : ℝ, 0 ≤ r → ∀ h₀ : H,
      ‖(finBasis ℝ H).equivFun h₀‖ ≤ A * (1 + r) ^ p →
…

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