Documentation

Mathlib.Analysis.SumIntegralComparisons

Comparing sums and integrals #

Summary #

It is often the case that error terms in analysis can be computed by comparing an infinite sum to the improper integral of an antitone function. This file will eventually enable that.

At the moment it contains four lemmas in this direction: AntitoneOn.integral_le_sum, AntitoneOn.sum_le_integral and versions for monotone functions, which can all be paired with a Filter.Tendsto to estimate some errors.

TODO: Add more lemmas to the API to directly address limiting issues

Main Results #

Tags #

analysis, comparison, asymptotics

theorem AntitoneOn.integral_le_sum {x₀ : } {a : } {f : } (hf : AntitoneOn f (Set.Icc x₀ (x₀ + a))) :
∫ (x : ) in x₀..x₀ + a, f x Finset.sum (Finset.range a) fun (i : ) => f (x₀ + i)
theorem AntitoneOn.integral_le_sum_Ico {a : } {b : } {f : } (hab : a b) (hf : AntitoneOn f (Set.Icc a b)) :
∫ (x : ) in a..b, f x Finset.sum (Finset.Ico a b) fun (x : ) => f x
theorem AntitoneOn.sum_le_integral {x₀ : } {a : } {f : } (hf : AntitoneOn f (Set.Icc x₀ (x₀ + a))) :
(Finset.sum (Finset.range a) fun (i : ) => f (x₀ + (i + 1))) ∫ (x : ) in x₀..x₀ + a, f x
theorem AntitoneOn.sum_le_integral_Ico {a : } {b : } {f : } (hab : a b) (hf : AntitoneOn f (Set.Icc a b)) :
(Finset.sum (Finset.Ico a b) fun (i : ) => f (i + 1)) ∫ (x : ) in a..b, f x
theorem MonotoneOn.sum_le_integral {x₀ : } {a : } {f : } (hf : MonotoneOn f (Set.Icc x₀ (x₀ + a))) :
(Finset.sum (Finset.range a) fun (i : ) => f (x₀ + i)) ∫ (x : ) in x₀..x₀ + a, f x
theorem MonotoneOn.sum_le_integral_Ico {a : } {b : } {f : } (hab : a b) (hf : MonotoneOn f (Set.Icc a b)) :
(Finset.sum (Finset.Ico a b) fun (x : ) => f x) ∫ (x : ) in a..b, f x
theorem MonotoneOn.integral_le_sum {x₀ : } {a : } {f : } (hf : MonotoneOn f (Set.Icc x₀ (x₀ + a))) :
∫ (x : ) in x₀..x₀ + a, f x Finset.sum (Finset.range a) fun (i : ) => f (x₀ + (i + 1))
theorem MonotoneOn.integral_le_sum_Ico {a : } {b : } {f : } (hab : a b) (hf : MonotoneOn f (Set.Icc a b)) :
∫ (x : ) in a..b, f x Finset.sum (Finset.Ico a b) fun (i : ) => f (i + 1)