English
A variant of the monotone convergence theorem for directed families with a countable index, giving equality of lintegrals with iSup.
Русский
Вариант теоремы монотонной сводимости для направленных семей с счётной индексацией, даёт равенство интегралов-линтегралов через 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 [Countable β] {f : β → α → ℝ≥0∞} (hf : ∀ b, AEMeasurable (f b) μ)
(h_directed : Directed (· ≤ ·) f) : ∫⁻ a, ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ a, f b a ∂μ :=
by
simp_rw [← iSup_apply]
let p : α → (β → ENNReal) → Prop := fun x f' => Directed LE.le f'
have hp : ∀ᵐ x ∂μ, p x fun i => f i x := by
filter_upwards [] with x i j
obtain ⟨z, hz₁, hz₂⟩ := h_directed i j
exact ⟨z, hz₁ x, hz₂ x⟩
have h_ae_seq_directed : Directed LE.le (aeSeq hf p) :=
by
intro b₁ b₂
obtain ⟨z, hz₁, hz₂⟩ := h_directed b₁ b₂
refine ⟨z, ?_, ?_⟩ <;>
· intro x
by_cases hx : x ∈ aeSeqSet hf p
· repeat rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
apply_rules [hz₁, hz₂]
· simp only [aeSeq, hx, if_false]
exact le_rfl
convert lintegral_iSup_directed_of_measurable (aeSeq.measurable hf p) h_ae_seq_directed using 1
· simp_rw [← iSup_apply]
rw [lintegral_congr_ae (aeSeq.iSup hf hp).symm]
· congr 1
ext1 b
rw [lintegral_congr_ae]
apply EventuallyEq.symm
exact aeSeq.aeSeq_n_eq_fun_n_ae hf hp _
