English
If f_n is an antitone sequence of functions with lower bound F and integral tends to ∫ F, then f_n → F almost everywhere.
Русский
Если f_n антитонная последовательность функций с нижней гранью F и интегралы сходятся к интегралу F, то f_n → F почти повсюду.
LaTeX
$$$\\\\forall a, Tendsto (f_n(a)) atTop (nhds F(a))$ a.e.$$
Lean4
/-- If an antitone sequence of functions has a lower bound and the sequence of integrals of these
functions tends to the integral of the lower bound, then the sequence of functions converges
almost everywhere to the lower bound. -/
theorem tendsto_of_integral_tendsto_of_antitone {μ : Measure α} {f : ℕ → α → ℝ} {F : α → ℝ}
(hf_int : ∀ n, Integrable (f n) μ) (hF_int : Integrable F μ)
(hf_tendsto : Tendsto (fun i ↦ ∫ a, f i a ∂μ) atTop (𝓝 (∫ a, F a ∂μ))) (hf_mono : ∀ᵐ a ∂μ, Antitone (fun i ↦ f i a))
(hf_bound : ∀ᵐ a ∂μ, ∀ i, F a ≤ f i a) : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a)) :=
by
let f' : ℕ → α → ℝ := fun i a ↦ -f i a
let F' : α → ℝ := fun a ↦ -F a
suffices ∀ᵐ a ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
by
filter_upwards [this] with a ha_tendsto
convert ha_tendsto.neg
· simp [f']
· simp [F']
refine tendsto_of_integral_tendsto_of_monotone (fun n ↦ (hf_int n).neg) hF_int.neg ?_ ?_ ?_
· convert hf_tendsto.neg
· rw [integral_neg]
· rw [integral_neg]
· filter_upwards [hf_mono] with a ha i j hij
simp [f', ha hij]
· filter_upwards [hf_bound] with a ha i
simp [f', F', ha i]
