The generic rank-one (Vandermonde) lemma, in Newton form. For H = W + sum_c sum_{t<C c} gamma_{c,t} v(a_{c,t}) v(a_{c,t})^T, v(a)i = a^i, with W and all nodes p-integral, nodes in one class pairwise congruent mod p, v_p(gamma{c,t}) >= w_{c,t} and w_c nondecreasing in t: v_p(det H) >= sum_c sum_{k<C c} min(w_{c,k} + 2k, 0).

theorem Zeta32.Outer.det_mul_expand {R : Type u_1} [CommRing R] {h : ℕ} {I : Type u_2} [Fintype I] (W : Matrix (Fin h) I R) (Cm : Matrix I (Fin h) R) : (W * Cm).det = ∑ f : Fin h → I, (∏ b : Fin h, Cm (f b) b) * (Matrix.of fun (a b : Fin h) => W a (f b)).det

theorem Zeta32.Outer.det_cols_eq_zero {R : Type u_1} [CommRing R] {h : ℕ} {I : Type u_2} (W : Matrix (Fin h) I R) (f : Fin h → I) (hf : ¬Function.Injective f) : (Matrix.of fun (a b : Fin h) => W a (f b)).det = 0

Newton coefficients over a node sequence

def Zeta32.Outer.newtonTail (a : ℕ → ℚ) (f : Polynomial ℚ) : ℕ → Polynomial ℚ

Successive monic quotients along the Newton interpolation nodes.

Equations

• Zeta32.Outer.newtonTail a f 0 = f
• Zeta32.Outer.newtonTail a f k.succ = Zeta32.Outer.newtonTail a f k /ₘ (Polynomial.X - Polynomial.C (a k))

noncomputable def Zeta32.Outer.ncoef (a : ℕ → ℚ) (f : Polynomial ℚ) (k : ℕ) : ℚ

Newton interpolation coefficient at the kth node.

Equations

• Zeta32.Outer.ncoef a f k = Polynomial.eval (a k) (Zeta32.Outer.newtonTail a f k)

noncomputable def Zeta32.Outer.Nb (a : ℕ → ℚ) (k : ℕ) : Polynomial ℚ

The kth Newton basis polynomial associated to the node sequence.

Equations

• Zeta32.Outer.Nb a k = ∏ s ∈ Finset.range k, (Polynomial.X - Polynomial.C (a s))

theorem Zeta32.Outer.newton_nodes (a : ℕ → ℚ) (f : Polynomial ℚ) (K : ℕ) : f = ∑ k ∈ Finset.range K, Polynomial.C (ncoef a f k) * Nb a k + Nb a K * newtonTail a f K

theorem Zeta32.Outer.Nb_eval_eq_zero (a : ℕ → ℚ) {k t : ℕ} (htk : t < k) : Polynomial.eval (a t) (Nb a k) = 0

theorem Zeta32.Outer.pow_eval_newton (a : ℕ → ℚ) (i : ℕ) {K t : ℕ} (ht : t < K) : a t ^ i = ∑ k ∈ Finset.range K, ncoef a (Polynomial.X ^ i) k * Polynomial.eval (a t) (Nb a k)

theorem Zeta32.Outer.newtonTail_GV (p : ℕ) [Fact (Nat.Prime p)] (a : ℕ → ℚ) (ha : ∀ (k : ℕ), Zeta5Irrational.VG p (a k) 0) {f : Polynomial ℚ} (hf : Zeta5Irrational.GV p f 0) (k : ℕ) : Zeta5Irrational.GV p (newtonTail a f k) 0

theorem Zeta32.Outer.ncoef_VG (p : ℕ) [Fact (Nat.Prime p)] (a : ℕ → ℚ) (ha : ∀ (k : ℕ), Zeta5Irrational.VG p (a k) 0) {f : Polynomial ℚ} (hf : Zeta5Irrational.GV p f 0) (k : ℕ) : Zeta5Irrational.VG p (ncoef a f k) 0

theorem Zeta32.Outer.X_pow_GV (p : ℕ) [Fact (Nat.Prime p)] (i : ℕ) : Zeta5Irrational.GV p (Polynomial.X ^ i) 0

theorem Zeta32.Outer.Nb_eval_VG (p : ℕ) [Fact (Nat.Prime p)] (a : ℕ → ℚ) {k t : ℕ} (hd : ∀ s < k, Zeta5Irrational.VG p (a t - a s) 1) : Zeta5Irrational.VG p (Polynomial.eval (a t) (Nb a k)) ↑k

The double expansion bound

theorem Zeta32.Outer.det_mul_GV2 (p : ℕ) [Fact (Nat.Prime p)] {h : ℕ} {I : Type u_1} [Fintype I] (W : Matrix (Fin h) I (Polynomial ℚ)) (Cm : Matrix I (Fin h) (Polynomial ℚ)) (ρ : I → ℚ) (τ : Fin h → ℚ) (hW : ∀ (a : Fin h) (i : I), Zeta5Irrational.GV p (W a i) 0) (hC : ∀ (i : I) (b : Fin h), Zeta5Irrational.GV p (Cm i b) (ρ i + τ b)) (Bd : ℚ) (hB : ∀ (f : Fin h → I), Function.Injective f → Bd ≤ ∑ b : Fin h, ρ (f b)) : Zeta5Irrational.GV p (W * Cm).det (Bd + ∑ b : Fin h, τ b)

theorem Zeta32.Outer.sum_min_le_of_injective {h : ℕ} {I : Type u_1} [Fintype I] (ρ : I → ℚ) (g : Fin h → I) (hg : Function.Injective g) : ∑ i : I, min (ρ i) 0 ≤ ∑ b : Fin h, ρ (g b)

theorem Zeta32.Outer.det_sandwich_GV (p : ℕ) [Fact (Nat.Prime p)] {h : ℕ} {I : Type u_1} [Fintype I] (A : Matrix (Fin h) I (Polynomial ℚ)) (M : Matrix I I (Polynomial ℚ)) (B : Matrix I (Fin h) (Polynomial ℚ)) (ρ : I → ℚ) (hA : ∀ (a : Fin h) (i : I), Zeta5Irrational.GV p (A a i) 0) (hB : ∀ (i : I) (b : Fin h), Zeta5Irrational.GV p (B i b) 0) (hM : ∀ (i j : I), Zeta5Irrational.GV p (M i j) (ρ i + ρ j)) : Zeta5Irrational.GV p (A * M * B).det (2 * ∑ i : I, min (ρ i) 0)

The class-wise rank-one lemma

@[reducible, inline]

abbrev Zeta32.Outer.RSlot {κ : Type u_1} (h : ℕ) (Cc : κ → ℕ) : Type u_1

Indices for the original matrix block and the residue-class interpolation blocks.

Equations

• Zeta32.Outer.RSlot h Cc = (Fin h ⊕ (c : κ) × Fin (Cc c))

noncomputable def Zeta32.Outer.Gc {κ : Type u_1} (Cc : κ → ℕ) (node : κ → ℕ → ℚ) (γ : κ → ℕ → Polynomial ℚ) (c : κ) (k l : ℕ) : Polynomial ℚ

The weighted Newton-basis Gram polynomial for a residue class.

Equations

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

noncomputable def Zeta32.Outer.rankA {h : ℕ} {κ : Type u_1} (Cc : κ → ℕ) (node : κ → ℕ → ℚ) (W : Matrix (Fin h) (Fin h) (Polynomial ℚ)) : Matrix (Fin h) (RSlot h Cc) (Polynomial ℚ)

Left factor in the residue-class block decomposition of the Hankel matrix.

Equations

• Zeta32.Outer.rankA Cc node W a (Sum.inl i_2) = W a i_2
• Zeta32.Outer.rankA Cc node W a (Sum.inr ⟨c, k⟩) = Polynomial.C (Zeta32.Outer.ncoef (node c) (Polynomial.X ^ ↑a) ↑k)

noncomputable def Zeta32.Outer.rankM {h : ℕ} {κ : Type u_1} [DecidableEq κ] (Cc : κ → ℕ) (node : κ → ℕ → ℚ) (γ : κ → ℕ → Polynomial ℚ) : Matrix (RSlot h Cc) (RSlot h Cc) (Polynomial ℚ)

Middle block matrix in the residue-class Hankel decomposition.

Equations

• Zeta32.Outer.rankM Cc node γ (Sum.inl i_2) (Sum.inl j_2) = if i_2 = j_2 then 1 else 0
• Zeta32.Outer.rankM Cc node γ (Sum.inr ⟨c, k⟩) (Sum.inr ⟨c', l⟩) = if c = c' then Zeta32.Outer.Gc Cc node γ c ↑k ↑l else 0
• Zeta32.Outer.rankM Cc node γ i j = 0

noncomputable def Zeta32.Outer.rankB {h : ℕ} {κ : Type u_1} (Cc : κ → ℕ) (node : κ → ℕ → ℚ) : Matrix (RSlot h Cc) (Fin h) (Polynomial ℚ)

Right factor in the residue-class block decomposition of the Hankel matrix.

Equations

• Zeta32.Outer.rankB Cc node (Sum.inl i_2) b = if i_2 = b then 1 else 0
• Zeta32.Outer.rankB Cc node (Sum.inr ⟨c, k⟩) b = Polynomial.C (Zeta32.Outer.ncoef (node c) (Polynomial.X ^ ↑b) ↑k)

theorem Zeta32.Outer.class_block {κ : Type u_1} (Cc : κ → ℕ) (node : κ → ℕ → ℚ) (γ : κ → ℕ → Polynomial ℚ) (c : κ) (a b : ℕ) : ∑ k : Fin (Cc c), ∑ l : Fin (Cc c), Polynomial.C (ncoef (node c) (Polynomial.X ^ a) ↑k) * Gc Cc node γ c ↑k ↑l * Polynomial.C (ncoef (node c) (Polynomial.X ^ b) ↑l) = ∑ t ∈ Finset.range (Cc c), γ c t * Polynomial.C (node c t ^ a * node c t ^ b)

theorem Zeta32.Outer.rank_decomp {h : ℕ} {κ : Type u_1} [Fintype κ] [DecidableEq κ] (Cc : κ → ℕ) (node : κ → ℕ → ℚ) (γ : κ → ℕ → Polynomial ℚ) (W : Matrix (Fin h) (Fin h) (Polynomial ℚ)) (a b : Fin h) : (rankA Cc node W * rankM Cc node γ * rankB Cc node) a b = W a b + ∑ c : κ, ∑ t ∈ Finset.range (Cc c), γ c t * Polynomial.C (node c t ^ ↑a * node c t ^ ↑b)

def Zeta32.Outer.rankρ {h : ℕ} {κ : Type u_1} (Cc : κ → ℕ) (w : κ → ℕ → ℚ) : RSlot h Cc → ℚ

Valuation weight on each original or interpolation matrix slot.

Equations

• Zeta32.Outer.rankρ Cc w (Sum.inl i_1) = 0
• Zeta32.Outer.rankρ Cc w (Sum.inr ⟨c, k⟩) = w c ↑k / 2 + ↑↑k

theorem Zeta32.Outer.rank_one_GV {h : ℕ} {κ : Type u_1} [Fintype κ] (Cc : κ → ℕ) (node : κ → ℕ → ℚ) (γ : κ → ℕ → Polynomial ℚ) (p : ℕ) [Fact (Nat.Prime p)] (w : κ → ℕ → ℚ) (W : Matrix (Fin h) (Fin h) (Polynomial ℚ)) (hW : ∀ (a b : Fin h), Zeta5Irrational.GV p (W a b) 0) (hnode : ∀ (c : κ) (t : ℕ), Zeta5Irrational.VG p (node c t) 0) (hsep : ∀ (c : κ) (s t : ℕ), s < Cc c → t < Cc c → s ≠ t → Zeta5Irrational.VG p (node c t - node c s) 1) (hγ : ∀ (c : κ), ∀ t < Cc c, Zeta5Irrational.GV p (γ c t) (w c t)) (hmono : ∀ (c : κ) (s t : ℕ), s ≤ t → t < Cc c → w c s ≤ w c t) : Zeta5Irrational.GV p (Matrix.of fun (a b : Fin h) => W a b + ∑ c : κ, ∑ t ∈ Finset.range (Cc c), γ c t * Polynomial.C (node c t ^ ↑a * node c t ^ ↑b)).det (∑ c : κ, ∑ k ∈ Finset.range (Cc c), min (w c k + 2 * ↑k) 0)

theorem Zeta32.Outer.rank_one_GV_rows {h : ℕ} {κ : Type u_1} [Fintype κ] (Cc : κ → ℕ) (node : κ → ℕ → ℚ) (γ : κ → ℕ → Polynomial ℚ) (p : ℕ) [Fact (Nat.Prime p)] (w : κ → ℕ → ℚ) (d : Fin h → ℚ) (hd : ∀ (a : Fin h), Zeta5Irrational.VG p (d a) 0) (W : Matrix (Fin h) (Fin h) (Polynomial ℚ)) (hW : ∀ (a b : Fin h), Zeta5Irrational.GV p (Polynomial.C (d a) * W a b) 0) (hnode : ∀ (c : κ) (t : ℕ), Zeta5Irrational.VG p (node c t) 0) (hsep : ∀ (c : κ) (s t : ℕ), s < Cc c → t < Cc c → s ≠ t → Zeta5Irrational.VG p (node c t - node c s) 1) (hγ : ∀ (c : κ), ∀ t < Cc c, Zeta5Irrational.GV p (γ c t) (w c t)) (hmono : ∀ (c : κ) (s t : ℕ), s ≤ t → t < Cc c → w c s ≤ w c t) : Zeta5Irrational.GV p (Matrix.of fun (a b : Fin h) => Polynomial.C (d a) * (W a b + ∑ c : κ, ∑ t ∈ Finset.range (Cc c), γ c t * Polynomial.C (node c t ^ ↑a * node c t ^ ↑b))).det (∑ c : κ, ∑ k ∈ Finset.range (Cc c), min (w c k + 2 * ↑k) 0)

Rank-one bound after scaling row a by a p-integral scalar d a; only the scaled W has to be integral.