Theory Zeta_5_Irrational
theory Zeta_5_Irrational
imports Zeta5_Archimedean_Bound Zeta5_Exact_Constants "HOL-Real_Asymp.Real_Asymp"
"Liouville_Numbers.Liouville_Numbers_Misc"
begin
section ‹The main theorem: ‹ζ(5)› is irrational›
text ‹Section 7 of the paper: Theorem 2.1 (‹Q⇩K⇩,⇩M ∈
ℤ[X]› of degree ‹h› with ‹Q⇩K⇩,⇩M(ζ(5)) >
0›), the limit
(7.1), the decay (2.7) for ‹M = 200›, the elementary irrationality criterion
(@{text irrational_of_int_poly_approx}: integer polynomials ‹Q⇩n› of degree
‹≤ d n› with
‹0 < Q⇩n(x) < exp(-c n⇧2)› force ‹x ∉ ℚ›),
and the main theorem @{text zeta5_irrational}. Lean theories
@{text Section7}, @{text Main}, @{text Claim}.›
lemma real_eval_smult: "real_eval (Polynomial.smult c P) x = of_rat c * real_eval P x"
by (simp add: real_eval_def map_poly_smult of_rat_mult)
lemma real_eval_QKM: "real_eval (QKM K M) zeta5 = of_rat (mKM K M) * real_eval (FK K) zeta5"
by (simp add: QKM_def real_eval_smult)
lemma real_eval_FK: "real_eval (FK K) zeta5 = of_rat (SK K) * real_eval (DeltaK K) zeta5"
by (simp add: FK_def real_eval_smult)
text ‹Theorem 2.1, first part: @{text "Q_{K,M} ∈ ℤ[X]"}, @{text "deg Q_{K,M} = h"},
@{text "Q_{K,M}(ζ(5)) > 0"}.›
theorem QKM_int_degree_pos:
assumes "StdHyp K M"
shows "(∃P :: int poly. map_poly of_int P = QKM K M) ∧
degree (QKM K M) = hof K ∧
0 < real_eval (QKM K M) zeta5"
proof (intro conjI)
show "∃P :: int poly. map_poly of_int P = QKM K M" by (rule QKM_int_poly[OF assms])
have hK: "40 dvd K" using assms by (simp add: StdHyp_def)
have "QKM K M = Polynomial.smult (mKM K M * SK K) (DeltaK K)"
by (simp add: QKM_def FK_def mult_ac)
thus "degree (QKM K M) = hof K"
using mKM_pos[of K M] SK_pos[of K] Delta_degree_lead_coeff[OF hK]
by (auto simp: degree_smult_eq)
show "0 < real_eval (QKM K M) zeta5"
using mKM_pos SK_pos Delta_zeta5_pos by (simp add: real_eval_QKM real_eval_FK)
qed
text ‹@{text "(24 K log K + 200 K)/K^2 → 0"} along @{text "K = 40n"}
(@{text real_asymp}).›
lemma error_term_small:
assumes "0 < ε"
shows "∀⇩F n in at_top.
(24 * real (40 * n) * ln (real (40 * n)) + 200 * real (40 * n)) / real (40 * n) ^ 2 ≤
ε"
proof -
define f where "f = (λn. (24 * real (40 * n) * ln (real (40 * n)) + 200 * real (40 * n)) /
real (40 * n) ^ 2)"
have "(f ⤏ 0) at_top" unfolding f_def by real_asymp
from tendstoD[OF this assms] have "∀⇩F n in at_top. f n ≤ ε"
by (elim eventually_mono) (auto simp: dist_real_def abs_less_iff)
thus ?thesis by (simp add: f_def)
qed
text ‹(7.1): @{text "limsup K^-^2 log Q_{K,M}(ζ(5)) ≤ A_M + Ubar"}
for @{text "M ∈ 40ℤ"}, @{text "M ≥ 40"}.›
theorem log_QKM_zeta5_limsup:
assumes "40 ≤ M" "40 dvd M" "0 < ε"
shows "∀⇩F n in at_top.
ln (real_eval (QKM (40 * n) M) zeta5) / real (40 * n) ^ 2 ≤
of_rat (AM M) + of_rat Ubar + ε"
proof -
have A: "∀⇩F n in at_top. ln (of_rat (mKM (40 * n) M)) / real (40 * n) ^ 2 ≤
of_rat (AM M) + ε / 2"
by (rule log_mKM_limsup_AM) (use assms in simp_all)
have B: "∀⇩F n in at_top.
(24 * real (40 * n) * ln (real (40 * n)) + 200 * real (40 * n)) / real (40 * n) ^ 2 ≤
ε / 2"
by (rule error_term_small) (use assms in simp)
have C: "∀⇩F n in at_top. (0 :: nat) < n" by (rule eventually_gt_at_top)
from A B C show ?thesis
proof eventually_elim
case (elim n)
have hK: "40 dvd 40 * n" "0 < 40 * n" using elim by simp_all
have K0: "0 < real (40 * n)" using elim by simp
have Fpos: "0 < real_eval (FK (40 * n)) zeta5"
and Flog: "ln (real_eval (FK (40 * n)) zeta5)
≤ of_rat Ubar * real (40 * n) ^ 2 + 24 * real (40 * n) * ln (real (40 * n)) + 200 *
real (40 * n)"
using log_FK_zeta5_bound[OF hK] by blast+
have ne: "mKM (40 * n) M ≠ 0" "real_eval (FK (40 * n)) zeta5 ≠ 0"
using mKM_pos[of "40 * n" M] Fpos by auto
have "ln (real_eval (QKM (40 * n) M) zeta5) =
ln (of_rat (mKM (40 * n) M)) + ln (real_eval (FK (40 * n)) zeta5)"
unfolding real_eval_QKM by (simp add: ln_mult ne)
hence eq1: "ln (real_eval (QKM (40 * n) M) zeta5) / real (40 * n) ^ 2 =
ln (of_rat (mKM (40 * n) M)) / real (40 * n) ^ 2 + ln (real_eval (FK (40 * n)) zeta5) /
real (40 * n) ^ 2"
by (simp add: add_divide_distrib)
have "ln (real_eval (FK (40 * n)) zeta5) / real (40 * n) ^ 2
≤ (of_rat Ubar * real (40 * n) ^ 2 + 24 * real (40 * n) * ln (real (40 * n)) + 200 *
real (40 * n)) / real (40 * n) ^ 2"
by (intro divide_right_mono Flog) simp
also have "… = of_rat Ubar + (24 * real (40 * n) * ln (real (40 * n)) + 200 * real (40 *
n)) / real (40 * n) ^ 2"
using K0 by (simp add: add_divide_distrib)
finally show ?case using elim eq1 by linarith
qed
qed
text ‹(2.7): @{text "0 < Q_{40n,200}(ζ(5)) < exp(-139n^2/5)"}
for all large @{text n}.›
theorem QKM_zeta5_decay:
"∀⇩F n in at_top.
0 < real_eval (QKM (40 * n) 200) zeta5 ∧
real_eval (QKM (40 * n) 200) zeta5 < exp (- (139 / 5 * real n ^ 2))"
proof -
define dq :: rat where "dq = 3089837638249482469 / 58872425992515135000"
have dpos: "0 < (of_rat dq :: real)" by (simp add: dq_def of_rat_divide)
have A: "∀⇩F n in at_top. ln (real_eval (QKM (40 * n) 200) zeta5) / real (40 *
n) ^ 2
≤ of_rat (AM 200) + of_rat Ubar + of_rat dq / 3200"
by (rule log_QKM_zeta5_limsup) (use dpos in simp_all)
from A eventually_ge_at_top[of "200000 :: nat"] show ?thesis
proof eventually_elim
case (elim n)
have h: "StdHyp (40 * n) 200" using elim by (auto simp: StdHyp_def)
have pos: "0 < real_eval (QKM (40 * n) 200) zeta5" using QKM_int_degree_pos[OF h] by blast
have n0: "0 < real n" using elim by simp
have K2: "real (40 * n) ^ 2 = 1600 * real n ^ 2" by (simp add: power_mult_distrib)
have "ln (real_eval (QKM (40 * n) 200) zeta5)
≤ (of_rat (AM 200) + of_rat Ubar + of_rat dq / 3200) * real (40 * n) ^ 2"
using elim by (subst (asm) pos_divide_le_eq) simp_all
also have "… = (of_rat (AM 200) + of_rat Ubar + of_rat dq / 3200) * (1600 * real n ^ 2)"
by (simp add: K2)
also have "… = (- (139 / 5) - of_rat dq / 2) * real n ^ 2"
proof -
have c: "(of_rat (AM 200) + of_rat Ubar + of_rat dq / 3200) * 1600 =
- (139 / 5) - (of_rat dq :: real) / 2"
unfolding dq_def AM_def Astar_def lam_q_def Ubar_def
by (simp add: of_rat_divide of_rat_add of_rat_diff of_rat_minus of_rat_mult)
show ?thesis by (subst mult.assoc[symmetric], subst c, rule refl)
qed
also have "… < - (139 / 5 * real n ^ 2)"
proof -
have "0 < of_rat dq / 2 * real n ^ 2" using dpos n0 by simp
thus ?thesis by (simp add: algebra_simps)
qed
finally have "ln (real_eval (QKM (40 * n) 200) zeta5) < - (139 / 5 * real n ^ 2)" .
hence "real_eval (QKM (40 * n) 200) zeta5 < exp (- (139 / 5 * real n ^ 2))"
using pos by (metis exp_less_cancel_iff exp_ln)
thus ?case using pos by simp
qed
qed
text ‹The abstract top-level argument:
if integer polynomials @{text "Q_n"} of degree at most @{text "dn"}
satisfy @{text "0 < Q_n(x) < exp(-cn^2)"} for large @{text n}, then @{text x} is irrational
(@{text "b^{dn} Q_n(a/b)"} is a positive integer that is eventually @{text "< 1"}).›
theorem irrational_of_int_poly_approx:
fixes x c :: real and Qs :: "nat ⇒ int poly"
assumes c: "0 < c" and deg: "⋀n. degree (Qs n) ≤ d * n"
and ev: "∀⇩F n in at_top. 0 < poly (map_poly of_int (Qs n)) x ∧
poly (map_poly of_int (Qs n)) x < exp (- (c * real n ^ 2))"
shows "x ∉ ℚ"
proof
assume "x ∈ ℚ"
then obtain a b where b: "b > 0" and x: "x = of_int a / of_int b" by (rule Rats_cases')
have b1: "(1::real) ≤ of_int b" using b by simp
define N where "N = nat ⌈real d * ln (of_int b) / c⌉"
have "∀⇩F n in at_top. N ≤ n" by (rule eventually_ge_at_top)
from this ev have "∀⇩F n in at_top. N ≤ n ∧
(0 < poly (map_poly of_int (Qs n)) x ∧
poly (map_poly of_int (Qs n)) x < exp (- (c * real n ^ 2)))" by (rule eventually_conj)
then obtain M where M: "∀n ≥ M. N ≤ n ∧
(0 < poly (map_poly of_int (Qs n)) x ∧
poly (map_poly of_int (Qs n)) x < exp (- (c * real n ^ 2)))"
by (auto simp: eventually_at_top_linorder)
define n where "n = M"
have n: "N ≤ n" and pos: "0 < poly (map_poly of_int (Qs n)) x"
and lt: "poly (map_poly of_int (Qs n)) x < exp (- (c * real n ^ 2))"
using M by (auto simp: n_def)
define Q where "Q = (map_poly of_int (Qs n) :: real poly)"
have Qcoeff: "Polynomial.coeff Q i ∈ ℤ" for i by (simp add: Q_def coeff_map_poly)
have ne: "poly Q (of_int a / of_int b) ≠ 0" using pos by (simp add: Q_def x)
have "1 / of_int b ^ degree Q ≤ ¦poly Q (of_int a / of_int b)¦"
using int_poly_rat_no_root_ge[OF Qcoeff b ne] by simp
also have "¦poly Q (of_int a / of_int b)¦ = poly Q x" using pos by (simp add: Q_def x)
finally have lower: "1 / of_int b ^ degree Q ≤ poly Q x" .
have "(of_int b :: real) ^ degree Q ≤ of_int b ^ (d * n)"
using b1 deg[of n] by (intro power_increasing) (simp_all add: Q_def degree_map_poly)
hence lower': "(1 :: real) / of_int b ^ (d * n) ≤ 1 / of_int b ^ degree Q"
using b by (intro divide_left_mono) (auto intro!: mult_pos_pos)
have "real d * ln (of_int b) / c ≤ real N" by (simp add: N_def real_nat_ceiling_ge)
also have "… ≤ real n" using n by simp
finally have "real d * ln (of_int b) ≤ c * real n" using c by (simp add: field_simps)
hence "real d * ln (of_int b) * real n ≤ c * real n * real n"
by (intro mult_right_mono) simp_all
hence "exp (- (c * real n ^ 2)) ≤ exp (- (real d * ln (of_int b) * real n))"
by (simp add: power2_eq_square)
also have e: "exp (real d * ln (of_int b) * real n) = (of_int b :: real) ^ (d * n)"
proof -
have "exp (real d * ln (of_int b) * real n) = exp (real (d * n) * ln (of_int b))"
by (simp add: algebra_simps)
also have "… = exp (ln (of_int b)) ^ (d * n)" by (rule exp_of_nat_mult)
also have "… = of_int b ^ (d * n)" using b by simp
finally show ?thesis .
qed
have "exp (- (real d * ln (of_int b) * real n)) = (1 :: real) / of_int b ^ (d * n)"
by (simp add: exp_minus e inverse_eq_divide)
finally have upper: "exp (- (c * real n ^ 2)) ≤ (1 :: real) / of_int b ^ (d * n)" .
show False using lower lower' lt upper unfolding Q_def by linarith
qed
text ‹@{text "ζ(5)"} is real: its Dirichlet series has real terms
(@{text "Zeta_Function.sums_zeta_nat"}).›
lemma zeta5_real: "zeta 5 ∈ ℝ"
proof -
have "(λk. Im (1 / of_nat (Suc k) ^ 5 :: complex)) sums Im (zeta 5)"
using sums_zeta_nat[of 5] by (intro sums_Im) simp
moreover have "Im (1 / of_nat (Suc k) ^ 5 :: complex) = 0" for k
proof -
have "(1 / of_nat (Suc k) ^ 5 :: complex) = of_real (1 / real (Suc k) ^ 5)" by simp
thus ?thesis by (simp only:) simp
qed
ultimately have "(λk. 0 :: real) sums Im (zeta 5)" by simp
hence "Im (zeta 5) = 0" using sums_unique2 sums_zero by blast
thus ?thesis by (simp add: complex_is_Real_iff)
qed
lemma zeta5_eq: "zeta 5 = of_real zeta5"
unfolding zeta5_def using zeta5_real by simp
text ‹The integer polynomials @{text "Q_{40n,200}"} (and @{text 0}
for small @{text n}).›
definition Qint :: "nat ⇒ int poly" where
"Qint n = (if StdHyp (40 * n) 200 then (SOME P. map_poly of_int P = QKM (40 * n) 200) else 0)"
lemma Qint_spec:
assumes "StdHyp (40 * n) 200"
shows "map_poly of_int (Qint n) = QKM (40 * n) 200"
using assms someI_ex[OF conjunct1[OF QKM_int_degree_pos[OF assms]]] by (simp add: Qint_def)
text ‹Theorem 1.1 for the real number zeta5.›
theorem zeta5_irrational_real: "zeta5 ∉ ℚ"
proof (rule irrational_of_int_poly_approx[where c = "139 / 5" and d = 37 and Qs = Qint])
show "0 < (139 / 5 :: real)" by simp
show "degree (Qint n) ≤ 37 * n" for n
proof (cases "StdHyp (40 * n) 200")
case True
have "degree (QKM (40 * n) 200) = hof (40 * n)" using QKM_int_degree_pos[OF True] by blast
moreover have "degree (map_poly of_int (Qint n) :: rat poly) = degree (Qint n)"
by (rule degree_map_poly) simp
ultimately show ?thesis using Qint_spec[OF True] by (simp add: hof_def)
next
case False
thus ?thesis by (simp add: Qint_def)
qed
show "∀⇩F n in at_top. 0 < poly (map_poly of_int (Qint n)) zeta5 ∧
poly (map_poly of_int (Qint n)) zeta5 < exp (- (139 / 5 * real n ^ 2))"
proof -
have "∀⇩F n in at_top. (200000 :: nat) ≤ n" by (rule eventually_ge_at_top)
with QKM_zeta5_decay show ?thesis
proof eventually_elim
case (elim n)
hence h: "StdHyp (40 * n) 200" by (auto simp: StdHyp_def)
have "real_eval (QKM (40 * n) 200) zeta5 = poly (map_poly of_int (Qint n)) zeta5"
unfolding Qint_spec[OF h, symmetric] real_eval_def
by (simp add: map_poly_map_poly o_def)
thus ?case using elim by simp
qed
qed
qed
text ‹Theorem 1.1, stated for the AFP's zeta: @{text "ζ(5) ∉ ℚ"}.›
theorem zeta5_irrational: "zeta 5 ∉ ℚ"
using zeta5_irrational_real by (simp add: zeta5_eq)
corollary Re_zeta5_irrational: "Re (zeta 5) ∉ ℚ"
using zeta5_irrational_real by (simp add: zeta5_def)
text ‹Sanity check of the statement: @{text "zeta 5"} is the familiar series
@{text "∑_{n≥1} n^{-5}"}.›
lemma zeta5_series: "zeta 5 = (∑n. 1 / of_nat (Suc n) ^ 5)"
using zeta_nat_conv_suminf[of 5] by simp
end