OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSampledVisits.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.CartanWordModel.sampledDirectionalVisitPath line 26

   Source documentation

   The root curve uses the normalized interval amplitude.

   def sampledDirectionalVisitPath (v : H) (i : Fin M.letterCount)
       (n : G) (h₀ : H) (r s b : ℝ) :
       Path (n * Exp h₀)
         (n * Exp ((b * Real.exp (r * s)) •
           (M.letter i : GroupLieAlgebra (𝓘(ℝ, EG)) G)) * Exp h₀) := by
   …

2. theorem OAI.PolycyclicRecognition.CartanWordModel.sampledDirectionalVisitPath_apply line 42

   Source documentation

   Scaling the root amplitude does not alter the parametrized geometric visit.

   theorem sampledDirectionalVisitPath_apply (v : H) (i : Fin M.letterCount)
       (n : G) (h₀ : H) (r s b : ℝ) (t : unitInterval) :
       M.sampledDirectionalVisitPath T hExp realize v i n h₀ r s b t =
         M.directionalVisitPath T hExp realize v i n h₀ r (b * Real.exp (r * s)) t := by
   …

3. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_sampled_directional_visit_bound line 58

   Source documentation

   One uniform constant controls the actual normalized interval samples, with no dependence on the starting sheet or the scale.

   theorem exists_sampled_directional_visit_bound
       (haarD : NilpotentExponentialHaarInput F.D.modelSpace F.D.carrier)
       (dynkinD : NilpotentDynkinExpansionInput F.D.modelSpace F.D.carrier)
       {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
       (eW : HeightSpace T.character ≃ₗ[ℝ] W) (π : G →* Multiplicative W)
       (hπ : ∀ x, (π (Exp x)).toAdd = eW (heightProjection T.character x))
       (v : Fin M.letterCount → H) (w₀ : W) (s : Fin M.letterCount → ℝ)
       (hs : ∀ i, cartanHeightWeight T H (M.weight i)
         (eW.symm (w₀ + eW (heightProjection T.character (v i)))) = s i)
       {A ρ : ℝ} (hA : 0 ≤ A) (hρ : 0 ≤ ρ) (p : ℕ) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ r : ℝ, 0 ≤ r → ∀ h₀ : H,
         ‖(finBasis ℝ H).equivFun h₀‖ ≤ A * (1 + r) ^ p →
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.cartanHeightWeight