NilpotentFlow.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Nilpotent corrections in a contracting weight flow

The nilpotent part of the infinitesimal action gives a polynomial bound for its actual analytic exponential. Coupled with scalar exponential contraction, it gives logarithmic metric distortion of the weight chart.

theorem OAI.PolycyclicRecognition.exp_smul_sub_one line 20

Source documentation

Split the scalar weight from the nilpotent part in the actual analytic exponential of the infinitesimal generator.

theorem exp_smul_sub_one
    {A : Type*} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A]
    (N : A) (t : ℝ) :
    NormedSpace.exp (t • (N - 1)) = Real.exp (-t) • NormedSpace.exp (t • N) := by
…

theorem OAI.PolycyclicRecognition.norm_exp_smul_nilpotent_le line 36

Source documentation

The actual exponential of a nilpotent operator has polynomial growth in its real parameter, with an explicit uniform coefficient.

theorem norm_exp_smul_nilpotent_le
    {A : Type*} [NormedRing A] [NormedAlgebra ℝ A] [NormOneClass A]
    (N : A) {c : ℕ} (hN : N ^ (c + 1) = 0) {t : ℝ} (ht : 0 ≤ t) :
    ‖NormedSpace.exp (t • N)‖ ≤
      ((c : ℝ) + 1) * (1 + ‖N‖) ^ c * (1 + t) ^ c := by
…

theorem OAI.PolycyclicRecognition.norm_contracted_nilpotent_flow_le line 64

Source documentation

The infinitesimal nilpotent correction, with its actual operator exponential, has exactly the polynomially corrected contraction needed above.

theorem norm_contracted_nilpotent_flow_le
    {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] [Nontrivial V]
    (N : V →L[ℝ] V) {c : ℕ} (hN : N ^ (c + 1) = 0)
    (v : V) {t : ℝ} (ht : 0 ≤ t) :
    ‖Real.exp (-t) • (NormedSpace.exp (t • N)) v‖ ≤
      (((c : ℝ) + 1) * (1 + ‖N‖) ^ c) * (1 + t) ^ c * Real.exp (-t) * ‖v‖ := by
…

theorem OAI.PolycyclicRecognition.logarithmic_distortion_of_nilpotent_flow line 84

Source documentation

A continuous weight chart with a nilpotent correction in its contracting action is logarithmically distorted. This is the individual weight-space estimate, before taking bounded products of generator directions.

theorem logarithmic_distortion_of_nilpotent_flow
    {G : Type*} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
    {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    [CompleteSpace V] [Nontrivial V] [ProperSpace V]
    (Exp : V → G) (hExp : Continuous Exp)
    (d : ℝ → G) (hd : Continuous d) (hd0 : d 0 = 1)
    (hmul : ∀ s t, d (s + t) = d s * d t)
    (N : V →L[ℝ] V) {c : ℕ} (hN : N ^ (c + 1) = 0)
    (hconj : ∀ v t, 0 ≤ t → Exp v =
      d t * Exp (Real.exp (-t) • (NormedSpace.exp (t • N)) v) * (d t)⁻¹) :
    ∃ D : ℝ, 0 < D ∧ ∀ v, dist 1 (Exp v) ≤ D * Real.log (2 + ‖v‖) := by
…

theorem OAI.PolycyclicRecognition.logarithmic_distortion_of_weight_generator line 102

Source documentation

The same distortion conclusion stated directly for a generator whose nilpotent part is N and whose real weight is -1.

theorem logarithmic_distortion_of_weight_generator
    {G : Type*} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
    {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    [CompleteSpace V] [Nontrivial V] [ProperSpace V]
    (Exp : V → G) (hExp : Continuous Exp)
    (d : ℝ → G) (hd : Continuous d) (hd0 : d 0 = 1)
    (hmul : ∀ s t, d (s + t) = d s * d t)
    (N : V →L[ℝ] V) {c : ℕ} (hN : N ^ (c + 1) = 0)
    (hconj : ∀ v t, 0 ≤ t → Exp v =
      d t * Exp ((NormedSpace.exp (t • (N - 1))) v) * (d t)⁻¹) :
    ∃ D : ℝ, 0 < D ∧ ∀ v, dist 1 (Exp v) ≤ D * Real.log (2 + ‖v‖) := by
…