ae_le_of_forall_setIntegral_le — Mathlib

English

If μ is sigma-finite, and f is integrable on all sets, and integrals over all measurable sets are nonnegative, then f is nonnegative almost everywhere.

Русский

Если мера μ сигма-сконечна, и f интегрируема на всех множествах, и интегралы по всем измеримым множествам неотрицательны, тогда f ≥ 0 a.e.

LaTeX

$$$0 \leq_{a.e.\,μ} f$ under sigma-finite hypotheses.$$

Lean4

theorem ae_le_of_forall_setIntegral_le {f g : α → ℝ} (hf : Integrable f μ) (hg : Integrable g μ)
    (hf_le : ∀ s, MeasurableSet s → μ s < ∞ → (∫ x in s, f x ∂μ) ≤ ∫ x in s, g x ∂μ) : f ≤ᵐ[μ] g :=
  by
  rw [← eventually_sub_nonneg]
  refine ae_nonneg_of_forall_setIntegral_nonneg (hg.sub hf) fun s hs => ?_
  rw [integral_sub' hg.integrableOn hf.integrableOn, sub_nonneg]
  exact hf_le s hs

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