English
For a nonnegative continuous function f, if μ(G) ≤ liminf μ_s(i,G) for all open G, then the integral of f with respect to μ is bounded by the liminf of the integrals with respect to μ_s(i).
Русский
Для неотрицимой непрерывной функции f, если μ(G) ≤ liminf μ_s(i,G) для всех открытых G, то интеграл f по μ ≤ liminf интегралов по μ_s(i).
LaTeX
$$$f\\ge 0$ continuous; \\forall G\\, (G\\text{ открыто}) \\Rightarrow μ(G) ≤ \\liminf_i μ_s(i,G) \\\\Rightarrow \\int f \\, dμ ≤ \\liminf_i \\int f \\, dμ_s(i)$$$
Lean4
theorem lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure {μ : Measure Ω} {μs : ℕ → Measure Ω}
{f : Ω → ℝ} (f_cont : Continuous f) (f_nn : 0 ≤ f) (h_opens : ∀ G, IsOpen G → μ G ≤ atTop.liminf (fun i ↦ μs i G)) :
∫⁻ x, ENNReal.ofReal (f x) ∂μ ≤ atTop.liminf (fun i ↦ ∫⁻ x, ENNReal.ofReal (f x) ∂(μs i)) :=
by
simp_rw [lintegral_eq_lintegral_meas_lt _ (Eventually.of_forall f_nn) f_cont.aemeasurable]
calc
∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a} ≤ ∫⁻ (t : ℝ) in Set.Ioi 0, atTop.liminf (fun i ↦ (μs i) {a | t < f a}) :=
?_ -- (i)
_ ≤ atTop.liminf (fun i ↦ ∫⁻ (t : ℝ) in Set.Ioi 0, (μs i) {a | t < f a}) :=
?_ -- (ii)
· -- (i)
exact (lintegral_mono (fun t ↦ h_opens _ (continuous_def.mp f_cont _ isOpen_Ioi))).trans (le_refl _)
· -- (ii)
exact
lintegral_liminf_le (fun n ↦ Antitone.measurable (fun s t hst ↦ measure_mono (fun ω hω ↦ lt_of_le_of_lt hst hω)))
