Quasinilpotence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.root_le_prefix_exponential line 14

Source documentation

Taking nth roots of the finite-prefix exponential bound, for n>0.

theorem root_le_prefix_exponential {a A B : ℝ} (ha : 0 ≤ a) {n : ℕ} (hn : 0 < n)
    (hbound : a ≤ Real.exp (B - (n : ℝ)*A)) :
    a ^ (1 / (n : ℝ)) ≤ Real.exp (B / (n : ℝ) - A) := by
…

theorem OAI.FiniteFactor.root_tendsto_zero_of_prefix_bounds line 28

Source documentation

The prefix is fixed before taking n→∞. Its additive loss B(q) may grow arbitrarily with q; no uniform estimate on that loss is required.

theorem root_tendsto_zero_of_prefix_bounds (a A B : ℕ → ℝ)
    (ha : ∀ n, 0 ≤ a n) (hA : Tendsto A atTop atTop)
    (hbound : ∀ (q n : ℕ), 0 < n → a n ≤ Real.exp (B q - (n : ℝ)*A q)) :
    Tendsto (fun n => a n ^ (1 / (n : ℝ))) atTop (𝓝 0) := by
…

theorem OAI.FiniteFactor.norm_quasinilpotent_of_prefix_bounds line 50

Source documentation

Operator form of the analytic reduction, using precisely the norm-root limit in MainTarget. This theorem does not assume spectral-radius theory.

theorem norm_quasinilpotent_of_prefix_bounds {R : Type*} [NormedRing R]
    (T : R) (A B : ℕ → ℝ) (hA : Tendsto A atTop atTop)
    (hbound : ∀ (q n : ℕ), 0 < n → ‖T^n‖ ≤ Real.exp (B q - (n : ℝ)*A q)) :
    Tendsto (fun n : ℕ => ‖T^n‖ ^ (1 / (n : ℝ))) atTop (𝓝 0) :=
…