radius_le_of_le — Mathlib

English

If ∀n, ‖p_n‖ ≤ ‖q_n‖, then radius(q) ≤ radius(p).

Русский

Если для всех n выполняется ‖p_n‖ ≤ ‖q_n‖, то radius(q) ≤ radius(p).

LaTeX

$$$\\forall n,\\; \\|p_n\\| \\le \\|q_n\\| \\Rightarrow q.radius \\le p.radius.$$$

Lean4

theorem radius_le_of_le {𝕜' E' F' : Type*} [NontriviallyNormedField 𝕜'] [NormedAddCommGroup E'] [NormedSpace 𝕜' E']
    [NormedAddCommGroup F'] [NormedSpace 𝕜' F'] {p : FormalMultilinearSeries 𝕜 E F}
    {q : FormalMultilinearSeries 𝕜' E' F'} (h : ∀ n, ‖p n‖ ≤ ‖q n‖) : q.radius ≤ p.radius :=
  by
  apply le_of_forall_nnreal_lt (fun r hr ↦ ?_)
  rcases norm_mul_pow_le_of_lt_radius _ hr with ⟨C, -, hC⟩
  apply le_radius_of_bound _ C (fun n ↦ ?_)
  apply le_trans _ (hC n)
  gcongr
  exact h n

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