integral_le_sum_Ico_of_le — Mathlib

English

Under proper dominance hypotheses, the integral of a function g over an interval is bounded by the corresponding sum of pointwise bounds f(i).

Русский

При разумных ограничениях интеграл функции g на интервале не превосходит соответствующую сумму по точкам.

LaTeX

$$$\int_{a}^{b} g(x) \, dx \le \sum_{i=a}^{b-1} f(i)$ under appropriate conditions$$

Lean4

theorem integral_le_sum_Ico_of_le (hab : a ≤ b) (h : ∀ i ∈ Ico a b, ∀ x ∈ Ico (i : ℝ) (i + 1 : ℕ), g x ≤ f i)
    (hg : IntegrableOn g (Set.Ico a b)) : ∫ x in a..b, g x ≤ ∑ i ∈ Finset.Ico a b, f i := by
  convert
      neg_le_neg
        (sum_Ico_le_integral_of_le (f := -f) (g := -g) hab (fun i hi x hx ↦ neg_le_neg (h i hi x hx)) hg.neg) <;>
    simp

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