English
If the weighted order tends to infinity, then the collection of all finite products ∏ i ∈ s f_i, parameterized by finite subsets s, is summable.
Русский
Если взвешенный порядок стремится к бесконечности, то множество всех конечных произведений ∏ i ∈ s f_i суммируемо.
LaTeX
$$Summable (λ x, x.prod (λ i, f i))$$
Lean4
/-- If the weighted order of a family of `MvPowerSeries` tends to infinity, the collection of all
possible products over `Finset` is summable. -/
theorem summable_prod_of_tendsto_weightedOrder_atTop_nhds_top {w : σ → ℕ}
(h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)) : Summable (∏ i ∈ ·, f i) :=
by
rcases isEmpty_or_nonempty ι with hempty | hempty
· apply Summable.of_finite
refine summable_iff_summable_coeff.mpr fun d ↦ summable_of_finite_support ?_
simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, eventually_atTop] at h
obtain ⟨i, hi⟩ := h (Finsupp.weight w d)
apply (Finset.Iio i).powerset.finite_toSet.subset
suffices ∀ s : Finset ι, coeff d (∏ 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_eq_zero_of_lt_weightedOrder w <| (hi x hxi).trans_le <| ?_
apply le_trans (Finset.single_le_sum (by simp) hxs) (le_weightedOrder_prod w _ _)
