Documentation

LeanPool.Zeta32.PrimeEdge.V0Table

S2b-4: the leading local values V⁰(u^e r_type) are the exact rationals of Blocks.lean (code/local_blocks_453.py). Each is a finite computation: polynomial division by (u+1)…(u+4) resp. (u+1)(u+2)(u+3), Lagrange residues, V⁰(u^e) = e B_{e-1} and V⁰((u+m)^{-1}) = 2 H_m^{(3)}.

Helpers (namespace V0Aux to avoid clashes with sibling files).

source
theorem Zeta32.PrimeEdge.V0Aux.locPoly_zero (s : ℚ) :
locPoly s 0 = 0
source
theorem Zeta32.PrimeEdge.V0Aux.locPoly_add (s : ℚ) (P Q : Polynomial ℚ) :
locPoly s (P + Q) = locPoly s P + locPoly s Q
source
theorem Zeta32.PrimeEdge.V0Aux.locPoly_C_mul_X_pow (s a : ℚ) (k : ℕ) :
locPoly s (Polynomial.C a * Polynomial.X ^ k) = a * locMoment s k
source
theorem Zeta32.PrimeEdge.V0Aux.locValue_eq_of_decomp (s : ℚ) (M : Finset ℕ) (S q R : Polynomial ℚ) (hR : R.natDegree < M.card) (hS : S = q * ∏ m ∈ M, (Polynomial.X + Polynomial.C ↑m) + R) :
locValue s S M = locPoly s q + ∑ m ∈ M, (Polynomial.eval (-↑m) S / ∏ m' ∈ M.erase m, (↑m' - ↑m)) * locPole s m

If S = q · T + R with T = ∏_{m ∈ M} (X + m) and deg R < |M|, then the polynomial part of locValue is locPoly q.

source
theorem Zeta32.PrimeEdge.V0Aux.H3_vals :
H 3 1 = 1 ∧ H 3 2 = 9 / 8 ∧ H 3 3 = 251 / 216 ∧ H 3 4 = 2035 / 1728
source
def Zeta32.PrimeEdge.V0Aux.tacticV0_decomp___ :
Lean.ParserDescr

Close locValue 0 S M = v from an explicit quotient q and remainder R with natDegree R ≤ d < |M|.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Zeta32.PrimeEdge.V0Aux.zero_1 :
    locValue 0 (Polynomial.X ^ 1) {1, 2, 3, 4} = 1 / 1296
    source
    theorem Zeta32.PrimeEdge.V0Aux.zero_2 :
    locValue 0 (Polynomial.X ^ 2) {1, 2, 3, 4} = 7 / 648
    source
    theorem Zeta32.PrimeEdge.V0Aux.zero_3 :
    locValue 0 (Polynomial.X ^ 3) {1, 2, 3, 4} = 1565 / 648
    source
    theorem Zeta32.PrimeEdge.V0Aux.zero_4 :
    locValue 0 (Polynomial.X ^ 4) {1, 2, 3, 4} = -15575 / 648
    source
    theorem Zeta32.PrimeEdge.V0Aux.zero_5 :
    locValue 0 (Polynomial.X ^ 5) {1, 2, 3, 4} = 101261 / 648
    source
    theorem Zeta32.PrimeEdge.V0Aux.zero_6 :
    locValue 0 (Polynomial.X ^ 6) {1, 2, 3, 4} = -545255 / 648
    source
    theorem Zeta32.PrimeEdge.V0Aux.zero_7 :
    locValue 0 (Polynomial.X ^ 7) {1, 2, 3, 4} = 2649929 / 648
    source
    theorem Zeta32.PrimeEdge.V0Aux.high_3 :
    locValue 0 (Polynomial.X ^ 3) {1, 2, 3} = -115 / 8
    source
    theorem Zeta32.PrimeEdge.V0Aux.high_4 :
    locValue 0 (Polynomial.X ^ 4) {1, 2, 3} = 481 / 8
    source
    theorem Zeta32.PrimeEdge.V0Aux.high_5 :
    locValue 0 (Polynomial.X ^ 5) {1, 2, 3} = -1731 / 8
    source
    theorem Zeta32.PrimeEdge.V0_zero_table (e : Fin 7) :
    locValue 0 (Polynomial.X ^ (↑e + 1)) {1, 2, 3, 4} = zeroMoment e

    V⁰(u^e r_0) = zeroMoment e, r_0 = u/((u+1)(u+2)(u+3)(u+4)).

    source
    theorem Zeta32.PrimeEdge.V0_low_table (e : Fin 5) :
    locValue 0 (Polynomial.X ^ (↑e + 3)) {1, 2, 3, 4} = lowMoment e

    V⁰(u^e r_L) = lowMoment e, r_L = u³/((u+1)(u+2)(u+3)(u+4)).

    source
    theorem Zeta32.PrimeEdge.V0_high_table (e : Fin 3) :
    locValue 0 (Polynomial.X ^ (↑e + 3)) {1, 2, 3} = highMoment e

    V⁰(u^e r_H) = highMoment e, r_H = u³/((u+1)(u+2)(u+3)).

    source
    theorem Zeta32.PrimeEdge.blockMoment_zero (p : ℕ) (e : Fin 7) :
    blockMoment p 0 ↑e = zeroMoment e
    source
    theorem Zeta32.PrimeEdge.blockMoment_low {p b : ℕ} (hb0 : b ≠ 0) (hb : b + 5 ≤ p) (e : Fin 5) :
    blockMoment p b ↑e = lowMoment e
    source
    theorem Zeta32.PrimeEdge.blockMoment_high {p b : ℕ} (hb0 : b ≠ 0) (hb : ¬b + 5 ≤ p) (e : Fin 3) :
    blockMoment p b ↑e = highMoment e