OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentConjugationDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.nilpotent_exp_apply_tendsto_zero_of_exponent_gap line 21

   Source documentation

   A uniformly nilpotent operator can grow exponentially more slowly than its input contracts. Its exponential still sends that input to zero.

   theorem nilpotent_exp_apply_tendsto_zero_of_exponent_gap
       {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] [Nontrivial V]
       (N : ℝ → V →L[ℝ] V) (v : ℝ → V) {m : ℕ}
       (hnil : ∀ r, (N r) ^ (m + 1) = 0)
       {A B α β : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hα : 0 ≤ α)
       (hgap : (m : ℝ) * α < β)
       (hN : ∀ᶠ r : ℝ in atTop, ‖N r‖ ≤ A * Real.exp (α * r))
       (hv : ∀ᶠ r : ℝ in atTop, ‖v r‖ ≤ B * Real.exp (-β * r)) :
       Tendsto (fun r => NormedSpace.exp (N r) (v r)) atTop (𝓝 0) := by
   …

2. theorem OAI.PolycyclicRecognition.nilpotent_exp_apply_tendsto_zero_of_subexponential_bounds line 63

   Source documentation

   The same exponential gap absorbs a common subexponential envelope in both the conjugating operator and the translated vector.

   theorem nilpotent_exp_apply_tendsto_zero_of_subexponential_bounds
       {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] [Nontrivial V]
       (N : ℝ → V →L[ℝ] V) (v : ℝ → V) {m : ℕ}
       (hnil : ∀ r, (N r) ^ (m + 1) = 0)
       {A B α β : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hα : 0 ≤ α)
       (hgap : (m : ℝ) * α < β)
       (ε : ℝ → ℝ) (hε : Tendsto ε atTop (𝓝 0))
       (hN : ∀ᶠ r : ℝ in atTop, ‖N r‖ ≤ A * Real.exp ((α + ε r) * r))
       (hv : ∀ᶠ r : ℝ in atTop, ‖v r‖ ≤ B * Real.exp ((-β + ε r) * r)) :
       Tendsto (fun r => NormedSpace.exp (N r) (v r)) atTop (𝓝 0) := by
   …