We prove the 1st order Euler-Maclaurin formula by specialising Abel summation and manipulating integrals.

noncomputable def B1 (x : ℝ) : ℝ

The 1st Bernoulli function.

Equations

• B1 x = x - ↑⌊x⌋₊ - 1 / 2

theorem aestronglyMeasurable_B1 : MeasureTheory.AEStronglyMeasurable B1 MeasureTheory.volume

theorem abs_B1_le_half {x : ℝ} (hx : 0 ≤ x) : |B1 x| ≤ 1 / 2

theorem integral_deriv_mul_add_const {𝕜 : Type u_1} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ} (c : 𝕜) (hab : a ≤ b) (h_int : IntervalIntegrable (deriv f) MeasureTheory.volume a b) (hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) : ∫ (t : ℝ) in a..b, (↑t + c) * deriv f t = (↑b + c) * f b - (↑a + c) * f a - ∫ (t : ℝ) in a..b, f t

theorem intervalIntegrable_deriv_mul_B1 {𝕜 : Type u_1} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (h_cont : ContinuousOn (deriv f) (Set.uIcc a b)) : IntervalIntegrable (fun (t : ℝ) => deriv f t * ↑(B1 t)) MeasureTheory.volume a b

theorem integral_deriv_mul_floor_add_one {𝕜 : Type u_1} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) (h_cont : ContinuousOn (deriv f) (Set.uIcc a b)) : ∫ (t : ℝ) in a..b, deriv f t * (↑⌊t⌋₊ + 1) = ((↑b + 1 / 2) * f b - (↑a + 1 / 2) * f a - ∫ (t : ℝ) in a..b, f t) - ∫ (t : ℝ) in a..b, deriv f t * ↑(B1 t)

theorem sum_eq_integral_add_integral_deriv {𝕜 : Type u_1} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) (h_cont : ContinuousOn (deriv f) (Set.uIcc a b)) : ∑ k ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k = (f a * ↑(B1 a) - f b * ↑(B1 b) + ∫ (t : ℝ) in a..b, f t) + ∫ (t : ℝ) in a..b, deriv f t * ↑(B1 t)