intervalIntegral_pos_of_pos — Mathlib

English

If f is strictly positive on the interval [a,b] and integrable on (a,b], then ∫_a^b f > 0.

Русский

Пусть f строго положительна на [a,b] и интегрируема на (a,b], тогда ∫_a^b f > 0.

LaTeX

$$$a < b \\Rightarrow (0 < f(x)\\;\\text{on } [a,b]) \\Rightarrow 0 < \\int_a^b f(x)\\,dx$$$

Lean4

/-- 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.) -/
theorem intervalIntegral_pos_of_pos {f : ℝ → ℝ} {a b : ℝ} (hfi : IntervalIntegrable f MeasureSpace.volume a b)
    (hpos : ∀ x, 0 < f x) (hab : a < b) : 0 < ∫ x in a..b, f x :=
  intervalIntegral_pos_of_pos_on hfi (fun x _ => hpos x) hab

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