English
If f ≤ g almost everywhere on s and both integrable, then the integral over s respects the pointwise order almost everywhere.
Русский
Если f ≤ g почти повсеместно на s, то интегралы сохраняют неотрицательное различие на s.
LaTeX
$$$$\\int_{x\\in s} f(x)\\,d\\mu \\le \\int_{x\\in s} g(x)\\,d\\mu.$$$$
Lean4
theorem setIntegral_mono_on_ae₀ (hs : NullMeasurableSet s μ) (h : ∀ᵐ x ∂μ, x ∈ s → f x ≤ g x) :
∫ x in s, f x ∂μ ≤ ∫ x in s, g x ∂μ :=
by
rw [setIntegral_congr_set hs.toMeasurable_ae_eq.symm, setIntegral_congr_set hs.toMeasurable_ae_eq.symm]
refine setIntegral_mono_on_ae ?_ ?_ ?_ ?_
· rwa [integrableOn_congr_set_ae hs.toMeasurable_ae_eq]
· rwa [integrableOn_congr_set_ae hs.toMeasurable_ae_eq]
· exact measurableSet_toMeasurable μ s
· filter_upwards [hs.toMeasurable_ae_eq.mem_iff, h] with x hx h
rwa [hx]
