The outer-range framework

μ = μ_{<} + μ_{≥} where μ_{≥} collects the moments μ(t^e) with e ≥ 2p - 3 (which may have v_p = -1). In any basis the μ_{≥}-part of the Hankel matrix has rank ≤ r and is p⁻¹ times an integral product U V; with weights w ≤ 0 for the integral part this gives v_p^G(Δ) ≥ 2 ∑ w - r.

noncomputable def Zeta5Irrational.μGe (p : ℕ) (Q : Polynomial ℚ) : ℚ

The moments e ≥ 2p - 3 of a polynomial.

Equations

• Zeta5Irrational.μGe p Q = ∑ e ∈ Finset.range (Q.natDegree + 1), if 2 * p ≤ e + 3 then Q.coeff e * Zeta5Irrational.μmono e else 0

theorem Zeta5Irrational.μGe_eq (p : ℕ) (Q : Polynomial ℚ) {N : ℕ} (hN : Q.natDegree < N) : μGe p Q = ∑ e ∈ Finset.range N, if 2 * p ≤ e + 3 then Q.coeff e * μmono e else 0

theorem Zeta5Irrational.μGe_add {p : ℕ} (P Q : Polynomial ℚ) : μGe p (P + Q) = μGe p P + μGe p Q

theorem Zeta5Irrational.μGe_C_mul {p : ℕ} (c : ℚ) (Q : Polynomial ℚ) : μGe p (Polynomial.C c * Q) = c * μGe p Q

theorem Zeta5Irrational.μGe_eq_zero {p : ℕ} {Q : Polynomial ℚ} (hQ : Q.natDegree + 3 < 2 * p) : μGe p Q = 0

theorem Zeta5Irrational.VG_p_μGe {p : ℕ} [hp : Fact (Nat.Prime p)] (hp5 : 5 ≤ p) {Q : Polynomial ℚ} (hQ : GV p Q 0) : VG p (↑p * μGe p Q) 0

theorem Zeta5Irrational.GV_divByMonic_D {p : ℕ} (K : ℕ) (Pz : Polynomial ℤ) : GV p (Polynomial.map (Int.castRingHom ℚ) Pz /ₘ D K) 0

The quotient of an integer polynomial by D_K has integral coefficients.

theorem Zeta5Irrational.μGe_sum {p : ℕ} {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial ℚ) : μGe p (∑ i ∈ s, f i) = ∑ i ∈ s, μGe p (f i)

theorem Zeta5Irrational.divByMonic_sum' {q : Polynomial ℚ} (hq : q.Monic) {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial ℚ) : (∑ i ∈ s, f i) /ₘ q = ∑ i ∈ s, f i /ₘ q

theorem Zeta5Irrational.D_pow_mul_X_pow_int (N e : ℕ) : ∃ (Pz : Polynomial ℤ), Polynomial.map (Int.castRingHom ℚ) Pz = D N ^ 6 * Polynomial.X ^ e

theorem Zeta5Irrational.outer_frame {p : ℕ} [hp : Fact (Nat.Prime p)] (hp5 : 5 ≤ p) (n : ℕ) (Ez : Fin (37 * n) → Polynomial ℤ) (hdegZ : ∀ (s : Fin (37 * n)), (Ez s).natDegree < 37 * n) {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ : ι → ZMod p) (hγ : Function.Injective γ) (Lc : ι → ℕ) (cls : Fin (37 * n) → ι) (idx : Fin (37 * n) → ℕ) (hidx : ∀ (a : Fin (37 * n)), idx a < Lc (cls a)) (hinj : ∀ (a b : Fin (37 * n)), cls a = cls b → idx a = idx b → a = b) (hred : ∀ (a : Fin (37 * n)), Polynomial.map (Int.castRingHom (ZMod p)) (Ez a) = (∏ c ∈ Finset.univ.erase (cls a), (Polynomial.X - Polynomial.C (γ c)) ^ Lc c) * (Polynomial.X - Polynomial.C (γ (cls a))) ^ idx a) (w : Fin (37 * n) → ℚ) (hw : ∀ (s : Fin (37 * n)), w s ≤ 0) (hA : ∀ (s t : Fin (37 * n)), GV p (μX (40 * n) (D (3 * n) ^ 6 * Polynomial.map (Int.castRingHom ℚ) (Ez s) * Polynomial.map (Int.castRingHom ℚ) (Ez t)) - Polynomial.C (μGe p (D (3 * n) ^ 6 * Polynomial.map (Int.castRingHom ℚ) (Ez s) * Polynomial.map (Int.castRingHom ℚ) (Ez t) /ₘ D (40 * n)))) (w s + w t)) : GV p (Δ n) (2 * ∑ s : Fin (37 * n), w s - ↑(37 * n - (2 * p + 22 * n - 3 - (37 * n - 1))))

The outer-range framework.