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.

It contains several lemmas in this direction, for antitone or monotone functions (or products of antitone and monotone functions), formulated for sums on range i or Ico a b. These are used to prove a version of the integral test for antitone functions.

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 interval.
• AntitoneOn.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 interval
• MonotoneOn.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 interval.
• MonotoneOn.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
• sum_mul_Ico_le_integral_of_monotone_antitone: the sum of f i * g i on an interval is bounded by the integral of f x * g (x - 1) if f is monotone and g is antitone.
• integral_le_sum_mul_Ico_of_antitone_monotone: the sum of f i * g i on an interval is bounded below by the integral of f x * g (x - 1) if f is antitone and g is monotone.
• AntitoneOn.summable_of_integrableOn_Ioi_zero and AntitoneOn.tsum_le_integral, the integral test for antitone functions.
• AntitoneOn.abs_tsum_sub_sum_range_le_integral: an error estimate for the difference between a sum and its partial sums in terms of an integral.
• AntitoneOn.integrableOn_Ioi_zero_of_summable and AntitoneOn.integral_le_tsum, the converse to the integral test.

Tags

analysis, comparison, asymptotics

theorem sum_Ico_le_integral_of_le {a b : ℕ} {f g : ℝ → ℝ} (hab : a ≤ b) (h : ∀ i ∈ Set.Ico a b, ∀ x ∈ Set.Ico ↑i ↑(i + 1), f ↑i ≤ g x) (hg : MeasureTheory.IntegrableOn g (Set.Ico ↑a ↑b) MeasureTheory.volume) : ∑ i ∈ Finset.Ico a b, f ↑i ≤ ∫ (x : ℝ) in ↑a..↑b, g x

theorem integral_le_sum_Ico_of_le {a b : ℕ} {f g : ℝ → ℝ} (hab : a ≤ b) (h : ∀ i ∈ Set.Ico a b, ∀ x ∈ Set.Ico ↑i ↑(i + 1), g x ≤ f ↑i) (hg : MeasureTheory.IntegrableOn g (Set.Ico ↑a ↑b) MeasureTheory.volume) : ∫ (x : ℝ) in ↑a..↑b, g x ≤ ∑ i ∈ Finset.Ico a b, f ↑i

theorem AntitoneOn.integral_le_sum {x₀ : ℝ} {a : ℕ} {f : ℝ → ℝ} (hf : AntitoneOn f (Set.Icc x₀ (x₀ + ↑a))) : ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i ∈ Finset.range a, 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 ≤ ∑ x ∈ Finset.Ico a b, f ↑x

theorem AntitoneOn.sum_le_integral {x₀ : ℝ} {a : ℕ} {f : ℝ → ℝ} (hf : AntitoneOn f (Set.Icc x₀ (x₀ + ↑a))) : ∑ i ∈ Finset.range a, 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)) : ∑ i ∈ Finset.Ico a b, 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))) : ∑ i ∈ Finset.range a, 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)) : ∑ x ∈ Finset.Ico a b, 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 ≤ ∑ i ∈ Finset.range a, 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 ≤ ∑ i ∈ Finset.Ico a b, f ↑(i + 1)

theorem sum_mul_Ico_le_integral_of_monotone_antitone {a b : ℕ} {f g : ℝ → ℝ} (hab : a ≤ b) (hf : MonotoneOn f (Set.Icc ↑a ↑b)) (hg : AntitoneOn g (Set.Icc (↑a - 1) (↑b - 1))) (fpos : 0 ≤ f ↑a) (gpos : 0 ≤ g (↑b - 1)) : ∑ i ∈ Finset.Ico a b, f ↑i * g ↑i ≤ ∫ (x : ℝ) in ↑a..↑b, f x * g (x - 1)

theorem integral_le_sum_mul_Ico_of_antitone_monotone {a b : ℕ} {f g : ℝ → ℝ} (hab : a ≤ b) (hf : AntitoneOn f (Set.Icc ↑a ↑b)) (hg : MonotoneOn g (Set.Icc (↑a - 1) (↑b - 1))) (fpos : 0 ≤ f ↑b) (gpos : 0 ≤ g (↑a - 1)) : ∫ (x : ℝ) in ↑a..↑b, f x * g (x - 1) ≤ ∑ i ∈ Finset.Ico a b, f ↑i * g ↑i

Comparison of infinite sums and integrals

theorem AntitoneOn.sum_Ico_le_integral {f : ℝ → ℝ} {a b : ℕ} (anti : AntitoneOn f (Set.Icc ↑a ↑b)) (integrable : MeasureTheory.IntegrableOn f (Set.Ioi ↑a) MeasureTheory.volume) (nonneg : ∀ t ∈ Set.Ioi ↑a, 0 ≤ f t) : ∑ n ∈ Finset.Ico a b, f ↑(n + 1) ≤ ∫ (x : ℝ) in Set.Ioi ↑a, f x

The partial sums of a nonnegative antitone function are bounded by the integral over (a, ∞).

theorem AntitoneOn.sum_range_le_integral {f : ℝ → ℝ} {N : ℕ} (anti : AntitoneOn f (Set.Icc 0 ↑N)) (integrable : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (nonneg : ∀ t ∈ Set.Ioi 0, 0 ≤ f t) : ∑ n ∈ Finset.range N, f ↑(n + 1) ≤ ∫ (x : ℝ) in Set.Ioi 0, f x

The partial sums of a nonnegative function are bounded by the integral over (0, ∞).

theorem AntitoneOn.summable_of_integrableOn_Ioi {f : ℝ → ℝ} {N : ℕ} (anti : AntitoneOn f (Set.Ici ↑N)) (integrable : MeasureTheory.IntegrableOn f (Set.Ioi ↑N) MeasureTheory.volume) (nonneg : ∀ t ∈ Set.Ioi ↑N, 0 ≤ f t) : Summable fun (n : ℕ) => f ↑n

Integral test: A function which is nonnegative, integrable and antitone for sufficiently large n is summable.

theorem AntitoneOn.summable_of_integrableOn_Ioi_zero {f : ℝ → ℝ} (anti : AntitoneOn f (Set.Ici 0)) (integrable : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (nonneg : ∀ t ∈ Set.Ioi 0, 0 ≤ f t) : Summable fun (n : ℕ) => f ↑n

Integral test: a nonnegative antitone function is summable if it is integrable.

theorem AntitoneOn.tsum_comp_add_le_integral {f : ℝ → ℝ} (N : ℕ) (anti : AntitoneOn f (Set.Ici ↑N)) (integrable : MeasureTheory.IntegrableOn f (Set.Ioi ↑N) MeasureTheory.volume) (nonneg : ∀ t ∈ Set.Ioi ↑N, 0 ≤ f t) : ∑' (n : ℕ), f ↑(n + N + 1) ≤ ∫ (x : ℝ) in Set.Ioi ↑N, f x

theorem AntitoneOn.tsum_add_one_le_integral {f : ℝ → ℝ} (anti : AntitoneOn f (Set.Ici 0)) (integrable : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (nonneg : ∀ t ∈ Set.Ioi 0, 0 ≤ f t) : ∑' (n : ℕ), f ↑(n + 1) ≤ ∫ (x : ℝ) in Set.Ioi 0, f x

Integral test: bounds the sum from 1 by an integral.

theorem AntitoneOn.tsum_le_integral {f : ℝ → ℝ} (anti : AntitoneOn f (Set.Ici 0)) (integrable : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (nonneg : ∀ t ∈ Set.Ioi 0, 0 ≤ f t) : ∑' (n : ℕ), f ↑n ≤ f 0 + ∫ (x : ℝ) in Set.Ioi 0, f x

Integral test: bounds the sum of a nonnegative antitone function by an integral.

theorem AntitoneOn.abs_tsum_sub_sum_range_le_integral {f : ℝ → ℝ} {N : ℕ} (hN : 1 ≤ N) (anti : AntitoneOn f (Set.Ici (↑N - 1))) (integrable : MeasureTheory.IntegrableOn f (Set.Ioi (↑N - 1)) MeasureTheory.volume) (nonneg : ∀ t ∈ Set.Ioi (↑N - 1), 0 ≤ f t) : |∑' (n : ℕ), f ↑n - ∑ n ∈ Finset.range N, f ↑n| ≤ ∫ (x : ℝ) in Set.Ioi (↑N - 1), f x

Bounds the difference between a sum and its partial sums by an integral.

theorem AntitoneOn.integrableOn_Ioi_of_summable_comp_add {f : ℝ → ℝ} {N : ℕ} (anti : AntitoneOn f (Set.Ici ↑N)) (summable : Summable fun (n : ℕ) => f ↑(n + N)) (nonneg : ∀ t ∈ Set.Ioi ↑N, 0 ≤ f t) : MeasureTheory.IntegrableOn f (Set.Ioi ↑N) MeasureTheory.volume

Converse to the integral test: a nonnegative, integrable, summable function is integrable.

theorem AntitoneOn.integrableOn_Ioi_zero_of_summable {f : ℝ → ℝ} (anti : AntitoneOn f (Set.Ici 0)) (summable : Summable fun (n : ℕ) => f ↑n) (nonneg : ∀ t ∈ Set.Ioi 0, 0 ≤ f t) : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume

Converse to the integral test: a nonnegative, integrable, summable function is integrable.

theorem AntitoneOn.integral_le_tsum_comp_add {f : ℝ → ℝ} (N : ℕ) (anti : AntitoneOn f (Set.Ici ↑N)) (summable : Summable fun (n : ℕ) => f ↑n) (nonneg : ∀ t ∈ Set.Ioi ↑N, 0 ≤ f t) : ∫ (x : ℝ) in Set.Ioi ↑N, f x ≤ ∑' (n : ℕ), f ↑(n + N)

The sum of a nonnegative, antitone function is bounded below by its integral.

theorem AntitoneOn.integral_le_tsum {f : ℝ → ℝ} (anti : AntitoneOn f (Set.Ici 0)) (summable : Summable fun (n : ℕ) => f ↑n) (nonneg : ∀ t ∈ Set.Ioi 0, 0 ≤ f t) : ∫ (x : ℝ) in Set.Ioi 0, f x ≤ ∑' (n : ℕ), f ↑n

The sum of a nonnegative, antitone function is bounded below by its integral.