English
If s_i is a directed family of sets, then the lintegral over μ restricted to the union equals the supremum of the lintegrals over μ restricted to each s_i.
Русский
Если {s_i} образуют направленную семью множеств, то линеграль по коллектору μ, ограниченной объединением, равен наибольшему пределу линеграля по μ, ограниченному каждому s_i.
LaTeX
$$$f.lintegral(μ.restrict(\\bigcup_i s_i)) = \\bigvee_i f.lintegral(μ.restrict(s_i))$$$
Lean4
theorem lintegral_restrict_iUnion_of_directed {ι : Type*} [Countable ι] (f : α →ₛ ℝ≥0∞) {s : ι → Set α}
(hd : Directed (· ⊆ ·) s) (μ : Measure α) :
f.lintegral (μ.restrict (⋃ i, s i)) = ⨆ i, f.lintegral (μ.restrict (s i)) :=
by
simp only [lintegral, Measure.restrict_iUnion_apply_eq_iSup hd (measurableSet_preimage ..), ENNReal.mul_iSup]
refine
finsetSum_iSup fun i j ↦
(hd i j).imp fun k ⟨hik, hjk⟩ ↦ fun a ↦
?_
-- TODO https://github.com/leanprover-community/mathlib4/pull/14739 make `gcongr` close this goal
constructor <;> · gcongr; refine Measure.restrict_mono ?_ le_rfl _; assumption
