summable_of_tendsto_order_atTop_nhds_top

English

If the order of f_i tends to infinity along atTop, then the family f is summable.

Русский

Если порядок f_i стремится к бесконечности вдоль atTop, то семейство f суммируемо.

LaTeX

$$$ \\text{Tendsto} (i \\mapsto (f(i)).order) \\text{ atTop } (nhds \\top) \\Rightarrow \\text{Summable } f $$$

Lean4

/-- A family of `PowerSeries` is summable if their order tends to infinity. -/
theorem summable_of_tendsto_order_atTop_nhds_top [LinearOrder ι] [LocallyFiniteOrderBot ι]
    (h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)) : Summable f :=
  by
  rcases isEmpty_or_nonempty ι with hempty | hempty
  · apply summable_empty
  rw [summable_iff_summable_coeff]
  intro n
  simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop] at h
  obtain ⟨i, hi⟩ := h n
  refine summable_of_finite_support <| (Set.finite_Iic i).subset ?_
  simp_rw [Function.support_subset_iff, Set.mem_Iic]
  intro k hk
  contrapose! hk
  exact coeff_of_lt_order _ <| by simpa using (hi k hk.le)

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