integral_nonneg — Mathlib

English

If f ≥ 0 almost everywhere, then its integral is nonnegative.

Русский

Если f ≥ 0 почти повсюду, то интеграл неотрицателен.

LaTeX

$$$$ 0 \\leq f_{integral} μ \\quad\\text{if } f \\ge 0 \\text{ a.e.} $$$$

Lean4

theorem integral_nonneg {f : α →ₛ F} (hf : 0 ≤ᵐ[μ] f) : 0 ≤ f.integral μ :=
  by
  rw [integral_eq]
  apply Finset.sum_nonneg
  rw [forall_mem_range]
  intro y
  by_cases hy : 0 ≤ f y
  · positivity
  · suffices μ (f ⁻¹' {f y}) = 0 by simp [this, measureReal_def]
    rw [← nonpos_iff_eq_zero]
    refine le_of_le_of_eq (measure_mono fun x hx ↦ ?_) (ae_iff.mp hf)
    simp only [Set.mem_preimage, mem_singleton_iff, mem_setOf_eq] at hx ⊢
    exact hx ▸ hy

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