English
If a sequence of nonnegative functions decreases pointwise (antitone) and the corresponding integrals converge to the integral of a lower bound, then the functions converge almost everywhere to that lower bound along the index.
Русский
Если последовательность функции неотрицательных значений убывает покоординатно и интегралы сходятся к интегралу нижней границы, то функции сходятся почти повсеместно к этой границе по индексу.
LaTeX
$$$\\text{hf_meas} \\Rightarrow \\text{tendsto AE} \\Rightarrow \\ldots$ (формула заполнена в виде абстрактной конжекции).$$
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_lintegral_tendsto_of_antitone {α : Type*} {mα : MeasurableSpace α} {f : ℕ → α → ℝ≥0∞} {F : α → ℝ≥0∞}
{μ : Measure α} (hf_meas : ∀ n, AEMeasurable (f n) μ)
(hf_tendsto : Tendsto (fun i ↦ ∫⁻ a, f i a ∂μ) atTop (𝓝 (∫⁻ a, F a ∂μ)))
(hf_mono : ∀ᵐ a ∂μ, Antitone (fun i ↦ f i a)) (h_bound : ∀ᵐ a ∂μ, ∀ i, F a ≤ f i a) (h0 : ∫⁻ a, f 0 a ∂μ ≠ ∞) :
∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a)) :=
by
have h_int_finite : ∫⁻ a, F a ∂μ ≠ ∞ :=
by
refine ((lintegral_mono_ae ?_).trans_lt h0.lt_top).ne
filter_upwards [h_bound] with a ha using ha 0
have h_exists : ∀ᵐ a ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) :=
by
filter_upwards [hf_mono] with a h_mono
rcases _root_.tendsto_of_antitone h_mono with h | h
· refine ⟨0, h.mono_right ?_⟩
rw [OrderBot.atBot_eq]
exact pure_le_nhds _
· exact h
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 ge_of_tendsto' h_tendsto (fun m ↦ h_le _)
suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ
by
refine (ae_eq_of_ae_le_of_lintegral_le hF'_le h_int_finite ?_ this.le).symm
exact ENNReal.aemeasurable_of_tendsto hf_meas hF'_tendsto
refine tendsto_nhds_unique ?_ hf_tendsto
exact lintegral_tendsto_of_tendsto_of_antitone hf_meas hf_mono h0 hF'_tendsto
