English
For a countable index set, the measure of the union equals the supremum of the measures of Accumulate f(i).
Русский
Для счётного индекса μ(⋃ i, f(i)) = ⨆ i, μ(Accumulate f(i)).
LaTeX
$$$ μ(⋃ i, f(i)) = \bigsup_i μ(Accumulate f(i)) $$$
Lean4
/-- Continuity from below:
the measure of the union of a directed sequence of (not necessarily measurable) sets
is the supremum of the measures. -/
theorem _root_.Directed.measure_iUnion [Countable ι] {s : ι → Set α} (hd : Directed (· ⊆ ·) s) :
μ (⋃ i, s i) = ⨆ i, μ (s i) := by
-- WLOG, `ι = ℕ`
rcases Countable.exists_injective_nat ι with ⟨e, he⟩
generalize ht : Function.extend e s ⊥ = t
replace hd : Directed (· ⊆ ·) t := ht ▸ hd.extend_bot he
suffices μ (⋃ n, t n) = ⨆ n, μ (t n)
by
simp only [← ht, Function.apply_extend μ, ← iSup_eq_iUnion, iSup_extend_bot he, Function.comp_def, Pi.bot_apply,
bot_eq_empty, measure_empty] at this
exact this.trans (iSup_extend_bot he _)
clear! ι
refine
le_antisymm ?_
(iSup_le fun i ↦ measure_mono <| subset_iUnion _ _)
-- Choose `T n ⊇ t n` of the same measure, put `Td n = disjointed T`
set T : ℕ → Set α := fun n => toMeasurable μ (t n)
set Td : ℕ → Set α := disjointed T
have hm : ∀ n, MeasurableSet (Td n) := .disjointed fun n ↦ measurableSet_toMeasurable _ _
calc
μ (⋃ n, t n) = μ (⋃ n, Td n) := by rw [iUnion_disjointed, measure_iUnion_toMeasurable]
_ ≤ ∑' n, μ (Td n) := (measure_iUnion_le _)
_ = ⨆ I : Finset ℕ, ∑ n ∈ I, μ (Td n) := ENNReal.tsum_eq_iSup_sum
_ ≤ ⨆ n, μ (t n) :=
iSup_le fun I => by
rcases hd.finset_le I with ⟨N, hN⟩
calc
(∑ n ∈ I, μ (Td n)) = μ (⋃ n ∈ I, Td n) :=
(measure_biUnion_finset ((disjoint_disjointed T).set_pairwise I) fun n _ => hm n).symm
_ ≤ μ (⋃ n ∈ I, T n) := (measure_mono (iUnion₂_mono fun n _hn => disjointed_subset _ _))
_ = μ (⋃ n ∈ I, t n) := (measure_biUnion_toMeasurable I.countable_toSet _)
_ ≤ μ (t N) := (measure_mono (iUnion₂_subset hN))
_ ≤ ⨆ n, μ (t n) := le_iSup (μ ∘ t) N
