Euler-Maclaurin formula #
This lets us approximate finite sums of C^k functions with integrals, with known bounds on the
remainder.
Euler-Maclaurin for a single [a, a + 1] interval #
theorem
EulerMaclaurin.intervalIntegrable_presaw_smul
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{t : Set ℝ}
{c : ℤ}
{n : ℕ}
(fc : ContDiffOn ℝ (↑n) f t)
{a b : ℝ}
(ab : a ≤ b)
(u : UniqueDiffOn ℝ t)
(abt : Set.Icc a b ⊆ t)
{s : ℕ}
:
IntervalIntegrable (fun (x : ℝ) => presaw s c x • iteratedDerivWithin n f t x) MeasureTheory.volume a b
theorem
EulerMaclaurin.presaw_smul_iteratedDeriv_by_parts
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{t : Set ℝ}
{a c : ℤ}
{s : ℕ}
[CompleteSpace E]
(fc : ContDiffOn ℝ (↑s + 1) f t)
(u : UniqueDiffOn ℝ t)
(abt : Set.Icc (↑a) (↑a + 1) ⊆ t)
:
The key integration by parts identity, presaw version
theorem
EulerMaclaurin.presaw_iterated_by_parts
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{t : Set ℝ}
{a : ℤ}
{s : ℕ}
[CompleteSpace E]
(fc : ContDiffOn ℝ (↑s + 1) f t)
(u : UniqueDiffOn ℝ t)
(abt : Set.Icc (↑a) (↑a + 1) ⊆ t)
:
Iterated integration by parts, presaw version
The full Euler-Maclaurin formula #
def
trapezoid_sum
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(f : ℝ → E)
(a : ℤ)
:
ℕ → E
Trapezoidal sum: the trapezoidal rule for integer step size on [a, a + n]
Equations
- trapezoid_sum f a 0 = 0
- trapezoid_sum f a n.succ = trapezoid_sum f a n + 2⁻¹ • (f (↑a + ↑n) + f (↑a + ↑n + 1))
Instances For
@[simp]
theorem
trapezoid_sum_zero
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{a : ℤ}
:
theorem
trapezoid_sum_succ
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{a : ℤ}
{n : ℕ}
:
theorem
ae_ne
{α : Type u_2}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
[MeasureTheory.NoAtoms μ]
(x : α)
:
theorem
intervalIntegrable_saw_smul
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{t : Set ℝ}
{a : ℤ}
{s n : ℕ}
(fc : ContDiffOn ℝ (↑s) f t)
(u : UniqueDiffOn ℝ t)
(abt : Set.Icc (↑a) (↑a + ↑n) ⊆ t)
:
IntervalIntegrable (fun (x : ℝ) => saw s x • iteratedDerivWithin s f t x) MeasureTheory.volume (↑a) (↑a + ↑n)
theorem
trapezoid_sum_eq_integral_add
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{t : Set ℝ}
{a : ℤ}
{s n : ℕ}
[CompleteSpace E]
(fc : ContDiffOn ℝ (↑s + 1) f t)
(u : UniqueDiffOn ℝ t)
(abt : Set.Icc (↑a) (↑a + ↑n) ⊆ t)
:
The Euler-Maclaurin formula