Documentation

Expdb.Mathlib.EulerMaclaurin

Arbitrary-order Euler--Maclaurin summation #

This file is adapted from Interval/EulerMaclaurin/Bernoulli.lean and Interval/EulerMaclaurin/EulerMaclaurin.lean in girving/interval at commit f4a3231fd735cdf6d5265864d9a9207744a7aca2, licensed under Apache-2.0.

The source has been modified, namespaced for Expdb, and updated for newer version of Mathlib.

Periodic Bernoulli functions #

source
noncomputable def Expdb.EulerMaclaurin.saw (s : ℕ) (x : ℝ) :
ℝ

The scaled periodic Bernoulli function of order s.

Equations
Instances For

    Explicit bounds #

    source
    noncomputable def Expdb.EulerMaclaurin.sawBound (s : ℕ) :
    ℝ

    An explicit uniform bound for the absolute value of saw s, obtained by summing the absolute values of the coefficients of the sth Bernoulli polynomial.

    Equations
    Instances For
      source
      theorem Expdb.EulerMaclaurin.abs_saw_le (s : ℕ) (x : ℝ) :
      |saw s x| ≤ sawBound s

      The absolute value of saw s is bounded by the explicit constant sawBound s.

      source
      @[simp]
      theorem Expdb.EulerMaclaurin.sawBound_nonneg {s : ℕ} :
      0 ≤ sawBound s

      The uniform bound for saw is nonnegative.

      Euler--Maclaurin on one unit interval #

      The full formula #

      source
      theorem Expdb.EulerMaclaurin.sum_Icc_eq_integral_add {s : ℕ} {a : ℤ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {t : Set ℝ} {n : ℕ} [CompleteSpace E] (fc : ContDiffOn ℝ (↑s + 1) f t) (u : UniqueDiffOn ℝ t) (abt : Set.Icc (↑a) (↑a + ↑n) ⊆ t) :
      ∑ k ∈ Finset.Icc a (a + ↑n), f ↑k = (∫ (x : ℝ) in ↑a..↑a + ↑n, f x) + 2⁻¹ • (f ↑a + f (↑a + ↑n)) + ∑ m ∈ Finset.range s, (-1) ^ m • saw (m + 2) 0 • (iteratedDerivWithin (m + 1) f t (↑a + ↑n) - iteratedDerivWithin (m + 1) f t ↑a) + (-1) ^ s • ∫ (x : ℝ) in ↑a..↑a + ↑n, saw (s + 1) x • iteratedDerivWithin (s + 1) f t x

      The arbitrary-order Euler--Maclaurin formula for a sum over consecutive integers.

      source
      theorem Expdb.EulerMaclaurin.norm_sum_Icc_nat_sub_integral_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {t : Set ℝ} [CompleteSpace E] {a b s : ℕ} (hab : a ≤ b) (fc : ContDiffOn ℝ (↑s + 1) f t) (u : UniqueDiffOn ℝ t) (abt : Set.Icc ↑a ↑b ⊆ t) {C₀ : ℝ} (hendpoint : ∀ x ∈ Set.Icc ↑a ↑b, ‖f x‖ ≤ C₀) (C : ℕ → ℝ) (hderiv : ∀ (k : ℕ), 1 ≤ k → k ≤ s + 1 → ∀ x ∈ Set.Icc ↑a ↑b, ‖iteratedDerivWithin k f t x‖ ≤ C k) :
      ‖∑ n ∈ Finset.Icc a b, f ↑n - ∫ (x : ℝ) in ↑a..↑b, f x‖ ≤ C₀ + ∑ m ∈ Finset.range s, |saw (m + 2) 0| * (2 * C (m + 1)) + sawBound (s + 1) * C (s + 1) * ↑(b - a)

      A convenient norm form of Euler--Maclaurin for natural endpoints. Uniform bounds on the function and its derivatives control the difference between the inclusive sum and its integral; the right-hand side records the endpoint, correction-term, and remainder contributions.