The entry functional and its local bound

For a numerator A, Lfun r n A = U_r(A / D_{5n}) (the proof notes, §0): U_r(t^e) = (e+1)B_e + 2rB_{e+1}, U_r((t+j)^{-1}) = 2jX + β_j, i.e.

Lfun r n A = (∑_j res_j · 2j) X + polynomialMoment r (A /ₘ D_{5n}) + ∑_j res_j β_j.

• Lfun_numerator : Lfun r n (numerator n m) = X · slope n m + intercept r n m;
• det_basis_change : a monic basis f_i of degree i does not change the Hankel determinant;
• Lfun_GV (the proof notes, Lemma 4, entrywise, by class-wise partial fractions instead of the Tate-algebra functional): if A has at least e_c zeros in every class c mod p (Adm), ℓ_c is the number of poles -j (1 ≤ j ≤ 5n) in class c, 5n < p², p ∤ den r and deg A ≤ 10n - 2, then every coefficient of Lfun r n A has v_p ≥ min_c (e_c + [c = 0] - ℓ_c) - 2.

The poles

def Zeta32.Arith.Local.Pl5 (n : ℕ) : Finset ℤ

The pole set {-1, …, -5n}.

Equations

• Zeta32.Arith.Local.Pl5 n = Finset.image (fun (j : ℕ) => -↑j) (Finset.Icc 1 (5 * n))

theorem Zeta32.Arith.Local.neg_natCast_injective : Function.Injective fun (j : ℕ) => -↑j

theorem Zeta32.Arith.Local.card_Pl5 (n : ℕ) : (Pl5 n).card = 5 * n

theorem Zeta32.Arith.Local.D_eq_piPl (m : ℕ) : D m = piPl (Finset.image (fun (j : ℕ) => -↑j) (Finset.Icc 1 m))

theorem Zeta32.Arith.Local.resP_Pl5 (A : Polynomial ℚ) (n j : ℕ) : resP A (Pl5 n) (-↑j) = Polynomial.eval (-↑j) A / ∏ l ∈ (Finset.Icc 1 (5 * n)).erase j, (↑l - ↑j)

The entry functional

noncomputable def Zeta32.Arith.Local.Lfun (r : ℚ) (n : ℕ) (A : Polynomial ℚ) : Polynomial ℚ

U_r(A / D_{5n}), as a polynomial in X.

Equations

• One or more equations did not get rendered due to their size.

theorem Zeta32.Arith.Local.Lfun_eq_Ufun (r : ℚ) (n : ℕ) (A : Polynomial ℚ) : Lfun r n A = Small.Ufun r n A

The local residue formula is the same numerator functional used by the small-prime Gram calculation.

theorem Zeta32.Arith.Local.Lfun_numerator (r : ℚ) (n m : ℕ) : Lfun r n (numerator n m) = Polynomial.X * Polynomial.C (slope n m) + Polynomial.C (intercept r n m)

theorem Zeta32.Arith.Local.Lfun_add (r : ℚ) (n : ℕ) (A B : Polynomial ℚ) : Lfun r n (A + B) = Lfun r n A + Lfun r n B

theorem Zeta32.Arith.Local.Lfun_C_mul (r : ℚ) (n : ℕ) (c : ℚ) (A : Polynomial ℚ) : Lfun r n (Polynomial.C c * A) = Polynomial.C c * Lfun r n A

Change of basis

@[reducible, inline]

noncomputable abbrev Zeta32.Arith.Local.coeffMat {h : ℕ} (E : Fin h → Polynomial ℚ) : Matrix (Fin h) (Fin h) ℚ

The coefficient matrix of a family of polynomials.

Equations

• Zeta32.Arith.Local.coeffMat E = Zeta5Irrational.coeffMat E

theorem Zeta32.Arith.Local.sum_coeffMat {h : ℕ} (E : Fin h → Polynomial ℚ) (hE : ∀ (a : Fin h), (E a).natDegree < h) (a : Fin h) : E a = ∑ k : Fin h, Polynomial.C (coeffMat E a k) * Polynomial.X ^ ↑k

theorem Zeta32.Arith.Local.det_coeffMat {h : ℕ} (E : Fin h → Polynomial ℚ) (hmon : ∀ (i : Fin h), (E i).Monic) (hdeg : ∀ (i : Fin h), (E i).natDegree = ↑i) : (coeffMat E).det = 1

theorem Zeta32.Arith.Local.det_basis_change {h : ℕ} (L : Polynomial ℚ → Polynomial ℚ) (hadd : ∀ (A B : Polynomial ℚ), L (A + B) = L A + L B) (hC : ∀ (c : ℚ) (A : Polynomial ℚ), L (Polynomial.C c * A) = Polynomial.C c * L A) (W : Polynomial ℚ) (f : Fin h → Polynomial ℚ) (hmon : ∀ (i : Fin h), (f i).Monic) (hdeg : ∀ (i : Fin h), (f i).natDegree = ↑i) : (Matrix.of fun (i k : Fin h) => L (f i * f k * W)).det = (Matrix.of fun (i k : Fin h) => L (Polynomial.X ^ (↑i + ↑k) * W)).det

Change of basis for a ℚ-linear functional on numerators.

theorem Zeta32.Arith.Local.hankel_eq_Lfun (r : ℚ) (n : ℕ) : Polynomial.X • (B n).map ⇑Polynomial.C + (A r n).map ⇑Polynomial.C = Matrix.of fun (i k : Fin (3 * n)) => Lfun r n (Polynomial.X ^ (↑i + ↑k) * D n ^ 4)

The Hankel matrix of Q is the matrix of Lfun on the monomial numerators.

theorem Zeta32.Arith.Local.Q_eq_det_basis (r : ℚ) (n : ℕ) (f : Fin (3 * n) → Polynomial ℚ) (hmon : ∀ (i : Fin (3 * n)), (f i).Monic) (hdeg : ∀ (i : Fin (3 * n)), (f i).natDegree = ↑i) : Q r n = (Matrix.of fun (i k : Fin (3 * n)) => Lfun r n (f i * f k * D n ^ 4)).det

Q in any monic basis f_i of degree i.

Valuations of the harmonic numbers and of β_j

theorem Zeta32.Arith.Local.VG_H {p : ℕ} [hp : Fact (Nat.Prime p)] {e j : ℕ} (hj : j < p ^ 2) : VG p (H e j) (-↑e)

theorem Zeta32.Arith.Local.VG_beta_weak {p : ℕ} [hp : Fact (Nat.Prime p)] {r : ℚ} (hr : VG p r 0) {j : ℕ} (hj : j < p ^ 2) : VG p (beta r j) (-3)

theorem Zeta32.Arith.Local.VG_beta_strong {p : ℕ} [hp : Fact (Nat.Prime p)] {r : ℚ} (hr : VG p r 0) {j : ℕ} (hj : j < p ^ 2) (hpj : p ∣ j) : VG p (beta r j) (-2)

The local bound

theorem Zeta32.Arith.Local.sep_Pl5 {p n : ℕ} (hn : 5 * n < p ^ 2) : Sep p (Pl5 n)

theorem Zeta32.Arith.Local.class_neg_eq_zero_iff {p : ℕ} [hp : Fact (Nat.Prime p)] (j : ℕ) : ↑(-↑j) = 0 ↔ p ∣ j

theorem Zeta32.Arith.Local.Lfun_GV {p : ℕ} [hp : Fact (Nat.Prime p)] {r : ℚ} (hr : VG p r 0) {n : ℕ} (hn : 5 * n < p ^ 2) {A : Polynomial ℚ} {e : ZMod p → ℤ} (hA : Adm p A e) (hdeg : A.natDegree + 2 ≤ 10 * n) (β : ℚ) (hβ : ∀ (c : ZMod p), β ≤ (↑(e c) + if c = 0 then 1 else 0) - ↑(plc p (Pl5 n) c).card) : GV p (Lfun r n A) (β - 2)

Local bound for one entry.