English
For a ≤ b and an antitone function f on Icc[a,b], the partial sum over Ico a b is bounded by the integral over a..b of f.
Русский
Для a ≤ b и антитонной f на Icc[a,b] частичная сумма по Ico a b ограничена интегралом по a..b от f.
LaTeX
$$$\sum_{i=a}^{b-1} f(i) \le \int_{a}^{b} f(x) \, dx$ under conditions$$
Lean4
theorem sum_le_integral (hf : AntitoneOn f (Icc x₀ (x₀ + a))) :
(∑ i ∈ Finset.range a, f (x₀ + (i + 1 : ℕ))) ≤ ∫ x in x₀..x₀ + a, f x :=
by
have hint : ∀ k : ℕ, k < a → IntervalIntegrable f volume (x₀ + k) (x₀ + (k + 1 : ℕ)) :=
by
intro k hk
refine (hf.mono ?_).intervalIntegrable
rw [uIcc_of_le]
· apply Icc_subset_Icc
· simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]
· simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]
· simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]
calc
(∑ i ∈ Finset.range a, f (x₀ + (i + 1 : ℕ))) =
∑ i ∈ Finset.range a, ∫ _ in x₀ + i..x₀ + (i + 1 : ℕ), f (x₀ + (i + 1 : ℕ)) :=
by simp
_ ≤ ∑ i ∈ Finset.range a, ∫ x in x₀ + i..x₀ + (i + 1 : ℕ), f x :=
by
apply Finset.sum_le_sum fun i hi => ?_
have ia : i + 1 ≤ a := Finset.mem_range.1 hi
refine intervalIntegral.integral_mono_on (by simp) (by simp) (hint _ ia) fun x hx => ?_
apply hf _ _ hx.2
· refine mem_Icc.2 ⟨le_trans (le_add_of_nonneg_right (Nat.cast_nonneg _)) hx.1, le_trans hx.2 ?_⟩
simp only [Nat.cast_le, add_le_add_iff_left, ia]
· refine mem_Icc.2 ⟨le_add_of_nonneg_right (Nat.cast_nonneg _), ?_⟩
simp only [add_le_add_iff_left, Nat.cast_le, ia]
_ = ∫ x in x₀..x₀ + a, f x :=
by
convert intervalIntegral.sum_integral_adjacent_intervals hint
simp only [Nat.cast_zero, add_zero]
