Tail estimate for abs. convergent series

Stream: Is there code for X?

[Michael Stoll]

I would like to use the following.

import Mathlib

variable {F : Type*} [NormedField F] [CompleteSpace F] {f : ℕ →* F}
variable (hsum : Summable (‖f ·‖))

example {ε : ℝ} (εpos : 0 < ε) :
     ∃ N₀ : ℕ, ∀ N ≥ N₀, ∀ s ⊆ {n | N ≤ n}, ‖∑' m : s, f m‖ < ε := sorry

Tthe assumptions on F can certainly be weakened, but in my use case, I need a field.)

Any hints?

[Michael Stoll]

This is the last sorry on the way to the Euler product, BTW.

[Michael Stoll]

My feeling is that it should come down to a fairly easy manipulation with filters, but I have no experience with this part of Mathlib so far.

[Terence Tao]

summable_iff_vanishing_norm seems close to what you want.

[Junyan Xu]

docs#tendsto_tsum_compl_atTop_zero is closer I think :)

[Kevin Buzzard]

Another hurdle is that docs#summable_abs_iff says Summable f iff Summable |f| but here we have some norm on a complete space rather than an absolute value.

[Junyan Xu]

I think this can be proven without the Summable hypothesis. I'm using docs#NormedAddCommGroup.tendsto_nhds_zero.

[Kevin Buzzard]

I mean, it's not true if $f(x)=1$ for all $x$? What do you mean?(it is true, for silly reasons :-) )

[Junyan Xu]

Hmm indeed the lemma docs#tendsto_tsum_compl_atTop_zero without the summability assumption isn't quite strong enough; it can deal with sets that contain an infinite interval but not a general set.

[Junyan Xu]

If it's not summable then the tsum (∑') is zero, and I think that's why tendsto_tsum_compl_atTop_zero doesn't have the summability assumption.

[Junyan Xu]

The statement seems a bit redundant: instead of ∀ N ≥ N₀, ∀ s ⊆ {n | N ≤ n} it's equivalent to say ∀ s ⊆ {n | N₀ ≤ n}.

[Junyan Xu]

Okay, I proved a slightly modified version (removing the redundancy and change to weak inequality to not make the proof more complicated):

import Mathlib

variable {F : Type*} [NormedField F] [CompleteSpace F] {f : ℕ →* F}
variable (hsum : Summable (‖f ·‖))

example {ε : ℝ} (εpos : 0 < ε) :
     ∃ N : ℕ, ∀ s ⊆ {n | N ≤ n}, ‖∑' m : s, f m‖ ≤ ε := by
  obtain ⟨t, ht⟩ := summable_iff_vanishing.mp hsum _ (Metric.closedBall_mem_nhds 0 εpos)
  use if emp : t.Nonempty then t.max' emp + 1 else 0
  refine fun s hs ↦ (norm_tsum_le_tsum_norm <| hsum.subtype _).trans ?_
  refine tsum_le_of_sum_le (hsum.subtype _) fun s' ↦ (le_abs_self _).trans ?_
  rw [← Finset.sum_subtype_map_embedding (g := fun i ↦ ‖f i‖) fun _ _ ↦ rfl]
  simp_rw [mem_closedBall_zero_iff, Real.norm_eq_abs, Finset.disjoint_left] at ht
  refine ht _ fun n hns' hnt ↦ ?_
  obtain ⟨⟨m, hms⟩, -, rfl⟩ := Finset.mem_map.mp hns'
  have := hs hms
  split_ifs at this with h
  · exact (t.le_max' _ hnt).not_lt ((Nat.lt_succ_self _).trans_le this)
  · exact h ⟨m, hnt⟩

[Junyan Xu]

I used docs#summable_iff_vanishing instead of docs#summable_iff_vanishing_norm (mentioned by Terry) because we can't use docs#summable_norm_iff as we're not working with a normed real vector space (edit: we can still use docs#summable_of_summable_norm though). Other key lemmas include docs#tsum_le_of_sum_le, docs#norm_tsum_le_tsum_norm, and docs#Summable.subtype.

[Junyan Xu]

I'm adding a general lemma as well as Nat specific version at #8194:

Summable f ↔ ∀ e ∈ 𝓝 (0 : α), ∃ s : Finset β, ∀ t : Set β, Disjoint t s → (∑' b : t, f b) ∈ e
Summable f ↔ ∀ e ∈ 𝓝 (0 : α), ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∑' b : t, f b) ∈ e

and the desired example can be obtained by taking e to be an open ball.

[Michael Stoll]

Thanks!