English
If f ≥ 0 almost everywhere with respect to μ on [a,b], then the interval integral ∫_a^b f dμ is nonnegative.
Русский
Если f ≥ 0 почти всюду относительно μ на [a,b], то интеграл по интервалу неотрицателен.
LaTeX
$$$hab: a \\le b,\\ (0 ≤^a μ f) \\Rightarrow 0 ≤ ∫_a^b f\\,dμ$$$
Lean4
/-- If `f` and `g` are continuous on `[a, b]`, `a < b`, `f x ≤ g x` on this interval, and
`f c < g c` at some point `c ∈ [a, b]`, then `∫ x in a..b, f x < ∫ x in a..b, g x`. -/
theorem integral_lt_integral_of_continuousOn_of_le_of_exists_lt {f g : ℝ → ℝ} {a b : ℝ} (hab : a < b)
(hfc : ContinuousOn f (Icc a b)) (hgc : ContinuousOn g (Icc a b)) (hle : ∀ x ∈ Ioc a b, f x ≤ g x)
(hlt : ∃ c ∈ Icc a b, f c < g c) : (∫ x in a..b, f x) < ∫ x in a..b, g x :=
by
apply
integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero hab.le (hfc.intervalIntegrable_of_Icc hab.le)
(hgc.intervalIntegrable_of_Icc hab.le)
· simpa only [measurableSet_Ioc, ae_restrict_eq] using (ae_restrict_mem measurableSet_Ioc).mono hle
contrapose! hlt
have h_eq : f =ᵐ[volume.restrict (Ioc a b)] g :=
by
simp only [← not_le, ← ae_iff] at hlt
exact EventuallyLE.antisymm ((ae_restrict_iff' measurableSet_Ioc).2 <| Eventually.of_forall hle) hlt
rw [Measure.restrict_congr_set Ioc_ae_eq_Icc] at h_eq
exact fun c hc ↦ (Measure.eqOn_Icc_of_ae_eq volume hab.ne h_eq hfc hgc hc).ge
