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 #
AntitoneOn.integral_le_sum: The integral of an antitone function is at most the sum of its values at integer steps aligning with the left-hand side of the intervalAntitoneOn.sum_le_integral: The sum of an antitone function along integer steps aligning with the right-hand side of the interval is at most the integral of the function along that intervalMonotoneOn.integral_le_sum: The integral of a monotone function is at most the sum of its values at integer steps aligning with the right-hand side of the intervalMonotoneOn.sum_le_integral: The sum of a monotone function along integer steps aligning with the left-hand side of the interval is at most the integral of the function along that interval
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)