norm_le_div_pow_of_pos_of_lt_radius

English

There exist a∈(0,1) and C>0 such that ‖p_n‖₊ * r^n ≤ C for all n.

Русский

Существуют a∈(0,1) и C>0 такие, что ‖p_n‖₊ r^n ≤ C для всех n.

LaTeX

$$$\\exists a\\in Ioo(0,1),\\exists C>0:\\forall n,\\|p_n\\|_+ \\cdot r^n \\le C.$$$

Lean4

/-- For `r` strictly smaller than the radius of `p`, then `‖pₙ‖ rⁿ` is bounded. -/
theorem norm_le_div_pow_of_pos_of_lt_radius (p : FormalMultilinearSeries 𝕜 E F) {r : ℝ≥0} (h0 : 0 < r)
    (h : (r : ℝ≥0∞) < p.radius) : ∃ C > 0, ∀ n, ‖p n‖ ≤ C / (r : ℝ) ^ n :=
  let ⟨C, hC, hp⟩ := p.norm_mul_pow_le_of_lt_radius h
  ⟨C, hC, fun n => Iff.mpr (le_div_iff₀ (pow_pos h0 _)) (hp n)⟩

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