radius_pi_le — Mathlib

English

Radius of the pi-power-series is bounded below by the radii of the coordinate series.

Русский

Радиус pi-представления ограничен снизу радиусами компонент.

LaTeX

$$$\\forall p:\\Pi i,\\; (FormalMultilinearSeries.pi p).radius \\ge \\min_i (p i).radius$$$

Lean4

theorem radius_pi_le (p : Π i, FormalMultilinearSeries 𝕜 E (Fm i)) (i : ι) :
    (FormalMultilinearSeries.pi p).radius ≤ (p i).radius :=
  by
  apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
  obtain ⟨C, -, hC⟩ : ∃ C > 0, ∀ n, ‖pi p n‖ * ↑r' ^ n ≤ C := norm_mul_pow_le_of_lt_radius _ hr'
  apply le_radius_of_bound _ C (fun n ↦ ?_)
  apply le_trans _ (hC n)
  gcongr
  rw [pi, ContinuousMultilinearMap.opNorm_pi]
  exact norm_le_pi_norm (fun i ↦ p i n) i

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