English
A bounded dominance condition implies a limsup inequality between integrals and limsup of integrands.
Русский
Пусть данные условия доминирования обеспечивают неравенство лиминального интеграла по отношению к лимсупу интегралов функций.
LaTeX
$$limsup (∫ f_n) ≤ ∫ limsup f_n$$
Lean4
theorem limsup_lintegral_le {f : ℕ → α → ℝ≥0∞} (g : α → ℝ≥0∞) (hf_meas : ∀ n, Measurable (f n))
(h_bound : ∀ n, f n ≤ᵐ[μ] g) (h_fin : ∫⁻ a, g a ∂μ ≠ ∞) :
limsup (fun n => ∫⁻ a, f n a ∂μ) atTop ≤ ∫⁻ a, limsup (fun n => f n a) atTop ∂μ :=
calc
limsup (fun n => ∫⁻ a, f n a ∂μ) atTop = ⨅ n : ℕ, ⨆ i ≥ n, ∫⁻ a, f i a ∂μ := limsup_eq_iInf_iSup_of_nat
_ ≤ ⨅ n : ℕ, ∫⁻ a, ⨆ i ≥ n, f i a ∂μ := (iInf_mono fun _ => iSup₂_lintegral_le _)
_ = ∫⁻ a, ⨅ n : ℕ, ⨆ i ≥ n, f i a ∂μ :=
by
refine (lintegral_iInf ?_ ?_ ?_).symm
· intro n
exact .biSup _ (Set.to_countable _) (fun i _ ↦ hf_meas i)
· intro n m hnm a
exact iSup_le_iSup_of_subset fun i hi => le_trans hnm hi
· refine ne_top_of_le_ne_top h_fin (lintegral_mono_ae ?_)
refine (ae_all_iff.2 h_bound).mono fun n hn => ?_
exact iSup_le fun i => iSup_le fun _ => hn i
_ = ∫⁻ a, limsup (fun n => f n a) atTop ∂μ := by simp only [limsup_eq_iInf_iSup_of_nat]
