TrajectoryProductLimits.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Common compact limits of normalized quotient trajectories

theorem OAI.PolycyclicRecognition.trajectory_compact_uniform_limit_of_log_increments line 17

Source documentation

The actual trajectory, normalized at its first point, equals the ordered product of its logarithmic increments. A common summable bound therefore gives uniform coordinate convergence and a common compact limit set.

theorem trajectory_compact_uniform_limit_of_log_increments
    {P E Q J : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] [TopologicalSpace Q] [ChartedSpace E Q] [Group Q]
    [LieGroup (𝓘(ℝ, E)) ⊤ Q] [T2Space Q] [Fintype J]
    (dynkin : NilpotentDynkinExpansionInput E Q)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) Q → Q) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) Q ≃ₜ Q) (hchart : ∀ v, chart v = Exp v)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) Q))
    (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) Q))
    (f : P → ℕ → Q) (X : P → ℕ → GroupLieAlgebra (𝓘(ℝ, E)) Q)
    (a : ℕ → ℝ) (ha : Summable a) (hX : ∀ p n, ‖b.equivFun (X p n)‖ ≤ a n)
    (hstep : ∀ p n, f p (n + 1) = f p n * Exp (X p n)) :
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput