English
If a summable sup-norm bound holds eventually for cofinite many indices, the uniform limit of partial sums holds on atTop.
Русский
Если почти все индексы удовлетворяют верхнюю границу норм, частичные суммы сходятся равномерно на бесконечности.
LaTeX
$$$\\text{tendstoUniformly_tsum_of_cofinite_eventually}$$$
Lean4
/-- An infinite sum of functions with eventually summable sup norm is the uniform limit of its
partial sums. Version relative to a set, with general index set. -/
theorem tendstoUniformlyOn_tsum_of_cofinite_eventually {ι : Type*} {f : ι → β → F} {u : ι → ℝ} (hu : Summable u)
{s : Set β} (hfu : ∀ᶠ n in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n) :
TendstoUniformlyOn (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' n, f n x) atTop s := by
classical
refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_
have := (tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos
simp only [gt_iff_lt, eventually_atTop, ge_iff_le, Finset.le_eq_subset] at *
obtain ⟨t, ht⟩ := this
rw [eventually_iff_exists_mem] at hfu
obtain ⟨N, hN, HN⟩ := hfu
refine ⟨hN.toFinset ∪ t, fun n hn x hx => ?_⟩
have A : Summable fun n => ‖f n x‖ :=
by
apply Summable.add_compl (s := hN.toFinset) Summable.of_finite
apply Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) _ (hu.subtype _)
simp only [comp_apply, Subtype.forall, Set.mem_compl_iff, Finset.mem_coe]
aesop
rw [dist_eq_norm, ← A.of_norm.sum_add_tsum_subtype_compl n, add_sub_cancel_left]
apply lt_of_le_of_lt _ (ht n (Finset.union_subset_right hn))
apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
apply (A.subtype _).tsum_le_tsum _ (hu.subtype _)
simp only [comp_apply, Subtype.forall, imp_false]
apply fun i hi => HN i ?_ x hx
have : i ∉ hN.toFinset := fun hg ↦ hi (Finset.union_subset_left hn hg)
simp_all
