English
If a subsequence of partial sums converges to a in a suitable sense and the norms are summable, then HasSum f a.
Русский
Если подпоследовательность частичных сумм сходится к a при условии суммируемости норм, то HasSum f a.
LaTeX
$$$\\text{HasSum } f a \\text{ under subsequence convergence and summable norms}$$$
Lean4
/-- If a function `f` is summable in norm, and along some sequence of finsets exhausting the space
its sum is converging to a limit `a`, then this holds along all finsets, i.e., `f` is summable
with sum `a`. -/
theorem hasSum_of_subseq_of_summable {f : ι → E} (hf : Summable fun a => ‖f a‖) {s : α → Finset ι} {p : Filter α}
[NeBot p] (hs : Tendsto s p atTop) {a : E} (ha : Tendsto (fun b => ∑ i ∈ s b, f i) p (𝓝 a)) : HasSum f a :=
tendsto_nhds_of_cauchySeq_of_subseq (cauchySeq_finset_of_summable_norm hf) hs ha
