Documentation

LeanPool.Zeta32.Arith.Small.Entry

the proof notes, §7, Lemma 7, one entry. With K = 5n, N = 4n + a + b and p_ab = binom(t+n,n)^4 binom(t,a) binom(t,b) (integer-valued), S_n D_n^4 E_a E_b = K!·p_ab; (b) the polynomial part is Σ_{K≤k≤N} c_k/binom(k,K)·binom(t,k-K) with integer Newton coefficients c_k, so its integer values have v_p ≥ -⌊log_p N⌋; (a) the residues are integers and v_p(β_j) ≥ -3⌊log_p j⌋ - v_p(den r); (c) polynomialMoment_VG. Every entry of binomGram r n has Gauss valuation ≥ -3⌊log_p(10n+2)⌋ - v_p(den r).

source
noncomputable def Zeta32.Arith.Small.pab (n a b : ℕ) :
Polynomial ℚ

binom(t+n,n)^4 binom(t,a) binom(t,b).

Equations
Instances For
    source
    noncomputable def Zeta32.Arith.Small.gramNum (n a b : ℕ) :
    Polynomial ℚ

    The literal binomial Gram numerator.

    Equations
    Instances For
      source
      theorem Zeta32.Arith.Small.gramNum_eq (n a b : ℕ) :
      gramNum n a b = Polynomial.C ↑(5 * n).factorial * pab n a b
      source
      theorem Zeta32.Arith.Small.pab_eval_int (p : ℕ) [Fact (Nat.Prime p)] (n a b : ℕ) (m : ℤ) :
      Zeta5Irrational.VG p (Polynomial.eval (↑m) (pab n a b)) 0
      source
      theorem Zeta32.Arith.Small.pab_natDegree_le (n a b : ℕ) :
      (pab n a b).natDegree ≤ 4 * n + a + b
      source
      noncomputable def Zeta32.Arith.Small.quotCoeff (n a b k : ℕ) :
      ℚ

      Newton coefficients of p_ab at -K.

      Equations
      Instances For
        source
        theorem Zeta32.Arith.Small.gramNum_divByMonic (n a b : ℕ) :
        gramNum n a b /ₘ D (5 * n) = ∑ k ∈ Finset.Ico (5 * n) (4 * n + a + b + 1), Polynomial.C (quotCoeff n a b k * (↑(k.choose (5 * n)))⁻¹) * binomPoly (k - 5 * n)

        The literal polynomial part of the binomial Gram entry.

        source
        theorem Zeta32.Arith.Small.quotCoeff_VG (p : ℕ) [Fact (Nat.Prime p)] (n a b k : ℕ) :
        Zeta5Irrational.VG p (quotCoeff n a b k) 0
        source
        theorem Zeta32.Arith.Small.gramQuot_eval_VG (p : ℕ) [Fact (Nat.Prime p)] (n a b : ℕ) (m : ℤ) :
        Zeta5Irrational.VG p (Polynomial.eval (↑m) (gramNum n a b /ₘ D (5 * n))) (-↑(Nat.log p (4 * n + a + b)))

        Every integer value of the quotient has v_p >= -log_p N.

        source
        theorem Zeta32.Arith.Small.gramQuot_natDegree_le (n a b : ℕ) :
        (gramNum n a b /ₘ D (5 * n)).natDegree ≤ 4 * n + a + b - 5 * n
        source
        theorem Zeta32.Arith.Small.gramRes_VG (p : ℕ) [Fact (Nat.Prime p)] (n a b : ℕ) {j : ℕ} (hj : 1 ≤ j) (hjK : j ≤ 5 * n) :
        Zeta5Irrational.VG p (Polynomial.eval (-↑j) (gramNum n a b) / ∏ l ∈ (Finset.Icc 1 (5 * n)).erase j, (↑l - ↑j)) 0

        The pole values β_j #

        source
        theorem Zeta32.Arith.Small.H_VG (p : ℕ) [Fact (Nat.Prime p)] (e j : ℕ) :
        Zeta5Irrational.VG p (H e j) (-↑e * ↑(Nat.log p j))
        source
        theorem Zeta32.Arith.Small.beta_VG (p : ℕ) [Fact (Nat.Prime p)] (r : ℚ) (j : ℕ) :
        Zeta5Irrational.VG p (beta r j) (-3 * ↑(Nat.log p j) - ↑(padicValNat p r.den))

        The entry bound #

        source
        theorem Zeta32.Arith.Small.binomGram_GV (p : ℕ) [Fact (Nat.Prime p)] (r : ℚ) (n : ℕ) (a b : Fin (3 * n)) :
        Zeta5Irrational.GV p (binomGram r n a b) (-3 * ↑(Nat.log p (10 * n + 2)) - ↑(padicValNat p r.den))

        the proof notes, §7: every entry of the binomial Gram matrix has Gauss valuation ≥ -3⌊log_p(10n+2)⌋ - v_p(den r).