Theory Zeta5_Definitions
theory Zeta5_Definitions
imports Rational_Padic_Valuations Arcsine_Distribution Logarithmic_Energy
"Zeta_Function.Zeta_Function"
"Kummer_Congruence.Rat_Congruence"
"Jordan_Normal_Form.Determinant"
"Jordan_Normal_Form.DL_Rank"
"HOL-Computational_Algebra.Polynomial_FPS"
"HOL-Library.Log_Nat"
begin
section ‹Definitions of the construction›
text ‹All definitions of the proof, transcribed from the Lean 4 theory @{text Defs} of the
domino14/zeta5 formalisation, which fixed the conventions used throughout:
▪ A rational function in ‹t› is a numerator polynomial together with a finite
set of simple
poles: @{text "muX S P"} is ‹μ⇩X(P(t) / ∏⇩j⇩∈⇩S (t +
j⇧2))› and @{text "tauX S P"} is
‹τ⇩X(P(x) / ∏⇩r⇩∈⇩S (x -
r))›. Values are polynomials in ‹ℚ[X]›;
the indeterminate ‹X› is
later specialised to ‹ζ(5)›.
▪ The ‹p›-adic field ‹ℚ⇩p› of the paper's Sections
3.1--3.2 is not used. Every ‹p›-adically
convergent series is replaced by its partial sum of length ‹M› (the @{text "_tr"}
definitions)
and the identities become congruences modulo high powers of ‹p›, so that the whole
development stays in HOL over ‹ℚ›.
▪ Matrices are those of the Jordan\_Normal\_Form library, indexed
by explicit lists of index
pairs instead of Lean's ‹Σ›-types.
Equation and section numbers refer to Fauzan's paper.›
subsection ‹Generic helpers›
text ‹Evaluation of a rational polynomial at a real (Lean: @{text "aeval x P"}).›
definition real_eval :: "rat poly ⇒ real ⇒ real" where
"real_eval P x = poly (map_poly of_rat P) x"
subsection ‹Section 2.1 Parameters (2.1)›
definition Nof :: "nat ⇒ nat" where "Nof K = 3 * K div 40"
definition hof :: "nat ⇒ nat" where "hof K = 37 * K div 40"
definition alpha_q :: rat where "alpha_q = 3 / 40"
definition lam_q :: rat where "lam_q = 37 / 40"
definition Hc_q :: rat where "Hc_q = 1 + 2 * alpha_q"
text ‹The real number ‹ζ(5)›;
@{text zeta} is the AFP's Riemann zeta function.›
definition zeta5 :: real where "zeta5 = Re (zeta 5)"
text ‹@{text "H_j^{(5)} = ∑_{v=1}^j v^{-5}"}.›
definition H5 :: "nat ⇒ rat" where "H5 j = (∑ v = 1..j. 1 / of_nat v ^ 5)"
text ‹@{text "D_m(t) = ∏_{j=1}^m (t + j^2)"}.›
definition Dm :: "nat ⇒ rat poly" where "Dm m = (∏ j =
1..m. pX + [:of_nat j ^ 2:])"
subsection ‹Section 2.1 The functional mu\_X (2.2), (2.3)›
text ‹(2.2): @{text "mu(t^e) = (-1)^e B_{2e+2} (2e+3)(2e+4)(2e+5)/24"},
with @{text "B_1 = -1/2"}
(both Mathlib's @{text bernoulli} and the AFP's polymorphic @{const bernoulli} use this
convention).›
definition muMono :: "nat ⇒ rat" where
"muMono e = (-1) ^ e * bernoulli (2 * e + 2) *
((2 * of_nat e + 3) * (2 * of_nat e + 4) * (2 * of_nat e + 5)) / 24"
definition muPoly :: "rat poly ⇒ rat" where
"muPoly P = (∑ e ≤ degree P. Polynomial.coeff P e * muMono e)"
text ‹(2.3): @{text "mu_X(1/(t+j^2)) = j^4(X - H_j) - 1/4 + 1/(2j)"}.›
definition muPole :: "nat ⇒ rat poly" where
"muPole j = [:of_nat j ^ 4:] * (pX - [:H5 j:]) - [:1 / 4:] + [:1 / (2 * of_nat j):]"
definition sqPoleProd :: "nat set ⇒ rat poly" where
"sqPoleProd S = (∏ j ∈ S. pX + [:of_nat j ^ 2:])"
text ‹Residue of @{text "P/∏_{k∈S}(t+k^2)"} at @{text "t = -j^2"}.›
definition sqResidue :: "nat set ⇒ rat poly ⇒ nat ⇒ rat" where
"sqResidue S P j = poly P (- (of_nat j ^ 2)) / (∏ k ∈
S - {j}. of_nat k ^ 2 - (of_nat j ^ 2))"
text ‹@{text "mu_X(P(t)/∏_{j∈S}(t+j^2))"}
by polynomial division and simple partial fractions
(meaningful for finite @{text S} with @{text "0 ∉ S"}).›
definition muX :: "nat set ⇒ rat poly ⇒ rat poly" where
"muX S P = [:muPoly (P div sqPoleProd S):] + (∑ j ∈ S. [:sqResidue S P j:] * muPole j)"
subsection ‹Section 2.1 The matrix, determinant and normalisation (2.4), (2.5)›
text ‹(2.4): @{text "G_K(X) = [mu_X(D_N(t)^6 t^{i+j} / D_K(t))]_{0 ≤ i,j < h}"}.›
definition GK :: "nat ⇒ rat poly mat" where
"GK K = Matrix.mat (hof K) (hof K) (λ(i, j). muX {1..K} (Dm (Nof K) ^ 6 * pX ^ (i + j)))"
definition DeltaK :: "nat ⇒ rat poly" where "DeltaK K = Determinant.det (GK K)"
text ‹(2.5): @{text "S_K = (K!)^{2h} 4^{h-1} /
((N!)^{12h} ∏_{i=1}^{h-1} ((2i)!)^2)"}.›
definition SK :: "nat ⇒ rat" where
"SK K = (fact K ^ (2 * hof K) * 4 ^ (hof K - 1)) /
(fact (Nof K) ^ (12 * hof K) * (∏ i = 1..hof K - 1. fact (2 * i) ^ 2))"
definition FK :: "nat ⇒ rat poly" where "FK K = [:SK K:] * DeltaK K"
subsection ‹Section 3 The functional ‹τ⇩X››
text ‹@{text "L(x^k) = B_k"}, extended linearly.›
definition Lfun :: "rat poly ⇒ rat" where
"Lfun P = (∑ k ≤ degree P. Polynomial.coeff P k * bernoulli k)"
text ‹@{text "τ(P) = L(P''')/24"} on polynomials.›
definition tau :: "rat poly ⇒ rat" where
"tau P = Lfun ((pderiv ^^ 3) P) / 24"
text ‹@{text "d(r) = r"} for @{text "r ≥ 0"} and @{text "-r-1"}
for @{text "r < 0"}.›
definition dIdx :: "int ⇒ nat" where
"dIdx r = (if 0 ≤ r then nat r else nat (- r - 1))"
text ‹@{text "τ_X(1/(x-r)) = H_{d(r)} - X"}.›
definition tauPole :: "int ⇒ rat poly" where
"tauPole r = [:H5 (dIdx r):] - pX"
definition linPoleProd :: "int set ⇒ rat poly" where
"linPoleProd S = (∏ r ∈ S. pX - [:of_int r:])"
definition linResidue :: "int set ⇒ rat poly ⇒ int ⇒ rat" where
"linResidue S P r = poly P (of_int r) / (∏ s ∈ S - {r}. of_int r - of_int s)"
text ‹@{text "τ_X(P(x)/∏_{r∈S}(x-r))"}
by polynomial division and simple partial fractions.›
definition tauX :: "int set ⇒ rat poly ⇒ rat poly" where
"tauX S P = [:tau (P div linPoleProd S):] + (∑ r ∈ S. [:linResidue S P r:] * tauPole r)"
text ‹The fourth Taylor coefficient @{text "g''''(0)/24"} of @{text "g = P/Q"} at 0 (needs
@{text "Q(0) ≠ 0"}).›
definition taylor4 :: "rat poly ⇒ rat poly ⇒ rat" where
"taylor4 P Q = fps_nth (fps_of_poly P * inverse (fps_of_poly Q)) 4"
text ‹The poles @{text "±j"},
@{text "j ∈ S"} (Lean: @{text signedPoles}).›
definition signedPoles :: "nat set ⇒ int set" where
"signedPoles S = int ` S ∪ (λj. - int j) ` S"
text ‹The poles @{text "-K ≤ r ≤ K"}, @{text "r ≠ 0"}, of Lemma 3.3.›
definition symPoles :: "nat ⇒ int set" where
"symPoles K = {r. - int K ≤ r ∧ r ≤ int K ∧ r ≠ 0}"
text ‹@{text A} is @{text p}-integer-valued on ‹ℤ› (Lean:
@{text IntValuedAt}).›
definition IntValuedAt :: "nat ⇒ rat poly ⇒ bool" where
"IntValuedAt p A ⟷
(∀x::int. poly A (of_int x) ≠ 0 ⟶
0 ≤ vp p (poly A (of_int x)))"
subsection ‹Section 3.1-3.2 The @{text p}-adic extension, in truncated rational form›
text ‹@{text "κ_d = d(d-1)(d-2) B_{d-3}/24"},
so that @{text "τ(z^d) = κ_d"}; it is 0 for @{text "d < 3"}.›
definition kappa :: "nat ⇒ rat" where
"kappa d = of_nat d * (of_nat d - 1) * (of_nat d - 2) * bernoulli (d - 3) / 24"
text ‹@{text τ} on polynomials through @{text κ} (equal to @{const tau}).›
definition tauK :: "rat poly ⇒ rat" where
"tauK Q = (∑ d ≤ degree Q. Polynomial.coeff Q d * kappa d)"
text ‹(3.5), truncated: the partial sum of length @{text M} of
@{text "τ^{an}(1/(z-s)) = -(1/4) ∑_{k≥0} C(k+3,3) B_k s^{-k-4}"} (for
@{text "v_p(s) < 0"}
the @{text k}-th term has valuation @{text "≥ k+3"},
so the tail is @{text "≡ 0 mod p^{M+3}"}).›
definition tauAnPole_tr :: "nat ⇒ rat ⇒ nat ⇒ rat" where
"tauAnPole_tr p s M =
- (1 / 4) * (∑ k < M. of_nat ((k + 3) choose 3) * bernoulli k * s powi (- (int k + 4)))"
text ‹(3.6), truncated: @{text "C_p = ∑_{a=1}^{p-1} τ^{an}(1/(x + a/p))"}.›
definition Cp_tr :: "nat ⇒ nat ⇒ rat" where
"Cp_tr p M = (∑ a = 1..p - 1. tauAnPole_tr p (- of_nat a / of_nat p) M)"
text ‹(3.6): @{text "Y = p^5 X + C_p"}.›
definition Yp_tr :: "nat ⇒ nat ⇒ rat poly" where
"Yp_tr p M = [:of_nat p ^ 5:] * pX + [:Cp_tr p M:]"
text ‹Value of @{text "τ_Y^{ext}"} on the simple pole @{text "1/(z-s)"}: near (integer)
poles take
@{text "H_{d(s)} - Y"}, far poles the truncated series.›
definition tauPoleP_tr :: "nat ⇒ rat poly ⇒ rat ⇒ nat
⇒ rat poly" where
"tauPoleP_tr p Y s M =
(if snd (quotient_of s) = 1 then [:H5 (dIdx (fst (quotient_of s))):] - Y
else [:tauAnPole_tr p s M:])"
definition qPoleProd :: "rat set ⇒ rat poly" where
"qPoleProd S = (∏ s ∈ S. pX - [:s:])"
definition qRes :: "rat set ⇒ rat poly ⇒ rat ⇒ rat" where
"qRes S P s = poly P s / (∏ s' ∈ S - {s}. s - s')"
text ‹@{text "τ_Y^{ext}(U(z)/∏_{s∈S}(z-s))"}
for distinct rational poles @{text S}, truncated at @{text M}.›
definition tauExt_tr :: "nat ⇒ rat poly ⇒ rat poly ⇒ rat set
⇒ nat ⇒ rat poly" where
"tauExt_tr p Y U S M =
[:tauK (U div qPoleProd S):] + (∑ s ∈ S. [:qRes S U s:] * tauPoleP_tr p Y s M)"
text ‹@{text "g(a + p x)"} written as @{text "U(x)/∏(x - s)"}: the numerator
@{text "p^{-|S|} P(a + p x)"}.›
definition distribNum :: "nat ⇒ int set ⇒ rat poly ⇒ nat
⇒ rat poly" where
"distribNum p S P a =
[:of_nat p powi (- int (card S)):] * pcompose P ([:of_nat a:] + [:of_nat p:] * pX)"
text ‹The poles @{text "(r - a)/p"} of @{text "g(a + p x)"}.›
definition distribPoles :: "nat ⇒ int set ⇒ nat ⇒ rat set" where
"distribPoles p S a = (λr. (of_int r - of_nat a) / of_nat p) ` S"
text ‹The Taylor coefficients of the analytic part
@{text "Q + ∑_{s∈F} ρ_s/(z-s)"}.›
definition fCoeff :: "rat poly ⇒ rat set ⇒ (rat ⇒ rat)
⇒ nat ⇒ rat" where
"fCoeff Q F ρ d = Polynomial.coeff Q d - (∑ s ∈ F. ρ s * inverse s ^ (d + 1))"
subsection ‹Section 3.3 Small primes›
text ‹@{text "q_0 = 1"}, @{text "q_i(t) = (-1)^i 2t D_{i-1}(t)/(2i)!"}.›
definition qBasis :: "nat ⇒ rat poly" where
"qBasis i = (if i = 0 then 1 else [:(-1) ^ i * 2 / fact (2 * i):] * pX * Dm (i - 1))"
text ‹@{text "f_i(t) = (D_N(t)/(N!)^2)^3 q_i(t)"}.›
definition fBasis :: "nat ⇒ nat ⇒ rat poly" where
"fBasis K i = ([:1 / fact (Nof K) ^ 2:] * Dm (Nof K)) ^ 3 * qBasis i"
subsection ‹Section 4.1 The inner range›
text ‹@{text "l_A(a) = #{1 ≤ j ≤ A : j ≡ ±a (mod p)}"}.›
definition ell :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"ell p A a = card {j ∈ {1..A}. j mod p = a mod p ∨ (j + a) mod p = 0}"
definition mHalf :: "nat ⇒ nat" where "mHalf p = (p - 1) div 2"
definition L0 :: "nat ⇒ nat" where "L0 M = 4 * M + 10"
text ‹Right-hand side of (4.4): @{text "h - L_0 + 3(N - m_N)"}.›
definition rhs44 :: "nat ⇒ nat ⇒ nat ⇒ int" where
"rhs44 K M p = int (hof K) - int (L0 M) + 3 * (int (Nof K) - int (Nof K div p))"
text ‹(4.4): @{text T} and @{text E} (integer division
by the positive number @{text "m = (p-1)/2"}).›
definition Tin :: "nat ⇒ nat ⇒ nat ⇒ int" where "Tin K M p =
rhs44 K M p div int (mHalf p)"
definition Ein :: "nat ⇒ nat ⇒ nat ⇒ int" where "Ein K M p =
rhs44 K M p mod int (mHalf p)"
text ‹@{text "b_a = 3 l_N(a)"}.›
definition bIn :: "nat ⇒ nat ⇒ nat ⇒ int" where "bIn K p a =
3 * int (ell p (Nof K) a)"
text ‹Position of class @{text a} in the ordering by decreasing @{text "l_K"}, ties
by increasing @{text a}.›
definition defaultPos :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"defaultPos K p a = card {c ∈ {1..mHalf p}. ell p K a < ell p K c ∨
(ell p K c = ell p K a ∧ c < a)}"
text ‹@{text "ε_a = 1"} for the first @{text E} classes in that ordering.›
definition epsIn :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ int"
where
"epsIn K M p a =
(if int (card {c ∈ {1..mHalf p}. defaultPos K p c < defaultPos K p a}) <
Ein K M p then 1 else 0)"
text ‹@{text "L_a = T - b_a + ε_a"}
for @{text "a ≥ 1"}, and @{text "L_0 = 4M + 10"}.›
definition Lin :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ int"
where
"Lin K M p a = (if a = 0 then int (L0 M) else Tin K M p - bIn K p a + epsIn K M p a)"
text ‹@{text "Z_a = T + ε_a"}.›
definition Zin :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ int"
where "Zin K M p a = Tin K M p + epsIn K M p a"
text ‹(4.6), (4.7): the row weights @{text "w_{a,i}"}.›
definition wIn :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat
⇒ rat" where
"wIn K M p a i =
(if a = 0 then
Min (insert (2 * of_nat i + 6 * of_nat (Nof K div p) - of_nat (K div p) + 1 / 2)
((λc. of_int (Zin K M p c) - (of_nat (ell p K c) + 4) /
2) ` {1..mHalf p}))
else of_nat i + of_int (bIn K p a) - (of_nat (ell p K a) + 4) / 2)"
text ‹(4.8): @{text "γ_p^in = 2 ∑_{a=0}^m ∑_{i<L_a} w_{a,i}"}.›
definition gammaIn :: "nat ⇒ nat ⇒ nat ⇒ rat" where
"gammaIn K M p = 2 * (∑ a ≤ mHalf p. ∑ i < nat (Lin K M p a). wIn K M p a i)"
text ‹Index list of the inner basis: pairs @{text "(a, i)"} with @{text "0 ≤ a ≤ m"},
@{text "i < L_a"}
(Lean's ‹Σ›-type @{text InnerIdx}, enumerated).›
definition inner_idx :: "nat ⇒ nat ⇒ nat ⇒ (nat ×
nat) list" where
"inner_idx K M p = concat (map (λa. map (λi. (a,
i)) [0..<nat (Lin K M p a)]) [0..<mHalf p + 1])"
text ‹(4.5): @{text "E_{a,i}(t) = ∏_{c ≠
a} (t + c^2)^{L_c} (t + a^2)^i"}.›
definition innerBasis :: "nat ⇒ nat ⇒ nat ⇒ nat ×
nat ⇒ rat poly" where
"innerBasis K M p x =
(∏ c ∈ {0..mHalf p} - {fst x}. (pX + [:of_nat c ^ 2:]) ^ nat (Lin K M p c)) *
(pX + [:of_nat (fst x) ^ 2:]) ^ snd x"
text ‹The Gram matrix of @{text "mu_X(D_N^6 ⋅ / D_K)"} in the inner basis.›
definition innerGram :: "nat ⇒ nat ⇒ nat ⇒ rat poly mat" where
"innerGram K M p = (let idx = inner_idx K M p in
Matrix.mat (length idx) (length idx)
(λ(x, y). muX {1..K} (Dm (Nof K) ^ 6 * innerBasis K M p (idx ! x) *
innerBasis K M p (idx ! y))))"
definition wInIdx :: "nat ⇒ nat ⇒ nat ⇒ nat ×
nat ⇒ rat" where
"wInIdx K M p x = wIn K M p (fst x) (snd x)"
subsection ‹Section 4.2 The outer range›
text ‹@{text "r_p = max(0, K + 4N - 2p + 2)"} from (4.10) (truncated subtraction).›
definition rOut :: "nat ⇒ nat ⇒ nat" where "rOut K p =
K + 4 * Nof K + 2 - 2 * p"
text ‹(4.14): @{text "γ_p^out"}, with @{text "v = K - p⌊K/p⌋"},
@{text "u = max(0, N+v-p+1)"},
@{text "t_p = min(N, v) + u"}.›
definition gammaOut :: "nat ⇒ nat ⇒ int" where
"gammaOut K p = (let v = K mod p; u = Nof K + v + 1 - p; tp = min (Nof K) v + u in
if K < 2 * p
then - 7 * (int K - int p) + 6 * int tp - 1 - min (int (rOut K p)) (int p - 1 - int (Nof K) +
int u)
else - 7 * (int K - int p) + 3 + 12 * int (Nof K) + 5 * int tp - min (int (rOut K p)) (int p +
int u))"
text ‹(4.9): the hypotheses of the outer-range estimate.›
definition OuterHyp :: "nat ⇒ nat ⇒ bool" where
"OuterHyp K p ⟷ 7 ≤ p ∧ p ≤ K ∧ K < 3 * p ∧
2 * K < p ^ 2 ∧ 2 * Nof K < p ∧ 5 * Nof K ≤ 2 * p - 2"
text ‹The poles of @{text "D_tail"} in the class @{text "±a (mod p)"}
(@{text "a = 0"}: multiples of @{text p}).›
definition outerClassPoles :: "nat ⇒ nat ⇒ nat ⇒ nat set" where
"outerClassPoles K p a = {j ∈ {Nof K + 1..K}. j mod p = a mod p ∨ (j + a) mod p = 0}"
definition outerCount :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"outerCount K p a = card (outerClassPoles K p a)"
definition outer_idx :: "nat ⇒ nat ⇒ (nat × nat) list" where
"outer_idx K p = concat (map (λa. map (λi. (a,
i)) [0..<outerCount K p a]) [0..<mHalf p + 1])"
text ‹(4.11): rows @{text "P_a q_{a,i}"} with @{text "P_a = D_tail/Q_a"};
the zero class is read as
@{text "P_0 (t + p^2)^i"} (ambiguity recorded in the Lean NOTES, finding 1).›
definition outerBasis :: "nat ⇒ nat ⇒ nat ×
nat ⇒ rat poly" where
"outerBasis K p x = (let a = fst x; i = snd x;
Pa = sqPoleProd ({Nof K + 1..K} - outerClassPoles K p a) in
if a = 0 then Pa * (pX + [:of_nat p ^ 2:]) ^ i
else (let l = ell p K a in
if i < l - 2 then Pa * (pX + [:of_nat a ^ 2:]) ^ i
else Pa * sqPoleProd {j ∈ outerClassPoles K p a. p <
j} * (pX + [:of_nat a ^ 2:]) ^ (i - (l - 2))))"
text ‹(4.12) and the zero-class weights.›
definition wOut :: "nat ⇒ nat ⇒ nat × nat ⇒ rat" where
"wOut K p x = (let a = fst x; i = snd x in
if a = 0 then (if outerCount K p 0 = 1 then - 1 / 2 else if i = 0 then - 2 else 0)
else (let l = ell p K a; d = (if a ≤ Nof K then 1 else 0 :: rat) in
if i < l - 2 then min 0 (of_nat i + 3 * d - (of_nat l + 4) / 2) else 0))"
text ‹The integer @{text "c_e ≡ p mu(t^e) (mod p)"} in @{text "[0, p)"},
with @{text "c_e = 0"} for @{text "e < 2p-3"}
(@{const qmod} is the AFP's residue of a rational modulo an integer).›
definition cCorr :: "nat ⇒ nat ⇒ rat" where
"cCorr p e = (if e < 2 * p - 3 then 0 else of_int ((of_nat p * muMono e) qmod int p))"
text ‹@{text "mu_X"} with the polynomial moments replaced
by @{text "mu^0(t^e) = mu(t^e) - c_e/p"}.›
definition muXmod :: "nat ⇒ nat set ⇒ rat poly ⇒ rat poly" where
"muXmod p S P =
[:∑ e ≤ degree (P div sqPoleProd S). Polynomial.coeff (P div sqPoleProd S) e *
(muMono e - cCorr p e / of_nat p):]
+ (∑ j ∈ S. [:sqResidue S P j:] * muPole j)"
text ‹The matrix @{text A} of (4.10).›
definition Aout :: "nat ⇒ nat ⇒ rat poly mat" where
"Aout K p = Matrix.mat (hof K) (hof K) (λ(i,
j). muXmod p {1..K} (Dm (Nof K) ^ 6 * pX ^ (i + j)))"
text ‹@{text A} in the outer basis.›
definition outerGram :: "nat ⇒ nat ⇒ rat poly mat" where
"outerGram K p = (let idx = outer_idx K p in
Matrix.mat (length idx) (length idx)
(λ(x, y). muXmod p {1..K} (Dm (Nof K) ^ 6 * outerBasis K p (idx ! x) *
outerBasis K p (idx ! y))))"
subsection ‹Section 5 Normalisation (5.1), (5.2), (2.6)›
definition vpS :: "nat ⇒ nat ⇒ int" where "vpS K p = vp p (SK K)"
text ‹(5.1): @{text "L_p(K, M)"}; @{text "γ_p^in"} is an integer (Lean
@{text gammaIn_isInt}), the floor
just keeps the definition total.›
definition Lp :: "nat ⇒ nat ⇒ nat ⇒ int" where
"Lp K M p =
(if p * M ≤ K then - 6 * int (hof K) * int (nat_log p (5 * K)) - int (hof K) *
int (multiplicity p (24::nat))
else if 3 * p ≤ K then vpS K p + floor (gammaIn K M p)
else if p ≤ K then vpS K p + gammaOut K p
else vpS K p)"
text ‹(5.2): @{text "m_{K,M} = ∏_{p ≤ 2h} p^{-L_p(K,M)}"}.›
definition mKM :: "nat ⇒ nat ⇒ rat" where
"mKM K M = (∏ p ∈ {p. p ≤ 2 * hof K ∧ prime p}. of_nat p powi (- Lp K M p))"
text ‹(2.6): @{text "Q_{K,M} = m_{K,M} F_K"}.›
definition QKM :: "nat ⇒ nat ⇒ rat poly" where "QKM K M =
[:mKM K M:] * FK K"
subsection ‹Section 5.1-5.3 Limiting functions (real-valued;
Lean namespace @{text Lim})›
definition alpha_r :: real where "alpha_r = 3 / 40"
definition lam_r :: real where "lam_r = 37 / 40"
definition Hc_r :: real where "Hc_r = 23 / 20"
definition pos_r :: "real ⇒ real" where "pos_r v = max v 0"
text ‹@{text "l(x, z) = ⌊x - z⌋ + ⌊x + z⌋ + 1"}.›
definition ell_r :: "real ⇒ real ⇒ real" where
"ell_r x z = of_int (floor (x - z)) + of_int (floor (x + z)) + 1"
text ‹(5.4): @{text "Γ(x)"}.›
definition Gam_r :: "real ⇒ real" where
"Gam_r x = (let T = of_int (floor (2 * Hc_r * x)); s = Hc_r * x - T / 2;
q = of_int (floor (2 * x)); nplus = (2 * x - q) / 2 in
interval_lebesgue_integral lborel (ereal 0) (ereal (1 / 2))
(λz. (T - 3 * ell_r (alpha_r * x) z) * (T + 3 * ell_r (alpha_r * x) z - ell_r x z -
5))
+ s * (2 * T - q - 5) + pos_r (s - nplus))"
text ‹@{text "J(u) = m u - m(m+1)/4"}, @{text "m = ⌊2u⌋"}.›
definition J_r :: "real ⇒ real" where
"J_r u = of_int (floor (2 * u)) * u - of_int (floor (2 * u)) * (of_int (floor (2 * u)) + 1) / 4"
text ‹(5.5): @{text "N(x)"}.›
definition Nfun_r :: "real ⇒ real" where
"Nfun_r x = 2 * lam_r * x * of_int (floor x) - 12 * lam_r * x * of_int (floor (alpha_r * x))
- 2 * J_r (lam_r * x)"
text ‹(5.6): @{text "R(x) = -Γ(x) - N(x)"}.›
definition R_r :: "real ⇒ real" where "R_r x = - Gam_r x - Nfun_r x"
text ‹(5.8): @{text "R_0(y)"}.›
definition R0_r :: "real ⇒ real" where
"R0_r y =
(if 1 / 3 < y ∧ y < 1 / 2 then
8 - 9 * y - 8 * alpha_r - 5 * min alpha_r (1 - 2 * y) - 5 * pos_r (1 + alpha_r - 3 * y)
else if 1 / 2 < y ∧ y < 1 then
7 * (1 - y) - 6 * min alpha_r (1 - y) - 6 * pos_r (1 + alpha_r - 2 * y) + pos_r (1 + 4 *
alpha_r - 2 * y)
else 0)"
text ‹(5.9): @{text "d(y)"}.›
definition dfun_r :: "real ⇒ real" where
"dfun_r y = (if 1 / 3 < y ∧ y < 1 / 2 then pos_r ((1 + 4 * alpha_r - 3 * y) - pos_r (1 +
alpha_r - 3 * y)) else 0)"
text ‹Integrand of (5.10).›
definition outer_integrand :: "real ⇒ real" where
"outer_integrand y = R0_r y - dfun_r y - 2 * lam_r * of_int (floor (1 / y))
+ (∑ j = 1..5. pos_r (2 * lam_r - real j * y))"
text ‹(5.12)-(5.13): fractional parts and the pieces @{text P}, @{text C} of the tail.›
definition G0_r :: "real ⇒ real" where "G0_r v = v * (1 - v) * (2 * v - 1) / 6"
definition Pper :: "real ⇒ real" where
"Pper x = 74 * frac (alpha_r * x) * (1 - frac (alpha_r * x)) - lam_r * frac x * (1 - frac x)"
definition Cper :: "real ⇒ real" where
"Cper x = 74 / alpha_r * G0_r (frac (alpha_r * x)) - lam_r * G0_r (frac x)"
text ‹(5.10): @{text "I_out = 127751/96000"}.›
definition Iout :: rat where "Iout = 127751 / 96000"
text ‹(5.19).›
definition Astar :: rat where "Astar = 9928298118277006344769 / 7535670527041937280000"
text ‹(5.20).›
definition AM :: "nat ⇒ rat" where
"AM M = Astar + 7 * lam_q / of_nat M - (2923 / 240 - 1 / 4) / of_nat M ^ 2 + 32 / of_nat M ^ 3"
text ‹(6.4): the constant @{text "Ubar"}.›
definition Ubar :: rat where "Ubar = - 2733991 / 2000000"
subsection ‹Section 6 The real determinant›
text ‹(2.10): @{text "w(y) = (2π)^4 y^5/12 ⋅ ∑_{l≥1} l^4 e^{-2πly}"}
(@{text suminf}; summable for @{text "y > 0"}).›
definition weight :: "real ⇒ real" where
"weight y = (2 * pi) ^ 4 * y ^ 5 / 12 * suminf (λl. real (l + 1) ^ 4 * exp (- 2 * pi *
real (l + 1) * y))"
text ‹(6.1): the external field @{text V}.›
definition Vf :: "real ⇒ real" where
"Vf t = 2 * pi * sqrt t + integral {0..1} (λu. ln (t + u ^ 2)) - 6 * integral {0..3 /
40} (λu. ln (t + u ^ 2))"
text ‹Table 1, scaled by @{text "10^1^2"}: @{text "(a_j, b_j, c_j)"}
for @{text "j = 1, …, 16"}.›
definition table1 :: "(nat × nat × nat) list" where
"table1 =
[(3906748086, 8992695531, 10515596180), (2312248264, 15340997855, 29471737793),
(1402286665, 25730180724, 42934365099), (881725356, 41909578246, 58204231966),
(578197906, 65851089563, 69037621310), (396324613, 99481037884, 78873099189),
(283911191, 144325727458, 84856120711), (212206188, 201105762729, 88396082127),
(165097686, 269345996903, 88303382125), (133347132, 347089554156, 85472321255),
(111522114, 430806704415, 78899184238), (96349355, 515561896511, 70353471918),
(85815639, 595448778546, 58838976615), (78667711, 664241383483, 44421321106),
(74129565, 716160577112, 30462865791), (71741310, 746637295669, 5959622577)]"
definition tA :: "nat × nat × nat ⇒ real" where "tA e =
real (fst e) / 10 ^ 12"
definition tB :: "nat × nat × nat ⇒ real" where "tB e =
real (fst (snd e)) / 10 ^ 12"
definition tC :: "nat × nat × nat ⇒ real" where "tC e =
real (snd (snd e)) / 10 ^ 12"
text ‹The comparison measure @{text "ρ = ∑ c_j ω_{[a_j,b_j]}"} of Lemma 6.1,
as one density w.r.t.
Lebesgue measure (Lean sums the sixteen scaled measures; the two agree).›
definition rho :: "real measure" where
"rho = density lborel (λt. ennreal (∑ e ← table1. tC e *
arcsine_dens (tA e) (tB e) t))"
text ‹@{text "I(mu) = integral integral log|t - u| dmu(t) dmu(u)"}.›
definition logEnergy :: "real measure ⇒ real" where
"logEnergy μ = integral⇧L μ (λt. logPot μ t)"
text ‹@{text "M_0 = -1329/200"}.›
definition M0c :: rat where "M0c = - 1329 / 200"
text ‹(6.3): @{text "C* = -2λ + 12αλ(1 - log α) + 3λ^2 -
2λ^2 log(2λ)"}.›
definition Cstar :: real where
"Cstar = - 2 * lam_r + 12 * alpha_r * lam_r * (1 - ln alpha_r) + 3 * lam_r ^ 2 - 2 * lam_r ^ 2 *
ln (2 * lam_r)"
text ‹The partial masses @{text "S_j = ∑_{i ≤ j} c_i"} of Appendix A.›
definition Spart :: "nat ⇒ real" where "Spart j =
(∑ e ← take j table1. tC e)"
end