English
If a monotone sequence has an upper bound and the sequence of integrals tends to the integral of the bound, 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. Auxiliary version assuming moreover that the
functions in the sequence are ae measurable. -/
theorem tendsto_of_lintegral_tendsto_of_monotone_aux {α : Type*} {mα : MeasurableSpace α} {f : ℕ → α → ℝ≥0∞}
{F : α → ℝ≥0∞} {μ : Measure α} (hf_meas : ∀ n, AEMeasurable (f n) μ) (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 h_bound_finite : ∀ᵐ a ∂μ, F a ≠ ∞ := by filter_upwards [ae_lt_top' hF_meas h_int_finite] with a ha using ha.ne
have h_exists : ∀ᵐ a ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) :=
by
filter_upwards [h_bound, h_bound_finite, hf_mono] with a h_le h_fin h_mono
have h_tendsto : Tendsto (fun i ↦ f i a) atTop atTop ∨ ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) :=
tendsto_of_monotone h_mono
rcases h_tendsto with h_absurd | h_tendsto
· rw [tendsto_atTop_atTop_iff_of_monotone h_mono] at h_absurd
obtain ⟨i, hi⟩ := h_absurd (F a + 1)
refine absurd (hi.trans (h_le _)) (not_le.mpr ?_)
exact ENNReal.lt_add_right h_fin one_ne_zero
· exact h_tendsto
classical
let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
have hF'_tendsto : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) :=
by
filter_upwards [h_exists] with a ha
simp_rw [F', dif_pos ha]
exact ha.choose_spec
suffices F' =ᵐ[μ] F by filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto
have hF'_le : F' ≤ᵐ[μ] F := by
filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto
exact le_of_tendsto' h_tendsto (fun m ↦ h_le _)
suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ from
ae_eq_of_ae_le_of_lintegral_le hF'_le (this ▸ h_int_finite) hF_meas this.symm.le
refine tendsto_nhds_unique ?_ hf_tendsto
exact lintegral_tendsto_of_tendsto_of_monotone hf_meas hf_mono hF'_tendsto
