The outer range: class counts

For a nonzero class c, the number of class members in (X, Y] is SX p Y c - SX p X c.

theorem Zeta5Irrational.jc_eq_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (j : ℕ) (c : Fin (m + 1)) : jc hm j = c ↔ ↑↑j = ↑↑↑c ∨ ↑↑j = -↑↑↑c

theorem Zeta5Irrational.neg_ne_self_zmod {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) {x : ZMod p} (hx : x ≠ 0) : x ≠ -x

theorem Zeta5Irrational.card_class {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) {c : Fin (m + 1)} (hc : c ≠ 0) (X : ℕ) : {j ∈ Finset.Icc 1 X | jc hm j = c}.card = SX p X ↑↑↑c

theorem Zeta5Irrational.card_class_Ioc {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) {c : Fin (m + 1)} (hc : c ≠ 0) {X Y : ℕ} (hXY : X ≤ Y) : {j ∈ Finset.Icc (X + 1) Y | jc hm j = c}.card = SX p Y ↑↑↑c - SX p X ↑↑↑c

noncomputable def Zeta5Irrational.GO (q a d : ℕ) : ℚ

The per-class outer weight sum G_q(a, δ).

Equations

• Zeta5Irrational.GO q a d = ∑ i ∈ Finset.range (2 * q + a - 2), min 0 (↑i + 3 * ↑d - (↑(2 * q + a) + 4) / 2)

theorem Zeta5Irrational.three_n_le_m {p m : ℕ} (hm : 2 * m + 1 = p) {n : ℕ} (hn : 1 ≤ n) (hout : 40 * n < 3 * p) : 3 * n ≤ m

theorem Zeta5Irrational.SX_small {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) {X : ℕ} (hX : X < p) {c : ℕ} (hc1 : 1 ≤ c) (hcm : c ≤ m) : SX p X ↑↑c = aCnt p X c

theorem Zeta5Irrational.class_data {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) {n : ℕ} (hn : 1 ≤ n) (hout : 40 * n < 3 * p) {c : Fin (m + 1)} (hc : c ≠ 0) : LoC hm n c = 2 * (40 * n / p) + aCnt p (40 * n % p) ↑c - aCnt p (3 * n) ↑c ∧ nbC hm n c = 2 * (40 * n / p) + aCnt p (40 * n % p) ↑c - 2 ∧ ellC hm n c = 2 * (40 * n / p) + aCnt p (40 * n % p) ↑c ∧ delC n c = aCnt p (3 * n) ↑c

theorem Zeta5Irrational.sum_wO_class {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) {n : ℕ} (hn : 1 ≤ n) (hout : 40 * n < 3 * p) {c : Fin (m + 1)} (hc : c ≠ 0) : ∑ i ∈ Finset.range (LoC hm n c), wO hm n c i = GO (40 * n / p) (aCnt p (40 * n % p) ↑c) (aCnt p (3 * n) ↑c)

theorem Zeta5Irrational.sum_wO_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) {n : ℕ} (hn : 1 ≤ n) (hout : 40 * n < 3 * p) : -4 ≤ ∑ i ∈ Finset.range (LoC hm n 0), wO hm n 0 i

noncomputable def Zeta5Irrational.bGO (q : ℕ) (i j : Fin 3) : ℝ

The class-function coefficients of the outer range.

Equations

• Zeta5Irrational.bGO q i j = Zeta5Irrational.bcoef (fun (a : ℕ) => Zeta5Irrational.bcoef (fun (b : ℕ) => ↑(Zeta5Irrational.GO q a b)) j) i

noncomputable def Zeta5Irrational.Eout (x : ℝ) : ℝ

The continuous outer function (in the variable x = K/p).

Equations

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

noncomputable def Zeta5Irrational.Cout (n p : ℕ) : ℝ

The additive error of the outer bound.

Equations

• Zeta5Irrational.Cout n p = 5 * ∑ i : Fin 3, ∑ j : Fin 3, |Zeta5Irrational.bGO (40 * n / p) i j| + 11

theorem Zeta5Irrational.outer_Lp_le {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 33 ≤ n) (hodd : 2 * (p / 2) + 1 = p) (hp7 : 7 ≤ p) (hout : 40 * n < 3 * p) (hsq : 2 * (40 * n) < p ^ 2) : -↑(Lp n p) ≤ ↑p * Eout (40 * ↑n / ↑p) + Cout n p

The outer per-prime bound.