the proof notes, §7 (c), the polynomial part of U_r.

Bf f = Σ f_e B'_e (bernoulli', B'_1 = +1/2) is the functional B of the proof notes, §0 on polynomials.

• shift rule B(f(t+1)) = B(f) + f'(1) (from sum_bernoulli');
• hence B(binom(t,k)) = binom(t,k+1)'(1), so v_p(B(binom(t,k))) ≥ -⌊log_p(k+1)⌋ (this replaces the closed form (-1)^{k+1}/(k(k+1)); only the valuation is used);
• polynomialMoment r g = B((t g)') + 2r B(t g);
• if deg g ≤ d and v_p(g(z)) ≥ β for all z ∈ ℤ, then v_p(polynomialMoment r g) ≥ β - 2⌊log_p(d+2)⌋ - v_p(den r).

@[reducible, inline]

noncomputable abbrev Zeta32.Arith.Small.Bf (f : Polynomial ℚ) : ℚ

B on polynomials: t^e ↦ B'_e.

Equations

• Zeta32.Arith.Small.Bf f = Zeta32.Arith.Local.Lbp f

theorem Zeta32.Arith.Small.Bf_add (f g : Polynomial ℚ) : Bf (f + g) = Bf f + Bf g

theorem Zeta32.Arith.Small.Bf_C_mul (c : ℚ) (f : Polynomial ℚ) : Bf (Polynomial.C c * f) = c * Bf f

theorem Zeta32.Arith.Small.Bf_zero : Bf 0 = 0

theorem Zeta32.Arith.Small.Bf_sum {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial ℚ) : Bf (∑ i ∈ s, f i) = ∑ i ∈ s, Bf (f i)

theorem Zeta32.Arith.Small.Bf_monomial (e : ℕ) (a : ℚ) : Bf ((Polynomial.monomial e) a) = a * bernoulli' e

theorem Zeta32.Arith.Small.Bf_eq_sum_range (f : Polynomial ℚ) {d : ℕ} (hd : f.natDegree ≤ d) : Bf f = ∑ k ∈ Finset.range (d + 1), f.coeff k * bernoulli' k

theorem Zeta32.Arith.Small.Bf_X_add_one_pow (m : ℕ) : Bf ((Polynomial.X + 1) ^ m) = bernoulli' m + ↑m

theorem Zeta32.Arith.Small.Bf_shift (f : Polynomial ℚ) : Bf (f.comp (Polynomial.X + 1)) = Bf f + Polynomial.eval 1 (Polynomial.derivative f)

Shift rule B(f(t+1)) = B(f) + f'(1) (the proof notes, §0).

theorem Zeta32.Arith.Small.Bf_binomPoly (k : ℕ) : Bf (binomPoly k) = Polynomial.eval 1 (Polynomial.derivative (binomPoly (k + 1)))

theorem Zeta32.Arith.Small.Bf_binomPoly_VG (p : ℕ) [Fact (Nat.Prime p)] (k : ℕ) : Zeta5Irrational.VG p (Bf (binomPoly k)) (-↑(Nat.log p (k + 1)))

theorem Zeta32.Arith.Small.Bf_VG (p : ℕ) [Fact (Nat.Prime p)] {h : Polynomial ℚ} {d : ℕ} (hd : h.natDegree ≤ d) (β : ℚ) (hv : ∀ (z : ℤ), Zeta5Irrational.VG p (Polynomial.eval (↑z) h) β) : Zeta5Irrational.VG p (Bf h) (β - ↑(Nat.log p (d + 1)))

v_p(B(h)) ≥ β - ⌊log_p(d+1)⌋ if deg h ≤ d and v_p(h(z)) ≥ β on ℤ.

theorem Zeta32.Arith.Small.polynomialMoment_monomial (r : ℚ) (e : ℕ) (a : ℚ) : polynomialMoment r ((Polynomial.monomial e) a) = a * moment r e

theorem Zeta32.Arith.Small.polynomialMoment_add (r : ℚ) (f g : Polynomial ℚ) : polynomialMoment r (f + g) = polynomialMoment r f + polynomialMoment r g

theorem Zeta32.Arith.Small.polynomialMoment_C_mul (r c : ℚ) (f : Polynomial ℚ) : polynomialMoment r (Polynomial.C c * f) = c * polynomialMoment r f

theorem Zeta32.Arith.Small.polynomialMoment_eq_Bf (r : ℚ) (g : Polynomial ℚ) : polynomialMoment r g = Bf (Polynomial.derivative (Polynomial.X * g)) + 2 * r * Bf (Polynomial.X * g)

U_r on polynomials: polynomialMoment r g = B((t g)') + 2r B(t g) (the proof notes, §0).

theorem Zeta32.Arith.Small.VG_two_mul_rat (p : ℕ) [Fact (Nat.Prime p)] (r : ℚ) : Zeta5Irrational.VG p (2 * r) (-↑(padicValNat p r.den))

theorem Zeta32.Arith.Small.polynomialMoment_VG (p : ℕ) [Fact (Nat.Prime p)] (r : ℚ) {g : Polynomial ℚ} {d : ℕ} (hd : g.natDegree ≤ d) (β : ℚ) (hv : ∀ (z : ℤ), Zeta5Irrational.VG p (Polynomial.eval (↑z) g) β) : Zeta5Irrational.VG p (polynomialMoment r g) (β - 2 * ↑(Nat.log p (d + 2)) - ↑(padicValNat p r.den))

the proof notes, §7 (c): v_p(U_r(g)) ≥ β - 2⌊log_p(d+2)⌋ - v_p(den r) for deg g ≤ d and v_p(g(z)) ≥ β on ℤ.