English
If a sequence is antitone in each point and the integrals converge to the integral of the limit, then the pointwise limit holds almost everywhere.
Русский
Если последовательность антитонна по каждой точке и интегралы сходятся к интегралу предельной функции, то почти всюду выполняется предел.
LaTeX
$$∀ a, Tendsto (f_n a) atTop (𝓝 F(a)) a.e.$$
Lean4
/-- If a monotone sequence of functions has an upper bound and the sequence of integrals of these
functions tends to the integral of the upper bound, then the sequence of functions converges
almost everywhere to the upper bound. -/
theorem tendsto_of_lintegral_tendsto_of_monotone {α : Type*} {mα : MeasurableSpace α} {f : ℕ → α → ℝ≥0∞} {F : α → ℝ≥0∞}
{μ : Measure α} (hF_meas : AEMeasurable F μ)
(hf_tendsto : Tendsto (fun i ↦ ∫⁻ a, f i a ∂μ) atTop (𝓝 (∫⁻ a, F a ∂μ)))
(hf_mono : ∀ᵐ a ∂μ, Monotone (fun i ↦ f i a)) (h_bound : ∀ᵐ a ∂μ, ∀ i, f i a ≤ F a)
(h_int_finite : ∫⁻ a, F a ∂μ ≠ ∞) : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a)) :=
by
have : ∀ n, ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f n ∧ ∫⁻ a, f n a ∂μ = ∫⁻ a, g a ∂μ := fun n ↦
exists_measurable_le_lintegral_eq _ _
choose g gmeas gf hg using this
let g' : ℕ → α → ℝ≥0∞ := Nat.rec (g 0) (fun n I x ↦ max (g (n + 1) x) (I x))
have M n : Measurable (g' n) := by
induction n with
| zero => simp [g', gmeas 0]
| succ n ih => exact Measurable.max (gmeas (n + 1)) ih
have I : ∀ n x, g n x ≤ g' n x := by
intro n x
cases n with
| zero
| succ => simp [g']
have I' : ∀ᵐ x ∂μ, ∀ n, g' n x ≤ f n x :=
by
filter_upwards [hf_mono] with x hx n
induction n with
| zero => simpa [g'] using gf 0 x
| succ n ih => exact max_le (gf (n + 1) x) (ih.trans (hx (Nat.le_succ n)))
have Int_eq n : ∫⁻ x, g' n x ∂μ = ∫⁻ x, f n x ∂μ :=
by
apply le_antisymm
· apply lintegral_mono_ae
filter_upwards [I'] with x hx using hx n
· rw [hg n]
exact lintegral_mono (I n)
have : ∀ᵐ a ∂μ, Tendsto (fun i ↦ g' i a) atTop (𝓝 (F a)) :=
by
apply tendsto_of_lintegral_tendsto_of_monotone_aux _ hF_meas _ _ _ h_int_finite
· exact fun n ↦ (M n).aemeasurable
· simp_rw [Int_eq]
exact hf_tendsto
· exact Eventually.of_forall (fun x ↦ monotone_nat_of_le_succ (fun n ↦ le_max_right _ _))
· filter_upwards [h_bound, I'] with x h'x hx n using (hx n).trans (h'x n)
filter_upwards [this, I', h_bound] with x hx h'x h''x
exact tendsto_of_tendsto_of_tendsto_of_le_of_le hx tendsto_const_nhds h'x h''x
