summable_of_tendsto_weightedOrder_atTop_nhds_top

English

If the weighted order of a family of mv power series tends to infinity, then the family is summable.

Русский

Если взвешенный порядок весов серии стремится к бесконечности, то семейство суммируемо.

LaTeX

$$⟨Tendsto (λ i, weightedOrder w (f i)) atTop (nhds top)⟩ → Summable f$$

Lean4

/-- A family of `MvPowerSeries` is summable if their weighted order tends to infinity. -/
theorem summable_of_tendsto_weightedOrder_atTop_nhds_top {w : σ → ℕ}
    (h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)) : Summable f :=
  by
  rcases isEmpty_or_nonempty ι with hempty | hempty
  · apply summable_empty
  rw [summable_iff_summable_coeff]
  simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop] at h
  intro d
  obtain ⟨i, hi⟩ := h (Finsupp.weight w d)
  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_eq_zero_of_lt_weightedOrder w <| hi k hk.le

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