CartanSegmentWordPath.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Specified segment paths for continuously varying words

The exponentially rescaled amplitudes are evaluated along the previously constructed segment visits. This retains both measurable samples and the uniform metric bounds needed for endpoint integration.

def OAI.PolycyclicRecognition.CartanWordModel.segmentScaledWord line 29
def OAI.PolycyclicRecognition.CartanWordModel.segmentWordPath line 33

theorem OAI.PolycyclicRecognition.CartanWordModel.continuous_segmentWordPath_sample line 50

Source documentation

Fixed-time samples remain continuous when the amplitudes of a fixed combinatorial word vary continuously.

theorem continuous_segmentWordPath_sample
    {Y : Type*} [TopologicalSpace Y]
    (v : H) (r : ℝ) (w : List (Fin M.letterCount × (Y → ℝ)))
    (hw : ∀ z ∈ w, Continuous z.2) (t : unitInterval) :
    Continuous (fun y => M.segmentWordPath T hExp realize v r
      (w.map (fun z => (z.1, z.2 y))) t) := by
…

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_segmentWordPath_bound line 85

Source documentation

Uniform metric and homomorphism-height bounds for the specified paths.

theorem exists_segmentWordPath_bound [IsIsometricSMul G G]
    {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (l : G →* Multiplicative W) (hl : Continuous fun g => (l g).toAdd)
    {L : ℝ} (hL : 0 ≤ L) (hbound : ∀ g, ‖(l g).toAdd‖ ≤ L * dist 1 g)
    (v : H) {B : ℝ} (hB : 0 ≤ B) (N : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ r : ℝ, 0 ≤ r →
      ∀ u : List (Fin M.letterCount × ℝ), u.length ≤ N → (∀ z ∈ u, |z.2| ≤ B) →
      PathMetricBound (M.segmentWordPath T hExp realize v r u)
        (C * r) (C * (1 + Real.log (2 + r))) ∧
      ∀ t, ∃ z ∈ segment ℝ (0 : W) (l (Exp v)).toAdd,
        (l (M.segmentWordPath T hExp realize v r u t)).toAdd = r • z := by
…

Mentions: OAI.PolycyclicRecognition.PathMetricBound