CartanTemplateVisits.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Cartan support visits for finitely many prescribed template directions

The directions are actual Cartan vectors. A convex target containing their images contains every support path, including the short root switches.

def OAI.PolycyclicRecognition.CartanWordModel.templateVisitPath line 34

Source documentation

The specified support visit, retained for measurable path sampling.

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_template_support_visit_bound line 48

Source documentation

One common metric bound for the finite family of support directions. Every value under the homomorphism lies exactly in the scaled target.

theorem exists_template_support_visit_bound
    (v : Fin M.letterCount → H) (E : Set W) (hE : Convex ℝ E) (hE0 : (0 : W) ∈ E)
    (hvE : ∀ i, (l (Exp (v i))).toAdd ∈ E)
    {B : ℝ} (hB : 0 ≤ B) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ r : ℝ, 0 ≤ r → ∀ n : G, l n = 1 →
      ∀ (i : Fin M.letterCount) (b : ℝ),
      |b| ≤ B * Real.exp (r * M.weight i (v i)) →
      ∃ γ : Path (n * 1) (n * Exp (b • (M.letter i : GroupLieAlgebra (𝓘(ℝ, EG)) G)) * 1),
        PathMetricBound γ (C * r) (C * (1 + Real.log (2 + r))) ∧
        (∀ t, ∃ z ∈ E,
          (l (γ t)).toAdd = r • z) ∧
        γ = M.templateVisitPath T hExp realize v i n r b := by
…

Mentions: OAI.PolycyclicRecognition.PathMetricBound