English
For a measurable f, and natural n, the nth eapprox of f is bounded above by the integral of f: (eapprox f n).lintegral μ ≤ ∫ f dμ.
Русский
Для измеримой f и任ной степени n величина интеграла eapprox f n не превосходит интеграл f по мере μ.
LaTeX
$$$$ (eapprox f n).lintegral \\mu \\le \\int f \\; d\\mu. $$$$
Lean4
theorem integral_eq_integral_Ioc_meas_le {f : α → ℝ} {M : ℝ} (f_intble : Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f)
(f_bdd : f ≤ᵐ[μ] (fun _ ↦ M)) : ∫ ω, f ω ∂μ = ∫ t in Ioc 0 M, μ.real {a : α | t ≤ f a} :=
by
rw [f_intble.integral_eq_integral_meas_le f_nn]
rw [setIntegral_eq_of_subset_of_ae_diff_eq_zero nullMeasurableSet_Ioi Ioc_subset_Ioi_self ?_]
apply Eventually.of_forall (fun t ht ↦ ?_)
have htM : M < t := by simp_all only [mem_diff, mem_Ioi, mem_Ioc, not_and, not_le]
have obs : μ {a | M < f a} = 0 := by
rw [measure_eq_zero_iff_ae_notMem]
filter_upwards [f_bdd] with a ha using not_lt.mpr ha
rw [measureReal_def, ENNReal.toReal_eq_zero_iff]
exact Or.inl <| measure_mono_null (fun a ha ↦ lt_of_lt_of_le htM ha) obs
