every unitInterval function is truncated summable

Stream: mathlib4

[Ira Fesefeldt]

I would like to prove that every function with co-domain in the unitInterval is summable if using the truncated sum - i.e. the sum which sets to 1 if it exceeds 1.

I believe that holds as every function is non negative and sums are always bounded by 1. However, my topology expertise definitely isn't sufficient for the proof and I cannot find any lemma (and I don't even know where to search for it), that could help me here.

Can someone maybe give me a pointer or some tips how to proceed? Even how to eliminate the neighborhood of s in the following example could help me!

import Mathlib.Topology.UnitInterval
import Mathlib.Topology.Algebra.InfiniteSum.Basic

open unitInterval Classical Set.Icc

noncomputable instance unit_cl : CompleteLinearOrder I := completeLinearOrder (by simp)

theorem truncatedAdd_mem_unit (i j : I) : min 1 ((i:ℝ) + j) ∈ I := by
  apply And.intro
  · exact le_min zero_le_one (add_nonneg i.property.1 j.property.1)
  · exact min_le_left 1 ((i:ℝ)+j)

noncomputable def truncatedAdd (i j : I) : I := ⟨min 1 (i + j), truncatedAdd_mem_unit i j⟩

noncomputable instance : Add unitInterval where
  add := truncatedAdd

noncomputable instance : OrderedAddCommMonoid unitInterval where
  add_assoc := sorry -- left out for brevity
  add_comm := sorry -- left out for brevity
  zero_add := sorry -- left out for brevity
  add_zero := sorry -- left out for brevity
  nsmul := nsmulRec
  add_le_add_left := sorry -- left out for brevity

theorem unitInterval_summable (f : α → I) : Summable f := by
  use (∑' a : α, f a)
  unfold HasSum
  rw [Filter.tendsto_def]
  intro s h_s
  simp only [Filter.mem_atTop_sets, ge_iff_le, Finset.le_eq_subset, Set.mem_preimage]
  sorry -- how to proceed from here

[Ira Fesefeldt]

I solved it :smiling_face:

The solution was to just copy what ENNReal did:

import Mathlib.Topology.UnitInterval
import Mathlib.Topology.Algebra.InfiniteSum.Basic
import Mathlib.Topology.Order.MonotoneConvergence

open unitInterval Classical Set.Icc

noncomputable instance unit_cl : CompleteLinearOrder I := completeLinearOrder (by simp)

theorem truncatedAdd_mem_unit (i j : I) : min 1 ((i:ℝ) + j) ∈ I := by
  apply And.intro
  · exact le_min zero_le_one (add_nonneg i.property.1 j.property.1)
  · exact min_le_left 1 ((i:ℝ)+j)

noncomputable def truncatedAdd (i j : I) : I := ⟨min 1 (i + j), truncatedAdd_mem_unit i j⟩

noncomputable instance : Add unitInterval where
  add := truncatedAdd

noncomputable instance : OrderedAddCommMonoid unitInterval where
  add_assoc := sorry
  add_comm := sorry
  zero_add := sorry
  add_zero := sorry
  nsmul := nsmulRec
  add_le_add_left := sorry

noncomputable instance : CanonicallyOrderedAddCommMonoid unitInterval where
  exists_add_of_le := sorry
  le_self_add := sorry

theorem hasSum (f : α → I) : HasSum f (⨆ s : Finset α, ∑ a ∈ s, f a) :=
  tendsto_atTop_iSup fun _ _ => Finset.sum_le_sum_of_subset

theorem isSummable (f : α → I) : Summable f := ⟨_,hasSum f⟩