sum_le_integral_Ico — Mathlib

English

Under opposite monotonicity, the integral is bounded above by the sum over Ico of f(i).

Русский

При противоположной монотонности интеграл ограничен сверху суммой по Ico f(i).

LaTeX

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

Lean4

theorem sum_le_integral_Ico (hab : a ≤ b) (hf : AntitoneOn f (Set.Icc a b)) :
    (∑ i ∈ Finset.Ico a b, f (i + 1 : ℕ)) ≤ ∫ x in a..b, f x :=
  by
  rw [(Nat.sub_add_cancel hab).symm, Nat.cast_add]
  conv =>
    congr
    congr
    congr
    rw [← zero_add a]
    · skip
    · skip
    · skip
    rw [add_comm]
  rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range]
  conv =>
    lhs
    congr
    congr
    · skip
    ext
    rw [add_assoc, Nat.cast_add]
  apply AntitoneOn.sum_le_integral
  simp only [hf, hab, Nat.cast_sub, add_sub_cancel]

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