Summing `ENat`

[SnirBroshi]

There are multiple ways to sum f : ι → ℕ∞, e.g.

• tsum f
• ⨆ s : Finset ι, s.sum f
• (Cardinal.sum <| Cardinal.ofENat.{0} ∘ f).toENat
• ENat.card <| Σ i, Set.Iio (f i)

#Is there code for X? > Summing `ENat`s without topology

ENNReal has theorems that relate the first two, e.g. ENNReal.hasSum and ENNReal.tsum_eq_iSup_sum.

There's a TODO to do the same for ENat.

#38489
#38193

import Mathlib

-- Relate summing `ENat`s to summing `ENNReal`s
example {ι : Type*} (f : ι → ℕ∞) : tsum f = tsum (ENat.toENNReal ∘ f) := sorry
example {ι : Type*} (f : ι → ℕ∞) : tsum f = .floor (tsum <| ENat.toENNReal ∘ f) := sorry
example {ι : Type*} (f : ι → ℕ∞) : tsum f = .ceil (tsum <| ENat.toENNReal ∘ f) := sorry

-- Summing with topology produces the same result as the order summation
-- TODO: is it possible to generalize this to any `OrderTopology α`, not just `ENat`/`ENNReal`?
example {ι : Type*} (f : ι → ℕ∞) : tsum f = ⨆ s : Finset ι, s.sum f := sorry

-- Relate `Cardinal.sum` with the order summation
example {ι : Type*} (f : ι → ℕ∞) :
    (Cardinal.sum <| Cardinal.ofENat.{0} ∘ f).toENat = ⨆ s : Finset ι, s.sum f :=
  sorry