Proving the `iUnion` Theorem for `OuterMeasure` Inductively

Stream: new members

[Peter Hansen]

Hello everyone,

I'm currently delving into measure theory within Lean and am tackling the iUnion theorem for an OuterMeasure structure. In Mathlib, there's already an elegant one-liner proof leveraging rel_iSup_tsum, but I'm curious about the possibility of an inductive approach. Here's the context:

import Mathlib.Tactic
import Mathlib.MeasureTheory.PiSystem

open BigOperators ENNReal

structure OuterMeasure (α : Type*) where
  measureOf : Set α → ℝ≥0∞
  empty : measureOf ∅ = 0
  mono : ∀ {s₁ s₂}, s₁ ⊆ s₂ → measureOf s₁ ≤ measureOf s₂
  iUnion_nat : ∀ s : ℕ → Set α, measureOf (⋃ i, s i) ≤ ∑' i, measureOf (s i)

variable {α : Type*}

instance instCoeFun : CoeFun (OuterMeasure α) (λ _ => Set α → ℝ≥0∞) where
  coe m := m.measureOf

theorem iUnion (m : OuterMeasure α) {β} [Countable β] (s : β → Set α) :
  m (⋃ i, s i) ≤ ∑' i, m (s i) :=
  rel_iSup_tsum m m.empty (· ≤ ·) m.iUnion_nat s

Before tackling this, I managed to prove the union theorem for two sets in a more traditional, textbook-like manner:

theorem union (m : OuterMeasure α) (s₁ s₂ : Set α) : m (s₁ ∪ s₂) ≤ m s₁ + m s₂ := sorry

Is there an established inductive principle for countable types in Lean that could facilitate such a proof building upon the union theorem?

[Eric Wieser]

It might be instructive to go through the proof within docs#rel_iSup_tsum

[Peter Hansen]

I suppose the proof might be inductive in the broadest sense of the word, but I was kinda hoping one could reason about countable types using their cardinality - if that makes sense. Something along the line of

protected theorem ifUnion (φ : OuterMeasure X) {n : ℕ} (S : ℕ → Set X) :
    φ (⋃ (i ≤  n) , S i) ≤ ∑ a in Finset.range (n + 1), φ (S a) := by
    simp only [← Nat.lt_succ]
    induction' n with n NH
    simp
    rw [@Finset.sum_range_succ, @biUnion_lt_succ]
    apply (φ.union _ _).trans (add_le_add NH _)
    rfl