CartanSegmentVisits.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Cartan segment visits for an arbitrary controlled homomorphism

The support direction is chosen in the actual Cartan algebra, before any factorization of the homomorphism through canonical height is known. The resulting path stays exactly over the segment of its two values.

def OAI.PolycyclicRecognition.CartanWordModel.segmentSupportDirection line 26
def OAI.PolycyclicRecognition.CartanWordModel.segmentSupportExponent line 29
theorem OAI.PolycyclicRecognition.CartanWordModel.segmentSupportDirection_weight line 32
theorem OAI.PolycyclicRecognition.CartanWordModel.segmentSupportDirection_norm line 39

def OAI.PolycyclicRecognition.CartanWordModel.segmentVisitPath line 61

Source documentation

The specified segment visit, retained for measurable path sampling.

def segmentVisitPath (v : 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_segment_support_visit_bound line 75

Source documentation

Uniform single-letter visits whose values under l stay in the scaled segment [0,l(exp v)], without assuming l = A ∘ π.

theorem exists_segment_support_visit_bound (v : H) {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.segmentSupportExponent 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 ∈ segment ℝ (0 : W) (l (Exp v)).toAdd,
          (l (γ t)).toAdd = r • z) ∧
        γ = M.segmentVisitPath T hExp realize v i n r b := by
…

Mentions: OAI.PolycyclicRecognition.PathMetricBound