English
For a directed family of measurable functions indexed by a countable β, the lintegral over the iSup equals the iSup of the lintegrals.
Русский
Для направленного семейства измеримых функций индексов по счётному β выполняется лимитный переход интегралов через iSup.
LaTeX
$$$$ \\int^{\\!-}_{a} \\big( \\bigvee_{b} f(b,a) \\big) d\\mu(a) = \\bigvee_{b} \\int^{\\!-}_{a} f(b,a) d\\mu(a). $$$$
Lean4
/-- **Monotone convergence theorem** for a supremum over a directed family and indexed by a
countable type. -/
theorem lintegral_iSup_directed_of_measurable [Countable β] {f : β → α → ℝ≥0∞} (hf : ∀ b, Measurable (f b))
(h_directed : Directed (· ≤ ·) f) : ∫⁻ a, ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ a, f b a ∂μ :=
by
cases nonempty_encodable β
cases isEmpty_or_nonempty β
· simp
inhabit β
have : ∀ a, ⨆ b, f b a = ⨆ n, f (h_directed.sequence f n) a :=
by
intro a
refine le_antisymm (iSup_le fun b => ?_) (iSup_le fun n => le_iSup (fun n => f n a) _)
exact le_iSup_of_le (encode b + 1) (h_directed.le_sequence b a)
calc
∫⁻ a, ⨆ b, f b a ∂μ = ∫⁻ a, ⨆ n, f (h_directed.sequence f n) a ∂μ := by simp only [this]
_ = ⨆ n, ∫⁻ a, f (h_directed.sequence f n) a ∂μ := (lintegral_iSup (fun n => hf _) h_directed.sequence_mono)
_ = ⨆ b, ∫⁻ a, f b a ∂μ :=
by
refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun b => ?_)
· exact le_iSup (fun b => ∫⁻ a, f b a ∂μ) _
· exact le_iSup_of_le (encode b + 1) (lintegral_mono <| h_directed.le_sequence b)
