English
Equality of pi-radius with iInf of component radii.
Русский
Радиус pi равен inf-снижению минимальных радиусов компонент.
LaTeX
$$$(FormalMultilinearSeries.pi p).radius = \\bigsqcap_i (p i).radius$$$
Lean4
theorem le_radius_pi (h : ∀ i, r ≤ (p i).radius) : r ≤ (FormalMultilinearSeries.pi p).radius :=
by
apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
have I i : ∃ C > 0, ∀ n, ‖p i n‖ * (r' : ℝ) ^ n ≤ C := norm_mul_pow_le_of_lt_radius _ (hr'.trans_le (h i))
choose C C_pos hC using I
obtain ⟨D, D_nonneg, hD⟩ : ∃ D ≥ 0, ∀ i, C i ≤ D :=
⟨∑ i, C i, Finset.sum_nonneg (fun i _ ↦ (C_pos i).le), fun i ↦
Finset.single_le_sum (fun j _ ↦ (C_pos j).le) (Finset.mem_univ _)⟩
apply le_radius_of_bound _ D (fun n ↦ ?_)
rcases le_or_gt ((r' : ℝ) ^ n) 0 with hr' | hr'
· exact le_trans (mul_nonpos_of_nonneg_of_nonpos (by positivity) hr') D_nonneg
· simp only [pi]
rw [← le_div_iff₀ hr', ContinuousMultilinearMap.opNorm_pi, pi_norm_le_iff_of_nonneg (by positivity)]
intro i
exact (le_div_iff₀ hr').2 ((hC i n).trans (hD i))
