Periodized Bernoulli polynomials

Mathlib's periodizedBernoulli k : UnitAddCircle → ℝ is the Bernoulli polynomial bernoulliFun k on [0, 1), extended periodically. At the class of a real number x it is bernoulliFun k (Int.fract x). This file proves what the general Euler-Maclaurin formula in Interval.EulerMaclaurin.Formula needs: the value on [m, m + 1) and at the integers, measurability (also for k = 1, where the function jumps at the integers), interval integrability of products, and integration by parts against a translated Bernoulli polynomial.

Main results

• periodizedBernoulli_coe: periodizedBernoulli k x = bernoulliFun k (Int.fract x).
• periodizedBernoulli_coe_of_mem_Ico_intCast: the value bernoulliFun k (x - m) on [m, m + 1).
• periodizedBernoulli_intCast: the value bernoulli k at an integer, with simp companions for natural numbers, numerals, 0 and 1.
• IntervalIntegrable.periodizedBernoulli_smul: products with interval integrable functions are interval integrable.
• integral_bernoulliFun_comp_sub_right_smul: integration by parts against t ↦ bernoulliFun n (t - c).

theorem AddCircle.measurable_liftIco {T : ℝ} [Fact (0 < T)] {β : Type u_1} [MeasurableSpace β] {a : ℝ} {f : ℝ → β} (hf : Measurable f) : Measurable (liftIco T a f)

The periodization AddCircle.liftIco T a f of a measurable function f : ℝ → β, which agrees with f on [a, a + T), is measurable.

theorem periodizedBernoulli_coe (k : ℕ) (x : ℝ) : periodizedBernoulli k ↑x = bernoulliFun k (Int.fract x)

The periodized Bernoulli polynomial at the class of a real number x is B_k at the fractional part of x. This is the bridge between periodizedBernoulli, defined on the unit circle, and the periodic function on ℝ.

theorem periodizedBernoulli_coe_of_mem_Ico_intCast {k : ℕ} {m : ℤ} {x : ℝ} (hx : x ∈ Set.Ico (↑m) (↑m + 1)) : periodizedBernoulli k ↑x = bernoulliFun k (x - ↑m)

On [m, m + 1), for an integer m, the periodized Bernoulli polynomial is the translate x ↦ bernoulliFun k (x - m) of the Bernoulli polynomial.

@[simp]

theorem periodizedBernoulli_intCast (k : ℕ) (m : ℤ) : periodizedBernoulli k ↑↑m = ↑(bernoulli k)

At an integer, the periodized Bernoulli polynomial is the Bernoulli number.

@[simp]

theorem periodizedBernoulli_natCast (k n : ℕ) : periodizedBernoulli k ↑↑n = ↑(bernoulli k)

At a natural number, the periodized Bernoulli polynomial is the Bernoulli number.

@[simp]

theorem periodizedBernoulli_ofNat (k n : ℕ) [n.AtLeastTwo] : periodizedBernoulli k ↑(OfNat.ofNat n) = ↑(bernoulli k)

At a numeral n ≥ 2, the periodized Bernoulli polynomial is the Bernoulli number.

@[simp]

theorem periodizedBernoulli_apply_one (k : ℕ) : periodizedBernoulli k ↑1 = ↑(bernoulli k)

The periodized Bernoulli polynomial of order k at the real number 1 is the Bernoulli number B_k. Here one in the name refers to the argument, not to the order.

@[simp]

theorem periodizedBernoulli_apply_zero (k : ℕ) : periodizedBernoulli k 0 = ↑(bernoulli k)

The periodized Bernoulli polynomial of order k at the zero of the circle is the Bernoulli number B_k. Here zero in the name refers to the argument, not to the order. It is the form to which simp reduces the value at the real number 0.

theorem measurable_periodizedBernoulli (k : ℕ) : Measurable (periodizedBernoulli k)

The periodized Bernoulli polynomial is measurable on the circle for every k, including k = 1, where it jumps at the origin.

theorem IntervalIntegrable.periodizedBernoulli_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} {g : ℝ → E} {a b : ℝ} (hg : IntervalIntegrable g MeasureTheory.volume a b) : IntervalIntegrable (fun (t : ℝ) => periodizedBernoulli k ↑t • g t) MeasureTheory.volume a b

The product of the periodized Bernoulli polynomial with an interval integrable function is interval integrable. No continuity is needed: the periodized Bernoulli polynomial is measurable and bounded.

theorem integral_bernoulliFun_comp_sub_right_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (n : ℕ) {f f' : ℝ → E} {a b c : ℝ} (hf : ∀ x ∈ Set.uIcc a b, HasDerivWithinAt f (f' x) (Set.uIcc a b) x) (hf' : IntervalIntegrable f' MeasureTheory.volume a b) : ∫ (t : ℝ) in a..b, bernoulliFun n (t - c) • f t = (↑n + 1)⁻¹ • (bernoulliFun (n + 1) (b - c) • f b - bernoulliFun (n + 1) (a - c) • f a - ∫ (t : ℝ) in a..b, bernoulliFun (n + 1) (t - c) • f' t)

Integration by parts against a translated Bernoulli polynomial. If f has derivative f' within [a, b], with f' interval integrable, then `∫ B_n(t - c) • f(t) dt = (n + 1)⁻¹ • (B_{n+1}(b - c) • f(b) - B_{n+1}(a - c) • f(a)

• ∫ B_{n+1}(t - c) • f'(t) dt)`.