OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanIntervalVisits.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.inclusion_rootIntervalSample line 27
2. theorem OAI.PolycyclicRecognition.CartanWordModel.supportVisitPath_apply_eq_sampled line 37

   Source documentation

   Coordinate descriptions of the same root curve produce the same visit.

   theorem supportVisitPath_apply_eq_sampled
       (v : H) (i : Fin M.letterCount) (n k : G) (h₀ : H) (r s b : ℝ)
       (f : ℝ → G) (hf : Continuous f) (hf₀ : f 0 = 1)
       (he : ∀ t, f t = Exp ((t * Real.exp (r * s)) •
         (M.letter i : GroupLieAlgebra (𝓘(ℝ, EG)) G)))
       (hd : Continuous (fun t : ℝ => Exp (t • (v : GroupLieAlgebra (𝓘(ℝ, EG)) G))))
       (hd₀ : Exp ((0 : ℝ) • (v : GroupLieAlgebra (𝓘(ℝ, EG)) G)) = 1)
       (hk : k = Exp h₀) (t : unitInterval) :
       supportVisitPath (fun t => Exp (t • (v : GroupLieAlgebra (𝓘(ℝ, EG)) G)))
         hd hd₀ f hf hf₀ n k r b t =
         M.sampledDirectionalVisitPath T hExp realize v i n h₀ r s b t := by
   …

   Mentions: OAI.PolycyclicRecognition.supportVisitPath