English
If the order of a family tends to infinity, then the family is summable.
Русский
Если порядок семейства стремится к бесконечности, то оно суммируемо.
LaTeX
$$$ \\text{Summable by order to } \\infty $$$
Lean4
/-- If the order of a family of `PowerSeries` tends to infinity, the collection of all
possible products over `Finset` is summable. -/
theorem summable_prod_of_tendsto_order_atTop_nhds_top (h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)) :
Summable (∏ i ∈ ·, f i) := by
rcases isEmpty_or_nonempty ι with hempty | hempty
· apply Summable.of_finite
refine (summable_iff_summable_coeff _).mpr fun n ↦ summable_of_finite_support ?_
simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, eventually_atTop] at h
obtain ⟨i, hi⟩ := h n
apply (Finset.Iio i).powerset.finite_toSet.subset
suffices ∀ s : Finset ι, coeff n (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i by simpa
intro s hs
contrapose! hs
obtain ⟨x, hxs, hxi⟩ := Set.not_subset.mp hs
rw [Set.mem_Iio, not_lt] at hxi
refine coeff_of_lt_order _ <| (hi x hxi).trans_le <| le_trans ?_ (le_order_prod _ _)
apply Finset.single_le_sum (by simp) hxs
