Class data and v_p(S_K) in the inner and outer ranges

• SX p X c = 2 ⌊X/p⌋ + a_c(X mod p) for 1 ≤ c ≤ m;
• -v_p(S_K) ≤ -2h⌊K/p⌋ + 12h⌊N/p⌋ + 2 ∑_{j ≥ 1} (h - jp/2)⁺ when p² > max(2h, N), p odd.

theorem Zeta5Irrational.succ_mod_cases (X q : ℕ) (hq : 0 < q) : (X + 1) % q = X % q + 1 ∧ (X + 1) / q = X / q ∨ X % q = q - 1 ∧ (X + 1) % q = 0 ∧ (X + 1) / q = X / q + 1

theorem Zeta5Irrational.count_res {p : ℕ} [hp : Fact (Nat.Prime p)] (r : ℕ) (hr1 : 1 ≤ r) (hrp : r < p) (X : ℕ) : {j ∈ Finset.Icc 1 X | ↑↑j = ↑↑r}.card = X / p + if r ≤ X % p then 1 else 0

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

SX on a class: SX p X c = 2 ⌊X/p⌋ + a_c(X mod p).

theorem Zeta5Irrational.SX_zero {p : ℕ} [hp : Fact (Nat.Prime p)] (X : ℕ) : SX p X 0 = 2 * (X / p)

v_p(S_K)

theorem Zeta5Irrational.padicValNat_factorial_ge {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} : k / p ≤ padicValNat p k.factorial

theorem Zeta5Irrational.padicValNat_factorial_small {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : k < p ^ 2) : padicValNat p k.factorial = k / p

noncomputable def Zeta5Irrational.layer (p J : ℕ) (t : ℝ) : ℝ

The layer-cake function T(t) = ∑_{j ≤ J} (t - j p/2)⁺.

Equations

• Zeta5Irrational.layer p J t = ∑ j ∈ Finset.Icc 1 J, max 0 (t - ↑j * ↑p / 2)

theorem Zeta5Irrational.layer_step {p : ℕ} [hp : Fact (Nat.Prime p)] (J i : ℕ) (hJ : 2 * i / p ≤ J) : ↑(2 * i / p) ≤ layer p J (↑i + 1) - layer p J ↑i

theorem Zeta5Irrational.sum_floor_le_layer {p : ℕ} [hp : Fact (Nat.Prime p)] (J H : ℕ) (hJ : 2 * H ≤ J * p) : ∑ i ∈ Finset.range H, ↑(2 * i / p) ≤ layer p J ↑H

Layer cake: ∑_{i < H} ⌊2i/p⌋ ≤ ∑_{j ≤ J} (H - jp/2)⁺ if 2H ≤ Jp.