Binomial polynomials binom(t,a), their integer values at all integers, Newton expansion at an arbitrary centre, derivatives at integers (v_p ≥ β - ⌊log_p e⌋), D_m = m!·binom(t+m,m), and the residue scale K!/∏_{l≠j}(l-j) ∈ ℤ.

@[reducible, inline]

noncomputable abbrev Zeta32.Arith.Small.binomPoly (a : ℕ) : Polynomial ℚ

binom(t,a)=descPochhammer a/a!.

Equations

• Zeta32.Arith.Small.binomPoly a = Zeta5Irrational.bin a

theorem Zeta32.Arith.Small.binomPoly_eval_nat (a m : ℕ) : Polynomial.eval (↑m) (binomPoly a) = ↑(m.choose a)

theorem Zeta32.Arith.Small.binomPoly_natDegree (a : ℕ) : (binomPoly a).natDegree = a

theorem Zeta32.Arith.Small.binomPoly_coeff_self (a : ℕ) : (binomPoly a).coeff a = (↑a.factorial)⁻¹

theorem Zeta32.Arith.Small.eq_of_eval_shift_nat {p q : Polynomial ℚ} (c : ℚ) (h : ∀ (m : ℕ), Polynomial.eval (c + ↑m) p = Polynomial.eval (c + ↑m) q) : p = q

Two rational polynomials agreeing on c+m for every natural m are equal.

theorem Zeta32.Arith.Small.binomPoly_zero : binomPoly 0 = 1

theorem Zeta32.Arith.Small.binomPoly_succ_comp_add_one (k : ℕ) : (binomPoly (k + 1)).comp (Polynomial.X + 1) = binomPoly (k + 1) + binomPoly k

theorem Zeta32.Arith.Small.binomPoly_eval_add_one (k : ℕ) (x : ℚ) : Polynomial.eval (x + 1) (binomPoly (k + 1)) = Polynomial.eval x (binomPoly (k + 1)) + Polynomial.eval x (binomPoly k)

theorem Zeta32.Arith.Small.binomPoly_eval_int (k : ℕ) (m : ℤ) : ∃ (z : ℤ), Polynomial.eval (↑m) (binomPoly k) = ↑z

binom(m,k) is an integer for every integer m, including negative m.

theorem Zeta32.Arith.Small.binomPoly_eval_int_VG (p k : ℕ) (m : ℤ) : Zeta5Irrational.VG p (Polynomial.eval (↑m) (binomPoly k)) 0

def Zeta32.Arith.Small.newtonCoeff (f : Polynomial ℚ) (c : ℚ) (k : ℕ) : ℚ

The k-th forward difference of the values of f, at step 1.

Equations

• Zeta32.Arith.Small.newtonCoeff f c k = (fwdDiff 1)^[k] (fun (x : ℚ) => Polynomial.eval x f) c

theorem Zeta32.Arith.Small.newtonCoeff_eq_sum (f : Polynomial ℚ) (c : ℚ) (k : ℕ) : newtonCoeff f c k = ∑ i ∈ Finset.range (k + 1), (-1) ^ (k - i) * ↑(k.choose i) * Polynomial.eval (c + ↑i) f

theorem Zeta32.Arith.Small.newtonCoeff_eq_zero {f : Polynomial ℚ} {d : ℕ} (hf : f.natDegree ≤ d) (c : ℚ) {k : ℕ} (hk : d < k) : newtonCoeff f c k = 0

theorem Zeta32.Arith.Small.newton_expansion {f : Polynomial ℚ} {d : ℕ} (hf : f.natDegree ≤ d) (c : ℚ) : f = ∑ k ∈ Finset.range (d + 1), Polynomial.C (newtonCoeff f c k) * (binomPoly k).comp (Polynomial.X - Polynomial.C c)

Newton expansion at an arbitrary rational centre c, degree window d.

theorem Zeta32.Arith.Small.newtonCoeff_VG (p : ℕ) [Fact (Nat.Prime p)] {f : Polynomial ℚ} (c r : ℚ) (k : ℕ) (hv : ∀ i ≤ k, Zeta5Irrational.VG p (Polynomial.eval (c + ↑i) f) r) : Zeta5Irrational.VG p (newtonCoeff f c k) r

VG bound on Newton coefficients from a window of consecutive values.

theorem Zeta32.Arith.Small.descPochhammer_eval_neg_one (k : ℕ) : Polynomial.eval (-1) (descPochhammer ℚ k) = (-1) ^ k * ↑k.factorial

theorem Zeta32.Arith.Small.binomPoly_derivative_eval_zero (k : ℕ) : Polynomial.eval 0 (Polynomial.derivative (binomPoly (k + 1))) = (-1) ^ k / (↑k + 1)

d/dx binom(x,k+1) at x=0 equals (-1)^k/(k+1).

theorem Zeta32.Arith.Small.binomPoly_derivative_eval_zero_zero : Polynomial.eval 0 (Polynomial.derivative (binomPoly 0)) = 0

theorem Zeta32.Arith.Small.derivative_eval_newton {f : Polynomial ℚ} {d : ℕ} (hf : f.natDegree ≤ d) (c : ℚ) : Polynomial.eval c (Polynomial.derivative f) = ∑ k ∈ Finset.range d, newtonCoeff f c (k + 1) * ((-1) ^ k / (↑k + 1))

The derivative at a Newton centre: f'(c)=sum_{k=1}^d Delta^k f(c) (-1)^(k-1)/k.

theorem Zeta32.Arith.Small.derivative_eval_VG (p : ℕ) [Fact (Nat.Prime p)] {f : Polynomial ℚ} {e : ℕ} (hf : f.natDegree ≤ e) (r : ℚ) (hv : ∀ (m : ℤ), Zeta5Irrational.VG p (Polynomial.eval (↑m) f) r) (m : ℤ) : Zeta5Irrational.VG p (Polynomial.eval (↑m) (Polynomial.derivative f)) (r - ↑(Nat.log p e))

Derivative values at integers from values at all integers.

D_m and the shifted binomial

theorem Zeta32.Arith.Small.D_succ (m : ℕ) : D (m + 1) = D m * (Polynomial.X + Polynomial.C (↑m + 1))

theorem Zeta32.Arith.Small.D_eq_desc (m : ℕ) : D m = (descPochhammer ℚ m).comp (Polynomial.X + Polynomial.C ↑m)

theorem Zeta32.Arith.Small.D_natDegree (m : ℕ) : (D m).natDegree = m

theorem Zeta32.Arith.Small.D_monic (m : ℕ) : (D m).Monic

theorem Zeta32.Arith.Small.desc_eq_C_mul_binomPoly (m : ℕ) : descPochhammer ℚ m = Polynomial.C ↑m.factorial * binomPoly m

noncomputable def Zeta32.Arith.Small.shiftBinom (n : ℕ) : Polynomial ℚ

binom(t+n,n).

Equations

• Zeta32.Arith.Small.shiftBinom n = (Zeta32.Arith.Small.binomPoly n).comp (Polynomial.X + Polynomial.C ↑n)

theorem Zeta32.Arith.Small.D_eq_shiftBinom (n : ℕ) : D n = Polynomial.C ↑n.factorial * shiftBinom n

theorem Zeta32.Arith.Small.shiftBinom_eval_int (p n : ℕ) (m : ℤ) : Zeta5Irrational.VG p (Polynomial.eval (↑m) (shiftBinom n)) 0

theorem Zeta32.Arith.Small.shiftBinom_natDegree (n : ℕ) : (shiftBinom n).natDegree = n

theorem Zeta32.Arith.Small.D_eval_nat (K m : ℕ) : Polynomial.eval (↑m) (D K) = ↑K.factorial * ↑((m + K).choose K)

theorem Zeta32.Arith.Small.shifted_binom_ratio {K k : ℕ} (hk : K ≤ k) : Polynomial.C ↑K.factorial * (binomPoly k).comp (Polynomial.X + Polynomial.C ↑K) = D K * (Polynomial.C (↑(k.choose K))⁻¹ * binomPoly (k - K))

K! binom(t+K,k) = D_K binom(t,k-K)/binom(k,K) for K <= k.

theorem Zeta32.Arith.Small.inv_choose_VG (p : ℕ) [hp : Fact (Nat.Prime p)] {k K N : ℕ} (hk : K ≤ k) (hkN : k ≤ N) : Zeta5Irrational.VG p (↑(k.choose K))⁻¹ (-↑(Nat.log p N))

Residue denominators

def Zeta32.Arith.Small.eraseProd (K j : ℕ) : ℚ

Product of the differences from j to all other indices in 1, …, K.

Equations

• Zeta32.Arith.Small.eraseProd K j = ∏ l ∈ (Finset.Icc 1 K).erase j, (↑l - ↑j)

theorem Zeta32.Arith.Small.D_eval_eq_prod (m : ℕ) (x : ℚ) : Polynomial.eval x (D m) = ∏ l ∈ Finset.Icc 1 m, (x + ↑l)

theorem Zeta32.Arith.Small.eraseProd_base {j : ℕ} (hj : 1 ≤ j) : eraseProd j j = (-1) ^ (j - 1) * ↑(j - 1).factorial

theorem Zeta32.Arith.Small.eraseProd_succ {K j : ℕ} (hjK : j ≤ K) : eraseProd (K + 1) j = eraseProd K j * (↑(K + 1) - ↑j)

theorem Zeta32.Arith.Small.eraseProd_eq {K j : ℕ} (hj : 1 ≤ j) (hjK : j ≤ K) : eraseProd K j = (-1) ^ (j - 1) * ↑(j - 1).factorial * ↑(K - j).factorial

theorem Zeta32.Arith.Small.residueScale_eq {K j : ℕ} (hj : 1 ≤ j) (hjK : j ≤ K) : ↑K.factorial / eraseProd K j = (-1) ^ (j - 1) * ↑K * ↑((K - 1).choose (j - 1))

theorem Zeta32.Arith.Small.residueScale_VG (p : ℕ) {K j : ℕ} (hj : 1 ≤ j) (hjK : j ≤ K) : Zeta5Irrational.VG p (↑K.factorial / eraseProd K j) 0