norm_mul_pow_le_of_lt_radius — Mathlib

English

There exists C>0 with ‖p_n‖ ≤ C / r^n for all n, whenever r is below the radius.

Русский

Существуют C>0 такие, что ‖p_n‖ ≤ C / r^n для всех n, если r ниже радиуса.

LaTeX

$$$\\exists C>0:\\forall n,\\|p_n\\| \\le C / r^n.$$$

Lean4

/-- For `r` strictly smaller than the radius of `p`, then `‖pₙ‖ rⁿ` is bounded. -/
theorem norm_mul_pow_le_of_lt_radius (p : FormalMultilinearSeries 𝕜 E F) {r : ℝ≥0} (h : (r : ℝ≥0∞) < p.radius) :
    ∃ C > 0, ∀ n, ‖p n‖ * (r : ℝ) ^ n ≤ C :=
  let ⟨_, ha, C, hC, h⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius h
  ⟨C, hC, fun n => (h n).trans <| mul_le_of_le_one_right hC.lt.le (pow_le_one₀ ha.1.le ha.2.le)⟩

Похожие утверждения