integral_mono_on_of_le_Ioo — Mathlib

English

If f and g are continuous on [a,b] with f ≤ g on Ioc(a,b) and there exists c ∈ Icc(a,b) with f(c) < g(c), then ∫_a^b f < ∫_a^b g.

Русский

Если f и g непрерывны на [a,b], f ≤ g на Ioc(a,b) и существует c ∈ Icc(a,b) с f(c) < g(c), то ∫_a^b f < ∫_a^b g.

LaTeX

$$$hab: a < b,\\ hfc: ContinuousOn f(Icc(a,b)),\\ hgc: ContinuousOn g(Icc(a,b)),\\ hle: f ≤ g на Ioc(a,b),\\ hlt: ∃c∈Icc(a,b), f(c)

Lean4

theorem integral_mono_on_of_le_Ioo [NoAtoms μ] (h : ∀ x ∈ Ioo a b, f x ≤ g x) :
    (∫ u in a..b, f u ∂μ) ≤ ∫ u in a..b, g u ∂μ :=
  by
  simp only [integral_of_le hab, integral_Ioc_eq_integral_Ioo]
  apply setIntegral_mono_on
  · apply hf.1.mono Ioo_subset_Ioc_self le_rfl
  · apply hg.1.mono Ioo_subset_Ioc_self le_rfl
  · exact measurableSet_Ioo
  · exact h

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