OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanTemplateWordPath.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.CartanWordModel.templateScaledWord line 29
2. def OAI.PolycyclicRecognition.CartanWordModel.templateWordPath line 33
3. theorem OAI.PolycyclicRecognition.CartanWordModel.continuous_templateWordPath_sample line 50

   Source documentation

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

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

4. theorem OAI.PolycyclicRecognition.CartanWordModel.continuous_templateWordPath_scheme line 86

   Source documentation

   Continuous parameters in a fixed conjugate scheme give continuous samples of the prescribed template path.

   theorem continuous_templateWordPath_scheme
       {Y : Type*} [TopologicalSpace Y] {n : ℕ}
       (v : Fin M.letterCount → H) (r : ℝ)
       (w : Fin n → List (Fin M.letterCount × ℝ)) (i : Fin n → Fin M.letterCount)
       (σ : Y → Fin n → ℝ) (hσ : Continuous σ) (t : unitInterval) :
       Continuous (fun y => M.templateWordPath T hExp realize v r
         (generatorSchemeWord w i (σ y)) t) := by
   …

   Mentions: OAI.PolycyclicRecognition.generatorSchemeWord

5. theorem OAI.PolycyclicRecognition.CartanWordModel.templateScaledWord_product line 104

   Source documentation

   Inclusion carries the actual rescaled template word to its ambient product, preserving every letter in the original order.

   theorem templateScaledWord_product (F : CartanFactorModel H Exp)
       (v : Fin M.letterCount → H) (r : ℝ) (z : List (Fin M.letterCount × ℝ)) :
       ((M.templateScaledWord v r z).map
         (fun q => Exp (q.2 • (M.letter q.1 : GroupLieAlgebra (𝓘(ℝ, EG)) G)))).prod =
       F.inclusionN (generatorGroupWord
         (fun j => Real.exp (r * M.weight j (v j)) • M.letter j) (F.ExpN ∘ F.N.equiv) z) := by
   …

   Mentions: OAI.PolycyclicRecognition.CartanFactorModel, OAI.PolycyclicRecognition.generatorGroupWord

6. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_templateWordPath_bound line 119

   Source documentation

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

   theorem exists_templateWordPath_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 : 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) (N : ℕ) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ r : ℝ, 0 ≤ r →
         ∀ u : List (Fin M.letterCount × ℝ), u.length ≤ N → (∀ z ∈ u, |z.2| ≤ B) →
         PathMetricBound (M.templateWordPath T hExp realize v r u)
           (C * r) (C * (1 + Real.log (2 + r))) ∧
         ∀ t, ∃ z ∈ E,
           (l (M.templateWordPath T hExp realize v r u t)).toAdd = r • z := by
   …

   Mentions: OAI.PolycyclicRecognition.PathMetricBound