integral_mono_ae — Mathlib

English

If μ ≤ ν and f is AE-nonnegative and integrable with respect to ν, then ∫ f dμ ≤ ∫ f dν.

Русский

Если μ ≤ ν и f неотрицательно по мере ν, то интеграл по μ не превосходит интеграл по ν.

LaTeX

$$$\\mu \\le ν \\Rightarrow \\text{AE nonneg f} \\Rightarrow ∫ f dμ ≤ ∫ f dν$.$$

Lean4

theorem integral_mono_ae {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) (h : f ≤ᵐ[μ] g) :
    ∫ x, f x ∂μ ≤ ∫ x, g x ∂μ := by
  rw [← sub_nonneg, ← integral_sub hg hf]
  refine integral_nonneg_of_ae ?_
  filter_upwards [h] with x hx
  simpa

Похожие утверждения