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

Adapted from PrimeNumberTheoremAnd revision 127b50e33f6033e2147921167a117af96d9ba4ea, via Jason Davies's Iwaniec linear sieve snapshot c8d01549d2ae640b36ec198c1f0f6495f1b036cf (both Apache-2.0). Blueprint-only machinery is omitted.

Supporting lemmas for Iwaniec's sieve and its prime-number-theorem input.

noncomputable def IwaniecLinearSievePNT.B1 (x : ℝ) : ℝ

The 1st Bernoulli function.

Equations

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

theorem IwaniecLinearSievePNT.aestronglyMeasurable_B1 : MeasureTheory.AEStronglyMeasurable B1 MeasureTheory.volume

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

theorem IwaniecLinearSievePNT.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 IwaniecLinearSievePNT.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 IwaniecLinearSievePNT.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 IwaniecLinearSievePNT.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)