The normalisation actually used

For every prime p ≤ 2h the local exponent Lp n p is one of the proved lower bounds for v_p^G(F_K):

• small primes p M ≤ K: the bound (3.12), small_prime_bound;
• inner range K < pM, 3p ≤ K: v_p(S_K) + ⌊2 ∑ wcap⌋ for the water-filling allocation (inner_bound_cap), when its side conditions hold;
• outer range K < 3p: v_p(S_K) + ⌊2 ∑ w - r⌋ (outer_bound), when its side conditions hold;

falling back to (3.12) otherwise. The normaliser is mN n = ∏_{p ≤ 2h} p^{-L_p}, and integral_mN proves mN n · F_K ∈ ℤ[X] for every n ≥ 1.

def Zeta5Irrational.Mcut : ℕ

The cutoff M separating small primes from the inner range.

Equations

• Zeta5Irrational.Mcut = 400

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

The small-prime exponent (3.12).

Equations

• Zeta5Irrational.Lsmall n p = -(6 * ↑(37 * n) * ↑(Nat.log p (200 * n)) + ↑(37 * n) * ↑(padicValNat p 24))

noncomputable def Zeta5Irrational.betaI (n p : ℕ) {m : ℕ} (c : Fin (m + 1)) : ℤ

The class offsets β_c = 6 ℓ_N(c) - ℓ_K(c) - 4.

Equations

• Zeta5Irrational.betaI n p c = 6 * ↑(Zeta5Irrational.SX p (3 * n) ↑↑↑c) - ↑(Zeta5Irrational.SX p (40 * n) ↑↑↑c) - 4

def Zeta5Irrational.kloI (n p : ℕ) : ℤ

The water-filling parameters.

Equations

• Zeta5Irrational.kloI n p = -2 * ↑(40 * n / p) - 6

def Zeta5Irrational.ktopI (n p : ℕ) : ℤ

Upper admissible allocation level in the inner-prime range.

Equations

• Zeta5Irrational.ktopI n p = 8 * ↑(40 * n / p) + 20

def Zeta5Irrational.L0I (n p : ℕ) : ℕ

Rows reserved for the zero residue class in the inner allocation.

Equations

• Zeta5Irrational.L0I n p = 3 * (40 * n / p) + 6

noncomputable def Zeta5Irrational.allocI (n p m : ℕ) : Fin (m + 1) → ℕ

The inner allocation.

Equations

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

def Zeta5Irrational.InnerOK (n p : ℕ) : Prop

The side conditions of the inner bound.

Equations

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

noncomputable def Zeta5Irrational.WI (n p : ℕ) : ℚ

The inner weight sum (for m = p / 2).

Equations

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

def Zeta5Irrational.OuterOK (n p : ℕ) : Prop

The side conditions of the outer bound.

Equations

• Zeta5Irrational.OuterOK n p = (2 * (p / 2) + 1 = p ∧ 7 ≤ p ∧ 40 * n < 3 * p ∧ 2 * (40 * n) < p ^ 2 ∧ 3 * n < p)

noncomputable def Zeta5Irrational.WO (n p : ℕ) : ℚ

The outer weight sum minus the rank loss (for m = p / 2).

Equations

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

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

The local exponent.

Equations

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

noncomputable def Zeta5Irrational.mN (n : ℕ) : ℚ

The normaliser m_K = ∏_{p ≤ 2h} p^{-L_p}.

Equations

• Zeta5Irrational.mN n = ∏ p ∈ Finset.range (2 * (37 * n) + 1) with Nat.Prime p, ↑p ^ (-Zeta5Irrational.Lp n p)

theorem Zeta5Irrational.mN_pos (n : ℕ) : 0 < mN n

Validity of the local exponents

theorem Zeta5Irrational.Sep_PlK {p K : ℕ} (hK : 2 * K < p ^ 2) : Sep p (PlK K)

theorem Zeta5Irrational.GV_F_of_Δ {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} {r : ℚ} (h : GV p (Δ n) r) : GV p (F n) (↑(vSK n p) + r)

theorem Zeta5Irrational.GV_F_Lsmall {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 1 ≤ n) : GV p (F n) ↑(Lsmall n p)

theorem Zeta5Irrational.GV_F_inner {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (h : InnerOK n p) : GV p (F n) (↑(vSK n p) + ↑⌊2 * WI n p⌋)

theorem Zeta5Irrational.GV_F_outer {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (h : OuterOK n p) : GV p (F n) (↑(vSK n p) + ↑⌊WO n p⌋)

theorem Zeta5Irrational.GV_F_Lp {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 1 ≤ n) : GV p (F n) ↑(Lp n p)

Every local exponent is valid.

Integrality

theorem Zeta5Irrational.padicValNat_factorial_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : k < p) : padicValNat p k.factorial = 0

theorem Zeta5Irrational.vSK_big {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 1 ≤ n) (hbig : 2 * (37 * n) < p) : vSK n p = 0

theorem Zeta5Irrational.OuterOK_big {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 1 ≤ n) (hbig : 2 * (37 * n) < p) : OuterOK n p

theorem Zeta5Irrational.WO_big {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hbig : 2 * (37 * n) < p) : 0 ≤ WO n p

theorem Zeta5Irrational.GV_F_big {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 1 ≤ n) (hbig : 2 * (37 * n) < p) : GV p (F n) 0

theorem Zeta5Irrational.padicValRat_mN (n p : ℕ) [Fact (Nat.Prime p)] : padicValRat p (mN n) = if p ≤ 2 * (37 * n) then -Lp n p else 0

theorem Zeta5Irrational.rat_int_of_VG {q : ℚ} (h : ∀ (p : ℕ), Fact (Nat.Prime p) → VG p q 0) : ∃ (z : ℤ), q = ↑z

A rational number which is p-integral at every prime is an integer.

theorem Zeta5Irrational.integral_mN {n : ℕ} (hn : 1 ≤ n) : ∃ (Q : Polynomial ℤ), Polynomial.map (Int.castRingHom ℚ) Q = Polynomial.C (mN n) * F n

Integrality (Proposition 5.1 for the normaliser mN).