integral_nonneg_of_ae_restrict — Mathlib

English

If f ≥ 0 everywhere on [a,b], then ∫_a^b f ≥ 0.

Русский

Если f неотрицательна на всём множестве [a,b], то интеграл неотрицателен.

LaTeX

$$$hab: a \\le b,\\ hf: \\forall u\\ (u∈Icc a b)\\;→ 0 ≤ f(u) \\Rightarrow 0 ≤ ∫_a^b f$$$

Lean4

theorem integral_nonneg_of_ae_restrict (hab : a ≤ b) (hf : 0 ≤ᵐ[μ.restrict (Icc a b)] f) : 0 ≤ ∫ u in a..b, f u ∂μ :=
  by
  let H := ae_restrict_of_ae_restrict_of_subset Ioc_subset_Icc_self hf
  simpa only [integral_of_le hab] using setIntegral_nonneg_of_ae_restrict H

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