The multiplication theorem for Lbp (the proof notes, §1 (i)): ∑_{b<p} Lbp (Q(p X - b)) = p · Lbp Q, proved by shift invariance and the binomial basis (a shift-invariant linear functional on ℚ[X] vanishes). Consequence for locPoly: ∑_{b<p} locPoly (r p) (Q(p X - b)) = p² · locPoly r Q.

theorem Zeta32.PrimeEdge.Lbp_C_mul (c : ℚ) (Q : Polynomial ℚ) : Arith.Local.Lbp (Polynomial.C c * Q) = c * Arith.Local.Lbp Q

theorem Zeta32.PrimeEdge.Lbp_shift (Q : Polynomial ℚ) : Arith.Local.Lbp (Q.comp (Polynomial.X + 1)) - Arith.Local.Lbp Q = Polynomial.eval 1 (Polynomial.derivative Q)

Shift rule for Lbp: Lbp (Q(X+1)) - Lbp Q = Q'(1).

noncomputable def Zeta32.PrimeEdge.Psi (p : ℕ) (Q : Polynomial ℚ) : ℚ

Ψ_p(Q) = ∑_{b<p} Lbp (Q(p X - b)).

Equations

• Zeta32.PrimeEdge.Psi p Q = ∑ b ∈ Finset.range p, Zeta32.Arith.Local.Lbp (Q.comp (Polynomial.C ↑p * Polynomial.X - Polynomial.C ↑b))

theorem Zeta32.PrimeEdge.Psi_add (p : ℕ) (P Q : Polynomial ℚ) : Psi p (P + Q) = Psi p P + Psi p Q

theorem Zeta32.PrimeEdge.Psi_C_mul (p : ℕ) (c : ℚ) (Q : Polynomial ℚ) : Psi p (Polynomial.C c * Q) = c * Psi p Q

theorem Zeta32.PrimeEdge.Psi_shift {p : ℕ} (hp : 0 < p) (Q : Polynomial ℚ) : Psi p (Q.comp (Polynomial.X + 1)) - Psi p Q = ↑p * Polynomial.eval 1 (Polynomial.derivative Q)

theorem Zeta32.PrimeEdge.shift_invariant_eq_zero (Φ : Polynomial ℚ → ℚ) (hadd : ∀ (P Q : Polynomial ℚ), Φ (P + Q) = Φ P + Φ Q) (hsmul : ∀ (c : ℚ) (Q : Polynomial ℚ), Φ (Polynomial.C c * Q) = c * Φ Q) (hshift : ∀ (Q : Polynomial ℚ), Φ (Q.comp (Polynomial.X + 1)) = Φ Q) (Q : Polynomial ℚ) : Φ Q = 0

A shift-invariant linear functional on ℚ[X] vanishes.

theorem Zeta32.PrimeEdge.Psi_eq {p : ℕ} (hp : 0 < p) (Q : Polynomial ℚ) : Psi p Q = ↑p * Arith.Local.Lbp Q

Multiplication theorem: ∑_{b<p} Lbp (Q(p X - b)) = p · Lbp Q.

theorem Zeta32.PrimeEdge.sum_locPoly_comp {p : ℕ} (hp : 0 < p) (r : ℚ) (Q : Polynomial ℚ) : ∑ b ∈ Finset.range p, locPoly (r * ↑p) (Q.comp (Polynomial.C ↑p * Polynomial.X - Polynomial.C ↑b)) = ↑p ^ 2 * locPoly r Q

∑_{b<p} locPoly (r p) (Q(p X - b)) = p² · locPoly r Q.