Outer range: the entry theorem

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

The μ-part below 2p - 3 of an integral polynomial is integral.

theorem Zeta5Irrational.μX_sub_μGe {p : ℕ} (K : ℕ) (P : Polynomial ℚ) : μX K P - Polynomial.C (μGe p (P /ₘ D K)) = Polynomial.C (μpoly (P /ₘ D K) - μGe p (P /ₘ D K)) + ∑ j ∈ Finset.Icc 1 K, Polynomial.C (res K P j) * poleValue j

μ_X minus its high part, expanded.

theorem Zeta5Irrational.entryO_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (cs : Fin (m + 1)) (is : ℕ) (ct : Fin (m + 1)) (it : ℕ) : D (3 * n) ^ 6 * Polynomial.map (Int.castRingHom ℚ) (tpolZ (rootsO hm n cs is)) * Polynomial.map (Int.castRingHom ℚ) (tpolZ (rootsO hm n ct it)) = tpol (entryO hm n cs is ct it)

theorem Zeta5Irrational.GV_entry_quot {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (cs : Fin (m + 1)) (is : ℕ) (ct : Fin (m + 1)) (it : ℕ) : GV p (tpol (entryO hm n cs is ct it) /ₘ D (40 * n)) 0

The integral numerator quotient.

theorem Zeta5Irrational.res_entry_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {cs ct : Fin (m + 1)} {is it j : ℕ} (hj : j ∈ Finset.Icc 1 (40 * n)) (h : j ≤ 3 * n ∨ jc hm j ≠ cs ∨ jc hm j ≠ ct) : res (40 * n) (tpol (entryO hm n cs is ct it)) j = 0

Residues vanish at poles j ≤ N and at tail poles outside the common class.

theorem Zeta5Irrational.pole_sum_reduce {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) (is it : ℕ) : ∑ j ∈ Finset.Icc 1 (40 * n), Polynomial.C (res (40 * n) (tpol (entryO hm n c is c it)) j) * poleValue j = ∑ j ∈ tailC hm n c, Polynomial.C (res (40 * n) (tpol (entryO hm n c is c it)) j) * poleValue j

The pole sum reduces to the tail poles of the common class.

theorem Zeta5Irrational.pole_sum_cross {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {cs ct : Fin (m + 1)} (hc : cs ≠ ct) (is it : ℕ) : ∑ j ∈ Finset.Icc 1 (40 * n), Polynomial.C (res (40 * n) (tpol (entryO hm n cs is ct it)) j) * poleValue j = 0

def Zeta5Irrational.ellC {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) : ℕ

ℓ(c) = #{j ≤ K : j ≡ ±c}.

Equations

• Zeta5Irrational.ellC hm n c = {j ∈ Finset.Icc 1 (40 * n) | Zeta5Irrational.jc hm j = c}.card

def Zeta5Irrational.delC {m : ℕ} (n : ℕ) (c : Fin (m + 1)) : ℕ

δ(c) = [c ≤ N].

Equations

• Zeta5Irrational.delC n c = if ↑c ≤ 3 * n then 1 else 0

noncomputable def Zeta5Irrational.wO {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) (i : ℕ) : ℚ

The outer weights (4.12).

Equations

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

theorem Zeta5Irrational.wO_nonpos {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) (i : ℕ) : wO hm n c i ≤ 0

theorem Zeta5Irrational.jc_eq_zero_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (j : ℕ) : jc hm j = 0 ↔ ↑p ∣ ↑j

theorem Zeta5Irrational.den_count {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {c : Fin (m + 1)} {j : ℕ} (hj : j ∈ Finset.Icc 1 (40 * n)) (hjc : jc hm j = c) : {i ∈ (Finset.Icc 1 (40 * n)).erase j | ↑↑i ^ 2 = ↑↑j ^ 2}.card = ellC hm n c - 1

Denominator count for a nonzero class.

theorem Zeta5Irrational.num_count {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {c : Fin (m + 1)} (hc0 : c ≠ 0) {is it j : ℕ} (hjc : jc hm j = c) : 6 * delC n c + is + it ≤ (Multiset.filter (fun (γ : ℤ) => ↑γ ^ 2 = ↑↑j ^ 2) (entryO hm n c is c it)).card

Numerator count for a nonzero class.

theorem Zeta5Irrational.ellC_pos {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {c : Fin (m + 1)} {j : ℕ} (hj : j ∈ Finset.Icc 1 (40 * n)) (hjc : jc hm j = c) : 1 ≤ ellC hm n c

theorem Zeta5Irrational.mem_Icc_of_tailC {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {c : Fin (m + 1)} {j : ℕ} (hj : j ∈ tailC hm n c) : j ∈ Finset.Icc 1 (40 * n)

theorem Zeta5Irrational.VG_res_entry {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (hp3 : 3 ≤ p) (hK : 2 * (40 * n) < p ^ 2) {c : Fin (m + 1)} (hc0 : c ≠ 0) {is it j : ℕ} (hj : j ∈ tailC hm n c) : VG p (res (40 * n) (tpol (entryO hm n c is c it)) j) (↑(6 * delC n c + is + it) - (↑(ellC hm n c) - 1))

Residue bound on a nonzero class.

theorem Zeta5Irrational.pole_case_a {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (hp3 : 3 ≤ p) (hK : 2 * (40 * n) < p ^ 2) {c : Fin (m + 1)} (hc0 : c ≠ 0) {is it : ℕ} (his : is < nbC hm n c) (hit : it < nbC hm n c) : GV p (∑ j ∈ tailC hm n c, Polynomial.C (res (40 * n) (tpol (entryO hm n c is c it)) j) * poleValue j) (wO hm n c is + wO hm n c it)

Case (a): both rows below nb.

theorem Zeta5Irrational.count_rootsO_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n i : ℕ) : i ≤ (Multiset.filter (fun (γ : ℤ) => ↑p ∣ γ) (rootsO hm n 0 i)).card

theorem Zeta5Irrational.mult_count {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (hpN : 3 * n < p) : {i ∈ Finset.Icc 1 (40 * n) | ↑p ∣ ↑i}.card ≤ nbC hm n 0 + 1

Multiples of p up to K are p and the big zero-class poles.

theorem Zeta5Irrational.nbC_zero_le {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (hK3 : 40 * n < 3 * p) : nbC hm n 0 ≤ 1

theorem Zeta5Irrational.pole_case_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (hp7 : 7 ≤ p) (hK3 : 40 * n < 3 * p) (hK : 2 * (40 * n) < p ^ 2) (hpN : 3 * n < p) (is it : ℕ) : GV p (∑ j ∈ tailC hm n 0, Polynomial.C (res (40 * n) (tpol (entryO hm n 0 is 0 it)) j) * poleValue j) (wO hm n 0 is + wO hm n 0 it)

Zero class.

theorem Zeta5Irrational.jc_small {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) {i : ℕ} (hi : i < p) : ↑(jc hm i) = i ∧ i ≤ m ∨ ↑(jc hm i) = p - i ∧ m < i

theorem Zeta5Irrational.jc_small_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) {c : Fin (m + 1)} {i : ℕ} (hi : i < p) (h : jc hm i = c) : i = ↑c ∨ i = p - ↑c

theorem Zeta5Irrational.ellC_le {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (hpN : 3 * n < p) {c : Fin (m + 1)} (hc0 : c ≠ 0) : ellC hm n c ≤ nbC hm n c + {i ∈ Finset.Icc 1 (40 * n) | jc hm i = c ∧ i < p}.card

Class members up to K: the big ones plus at most the two small ones.

theorem Zeta5Irrational.small_sub {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {c : Fin (m + 1)} : {i ∈ Finset.Icc 1 (40 * n) | jc hm i = c ∧ i < p} ⊆ {↑c, p - ↑c}

theorem Zeta5Irrational.small_card_le {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) {c : Fin (m + 1)} : {i ∈ Finset.Icc 1 (40 * n) | jc hm i = c ∧ i < p}.card ≤ 2

theorem Zeta5Irrational.pole_case_b {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (hp3 : 3 ≤ p) (hK : 2 * (40 * n) < p ^ 2) (hpN : 3 * n < p) {c : Fin (m + 1)} (hc0 : c ≠ 0) {is it : ℕ} (his : nbC hm n c ≤ is) : GV p (∑ j ∈ tailC hm n c, Polynomial.C (res (40 * n) (tpol (entryO hm n c is c it)) j) * poleValue j) 0

Case (b): one row at or above nb; the pole sum is integral.

theorem Zeta5Irrational.entryO_comm {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) (is it : ℕ) : entryO hm n c is c it = entryO hm n c it c is

theorem Zeta5Irrational.outer_entry {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (hp7 : 7 ≤ p) (hK3 : 40 * n < 3 * p) (hK : 2 * (40 * n) < p ^ 2) (hpN : 3 * n < p) (cs : Fin (m + 1)) (is : ℕ) (ct : Fin (m + 1)) (it : ℕ) : GV p (μX (40 * n) (tpol (entryO hm n cs is ct it)) - Polynomial.C (μGe p (tpol (entryO hm n cs is ct it) /ₘ D (40 * n)))) (wO hm n cs is + wO hm n ct it)

The outer entry theorem.

theorem Zeta5Irrational.outer_bound {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (hp7 : 7 ≤ p) (hK3 : 40 * n < 3 * p) (hK : 2 * (40 * n) < p ^ 2) (hpN : 3 * n < p) : GV p (Δ n) (2 * ∑ c : Fin (m + 1), ∑ i ∈ Finset.range (LoC hm n c), wO hm n c i - ↑(37 * n - (2 * p + 22 * n - 3 - (37 * n - 1))))

The outer-range bound v^G(Δ) ≥ 2 ∑ w − r.