GradedFlowLimit.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Convergence of horizontal flows in graded coordinates

def OAI.PolycyclicRecognition.dynkinFlowMap line 19
Source documentation
Right multiplication along the exponential line with velocity v, recorded jointly in its base point and time.
```
def dynkinFlowMap {c : ℕ} (a : DynkinCoefficients c 2)
    (B : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) (v : (Fin n → ℝ)) : C((Fin n → ℝ) × ℝ, (Fin n → ℝ)) :=
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients
theorem OAI.PolycyclicRecognition.continuous_dynkinFlowMap line 27
Source documentation
The polynomial flow depends continuously on its bracket and velocity in the topology of uniform convergence on compact sets.
```
theorem continuous_dynkinFlowMap {c : ℕ} (a : DynkinCoefficients c 2) :
    Continuous (fun p : ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) × (Fin n → ℝ) => dynkinFlowMap (n := n) a p.1 p.2) := by
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.dynkinFlowMap
theorem OAI.PolycyclicRecognition.dynkinFlowMap_tendsto line 37

theorem OAI.PolycyclicRecognition.dynkinFlowMap_tendstoUniformlyOn line 48

Source documentation

Simultaneous convergence of base points and times on any fixed compact set. This is the flow convergence used by chart profiles.

theorem dynkinFlowMap_tendstoUniformlyOn {c : ℕ} (a : DynkinCoefficients c 2)
    {ι : Type*} {l : Filter ι} {B : ι → (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)}
    {B₀ : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)} {v : ι → (Fin n → ℝ)} {v₀ : (Fin n → ℝ)}
    (hB : Tendsto B l (𝓝 B₀)) (hv : Tendsto v l (𝓝 v₀))
    {K : Set ((Fin n → ℝ) × ℝ)} (hK : IsCompact K) :
    TendstoUniformlyOn (fun i z => dynkinProduct a (B i) z.1 (z.2 • v i))
      (fun z => dynkinProduct a B₀ z.1 (z.2 • v₀)) l K :=
…

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

theorem OAI.PolycyclicRecognition.rescaled_horizontal_flow_tendstoUniformlyOn line 62

Source documentation

Actual rescaled exponential lines tend to the line of the degree-one part of their velocity, with the limiting graded multiplication.

theorem rescaled_horizontal_flow_tendstoUniformlyOn
    {c : ℕ} (a : DynkinCoefficients c 2) (b : Basis (Fin n) ℝ L)
    (cost : Fin n → ℝ)
    (hweight : ∀ i j k, b.repr ⁅b i, b j⁆ k ≠ 0 → cost i + cost j ≤ cost k)
    (v : L) (hv : ∀ j, b.repr v j ≠ 0 → 1 ≤ cost j)
    {K : Set ((Fin n → ℝ) × ℝ)} (hK : IsCompact K) :
    TendstoUniformlyOn
      (fun r z => dynkinProduct a (basisBracket (exponentialRescaleBasis b cost r))
        z.1 (z.2 • (exponentialRescaleBasis b cost r).equivFun (Real.exp r • v)))
      (fun z => dynkinProduct a (gradedCoordinateBracket b cost)
        z.1 (z.2 • gradedGenerator b cost 1 v)) atTop K := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.basisBracket, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.gradedCoordinateBracket, OAI.PolycyclicRecognition.gradedGenerator