le_mul_pow_of_radius_pos — Mathlib

English

The radius of the sum p+q is at least the minimum of the radii of p and q.

Русский

Радиус суммы p+q не меньше минимума радиусов p и q.

LaTeX

$$$\\min(p.radius, q.radius) \\le (p+q).radius.$$$

Lean4

/-- If the radius of `p` is positive, then `‖pₙ‖` grows at most geometrically. -/
theorem le_mul_pow_of_radius_pos (p : FormalMultilinearSeries 𝕜 E F) (h : 0 < p.radius) :
    ∃ (C r : _) (_ : 0 < C) (_ : 0 < r), ∀ n, ‖p n‖ ≤ C * r ^ n :=
  by
  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨r, r0, rlt⟩
  have rpos : 0 < (r : ℝ) := by simp [ENNReal.coe_pos.1 r0]
  rcases norm_le_div_pow_of_pos_of_lt_radius p rpos rlt with ⟨C, Cpos, hCp⟩
  refine ⟨C, r⁻¹, Cpos, by simp only [inv_pos, rpos], fun n => ?_⟩
  rw [inv_pow, ← div_eq_mul_inv]
  exact hCp n

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