The Bernoulli functional and the binomial basis

• Lb Q = ∑ Q_n B_n (B₁ = -1/2), Lbp Q = ∑ Q_n B'_n (B'₁ = +1/2), Lbp Q = Lb Q + Q_1;
• bin k = x(x-1)⋯(x-k+1)/k!, Lb (bin k) = (-1)^k/(k+1), derivative_bin, newton;
• BinRep: combinations of bin 0, …, bin k with coefficients of valuation ≥ r;
• VG_polynomialMoment: if v_p((X q)(m)) ≥ β for 0 ≤ m ≤ d, deg (X q) ≤ d, d + 1 < p² and r is p-integral, then v_p(polynomialMoment r q) ≥ β - 2.

noncomputable def Zeta32.Arith.Local.Lbp (Q : Polynomial ℚ) : ℚ

Lbp Q = ∑_n Q_n B'_n (the convention B'₁ = +1/2 of Zeta32.moment).

Equations

• Zeta32.Arith.Local.Lbp Q = Q.sum fun (n : ℕ) (a : ℚ) => a * bernoulli' n

theorem Zeta32.Arith.Local.Lbp_add (P Q : Polynomial ℚ) : Lbp (P + Q) = Lbp P + Lbp Q

theorem Zeta32.Arith.Local.Lbp_monomial (n : ℕ) (a : ℚ) : Lbp ((Polynomial.monomial n) a) = a * bernoulli' n

theorem Zeta32.Arith.Local.Lbp_eq (Q : Polynomial ℚ) : Lbp Q = Lb Q + Q.coeff 1

Lbp Q = Lb Q + Q_1.

The binomial basis

Valuations in the binomial basis

theorem Zeta32.Arith.Local.BinRep.eval_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} {r : ℚ} {Q : Polynomial ℚ} (h : BinRep p k r Q) : VG p (Polynomial.eval 0 Q) r

The value at 0 of a binomial representation is its 0-th coefficient.

The polynomial part of U_r

theorem Zeta32.Arith.Local.polynomialMoment_eq (r : ℚ) (q : Polynomial ℚ) : polynomialMoment r q = Lbp (Polynomial.derivative (Polynomial.X * q)) + 2 * r * Lbp (Polynomial.X * q)

polynomialMoment r q = Lbp ((X q)') + 2 r Lbp (X q).

theorem Zeta32.Arith.Local.nat_log_le_one {p d : ℕ} (hdp : d + 1 < p ^ 2) : Nat.log p (d + 1) ≤ 1

theorem Zeta32.Arith.Local.VG_polynomialMoment {p : ℕ} [hp : Fact (Nat.Prime p)] {r : ℚ} (hr : VG p r 0) {q : Polynomial ℚ} {d : ℕ} (hd : (Polynomial.X * q).natDegree ≤ d) (hdp : d + 1 < p ^ 2) {β : ℚ} (hv : ∀ m ≤ d, VG p (Polynomial.eval (↑m) (Polynomial.X * q)) β) : VG p (polynomialMoment r q) (β - 2)

Polynomial part: loss at most 2.