Theorems · Theorem · measure theory

intervalIntegral.intervalIntegral_pos_of_pos

∀ {f : ℝ → ℝ} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b → (∀ (x : ℝ), 0 < f x) → a < b → 0 < ∫ (x : ℝ) in a..b, f x

If f : ℝ → ℝ is strictly positive everywhere, and integrable on (a, b] for real numbers a < b, then its integral over a..b is strictly positive. (See intervalIntegral_pos_of_pos_on for a version only assuming positivity of f on (a, b) rather than everywhere.)

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

2 results in Mathlib

Foundations

Depth 259 from the axioms · uses propext, Classical.choice, Quot.sound