The Bernoulli functional and the binomial basis

• Lb Q = ∑ Q_n B_n (the Bernoulli umbral functional, B₁ = -1/2);
• Lb_shift : Lb (Q(x+1)) - Lb Q = Q'(0);
• bin k = x(x-1)⋯(x-k+1)/k!, bin_eval_nat : bin k (m) = choose m k;
• Lb_bin : Lb (bin k) = (-1)^k/(k+1);
• derivative_bin : bin_k' = ∑_{j=1}^k (-1)^{j-1}/j · bin_{k-j};
• newton : P = ∑_{k ≤ d} Δ^k P(0) · bin k for deg P ≤ d.

theorem Zeta5Irrational.poly_eq_of_nat {P Q : Polynomial ℚ} (h : ∀ (n : ℕ), Polynomial.eval (↑n) P = Polynomial.eval (↑n) Q) : P = Q

Polynomials over ℚ that agree at all natural numbers are equal.

The Bernoulli functional

noncomputable def Zeta5Irrational.Lb (Q : Polynomial ℚ) : ℚ

Lb Q = ∑_n Q_n B_n.

Equations

• Zeta5Irrational.Lb Q = Q.sum fun (n : ℕ) (a : ℚ) => a * bernoulli n

theorem Zeta5Irrational.Lb_add (P Q : Polynomial ℚ) : Lb (P + Q) = Lb P + Lb Q

theorem Zeta5Irrational.Lb_smul (c : ℚ) (Q : Polynomial ℚ) : Lb (c • Q) = c * Lb Q

theorem Zeta5Irrational.Lb_C_mul (c : ℚ) (Q : Polynomial ℚ) : Lb (Polynomial.C c * Q) = c * Lb Q

theorem Zeta5Irrational.Lb_monomial (n : ℕ) (a : ℚ) : Lb ((Polynomial.monomial n) a) = a * bernoulli n

theorem Zeta5Irrational.Lb_X_pow (n : ℕ) : Lb (Polynomial.X ^ n) = bernoulli n

theorem Zeta5Irrational.Lb_sum {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial ℚ) : Lb (∑ i ∈ s, f i) = ∑ i ∈ s, Lb (f i)

theorem Zeta5Irrational.Lb_neg (Q : Polynomial ℚ) : Lb (-Q) = -Lb Q

theorem Zeta5Irrational.Lb_sub (P Q : Polynomial ℚ) : Lb (P - Q) = Lb P - Lb Q

theorem Zeta5Irrational.Lb_shift (Q : Polynomial ℚ) : Lb (Q.comp (Polynomial.X + 1)) - Lb Q = Polynomial.eval 0 (Polynomial.derivative Q)

Shift identity: Lb (Q(x+1)) - Lb Q = Q'(0).

The binomial basis

noncomputable def Zeta5Irrational.bin (k : ℕ) : Polynomial ℚ

bin k = x(x-1)⋯(x-k+1)/k!.

Equations

• Zeta5Irrational.bin k = Polynomial.C (↑k.factorial)⁻¹ * descPochhammer ℚ k

theorem Zeta5Irrational.bin_eval_nat (k m : ℕ) : Polynomial.eval (↑m) (bin k) = ↑(m.choose k)

theorem Zeta5Irrational.bin_zero : bin 0 = 1

theorem Zeta5Irrational.bin_eval_zero {k : ℕ} (hk : 1 ≤ k) : Polynomial.eval 0 (bin k) = 0

theorem Zeta5Irrational.bin_comp_add_one (k : ℕ) : (bin (k + 1)).comp (Polynomial.X + 1) = bin (k + 1) + bin k

Pascal: bin (k+1) (x+1) = bin (k+1) x + bin k x.

theorem Zeta5Irrational.descPochhammer_eval_neg_one (n : ℕ) : Polynomial.eval (-1) (descPochhammer ℚ n) = (-1) ^ n * ↑n.factorial

theorem Zeta5Irrational.bin_derivative_eval_zero (k : ℕ) : Polynomial.eval 0 (Polynomial.derivative (bin (k + 1))) = (-1) ^ k / (↑k + 1)

bin_k'(0) = (-1)^{k-1}/k.

theorem Zeta5Irrational.Lb_bin (k : ℕ) : Lb (bin k) = (-1) ^ k / (↑k + 1)

Lb (bin k) = (-1)^k/(k+1).

theorem Zeta5Irrational.eq_C_of_comp_add_one {Q : Polynomial ℚ} (h : Q.comp (Polynomial.X + 1) = Q) : Q = Polynomial.C (Polynomial.eval 0 Q)

A polynomial invariant under x ↦ x + 1 is constant.

noncomputable def Zeta5Irrational.dcoef (j : ℕ) : ℚ

The coefficients of the derivative in the binomial basis.

Equations

• Zeta5Irrational.dcoef j = (-1) ^ (j - 1) / ↑j

theorem Zeta5Irrational.derivative_bin (k : ℕ) : Polynomial.derivative (bin k) = ∑ j ∈ Finset.Icc 1 k, Polynomial.C (dcoef j) * bin (k - j)

Derivative of the binomial polynomials.

Newton expansion

theorem Zeta5Irrational.newton (P : Polynomial ℚ) {d : ℕ} (hd : P.natDegree ≤ d) : P = ∑ k ∈ Finset.range (d + 1), Polynomial.C ((fwdDiff 1)^[k] (fun (x : ℚ) => Polynomial.eval x P) 0) * bin k

Newton expansion of a polynomial in the binomial basis.