OAI/GroupTheory/PolycyclicRecognition/Geometry/MovingBaseFlow.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.basedDynkinFlowMap line 16

   Source documentation

   A rescaled Cartan leg with its moving initial coordinate retained.

   def basedDynkinFlowMap {c : ℕ} (a : DynkinCoefficients c 2)
       (B : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ))
       (base v : Fin n → ℝ) : C(ℝ, Fin n → ℝ) :=
   …

   Mentions: OAI.PolycyclicRecognition.DynkinCoefficients

2. theorem OAI.PolycyclicRecognition.continuous_basedDynkinFlowMap line 23
3. theorem OAI.PolycyclicRecognition.exists_compact_eventual_based_dynkin_leg line 40

   Source documentation

   All sufficiently late actual legs lie in one compact part of the open profile domain, even though the initial pivot coordinate varies.

   theorem exists_compact_eventual_based_dynkin_leg
       {c : ℕ} (a : DynkinCoefficients c 2)
       (B : ℕ → (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ))
       (B₀ : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ))
       (base v : ℕ → Fin n → ℝ) (base₀ v₀ : Fin n → ℝ)
       (hB : Tendsto B atTop (𝓝 B₀)) (hb : Tendsto base atTop (𝓝 base₀))
       (hv : Tendsto v atTop (𝓝 v₀))
       (U : Set (Fin n → ℝ)) (hU : IsOpen U)
       (hinside : ∀ t ∈ Icc (0 : ℝ) 1, dynkinProduct a B₀ base₀ (t • v₀) ∈ U) :
       ∃ Q : Set (Fin n → ℝ), IsCompact Q ∧ Q ⊆ U ∧
         ∀ᶠ k in atTop, ∀ t ∈ Icc (0 : ℝ) 1,
           dynkinProduct a (B k) (base k) (t • v k) ∈ Q := by
   …

   Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.dynkinProduct