English
If μ.restrict s and μ.restrict t are sigma-finite, then μ.restrict (s ∪ t) is sigma-finite.
Русский
Если μ.restrict s и μ.restrict t сигма-конечны, то μ.restrict (s ∪ t) сигма-конечна.
LaTeX
$$instance [SigmaFinite (μ.restrict s)] [SigmaFinite (μ.restrict t)] : SigmaFinite (μ.restrict (s ∪ t))$$
Lean4
instance sigmaFinite {ι} [Finite ι] (μ : ι → Measure α) [∀ i, SigmaFinite (μ i)] : SigmaFinite (sum μ) :=
by
cases nonempty_fintype ι
have : ∀ n, MeasurableSet (⋂ i : ι, spanningSets (μ i) n) := fun n =>
MeasurableSet.iInter fun i => measurableSet_spanningSets (μ i) n
refine ⟨⟨⟨fun n => ⋂ i, spanningSets (μ i) n, fun _ => trivial, fun n => ?_, ?_⟩⟩⟩
· rw [sum_apply _ (this n), tsum_fintype, ENNReal.sum_lt_top]
rintro i -
exact (measure_mono <| iInter_subset _ i).trans_lt (measure_spanningSets_lt_top (μ i) n)
· rw [iUnion_iInter_of_monotone]
· simp_rw [iUnion_spanningSets, iInter_univ]
exact fun i => monotone_spanningSets (μ i)
