The bound (3.9) for the polynomial functional τ(P) = L(P''')/24

If deg P ≤ d and v_p(P(m)) ≥ β for m = 0, …, d, then v_p(τ(P)) ≥ β - 4 ⌊log_p (d+1)⌋ - v_p(24).

noncomputable def Zeta5Irrational.tau (P : Polynomial ℚ) : ℚ

τ(P) = L(P''')/24.

Equations

• Zeta5Irrational.tau P = Zeta5Irrational.Lb ((⇑Polynomial.derivative)^[3] P) / 24

def Zeta5Irrational.BinRep (p k : ℕ) (r : ℚ) (Q : Polynomial ℚ) : Prop

Q is a combination of bin 0, …, bin k with coefficients of valuation ≥ r.

Equations

• Zeta5Irrational.BinRep p k r Q = ∃ (e : ℕ → ℚ), Q = ∑ m ∈ Finset.range (k + 1), Polynomial.C (e m) * Zeta5Irrational.bin m ∧ ∀ m ≤ k, Zeta5Irrational.VG p (e m) r

theorem Zeta5Irrational.derivative_bin' {k m : ℕ} (hm : m ≤ k) : Polynomial.derivative (bin m) = ∑ n ∈ Finset.range (k + 1), Polynomial.C (if n < m then dcoef (m - n) else 0) * bin n

theorem Zeta5Irrational.VG_dcoef {p : ℕ} [hp : Fact (Nat.Prime p)] {j k : ℕ} (hj : 1 ≤ j) (hjk : j ≤ k) : VG p (dcoef j) (-↑(Nat.log p k))

theorem Zeta5Irrational.BinRep.derivative {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} {r : ℚ} {Q : Polynomial ℚ} (h : BinRep p k r Q) : BinRep p k (r - ↑(Nat.log p k)) (Polynomial.derivative Q)

Differentiation loses at most ⌊log_p k⌋ in the binomial basis.

theorem Zeta5Irrational.BinRep.Lb {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} {r : ℚ} {Q : Polynomial ℚ} (h : BinRep p k r Q) : VG p (Zeta5Irrational.Lb Q) (r - ↑(Nat.log p (k + 1)))

The Bernoulli functional loses at most ⌊log_p (k+1)⌋.

theorem Zeta5Irrational.BinRep.mono {p k : ℕ} {r s : ℚ} {Q : Polynomial ℚ} (h : BinRep p k r Q) (hs : s ≤ r) : BinRep p k s Q

theorem Zeta5Irrational.binRep_of_values {p : ℕ} [hp : Fact (Nat.Prime p)] {P : Polynomial ℚ} {d : ℕ} (hd : P.natDegree ≤ d) {β : ℚ} (hv : ∀ m ≤ d, VG p (Polynomial.eval (↑m) P) β) : BinRep p d β P

Values at 0, …, d give a binomial representation.

theorem Zeta5Irrational.VG_inv_24 {p : ℕ} [hp : Fact (Nat.Prime p)] : VG p 24⁻¹ (-↑(padicValNat p 24))

theorem Zeta5Irrational.tau_bound {p : ℕ} [hp : Fact (Nat.Prime p)] {P : Polynomial ℚ} {d : ℕ} (hd : P.natDegree ≤ d) {β : ℚ} (hv : ∀ m ≤ d, VG p (Polynomial.eval (↑m) P) β) : VG p (tau P) (β - 4 * ↑(Nat.log p (d + 1)) - ↑(padicValNat p 24))

(3.9): v_p(τ(P)) ≥ β - 4 ⌊log_p (d+1)⌋ - v_p(24) if deg P ≤ d and v_p(P(m)) ≥ β for 0 ≤ m ≤ d.