English
Antitone sequence f_n with a lower bound F and converging integrals implies almost everywhere convergence to F; i.e., Tendsto f_n a.e. to F.
Русский
Антитоновая последовательность f_n с нижней гранью F и сходящимися интегралами приводит к почти повсеместной сходимости f_n к F.
LaTeX
$$$\\\\forall n, Integrable(f_n) \\\\Rightarrow Tendsto f_n a.e. to F$$$
Lean4
/-- Monotone convergence theorem for real-valued functions and Bochner integrals -/
theorem integral_tendsto_of_tendsto_of_antitone {μ : Measure α} {f : ℕ → α → ℝ} {F : α → ℝ}
(hf : ∀ n, Integrable (f n) μ) (hF : Integrable F μ) (h_mono : ∀ᵐ x ∂μ, Antitone fun n ↦ f n x)
(h_tendsto : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))) :
Tendsto (fun n ↦ ∫ x, f n x ∂μ) atTop (𝓝 (∫ x, F x ∂μ)) :=
by
suffices Tendsto (fun n ↦ ∫ x, -f n x ∂μ) atTop (𝓝 (∫ x, -F x ∂μ))
by
suffices Tendsto (fun n ↦ ∫ x, - -f n x ∂μ) atTop (𝓝 (∫ x, - -F x ∂μ)) by simpa [neg_neg] using this
convert this.neg <;> rw [integral_neg]
refine integral_tendsto_of_tendsto_of_monotone (fun n ↦ (hf n).neg) hF.neg ?_ ?_
· filter_upwards [h_mono] with x hx n m hnm using neg_le_neg_iff.mpr <| hx hnm
· filter_upwards [h_tendsto] with x hx using hx.neg
