English
If f is integrable on (a,b] and positive on the interior with a < b, then its integral over a..b is strictly positive.
Русский
Если f интегрируема на (a,b], положительна внутри интервала и a < b, то интеграл по [a,b] строго положителен.
LaTeX
$$$0 < \\int x in a..b, f x \\, dx$ при $hab: a < b$, $hfi: IntervalIntegrable f \\mu a b$, $\\forall x\\in I^o(a,b): f(x) > 0$.$$
Lean4
/-- If `f : ℝ → ℝ` is integrable on `(a, b]` for real numbers `a < b`, and positive on the interior
of the interval, then its integral over `a..b` is strictly positive. -/
theorem intervalIntegral_pos_of_pos_on {f : ℝ → ℝ} {a b : ℝ} (hfi : IntervalIntegrable f volume a b)
(hpos : ∀ x : ℝ, x ∈ Ioo a b → 0 < f x) (hab : a < b) : 0 < ∫ x : ℝ in a..b, f x :=
by
have hsupp : Ioo a b ⊆ support f ∩ Ioc a b := fun x hx => ⟨mem_support.mpr (hpos x hx).ne', Ioo_subset_Ioc_self hx⟩
have h₀ : 0 ≤ᵐ[volume.restrict (uIoc a b)] f :=
by
rw [EventuallyLE, uIoc_of_le hab.le]
refine ae_restrict_of_ae_eq_of_ae_restrict Ioo_ae_eq_Ioc ?_
rw [ae_restrict_iff' measurableSet_Ioo]
filter_upwards with x hx using (hpos x hx).le
rw [integral_pos_iff_support_of_nonneg_ae' h₀ hfi]
exact ⟨hab, ((Measure.measure_Ioo_pos _).mpr hab).trans_le (measure_mono hsupp)⟩
