The p-adic valuation of S_K (5.3)

v_p(S_K) = 2h v_p(K!) - 12h v_p(N!) - 2 ∑_{i=1}^{h-1} v_p((2i)!) + (h-1) v_p(4), where each factorial valuation is given by Legendre's formula (padicValNat_factorial).

noncomputable def Zeta5Irrational.vSK (n p : ℕ) : ℤ

v_p(S_K).

Equations

• Zeta5Irrational.vSK n p = padicValRat p (Zeta5Irrational.S n)

theorem Zeta5Irrational.padicValNat_finset_prod (p : ℕ) [hp : Fact (Nat.Prime p)] {ι : Type u_1} (s : Finset ι) (f : ι → ℕ) (hf : ∀ i ∈ s, f i ≠ 0) : padicValNat p (∏ i ∈ s, f i) = ∑ i ∈ s, padicValNat p (f i)

theorem Zeta5Irrational.S_eq_div (n : ℕ) : S n = ↑((40 * n).factorial ^ (2 * (37 * n)) * 4 ^ (37 * n - 1)) / ↑((3 * n).factorial ^ (12 * (37 * n)) * ∏ i ∈ Finset.Icc 1 (37 * n - 1), (2 * i).factorial ^ 2)

S_K as a quotient of natural numbers.

theorem Zeta5Irrational.vS_eq {n : ℕ} (hn : 0 < n) {p : ℕ} (hp : Nat.Prime p) : vSK n p = 2 * (37 * ↑n) * ↑(padicValNat p (40 * n).factorial) - 12 * (37 * ↑n) * ↑(padicValNat p (3 * n).factorial) - 2 * ∑ i ∈ Finset.Icc 1 (37 * n - 1), ↑(padicValNat p (2 * i).factorial) + (37 * ↑n - 1) * ↑(padicValNat p 4)

(5.3): the valuation of S_K in terms of factorial valuations.