OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentCoordinateFlow.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.coordinateEnd line 16
2. theorem OAI.PolycyclicRecognition.coordinateEnd_apply line 20
3. theorem OAI.PolycyclicRecognition.coordinateEnd_pow_apply line 23
4. theorem OAI.PolycyclicRecognition.coordinateEnd_pow_zero line 31
5. def OAI.PolycyclicRecognition.finiteEndFlow line 40

   Source documentation

   The polynomial is independent of a norm or coordinates on the algebra.

   def finiteEndFlow (D : Module.End ℝ V) (k : ℕ) (t : ℝ) (v : V) : V :=
   …

6. theorem OAI.PolycyclicRecognition.finiteEndFlow_smul line 43
7. theorem OAI.PolycyclicRecognition.coordinate_finiteEndFlow line 51
8. theorem OAI.PolycyclicRecognition.finiteEndFlow_map line 61
9. theorem OAI.PolycyclicRecognition.finiteEndFlow_eq_exp line 72
10. theorem OAI.PolycyclicRecognition.eventually_uniform_nilpotent_exp_ball line 85

    Source documentation

    Uniformity over the shrinking input ball follows from the same nilpotent exponential estimate, by choosing a violating vector if one exists.

    theorem eventually_uniform_nilpotent_exp_ball [Nonempty (Fin n)]
        (D : ℝ → (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) (t : ℝ → ℝ) {m : ℕ}
        (hD : ∀ r, D r ^ (m + 1) = 0) {A α η : ℝ}
        (hA : 0 ≤ A) (hα : 0 ≤ α) (hgap : (m : ℝ) * α < η)
        (ε : ℝ → ℝ) (hε : Tendsto ε atTop (𝓝 0))
        (hbound : ∀ᶠ r in atTop, ‖D r‖ ≤ A)
        (ht : ∀ᶠ r in atTop, |t r| ≤ Real.exp ((α + ε r) * r)) :
        ∀ᶠ r in atTop, ∀ v : Fin n → ℝ, ‖v‖ ≤ Real.exp (-η * r) →
          ‖NormedSpace.exp (t r • D r) v‖ ≤ 1 := by
    …