Finite HasSum implies Countable support

Stream: Is there code for X?

[Joachim Breitner]

Do we have something like HasSum f c → f.support.Countable, where f : α → Real? (Is it even true?)

[Eric Rodriguez]

(deleted)

[Eric Rodriguez]

It should be true, there's an argument in math.se, I'll dig it up

[Joachim Breitner]

There is one at https://math.stackexchange.com/a/4228200/53195, not sure if it’s the most suitable argument to put into mathlib

[Eric Rodriguez]

Yes, a little care has to be taken because I think some of the argument can come from the fact there's no reordering allowed in mathlib

[Kevin Buzzard]

Without looking at the links: my instinct would be to prove
1) If you're summable then for all eps > 0 there's a finite subset S of alpha with the property that the sum over any finite subset of alpha disjoint from S has abs value less than eps
2) If you're summable then for all eps > 0 the set {x : |f(x)|>eps} is finite
3) done

[Joachim Breitner]

Not pretty yet, but works:

import Mathlib.Topology.Instances.ENNReal

theorem HasSum.countable_support (f : α → NNReal) (h : Summable f) : f.support.Countable := by
  let eps := fun (n : ℕ) => (1/(n+1) : NNReal)
  let s := fun (n : ℕ) => { x : α | eps n ≤ f x }
  have hf : f.support ⊆ ⋃ (n : ℕ), s n := by
    intro a ha
    change f a ≠ 0 at ha
    have ⟨N, hN⟩ := exists_nat_one_div_lt (by positivity : 0 < ((f a):Real))
    exact Set.mem_iUnion_of_mem N hN.le
  apply Set.Countable.mono hf
  rw [Set.countable_iUnion_iff]
  intro n
  apply Set.Finite.countable
  rw [← Set.finite_coe_iff]
  apply Finite.of_summable_const (ι := s n) (b := (eps n : Real))
  . simp; positivity
  . have hs : Summable ((s n).indicator (fun _ => (eps n : NNReal))) :=
      NNReal.summable_of_le (fun a ↦ Set.indicator_le (fun b hb ↦ hb) a) h
    rw [← summable_subtype_iff_indicator] at hs
    rwa [NNReal.summable_coe]

[Kevin Buzzard]

I think there's already the statement that if eps>0 then there's some natural n>0 such that 1/n<eps.

[Kevin Buzzard]

docs#exists_nat_one_div_lt

[Joachim Breitner]

Thanks! Indeed a bit better (updated post above).
PR’ed at https://github.com/leanprover-community/mathlib4/pull/6473