Bernoulli polynomials

Mathlib has a lot of this, so possibly I should shift to using those results in future. See periodizedBernoulli in particular.

The Bernoulli polynomials

Multiplication theorem

theorem integrable_bernoulliFun_comp_add_right {s : ℕ} {a b c : ℝ} : IntervalIntegrable (fun (x : ℝ) => bernoulliFun s (x + c)) MeasureTheory.volume a b

The presaw functions

These are saw s x smoothly extended from a particular [a,a+1) interval.

def presaw (s : ℕ) (a : ℤ) (x : ℝ) : ℝ

The saw functions are scaled, shifted versions of the Bernoulli polynomials

Equations

• presaw s a x = (↑s.factorial)⁻¹ • bernoulliFun s (x - ↑a)

theorem contDiff_presaw {s : ℕ} {a : ℤ} : ContDiff ℝ ⊤ (presaw s a)

presaw is smooth

@[simp]

theorem presaw_start {a : ℤ} {x : ℝ} : presaw 0 a x = 1

theorem hasDerivAt_presaw {s : ℕ} {a : ℤ} {x : ℝ} : HasDerivAt (presaw (s + 1) a) (presaw s a x) x

@[simp]

theorem deriv_presaw {s : ℕ} {a : ℤ} {x : ℝ} : deriv (presaw (s + 1) a) x = presaw s a x

@[simp]

theorem presaw_zero {a : ℤ} {x : ℝ} : presaw 0 a x = 1

The saw functions

def saw (s : ℕ) (x : ℝ) : ℝ

The saw functions are scaled, periodic versions of the Bernoulli polynomials

Equations

• saw s x = (↑s.factorial)⁻¹ • bernoulliFun s (Int.fract x)

theorem saw_eqOn {s : ℕ} {a : ℤ} : Set.EqOn (saw s) (presaw s a) (Set.Ico (↑a) (↑a + 1))

Saw is nice on [a,a+1)

@[simp]

theorem presaw_coe_same {s : ℕ} {a : ℤ} : presaw s a ↑a = saw s 0

presaw at integer values in terms of saw

@[simp]

theorem presaw_coe_succ {s : ℕ} {a : ℤ} : presaw (s + 2) a (↑a + 1) = saw (s + 2) 0

presaw at integer values in terms of saw

@[simp]

theorem presaw_one_coe_succ {a : ℤ} : presaw 1 a (↑a + 1) = 1 / 2

presaw at integer values in terms of saw

theorem contDiff_saw {s : ℕ} {a : ℤ} : ContDiffOn ℝ ⊤ (saw s) (Set.Ico (↑a) (↑a + 1))

Saw is nice on [a,a+1)

@[simp]

theorem saw_zero {x : ℝ} : saw 0 x = 1

@[simp]

theorem saw_int {s : ℕ} {x : ℤ} : saw s ↑x = saw s 0

theorem hasDerivAt_saw {s : ℕ} {a : ℤ} {x : ℝ} (m : x ∈ Set.Ioo (↑a) (↑a + 1)) : HasDerivAt (saw (s + 1)) (saw s x) x

@[simp]

theorem deriv_saw {s : ℕ} {a : ℤ} {x : ℝ} (m : x ∈ Set.Ioo (↑a) (↑a + 1)) : deriv (saw (s + 1)) x = saw s x

theorem saw_one {x : ℝ} : saw 1 x = Int.fract x - 1 / 2

saw 1 is a saw-tooth function

@[simp]

theorem saw_one_zero : saw 1 0 = -2⁻¹

theorem continuous_saw {s : ℕ} : Continuous (saw (s + 2))

saw is continuous for 2 ≤ s

Saw values at 0

theorem saw_eval_zero {s : ℕ} : saw s 0 = (↑s.factorial)⁻¹ * ↑(bernoulli s)

Explicit bounds on Bernoulli polynomials

We first count the zeros of even and odd Bernoulli polynomials by induction, using Rolle's theorem.

theorem bernoulliFun_rolle {s : ℕ} (s0 : s ≠ 0) {x y : ℝ} (xy : x < y) (e : bernoulliFun s x = bernoulliFun s y) : ∃ z ∈ Set.Ioo x y, bernoulliFun (s - 1) z = 0

Rolle's theorem specialised to the Bernoulli polynomials

def pres (s : ℕ) (x y b : ℝ) : ℕ∞

Number of Bernoulii polynomial preimages in an open interval

Equations

• pres s x y b = (Set.Ioo x y ∩ bernoulliFun s ⁻¹' {b}).encard

theorem pres_eq_reflect {s : ℕ} {x y b : ℝ} : pres s (1 - y) (1 - x) ((-1) ^ s * b) = pres s x y b

Reflecting pres about the midpoint

@[simp]

theorem pres_zero_eq_zero {x y : ℝ} : pres 0 x y 0 = 0

bernoulliFun 0 has no zeros

@[simp]

theorem pres_one_eq_zero : pres 1 0 2⁻¹ 0 = 0

bernoulliFun 1 has no zeros in Ioo 0 2⁻¹

@[simp]

theorem pres_two_eq_zero : pres 2 0 1 6⁻¹ = 0

bernoulliFun 2 never hits bernoulli 2 in Ioo 0 1

@[simp]

theorem pres_two_eq_one : pres 2 0 2⁻¹ 0 = 1

bernoulliFun 2 has exactly one zero in Ioo 0 2⁻¹

theorem pres_eq_zero {s : ℕ} {x y b : ℝ} (xy : x < y) (h : pres s x y 0 ≤ 1) (xb : bernoulliFun (s + 1) x = b) (yb : bernoulliFun (s + 1) y = b) : pres (s + 1) x y b = 0

If there's at most one derivative zero betwen two preimages, there are no preimages between

theorem pres_le_one {s : ℕ} {x y b : ℝ} (h : pres s x y 0 = 0) : pres (s + 1) x y b ≤ 1

If there's no derivative zeros in an interval, there is at most one preimage

theorem pres_union_le {s : ℕ} {x y z b : ℝ} (xy : x < y) (yz : y < z) : pres s x z b ≤ pres s x y b + 1 + pres s y z b

Bound pres on an interval by breaking it into two pieces

theorem bernoulliFun_zeros (s : ℕ) (s1 : 2 ≤ s) : if Even s then pres s 0 1 ↑(bernoulli s) = 0 ∧ pres s 0 2⁻¹ 0 ≤ 1 else pres s 0 2⁻¹ 0 = 0

Count various preimages of Bernoulli polynomials

theorem bernoulliFun_pres_eq_zero (s : ℕ) (o : Odd s) : pres s 0 2⁻¹ 0 = 0

theorem abs_bernoulliFun_le_half (s : ℕ) : |bernoulliFun s 2⁻¹| ≤ ↑|bernoulli s|

theorem IsLocalMax.deriv_eq_zero_of_abs {f : ℝ → ℝ} {y : ℝ} (m : IsLocalMax (fun (x : ℝ) => |f x|) y) : deriv f y = 0

theorem abs_bernoulliFun_le_even (s : ℕ) {x : ℝ} (m : x ∈ Set.Icc 0 1) : |bernoulliFun (2 * s) x| ≤ ↑|bernoulli (2 * s)|

Nonexplicit bounds on Bernoulli polynomials

theorem exists_max_bernoulli (s : ℕ) : ∃ x ∈ Set.Icc 0 1, IsMaxOn (fun (x : ℝ) => |bernoulliFun s x|) (Set.Icc 0 1) x

def bernoulliBound (s : ℕ) : ℝ

The maximum absolute value of each Bernoulli polynomial

Equations

• bernoulliBound s = |bernoulliFun s ⋯.choose|

def sawBound (s : ℕ) : ℝ

The maximum absolute value of each saw function

Equations

• sawBound s = (↑s.factorial)⁻¹ * bernoulliBound s

theorem abs_bernoulliFun_le (s : ℕ) (x : ℝ) (m : x ∈ Set.Icc 0 1) : |bernoulliFun s x| ≤ bernoulliBound s

theorem abs_saw_le (s : ℕ) (x : ℝ) : |saw s x| ≤ sawBound s

@[simp]

theorem bernoulliBound_nonneg {s : ℕ} : 0 ≤ bernoulliBound s

@[simp]

theorem sawBound_nonneg {s : ℕ} : 0 ≤ sawBound s

@[simp]

theorem bernoulliBound_eq_abs_bernoulli (s : ℕ) : bernoulliBound (2 * s) = ↑|bernoulli (2 * s)|

@[simp]

theorem bernoulliBound_eq_abs_bernoulli' (s : ℕ) (e : Even s) : bernoulliBound s = ↑|bernoulli s|