Theory Transcendence_Series
section ‹The transcendence of certain infinite series›
theory "Transcendence_Series" imports
"HOL-Analysis.Multivariate_Analysis"
"HOL-Computational_Algebra.Polynomial"
Prime_Number_Theorem.Prime_Number_Theorem_Library
begin
text ‹
We formalise the proofs of two transcendence criteria by J. Han\v{c}l and P. Rucki that
assert the transcendence of the sums of certain infinite series built up by sequences that
fulfil certain properties (Theorems 2.1 and 2.2 in \<^cite>‹"hancl2005"›, HanclRucki1 and HanclRucki2
here respectively). Both proofs make use of Roth's celebrated theorem on diophantine approximations
to algebraic numbers from 1955 \<^cite>‹"roth_1955"› which we assume and implement within the locale
RothsTheorem.
A small mistake was detected in the original proof of Theorem 2.1, and the authors gave us a fix for the problem (by email).
Our formalised proof incorporates this correction (see the Remark in the proof of HanclRucki1).
›
subsection ‹Misc›
lemma powr_less_inverse_iff:
fixes x y z::real
assumes "x>0" "y>0" "z>0"
shows "x powr y < z ⟷ x < z powr (inverse y)"
proof
assume "x powr y < z"
from powr_less_mono2[OF _ _ this,of "inverse y"]
show "x < z powr inverse y"
using assms by (auto simp:powr_powr)
next
assume *:"x < z powr inverse y"
from powr_less_mono2[OF _ _ *,of y] show "x powr y < z"
using assms by (auto simp:powr_powr)
qed
lemma powr_less_inverse_iff':
fixes x y z::real
assumes "x>0" "y>0" "z>0"
shows "z< x powr y ⟷ z powr (inverse y) < x"
using powr_less_inverse_iff[symmetric,of _ "inverse y"] assms by auto
lemma powr_less_eq_inverse_iff:
fixes x y z::real
assumes "x>0" "y>0" "z>0"
shows "x powr y ≤ z ⟷ x ≤ z powr (inverse y)"
by (meson assms not_less powr_less_inverse_iff')
lemma powr_less_eq_inverse_iff':
fixes x y z::real
assumes "x>0" "y>0" "z>0"
shows "z ≤ x powr y ⟷ z powr (inverse y) ≤ x"
by (simp add: assms powr_less_eq_inverse_iff)
lemma tendsto_PInfty_mono:
assumes "(ereal o f) ⇢ ∞" "∀⇩F x in sequentially. f x ≤ g x"
shows "(ereal o g) ⇢ ∞"
using assms unfolding comp_def tendsto_PInfty_eq_at_top
by (elim filterlim_at_top_mono, simp)
lemma limsup_infinity_imp_Inf_many:
assumes "limsup f = ∞"
shows "(∀ m. (∃⇩∞i. f i > ereal m))" unfolding INFM_nat
proof (clarify,rule ccontr)
fix m k assume "¬ (∃n>k. ereal m < f n)"
then have "∀n>k. f n ≤ ereal m" by auto
then have "∀⇩F n in sequentially. f n ≤ ereal m"
using eventually_at_top_dense by blast
then have "limsup f ≤ ereal m" using Limsup_bounded by auto
then show False using assms by simp
qed
lemma snd_quotient_plus_leq:
defines "de≡(snd o quotient_of)"
shows "de (x+y) ≤ de x * de y "
proof -
obtain x1 x2 y1 y2 where xy: "quotient_of x = (x1,x2)" "quotient_of y=(y1,y2)"
by (meson surj_pair)
have "x2>0" "y2>0" using xy quotient_of_denom_pos by blast+
then show ?thesis
unfolding de_def comp_def rat_plus_code xy
apply (auto split:prod.split simp:Rat.normalize_def Let_def)
by (smt div_by_1 gcd_pos_int int_div_less_self mult_eq_0_iff mult_sign_intros(1))
qed
lemma quotient_of_inj: "inj quotient_of"
unfolding inj_def by (simp add: quotient_of_inject)
lemma infinite_inj_imageE:
assumes "infinite A" "inj_on f A" "f ` A ⊆ B"
shows "infinite B"
using assms inj_on_finite by blast
lemma incseq_tendsto_limsup:
fixes f::"nat ⇒ 'a::{complete_linorder,linorder_topology}"
assumes "incseq f"
shows "f ⇢ limsup f"
using LIMSEQ_SUP assms convergent_def convergent_ereal tendsto_Limsup
trivial_limit_sequentially by blast
subsection ‹Main proofs›
text ‹Since the proof of Roth's theorem has not been formalized yet, we formalize the statement in a locale
and use it as an assumption.›
locale RothsTheorem =
assumes RothsTheorem:"∀ξ κ. algebraic ξ ∧ ξ ∉ ℚ ∧ infinite {(p,q). q>0 ∧
coprime p q ∧ ¦ξ - of_int p / of_int q¦ < 1 / q powr κ} ⟶ κ ≤ 2"
theorem (in RothsTheorem) HanclRucki1:
fixes a b ::"nat⇒int" and δ ::real
defines "aa≡(λn. real_of_int (a n))" and "bb≡(λn. real_of_int (b n))"
assumes a_pos:"∀ k. a k >0" and b_pos:"∀ k. b k >0" and "δ >0"
and limsup_infy:"limsup (λ k. aa (k+1)/(∏i = 0..k. aa i)powr(2+δ)*(1/bb (k+1))) = ∞"
and liminf_1:"liminf (λk. aa (k+1) / aa k * bb k / bb (k+1)) > 1"
shows "¬ algebraic(suminf (λ k. bb k / aa k))"
proof -
have summable:"summable (λ k. bb k / aa k)"
proof (rule ratio_test_convergence)
have [simp]:"aa k>0" "bb k>0" for k
unfolding aa_def bb_def using a_pos b_pos by auto
show "∀⇩F n in sequentially. 0 < bb n / aa n"
by auto
show "1 < liminf (λn. ereal (bb n / aa n / (bb (Suc n) / aa (Suc n))))"
using liminf_1 by (auto simp:algebra_simps)
qed
have [simp]: "aa k>0" "bb k>0" for k unfolding aa_def bb_def
by (auto simp add: a_pos b_pos)
have ab_1:"aa k≥1" "bb k≥1" for k
unfolding aa_def bb_def using a_pos b_pos
by (auto simp add: int_one_le_iff_zero_less)
define B where "B ≡ liminf (λx. ereal (aa (x + 1) / aa x * bb x / bb (x + 1)))"
define M where "M ≡ (case B of ereal m ⇒ (m+1)/2 | _ ⇒ 2)"
have "M > 1" "M < B"
using liminf_1 unfolding M_def
by (auto simp add: M_def B_def split: ereal.split)
text ‹
Remark:
In the original proof of Theorem 2.1 in \<^cite>‹"hancl2005"›
it was claimed in p.534 that from assumption (3) (i.e. @{thm liminf_1}),
we obtain that:
$\forall A>1~\exists k_0~ \forall k > k_0~ \frac{1}{A} \frac{b_k}{ a_k} > \frac{ b_{k+1}}{ a_{k+1}} $,
however note the counterexample where
$a_{k+1}= k (a_1 a_2 ... a_k)^{\lceil 2+ \delta \rceil}$ if k is odd, and
$a_{k+1} = 2 a_k$ otherwise, with $b_k =1$ for all $k$.
In commmunication by email the authors suggested to replace the claim
$\forall A>1~\exists k_0~ \forall k > k_0~ \frac{1}{A} \frac{b_k}{ a_k} > \frac{ b_{k+1}}{ a_{k+1}} $
with
$\exists A>1~\exists k_0~ \forall k > k_0~ \frac{1}{A} \frac{b_k}{ a_k} > \frac{ b_{k+1}}{ a_{k+1}} $
which solves the problem and the proof proceeds as in the paper.
The witness for $\exists A>1 $ is denoted by $M$ here.›
have bb_aa_event:"∀⇩F k in sequentially. (1/M)*(bb k / aa k)> bb(k+1)/ aa (k+1)"
using less_LiminfD[OF ‹M < B›[unfolded B_def],simplified]
by eventually_elim (use ‹M > 1› in ‹auto simp: field_simps›)
have bb_aa_p:"∀⇩F k in sequentially. ∀p. bb(k+p)/ aa (k+p) ≤ (1/M^p)*(bb k / aa k)"
proof -
obtain k0 where k0_ineq:
"∀n≥k0. bb (n + 1) / aa (n + 1) < 1 / M * (bb n / aa n)"
using bb_aa_event unfolding eventually_sequentially
by auto
have "bb(k+p)/ aa (k+p) ≤ (1/M^p)*(bb k / aa k)" when "k≥k0" for p k
proof (induct p)
case 0
then show ?case by auto
next
case (Suc p)
have " bb (k + Suc p) / aa (k + Suc p) < 1 / M * (bb (k+p) / aa (k+p))"
using k0_ineq[rule_format,of "k+p"] that by auto
also have "... ≤ 1 / M ^(Suc p) * (bb k / aa k)"
using Suc ‹M>1› by (auto simp add:field_simps)
finally show ?case by auto
qed
then show ?thesis unfolding eventually_sequentially by auto
qed
define ξ where "ξ = suminf (λ k. bb k / aa k)"
have ξ_Inf_many:"∃⇩∞ k. ¦ξ - (∑k = 0..k. bb k / aa k)¦ < 1 / prod aa {0..k} powr (2 + δ)"
proof -
have "¦ξ - (∑i = 0..k. bb i / aa i)¦ = ¦∑i. bb (i+(k+1)) / aa (i+(k+1))¦" for k
unfolding ξ_def
apply (subst suminf_minus_initial_segment[of _ "k+1",OF summable])
using atLeast0AtMost lessThan_Suc_atMost by auto
moreover have "∃⇩∞ k. ¦∑i. bb(i+(k+1))/ aa (i+(k+1))¦
< 1 / prod aa {0..k} powr (2 + δ)"
proof -
define P where "P ≡ (λ i. ∀p. bb (i + 1 + p) / aa (i + 1 + p)
≤ 1 / M ^ p * (bb (i + 1) / aa (i + 1)))"
define Q where "Q ≡ (λ i. ereal (M / (M - 1))
< ereal (aa (i + 1) / prod aa {0..i} powr (2 + δ) * (1 / bb (i + 1))))"
have "∀⇩∞ i. P i"
using bb_aa_p[THEN sequentially_offset, of 1] cofinite_eq_sequentially
unfolding P_def by auto
moreover have "∃⇩∞i. Q i"
using limsup_infy[THEN limsup_infinity_imp_Inf_many,rule_format,of "(M / (M -1))"]
unfolding Q_def .
moreover have "¦∑i. bb(i+(k+1))/ aa (i+(k+1))¦
< 1 / prod aa {0..k} powr (2 + δ)"
when "P k" "Q k" for k
proof -
have summable_M:"summable (λi. 1 / M ^ i)"
apply (rule summable_ratio_test[of "1/M"])
using ‹M>1› by auto
have "(∑i. bb (i + (k + 1)) / aa (i + (k + 1))) ≥ 0"
apply (rule suminf_nonneg)
subgoal using summable_ignore_initial_segment[OF summable,of "k+1"] by auto
subgoal by (simp add: less_imp_le)
done
then have "¦∑i. bb (i + (k + 1)) / aa (i + (k + 1))¦
= (∑i. bb (i + (k + 1)) / aa (i + (k + 1)))"
by auto
also have "... ≤ (∑i. 1 / M ^ i * (bb (k + 1) / aa (k + 1)))"
apply (rule suminf_le)
subgoal using that(1) unfolding P_def by (auto simp add:algebra_simps)
subgoal using summable_ignore_initial_segment[OF summable,of "k+1"] by auto
subgoal using summable_mult2[OF summable_M,of " bb (k + 1) / aa (k + 1)"]
by auto
done
also have "... = (bb (k + 1) / aa (k + 1)) * (∑i. 1 / M ^ i)"
using suminf_mult2[OF summable_M,of " bb (k + 1) / aa (k + 1)"]
by (auto simp:algebra_simps)
also have "... = (bb (k + 1) / aa (k + 1)) * (∑i. (1 / M) ^ i)"
using ‹M>1› by (auto simp: field_simps)
also have "... = (bb (k + 1) / aa (k + 1)) * (M / (M -1))"
apply (subst suminf_geometric)
using ‹M>1› by (auto simp: field_simps)
also have "... < (bb (k + 1) / aa (k + 1)) * (aa (k + 1) /
prod aa {0..k} powr (2 + δ) * (1 / bb (k + 1)))"
apply (subst mult_less_cancel_left_pos)
using that(2) unfolding Q_def by auto
also have "... = 1/ prod aa {0..k} powr (2 + δ)"
using ab_1[of "Suc k"] by auto
finally show ?thesis .
qed
ultimately show ?thesis by (smt INFM_conjI INFM_mono)
qed
ultimately show ?thesis by auto
qed
define pq where "pq ≡ (λk. quotient_of (∑i=0..k. of_int (b i) / of_int (a i)))"
define p q where "p ≡ fst ∘ pq" and "q = snd ∘ pq"
have coprime_pq:"coprime (p k) (q k)"
and q_pos:"q k > 0" and pq_sum:"p k / q k = (∑i=0..k. b i / a i)" for k
proof -
have eq: "quotient_of (∑i=0..k. of_int (b i) / of_int (a i)) = (p k, q k)"
by (simp add: p_def q_def pq_def)
from quotient_of_coprime[OF eq] show "coprime (p k) (q k)" .
from quotient_of_denom_pos[OF eq] show "q k > 0" .
have "(∑i=0..k. b i / a i) = of_rat (∑i=0..k. of_int (b i) / of_int (a i))"
by (simp add: of_rat_sum of_rat_divide)
also have "(∑i=0..k. rat_of_int (b i) / rat_of_int (a i)) =
rat_of_int (p k) / rat_of_int (q k)"
using quotient_of_div[OF eq] by simp
finally show "p k / q k = (∑i=0..k. b i / a i)" by (simp add:of_rat_divide)
qed
have ξ_Inf_many2:"∃⇩∞ k. ¦ξ - p k / q k¦ < 1 / q k powr (2 + δ)"
using ξ_Inf_many
proof (elim INFM_mono)
fix k assume asm:"¦ξ - (∑k = 0..k. bb k / aa k)¦ < 1 / prod aa {0..k} powr (2 + δ)"
have "¦ξ - real_of_int (p k) / real_of_int (q k)¦
= ¦ξ - (∑k = 0..k. bb k / aa k)¦"
using pq_sum unfolding aa_def bb_def by auto
also have "... < 1 / prod aa {0..k} powr (2 + δ)"
using asm by auto
also have "... ≤ 1 / q k powr (2 + δ)"
proof -
have "q k ≤ prod aa {0..k}"
proof (induct k)
case 0
then show ?case unfolding q_def pq_def aa_def
apply (simp add:rat_divide_code of_int_rat quotient_of_Fract)
using ab_1[of 0,unfolded aa_def bb_def] unfolding Let_def normalize_def
apply auto
by (metis div_by_1 gcd_pos_int less_imp_le less_trans nonneg1_imp_zdiv_pos_iff
not_less zdiv_mono2)
next
case (Suc k)
define de where "de ≡snd ∘ quotient_of"
have "real_of_int (q (Suc k))
= de (∑i=0..Suc k. of_int (b i) / of_int (a i))"
unfolding q_def pq_def de_def by simp
also have "... = de ((∑i=0..k. of_int (b i) / of_int (a i))
+ of_int (b (Suc k)) / of_int (a (Suc k)))"
by simp
also have "... ≤ de (∑i=0..k. of_int (b i) / of_int (a i))
* de (of_int (b (Suc k)) / of_int (a (Suc k)))"
using snd_quotient_plus_leq[folded de_def] by presburger
also have "... = q k * de (of_int (b (Suc k)) / of_int (a (Suc k)))"
unfolding q_def pq_def de_def by auto
also have "... = q k * snd (Rat.normalize (b (Suc k), a (Suc k)))"
by (simp add:rat_divide_code of_int_rat quotient_of_Fract de_def)
also have "... ≤ q k * aa (Suc k)"
using ab_1[of "Suc k"] q_pos[of "k"]
unfolding normalize_def aa_def bb_def Let_def
apply auto
by (metis div_by_1 int_one_le_iff_zero_less less_trans
nonneg1_imp_zdiv_pos_iff not_less zdiv_mono2 zero_less_one)
also have "... ≤ prod aa {0..k} * aa (Suc k)"
using Suc ab_1[of "Suc k"] by auto
also have "... = prod aa {0..Suc k}"
by (simp add: prod.atLeast0_atMost_Suc)
finally show ?case .
qed
then show ?thesis
by (smt ‹0 < δ› frac_le of_int_0 of_int_le_iff powr_gt_zero
powr_mono2 q_pos)
qed
finally show "¦ξ - real_of_int (p k) / real_of_int (q k)¦ < 1 / real_of_int (q k) powr (2 + δ)" .
qed
define pqs where "pqs ≡{(p, q). q>0 ∧ coprime p q
∧ ¦ξ - real_of_int p / real_of_int q¦ < 1 / q powr (2 + δ)}"
have ξ_infinite:"infinite pqs"
proof -
define A where "A ≡ {k. ¦ξ - (p k) / (q k)¦ < 1 / (q k) powr (2 + δ)}"
have "∃⇩∞ k. ¦ξ - p k / q k¦ < 1 / q k powr (2 + δ)"
using ξ_Inf_many2 .
then have "infinite A"
unfolding Inf_many_def A_def by auto
moreover have "inj_on (λk. (p k, q k)) A"
proof -
define g where "g ≡ (λi. rat_of_int (b i) / rat_of_int (a i))"
define f where "f ≡ (λk. ∑i = 0..k. g i)"
have g_pos:"g i>0" for i
unfolding g_def by (simp add: a_pos b_pos)
have "strict_mono f" unfolding strict_mono_def f_def
proof safe
fix x y::nat assume "x < y"
then have "sum g {0..y} - sum g {0..x} = sum g {x<..y}"
apply (subst Groups_Big.sum_diff[symmetric])
by (auto intro:arg_cong2[where f=sum])
also have "... > 0"
apply (rule ordered_comm_monoid_add_class.sum_pos)
using ‹x<y› g_pos by auto
finally have "sum g {0..y} - sum g {0..x} >0" .
then show "sum g {0..x} < sum g {0..y}" by auto
qed
then have "inj f" using strict_mono_imp_inj_on by auto
then have "inj (quotient_of o f)" by (simp add: inj_compose quotient_of_inj)
then have "inj (λk. (p k, q k))"
unfolding f_def p_def q_def pq_def comp_def
apply (fold g_def)
by auto
then show ?thesis by (auto elim:subset_inj_on)
qed
moreover have "(λk. (p k, q k)) ` A ⊆ pqs"
unfolding A_def pqs_def using coprime_pq q_pos by auto
ultimately show ?thesis
apply (elim infinite_inj_imageE)
by auto
qed
moreover have "finite pqs" if "ξ ∈ ℚ"
proof -
obtain m n where ξ_mn:"ξ = (of_int m / of_int n)" and "coprime m n" "n>0"
proof -
obtain m n where mn:"¦ξ¦ = (of_nat m / of_nat n)" "coprime m n" "n≠0"
using Rats_abs_nat_div_natE[OF ‹ξ ∈ ℚ› Rats_abs_nat_div_natE]
by metis
define m' and n'::int
where "m'=(if ξ > 0 then nat m else -nat m)" and "n'=nat n"
then have "ξ = (of_int m' / of_int n')" "coprime m' n'" "n'>0"
using mn by auto
then show ?thesis using that by auto
qed
have "pqs ⊆ {(m,n)} ∪ {x. x ∈pqs ∧ - ¦m¦ - 1 ≤fst x ∧ fst x ≤ ¦m¦ + 1 ∧ 0<snd x ∧ snd x < n }"
proof (rule subsetI)
fix x assume "x ∈ pqs"
define p q where "p ≡ fst x" and "q=snd x"
have "q>0" "coprime p q" and pq_less:"¦ξ - p / q¦ < 1 / q powr (2 + δ)"
using ‹x∈pqs› unfolding p_def q_def pqs_def by auto
have q_lt_n:"q<n" when "m≠p ∨ n≠q"
proof -
have "m * q ≠ n * p" using that ‹coprime m n› ‹coprime p q› ‹q>0› ‹n>0›
by (metis eq_rat(1) fst_conv int_one_le_iff_zero_less mult.commute normalize_stable
not_one_le_zero quotient_of_Fract snd_conv)
then have "1/(n*q) ≤ ¦m/n - p/q¦"
using ‹q>0› ‹n>0›
apply (auto simp:field_simps)
by (metis add_diff_cancel_left' diff_diff_eq2 diff_zero less_irrefl not_le of_int_diff
of_int_lessD of_int_mult)
also have "... < 1 / q powr (2 + δ)"
using pq_less unfolding ξ_mn by auto
also have "... ≤ 1 / q ^2"
proof -
have "real_of_int (q⇧2) = q powr 2"
apply (subst powr_numeral)
unfolding power2_eq_square using ‹q>0› by auto
also have "... ≤ q powr (2 + δ)"
apply (rule powr_mono)
using ‹q>0› ‹δ>0› by auto
finally have "real_of_int (q⇧2) ≤ real_of_int q powr (2 + δ)" .
moreover have "real_of_int q powr (2 + δ) > 0" using ‹0 < q› by auto
ultimately show ?thesis by (auto simp:field_simps)
qed
finally have " 1 / (n * q) < 1 / q⇧2" .
then show ?thesis using ‹q>0› ‹n>0›
unfolding power2_eq_square by (auto simp:field_simps)
qed
moreover have "- ¦m¦ - 1 ≤ p ∧ p ≤ ¦m¦ + 1" when "m≠p ∨ n≠q"
proof -
define qn where "qn ≡ q/n"
have "0<qn" "qn<1" unfolding qn_def using q_lt_n[OF ‹m≠p ∨ n≠q›] ‹q>0› by auto
have "¦m/n - p / q¦ < 1 / q powr (2 + δ)" using pq_less unfolding ξ_mn by simp
then have "¦p / q - m/n¦ < 1 / q powr (2 + δ)" by simp
then have " m/n- 1 / q powr (2 + δ) < p/q ∧ p/q < m/n + 1 / q powr (2 + δ)"
unfolding abs_diff_less_iff by auto
then have "qn*m- q / q powr (2 + δ) < p ∧ p < qn*m + q / q powr (2 + δ)"
unfolding qn_def using ‹q>0› by (auto simp:field_simps)
moreover have "- ¦m¦ - 1 ≤ qn*m- q / q powr (2 + δ)"
proof -
have "- ¦m¦ ≤ qn*m" using ‹0<qn› ‹qn<1›
apply (cases "m≥0")
subgoal
apply simp
by (meson less_eq_real_def mult_nonneg_nonneg neg_le_0_iff_le of_int_0_le_iff order_trans)
subgoal by simp
done
moreover have "- 1 ≤ - q / q powr (2 + δ)"
proof -
have "q = q powr 1" using ‹0 < q› by auto
also have "... ≤q powr (2 + δ)"
apply (rule powr_mono)
using ‹q>0› ‹δ>0› by auto
finally have "q ≤ q powr (2 + δ)" .
then show ?thesis using ‹0 < q› by auto
qed
ultimately show ?thesis by auto
qed
moreover have "qn*m + q / q powr (2 + δ) ≤ ¦m¦ + 1"
proof -
have "qn*m ≤ ¦m¦" using ‹0<qn› ‹qn<1›
apply (cases "m≥0")
subgoal by (simp add: mult_left_le_one_le)
subgoal by (smt of_int_0_le_iff zero_le_mult_iff)
done
moreover have "q / q powr (2 + δ) ≤ 1"
proof -
have "q = q powr 1" using ‹0 < q› by auto
also have "... ≤q powr (2 + δ)"
apply (rule powr_mono)
using ‹q>0› ‹δ>0› by auto
finally have "q ≤ q powr (2 + δ)" .
then show ?thesis using ‹0 < q› by auto
qed
ultimately show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
ultimately show "x ∈ {(m, n)} ∪ {x ∈ pqs. - ¦m¦ - 1 ≤ fst x ∧ fst x ≤ ¦m¦ + 1
∧ 0 < snd x ∧ snd x < n}"
using ‹x ∈ pqs› ‹q>0› unfolding p_def q_def by force
qed
moreover have "finite {x. x ∈pqs ∧ - ¦m¦ - 1 ≤fst x ∧ fst x ≤ ¦m¦ + 1 ∧ 0<snd x ∧ snd x < n }"
proof -
have "finite ({- ¦m¦ - 1..¦m¦ +1} × {0<..<n})" by blast
moreover have "{x. x ∈pqs ∧ - ¦m¦ - 1 ≤fst x ∧ fst x ≤ ¦m¦ + 1 ∧ 0<snd x ∧ snd x < n } ⊆
({- ¦m¦ - 1..¦m¦ +1} × {0<..<n})"
by auto
ultimately show ?thesis
apply (elim rev_finite_subset)
by blast
qed
ultimately show ?thesis using finite_subset by auto
qed
ultimately show ?thesis
apply (fold ξ_def)
using RothsTheorem[rule_format,of ξ "2 + δ",folded pqs_def] ‹δ >0› by auto
qed
theorem (in RothsTheorem) HanclRucki2:
fixes a b ::"nat⇒int" and δ ε ::real
defines "aa≡(λn. real_of_int (a n))" and "bb≡(λn. real_of_int (b n))"
assumes a_pos:"∀ k. a k >0" and b_pos:"∀ k. b k >0" and "δ >0"
and "ε >0"
and limsup_infi:"limsup (λ k.(aa (k+1)/(∏i = 0..k. aa i)powr(2+(2/ε) + δ))
* (1/(bb (k+1)))) = ∞"
and ratio_large:"∀ k. ( k ≥ t ⟶ (( aa(k+1)/bb( k+1)) ) powr(1/(1+ε))
≥ (( aa k/bb k) powr(1/(1+ε)))+1)"
shows "¬ algebraic(suminf (λ k. bb k /aa k)) "
proof-
have aa_bb_pos[simp]:"aa k>0" "bb k>0" for k
unfolding aa_def bb_def using a_pos b_pos by auto
have summable:"summable (λ k. bb k / aa k)"
proof -
define c0 where "c0≡(aa t/bb t) powr(1/(1+ε)) - t"
have ab_k:"(aa k / bb k) powr(1/(1+ε)) ≥ k + c0" when "k≥t" for k
using that
proof (induct k)
case 0
then show ?case unfolding c0_def by simp
next
case (Suc k)
have ?case when "¬ t≤k"
proof -
have "t = Suc k" using that Suc.prems by linarith
then show ?thesis unfolding c0_def by auto
qed
moreover have ?case when "t ≤ k"
proof -
have "(aa(k+1)/bb(k+1)) powr(1/(1+ε))
≥ ( aa k/bb k) powr(1/(1+ε))+1"
using ratio_large[rule_format,OF that] by blast
then show ?thesis using Suc(1)[OF that] by simp
qed
ultimately show ?case by auto
qed
have "summable (λk. 1 / (k + c0) powr (1+ε))"
proof -
have "c0 + t > 0" unfolding c0_def
using aa_bb_pos[of t] by (simp,linarith)
then have "summable (λk. 1 / (k + (c0+t)) powr (1+ε))"
using summable_hurwitz_zeta_real[of "1+ε" "c0+t"]
apply (subst (asm) powr_minus_divide)
using ‹ε>0› by auto
then show ?thesis
apply (rule_tac summable_offset[of _ t])
by (auto simp:algebra_simps)
qed
moreover have "bb k / aa k ≤ 1 / (k + c0) powr (1+ε)" when "k≥t" for k
proof -
have "(aa t / bb t) powr (1 / (1 + ε)) > 0"
apply simp
by (metis ‹⋀k. 0 < aa k› ‹⋀k. 0 < bb k› less_numeral_extra(3))
then have "k + c0 >0" unfolding c0_def using that by linarith
then have "aa k / bb k ≥ (k + c0) powr (1+ε)"
using ab_k[OF that]
apply (subst (asm) powr_less_eq_inverse_iff')
using ‹ε >0› by auto
then have "inverse (aa k / bb k) ≤ inverse ((k + c0) powr (1+ε))"
apply (elim le_imp_inverse_le)
using ‹k + c0 >0› by auto
then show ?thesis by (simp add: inverse_eq_divide)
qed
ultimately show ?thesis
apply (elim summable_comparison_test'[where N=t])
using aa_bb_pos by (simp add: less_eq_real_def)
qed
have 7:"∃⇩∞ k. 1 / (M powr (ε/(1+ε)) * (∏i = 0..k. aa i)
powr(2+ δ * ε / (1+ε))) > (bb (k+1) / aa(k+1)) powr (ε / (1+ε))"
when "M > 0" for M
proof -
define tt where "tt ≡ (λi. prod aa {0..i} powr (2 + 2 / ε + δ))"
have tt_pos:"tt i > 0" for i
unfolding tt_def
apply(subst powr_gt_zero,induct i)
subgoal by (metis aa_bb_pos(1) order_less_irrefl prod_pos)
subgoal by (metis ‹⋀k. 0 < aa k› order_less_irrefl prod_pos)
done
have "∃⇩∞i. M < (aa (i + 1) / tt i * (1 / bb (i + 1)))"
using limsup_infinity_imp_Inf_many[OF limsup_infi,rule_format,of M]
unfolding tt_def by auto
then have "∃⇩∞i. 1 / (M * tt i) > (bb (i+1) / aa (i+1))"
apply (elim INFM_mono)
using ‹M>0› tt_pos by (auto simp:divide_simps algebra_simps)
then have "∃⇩∞i. (1 / (M * tt i)) powr (ε/(1+ε))
> (bb (i+1) / aa (i+1)) powr (ε/(1+ε))"
apply (elim INFM_mono powr_less_mono2[rotated 2])
by (simp_all add: assms(6) pos_add_strict less_eq_real_def)
moreover have "tt i powr (ε/(1+ε)) = prod aa {0..i} powr (2 + δ * ε / (1+ε))"
for i
unfolding tt_def
apply (auto simp:powr_powr)
using ‹ε>0› by (simp add:divide_simps,simp add:algebra_simps)
ultimately show ?thesis
apply (elim INFM_mono)
by (smt nonzero_mult_div_cancel_left powr_divide powr_mult powr_one_eq_one
that tt_pos zero_less_divide_iff)
qed
have 8:"∀⇩F k in sequentially. ∀s. (( aa(k+s)/bb( k+s))) ≥
((( aa k/bb k) powr(1/(1+ε))) +s)powr(1+ε)"
using eventually_ge_at_top[of t]
proof eventually_elim
case (elim k)
define ff where "ff ≡ (λk. (aa k / bb k) powr (1 / (1 + ε)))"
have 11:"ff k+s ≤ ff (k+s)" for s
proof (induct s)
case 0
then show ?case unfolding ff_def by auto
next
case (Suc s)
then have "ff k + Suc s ≤ ff (k+Suc s)"
using ratio_large[rule_format,of "k+s"] ‹ t ≤ k› unfolding ff_def by auto
then show ?case by simp
qed
then have "(ff k+s) powr (1+ε) ≤ ff (k+s) powr (1+ε)" for s
apply (rule powr_mono2[of "1+ε",rotated 2])
unfolding ff_def using ‹ε>0› by auto
then show ?case unfolding ff_def using ‹ε>0›
apply (auto simp add:powr_powr)
by (simp add: a_pos aa_def b_pos bb_def le_less)
qed
have 9: "(∑r. 1/((z+real r)powr(1+ε))) ≤ 1/(ε *(z-1) powr ε)"
"summable (λi. 1/((z+ real i)powr(1+ε)))"
when "z>1" for z
proof -
define f where "f ≡ (λr. 1/((z+ r)powr(1+ε)))"
have "((λx. f (x - 1)) has_integral ((z-1) powr - ε) / ε) {0..}"
proof -
have "((λx. (z-1 + x) powr (- 1 - ε)) has_integral ((z-1) powr - ε) / ε) {0<..}"
using powr_has_integral_at_top[of 0 "z-1" "- 1 - ε",simplified] ‹z>1› ‹ε>0›
by auto
then have "((λx. (z-1 + x) powr (- 1 - ε)) has_integral ((z-1) powr - ε) / ε) {0..}"
apply (subst (asm) has_integral_closure[symmetric])
by (auto simp add: negligible_convex_frontier)
then show ?thesis
apply (rule has_integral_cong[THEN iffD1, rotated 1])
unfolding f_def by (smt powr_minus_divide)
qed
moreover have "⋀x. 0 ≤ x ⟹ 0 ≤ f (x - 1)" unfolding f_def by simp
moreover have "⋀x y. 0 ≤ x ⟹ x ≤ y ⟹ f (y - 1) ≤ f (x - 1)" unfolding f_def
by (smt assms(6) frac_le powr_mono2 powr_nonneg_iff that)
ultimately have "summable (λi. f (real i))" "(∑i. f (real i)) ≤ (z - 1) powr - ε / ε"
using decreasing_sum_le_integral[of "λx. f (x-1)" "((z-1) powr - ε) / ε",simplified]
by auto
moreover have "(z - 1) powr - ε / ε = 1/(ε *(z-1) powr ε)"
by (simp add: powr_minus_divide)
ultimately show "(∑i. f (real i)) ≤ 1/(ε *(z-1) powr ε)" by auto
show "summable (λi. f (real i))" using ‹summable (λi. f (real i))› .
qed
have u:"(λk.( aa k / bb k)) ⇢ ∞"
proof -
define ff where "ff≡(λx. ereal (aa x / bb x))"
have "limsup ff = ∞"
proof -
define tt where "tt ≡ (λi. prod aa {0..i} powr (2 + 2 / ε + δ))"
have "tt i ≥ 1" for i
unfolding tt_def
apply (rule ge_one_powr_ge_zero)
subgoal
apply (rule linordered_nonzero_semiring_class.prod_ge_1)
by (simp add: a_pos aa_def int_one_le_iff_zero_less)
subgoal by (simp add: ‹ε>0› ‹δ>0› less_imp_le)
done
then have "limsup (λx. (aa (x + 1) / tt x * (1 / bb (x + 1))))
≤ limsup (λx. aa (x + 1) / bb (x + 1))"
apply (intro Limsup_mono eventuallyI)
apply (auto simp add:field_simps order.order_iff_strict)
by (metis aa_bb_pos(1) div_by_1 frac_less2 less_irrefl less_numeral_extra(1)
not_le)
also have "... = limsup (λx. aa x / bb x)"
by (subst limsup_shift,simp)
finally have "limsup (λx. ereal (aa (x + 1) / tt x * (1 / bb (x + 1))))
≤ limsup (λx. ereal (aa x / bb x))" .
moreover have "limsup (λx. ereal (aa (x + 1) / tt x * (1 / bb (x + 1))))
= ∞" using limsup_infi unfolding tt_def by auto
ultimately show ?thesis
unfolding ff_def using ereal_infty_less_eq2(1) by blast
qed
then have "limsup (λk. ff (k+t)) = ∞"
by (simp add: limsup_shift_k)
moreover have "incseq (λk. ff (k+t))"
proof (rule incseq_SucI)
fix k::nat
define gg where "gg≡(λx. (aa x / bb x))"
have "(gg (k+t)) powr (1 / (1 + ε)) + 1
≤ (gg (Suc (k+t))) powr (1 / (1 + ε))"
using ratio_large[rule_format, of "k+t",simplified] unfolding gg_def
by auto
then have "(gg (k+t)) powr (1 / (1 + ε))
≤ (gg (Suc (k+t))) powr (1 / (1 + ε))"
by auto
then have "gg (k+t)≤ gg (Suc (k+t))"
by (smt aa_bb_pos(1) aa_bb_pos(2) assms(6) divide_pos_pos gg_def
powr_less_mono2)
then show "ff (k + t) ≤ ff (Suc k + t)"
unfolding gg_def ff_def by auto
qed
ultimately have "(λk. ff (k+t)) ⇢ ∞" using incseq_tendsto_limsup
by fastforce
then show ?thesis unfolding ff_def
unfolding tendsto_def
apply (subst eventually_sequentially_seg[symmetric,of _ t])
by simp
qed
define ξ where "ξ = suminf (λ k. bb k / aa k)"
have 10:"∀⇩F k in sequentially. ¦ξ - (∑k = 0..k. bb k / aa k)¦
< 2 / ε * (bb (k+1) / aa (k+1)) powr (ε / (1+ε))"
using 8[THEN sequentially_offset,of 1] eventually_ge_at_top[of t]
u[unfolded tendsto_PInfty,rule_format,THEN sequentially_offset
,of "(2 powr (1/ε) / (2 powr (1/ε) - 1)) powr (1+ε)" 1]
proof eventually_elim
case (elim k)
define tt where "tt ≡ (aa (k + 1) / bb (k + 1)) powr (1 / (1 + ε))"
have "tt>1"
proof -
have "(aa k / bb k) powr (1 / (1 + ε)) > 0"
by (metis a_pos aa_def b_pos bb_def divide_eq_0_iff less_irrefl
of_int_eq_0_iff powr_gt_zero)
then show ?thesis using ratio_large[rule_format,OF ‹k≥t›] unfolding tt_def by argo
qed
have "¦ξ - (∑i = 0..k. bb i / aa i)¦ = ¦∑i. bb (i+(k+1)) / aa (i+(k+1))¦"
unfolding ξ_def
apply (subst suminf_minus_initial_segment[of _ "k+1",OF summable])
using atLeast0AtMost lessThan_Suc_atMost by auto
also have "... = (∑i. bb (i+(k+1)) / aa (i+(k+1)))"
proof -
have "(∑i. bb (i+(k+1)) / aa (i+(k+1))) > 0"
apply (rule suminf_pos)
subgoal using summable[THEN summable_ignore_initial_segment,of "k+1"] .
subgoal by (simp add: a_pos aa_def b_pos bb_def)
done
then show ?thesis by auto
qed
also have "... ≤ (∑i. 1 / (tt + i) powr (1 + ε))"
proof (rule suminf_le)
define ff where "ff ≡ (λk n. (aa (k+1) / bb (k+1)) powr (1 / (1 + ε)) + real n)"
have "bb (n + (k + 1)) / aa (n + (k + 1)) ≤ 1 / (ff k n) powr (1 + ε)" for n
proof -
have "ff k n powr (1 + ε) ≤ aa (k + n +1 ) / bb (k + n+1 )"
using elim(1)[rule_format,of n] unfolding ff_def by auto
moreover have "ff k n powr (1 + ε) > 0"
unfolding ff_def by (smt elim(2) of_nat_0_le_iff powr_gt_zero ratio_large)
ultimately have "1 / ff k n powr (1 + ε) ≥ bb (k + (n + 1)) / aa (k + (n + 1))"
apply (drule_tac le_imp_inverse_le)
by (auto simp add: inverse_eq_divide)
then show ?thesis by (auto simp:algebra_simps)
qed
then show "⋀n. bb (n + (k + 1)) / aa (n + (k + 1)) ≤ 1 / (tt + real n) powr (1 + ε)"
unfolding ff_def tt_def by auto
show "summable (λi. bb (i + (k + 1)) / aa (i + (k + 1)))"
using summable[THEN summable_ignore_initial_segment,of "k+1"] .
show "summable (λx. 1 / (tt + real x) powr (1 + ε))"
using 9(2)[OF ‹tt>1›] .
qed
also have "... ≤ 1/(ε *(tt-1) powr ε)"
using 9[OF ‹tt>1›] by simp
also have "... < 2 / (ε *tt powr ε)"
proof -
have "((2 powr (1/ε) / (2 powr (1/ε) - 1)) powr (1 + ε)) < (aa (k+1) / bb (k+1))"
using elim(3) by auto
then have "2 powr (1/ε) / (2 powr (1/ε) - 1) < tt"
unfolding tt_def
apply (drule_tac powr_less_mono2[rotated 2,where a="1/ (1 + ε)"])
using ‹ε>0› apply (auto simp:powr_powr )
by (subst (asm) powr_one,auto simp add:field_simps)
then have " tt < (tt-1) * (2 powr (1/ε))"
using ‹ε>0› by (auto simp:divide_simps algebra_simps)
then have "tt powr ε < 2 * (tt - 1) powr ε"
apply (drule_tac powr_less_mono2[rotated 2,where a="ε"])
using ‹ε>0› ‹tt>1› by (auto simp:powr_powr powr_mult)
then show ?thesis
using ‹ε>0› ‹tt>1› by (auto simp:divide_simps)
qed
also have "... = 2 / ε * (bb (k + 1) / aa (k + 1)) powr (ε / (1 + ε))"
unfolding tt_def
using ‹ε>0›
by (auto simp:powr_powr divide_simps algebra_simps powr_divide less_imp_le)
finally show ?case .
qed
define pq where "pq ≡ (λk. quotient_of (∑i=0..k. of_int (b i) / of_int (a i)))"
define p q where "p ≡ fst ∘ pq" and "q = snd ∘ pq"
have coprime_pq:"coprime (p k) (q k)"
and q_pos:"q k > 0" and pq_sum:"p k / q k = (∑i=0..k. b i / a i)" for k
proof -
have eq: "quotient_of (∑i=0..k. of_int (b i) / of_int (a i)) = (p k, q k)"
by (simp add: p_def q_def pq_def)
from quotient_of_coprime[OF eq] show "coprime (p k) (q k)" .
from quotient_of_denom_pos[OF eq] show "q k > 0" .
have "(∑i=0..k. b i / a i) = of_rat (∑i=0..k. of_int (b i) / of_int (a i))"
by (simp add: of_rat_sum of_rat_divide)
also have "(∑i=0..k. rat_of_int (b i) / rat_of_int (a i)) =
rat_of_int (p k) / rat_of_int (q k)"
using quotient_of_div[OF eq] by simp
finally show "p k / q k = (∑i=0..k. b i / a i)" by (simp add:of_rat_divide)
qed
have ξ_Inf_many:"∃⇩∞ k. ¦ξ - p k / q k¦ < 1 / q k powr (2 + δ * ε / (1 + ε))"
proof -
have *:"∃⇩∞k. (bb (Suc k) / aa (Suc k)) powr (ε / (1 + ε))
< ε / (2 * prod aa {0..k} powr (2 + δ * ε / (1 + ε)))"
using 7[of "(2 / ε) powr ((1+ε)/ ε)"] ‹ε>0›
by (auto simp:powr_powr)
have **:"∀⇩∞k. ¦ξ - (∑k = 0..k. bb k / aa k)¦
< 2 / ε * (bb (k + 1) / aa (k + 1)) powr (ε / (1 + ε))"
using 10[unfolded cofinite_eq_sequentially[symmetric]] .
from INFM_conjI[OF * **] show ?thesis
proof (elim INFM_mono)
fix k assume asm:"(bb (Suc k) / aa (Suc k)) powr (ε / (1 + ε))
< ε / (2 * prod aa {0..k} powr (2 + δ * ε / (1 + ε))) ∧
¦ξ - (∑k = 0..k. bb k / aa k)¦
< 2 / ε * (bb (k + 1) / aa (k + 1)) powr (ε / (1 + ε))"
have "¦ξ - real_of_int (p k) / real_of_int (q k)¦
= ¦ξ - (∑k = 0..k. bb k / aa k)¦"
using pq_sum unfolding aa_def bb_def by auto
also have "... < (2 / ε) * (bb (k+1) / aa (k+1)) powr (ε / (1+ε))"
using asm by auto
also have "... < (2 / ε) * (ε / (2 * prod aa {0..k} powr (2 + δ * ε / (1 + ε))))"
apply (rule mult_strict_left_mono)
using asm ‹ε>0› by auto
also have "... = 1/ prod aa {0..k} powr (2 + δ * ε / (1 + ε))"
using ‹ε>0› by auto
also have "... ≤ 1 / q k powr (2 + δ * ε / (1 + ε))"
proof -
have "q k ≤ prod aa {0..k}"
proof (induct k)
case 0
then show ?case unfolding q_def pq_def aa_def
apply (simp add:rat_divide_code of_int_rat quotient_of_Fract)
using aa_bb_pos[of 0,unfolded aa_def bb_def] unfolding Let_def normalize_def
apply auto
by (metis div_by_1 less_imp_le less_trans nonneg1_imp_zdiv_pos_iff
not_less zdiv_mono2)
next
case (Suc k)
define de where "de ≡ snd ∘ quotient_of"
have "real_of_int (q (Suc k))
= de (∑i=0..Suc k. of_int (b i) / of_int (a i))"
unfolding q_def pq_def de_def by simp
also have "... = de ((∑i=0..k. of_int (b i) / of_int (a i))
+ of_int (b (Suc k)) / of_int (a (Suc k)))"
by simp
also have "... ≤ de (∑i=0..k. of_int (b i) / of_int (a i))
* de (of_int (b (Suc k)) / of_int (a (Suc k)))"
using snd_quotient_plus_leq[folded de_def] by presburger
also have "... = q k * de (of_int (b (Suc k)) / of_int (a (Suc k)))"
unfolding q_def pq_def de_def by auto
also have "... = q k * snd (Rat.normalize (b (Suc k), a (Suc k)))"
by (simp add:rat_divide_code of_int_rat quotient_of_Fract de_def)
also have "... ≤ q k * aa (Suc k)"
using aa_bb_pos[of "Suc k"] q_pos[of "k"]
unfolding normalize_def aa_def bb_def Let_def
apply auto
by (metis div_by_1 int_one_le_iff_zero_less less_trans
nonneg1_imp_zdiv_pos_iff not_less zdiv_mono2 zero_less_one)
also have "... ≤ prod aa {0..k} * aa (Suc k)"
using Suc aa_bb_pos[of "Suc k"] by auto
also have "... = prod aa {0..Suc k}"
by (simp add: prod.atLeast0_atMost_Suc)
finally show ?case .
qed
then show ?thesis
apply (rule_tac divide_left_mono)
apply (rule powr_mono2)
using ‹δ>0› ‹ε>0› q_pos[of k]
apply (auto simp:powr_mult[symmetric])
by (metis aa_bb_pos(1) less_irrefl)
qed
finally show "¦ξ - p k / q k¦ < 1 / q k powr (2 + δ * ε / (1 + ε))" .
qed
qed
define pqs where "pqs ≡ {(p, q). q>0 ∧ coprime p q ∧ ¦ξ - real_of_int p / real_of_int q¦
< 1 / q powr (2 + δ * ε / (1 + ε))}"
have ξ_infinite:"infinite pqs"
proof -
define A where "A ≡ {k. ¦ξ - (p k) / (q k)¦ < 1 / (q k) powr (2 + δ * ε / (1 + ε))}"
note ξ_Inf_many
then have "infinite A"
unfolding Inf_many_def A_def by auto
moreover have "inj_on (λk. (p k, q k)) A"
proof -
define g where "g ≡ (λi. rat_of_int (b i) / rat_of_int (a i))"
define f where "f ≡ (λk. ∑i = 0..k. g i)"
have g_pos:"g i>0" for i
unfolding g_def by (simp add: a_pos b_pos)
have "strict_mono f" unfolding strict_mono_def f_def
proof safe
fix x y::nat assume "x < y"
then have "sum g {0..y} - sum g {0..x} = sum g {x<..y}"
apply (subst Groups_Big.sum_diff[symmetric])
by (auto intro:arg_cong2[where f=sum])
also have "... > 0"
apply (rule ordered_comm_monoid_add_class.sum_pos)
using ‹x<y› g_pos by auto
finally have "sum g {0..y} - sum g {0..x} >0" .
then show "sum g {0..x} < sum g {0..y}" by auto
qed
then have "inj f" using strict_mono_imp_inj_on by auto
then have "inj (quotient_of o f)" by (simp add: inj_compose quotient_of_inj)
then have "inj (λk. (p k, q k))"
unfolding f_def p_def q_def pq_def comp_def
apply (fold g_def)
by auto
then show ?thesis by (auto elim:subset_inj_on)
qed
moreover have "(λk. (p k, q k)) ` A ⊆ pqs"
unfolding A_def pqs_def using coprime_pq q_pos by auto
ultimately show ?thesis
apply (elim infinite_inj_imageE)
by auto
qed
moreover have "finite pqs" if "ξ ∈ ℚ"
proof -
obtain m n where ξ_mn:"ξ = (of_int m / of_int n)" and "coprime m n" "n>0"
proof -
obtain m n where mn:"¦ξ¦ = (of_nat m / of_nat n)" "coprime m n" "n≠0"
using Rats_abs_nat_div_natE[OF ‹ξ ∈ ℚ› Rats_abs_nat_div_natE]
by metis
define m' and n'::int
where "m'=(if ξ > 0 then nat m else -nat m)" and "n'=nat n"
then have "ξ = (of_int m' / of_int n')" "coprime m' n'" "n'>0"
using mn by auto
then show ?thesis using that by auto
qed
have "pqs ⊆ {(m,n)} ∪ {x. x ∈pqs ∧ - ¦m¦ - 1 ≤fst x ∧ fst x ≤ ¦m¦ + 1 ∧ 0<snd x ∧ snd x < n }"
proof (rule subsetI)
fix x assume "x ∈ pqs"
define p q where "p ≡ fst x" and "q=snd x"
have "q>0" "coprime p q" and pq_less:"¦ξ - p / q¦
< 1 / q powr (2 + δ * ε / (1 + ε))"
using ‹x∈pqs› unfolding p_def q_def pqs_def by auto
have q_lt_n:"q<n" when "m≠p ∨ n≠q"
proof -
have "m * q ≠ n * p" using that ‹coprime m n› ‹coprime p q› ‹q>0› ‹n>0›
by (metis eq_rat(1) fst_conv int_one_le_iff_zero_less mult.commute normalize_stable
not_one_le_zero quotient_of_Fract snd_conv)
then have "1/(n*q) ≤ ¦m/n - p/q¦"
using ‹q>0› ‹n>0›
apply (auto simp:field_simps)
by (metis add_diff_cancel_left' diff_diff_eq2 diff_zero less_irrefl not_le of_int_diff
of_int_lessD of_int_mult)
also have "... < 1 / q powr (2 + δ * ε / (1 + ε))"
using pq_less unfolding ξ_mn by auto
also have "... ≤ 1 / q ^2"
proof -
have "real_of_int (q⇧2) = q powr 2"
apply (subst powr_numeral)
unfolding power2_eq_square using ‹q>0› by auto
also have "... ≤ q powr (2 + δ * ε / (1 + ε))"
apply (rule powr_mono)
using ‹q>0› ‹δ>0› ‹ε>0› by auto
finally have "real_of_int (q⇧2)
≤ real_of_int q powr (2 + δ * ε / (1 + ε))" .
moreover have "real_of_int q powr (2 + δ * ε / (1 + ε)) > 0" using ‹0 < q› by auto
ultimately show ?thesis by (auto simp:field_simps)
qed
finally have " 1 / (n * q) < 1 / q⇧2" .
then show ?thesis using ‹q>0› ‹n>0›
unfolding power2_eq_square by (auto simp:field_simps)
qed
moreover have "- ¦m¦ - 1 ≤ p ∧ p ≤ ¦m¦ + 1" when "m≠p ∨ n≠q"
proof -
define qn where "qn ≡ q/n"
have "0<qn" "qn<1" unfolding qn_def using q_lt_n[OF ‹m≠p ∨ n≠q›] ‹q>0› by auto
have "¦m/n - p / q¦ < 1 / q powr (2 + δ * ε / (1 + ε))"
using pq_less unfolding ξ_mn by simp
then have "¦p / q - m/n¦ < 1 / q powr (2 + δ * ε / (1 + ε))" by simp
then have " m/n- 1 / q powr (2 + δ * ε / (1 + ε))
< p/q ∧ p/q < m/n + 1 / q powr (2 + δ * ε / (1 + ε))"
unfolding abs_diff_less_iff by auto
then have "qn*m- q / q powr (2 + δ * ε / (1 + ε)) < p
∧ p < qn*m + q / q powr (2 + δ * ε / (1 + ε))"
unfolding qn_def using ‹q>0› by (auto simp:field_simps)
moreover have "- ¦m¦ - 1 ≤ qn*m- q / q powr (2 + δ * ε / (1 + ε))"
proof -
have "- ¦m¦ ≤ qn*m" using ‹0<qn› ‹qn<1›
apply (simp add: abs_if)
by (smt (verit, best) mult_nonneg_nonneg of_int_nonneg)
moreover have "- 1 ≤ - q / q powr (2 + δ * ε / (1 + ε))"
proof -
have "q = q powr 1" using ‹0 < q› by auto
also have "... ≤q powr (2 + δ * ε / (1 + ε))"
apply (rule powr_mono)
using ‹q>0› ‹δ>0› ‹ε>0› by auto
finally have "q ≤ q powr (2 + δ * ε / (1 + ε))" .
then show ?thesis using ‹0 < q› by auto
qed
ultimately show ?thesis by auto
qed
moreover have "qn*m + q / q powr (2 + δ * ε / (1 + ε)) ≤ ¦m¦ + 1"
proof -
have "qn*m ≤ ¦m¦" using ‹0<qn› ‹qn<1›
apply (simp add: abs_if mult_left_le_one_le)
by (meson less_eq_real_def mult_pos_neg neg_0_less_iff_less of_int_less_0_iff order_trans)
moreover have "q / q powr (2 + δ * ε / (1 + ε)) ≤ 1"
proof -
have "q = q powr 1" using ‹0 < q› by auto
also have "... ≤q powr (2 + δ * ε / (1 + ε))"
apply (rule powr_mono)
using ‹q>0› ‹δ>0› ‹ε>0› by auto
finally have "q ≤ q powr (2 + δ * ε / (1 + ε))" .
then show ?thesis using ‹0 < q› by auto
qed
ultimately show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
ultimately show "x ∈ {(m, n)} ∪ {x ∈ pqs. - ¦m¦ - 1 ≤ fst x ∧ fst x ≤ ¦m¦ + 1
∧ 0 < snd x ∧ snd x < n}"
using ‹x ∈ pqs› ‹q>0› unfolding p_def q_def by force
qed
moreover have "finite {x. x ∈pqs ∧ - ¦m¦ - 1 ≤fst x ∧ fst x ≤ ¦m¦ + 1 ∧ 0<snd x ∧ snd x < n }"
proof -
have "finite ({- ¦m¦ - 1..¦m¦ +1} × {0<..<n})" by blast
moreover have "{x. x ∈pqs ∧ - ¦m¦ - 1 ≤fst x ∧ fst x ≤ ¦m¦ + 1 ∧ 0<snd x ∧ snd x < n } ⊆
({- ¦m¦ - 1..¦m¦ +1} × {0<..<n})"
by auto
ultimately show ?thesis
using finite_subset by blast
qed
ultimately show ?thesis using finite_subset by auto
qed
ultimately show ?thesis
apply (fold ξ_def)
using RothsTheorem[rule_format,of ξ "2 + δ * ε / (1 + ε)",folded pqs_def]
‹δ >0› ‹ε>0›
apply (auto simp:divide_simps )
by (meson mult_le_0_iff not_less)
qed
subsection‹ Acknowledgements›
text‹A.K.-A. and W.L. were supported by the ERC Advanced Grant ALEXANDRIA (Project 742178)
funded by the European Research Council and led by Professor Lawrence Paulson
at the University of Cambridge, UK. Thanks to Iosif Pinelis for his clarification on
MathOverflow regarding the summmability of the series in @{thm [source] RothsTheorem.HanclRucki2}
@{url "https://mathoverflow.net/questions/323069/why-is-this-series-summable"}
and to Manuel Eberl for his helpful comments.›
end