Quelle Kronecker_Approximation_Theorem.thy Sprache: Isabelle

chapter \<open>Kronecker's Theorem with Applications\<close>

theory Kronecker_Approximation_Theorem

imports Complex_Transcendental Henstock_Kurzweil_Integration
 "HOL-Real_Asymp.Real_Asymp"

begin

section \<open>Dirichlet's Approximation Theorem\<close>

text \<open>Simultaneous version. From Hardy and Wright, An Introduction to the Theory of Numbers, page 170.\<close>
theorem Dirichlet_approx_simult:
 fixes \<theta> :: "nat \<Rightarrow> real" and N n :: nat
 assumes "N > 0"
 obtains q p where "0 "q \ int (N^n)"
 and "\i. i \of_int q * \ i - of_int(p i)\ < 1/N"
proof -
 have lessN: "nat \x * real N\ < N" if "0 \ x" "x < 1" for x
 proof -
 have "\x * real N\ < N"
 using that by (simp add: assms floor_less_iff)
 with assms show ?thesis by linarith
 qed
 define interv where "interv \ \k. {real k/N..< Suc k/N}"
 define fracs where "fracs \ \k. map (\i. frac (real k * \ i)) [0..
 define X where "X \ fracs ` {..N^n}"
 define Y where "Y \ set (List.n_lists n (map interv [0..
 have interv_iff: "interv k = interv k' \ k=k'" for k k'
 using assms by (auto simp: interv_def Ico_eq_Ico divide_strict_right_mono)
 have in_interv: "x \ interv (nat \x * real N\)" if "x\0" for x
 using that assms by (simp add: interv_def divide_simps) linarith
 have False
 if non: "\a b. b \ N^n \ a < b \ $\ifrac (real b * \ i) - frac (real a * \ i)\ < 1/N)"
 proof -
 have "inj_on (\k. map (\i. frac (k * \ i)) [0..
 using that assms by (intro linorder_inj_onI) fastforce+
 then have caX: "card X = Suc (N^n)"
 by (simp add: X_def fracs_def card_image)
 have caY: "card Y \ N^n"
 by (metis Y_def card_length diff_zero length_map length_n_lists length_upt)
 define f where "f \ \l. map (\x. interv (nat \x * real N$) l"
 have "f ` X \ Y"
 by (auto simp: f_def Y_def X_def fracs_def o_def set_n_lists frac_lt_1 lessN)
 then have "\ inj_on f X"
 using Y_def caX caY card_inj_on_le not_less_eq_eq by fastforce
 then obtain x x' where "x\x'" "x \ X" "x' \ X" and eq: "f x = f x'"
 by (auto simp: inj_on_def)
 then obtain c c' where c: "c \ c'" "c \ N^n" "c' \ N^n"
 and xeq: "x = fracs c" and xeq': "x' = fracs c'"
 unfolding X_def by (metis atMost_iff image_iff)
 have [simp]: "length x' = n"
 by (auto simp: xeq' fracs_def)
 have ge0: "x'!i \ 0" if "i
 using that \<open>x' \<in> X\<close> by (auto simp: X_def fracs_def)
 have "f x \ Y"
 using \<open>f ` X \<subseteq> Y\<close> \<open>x \<in> X\<close> by blast
 define k where "k \ map (\r. nat \r * real N\) x"
 have "\frac (real c * \ i) - frac (real c' * \ i)\ < 1/N" if "i < n" for i
 proof -
 have k: "x!i \ interv(k!i)"
 using \<open>i<n\<close> assms by (auto simp: divide_simps k_def interv_def xeq fracs_def) linarith
 then have k': "x'!i \<in> interv(k!i)"
 using \<open>i<n\<close> eq assms ge0[OF \<open>i<n\<close>]
 by (auto simp: k_def f_def divide_simps map_equality_iff in_interv interv_iff)
 with assms k show ?thesis
 using \<open>i<n\<close> by (auto simp add: xeq xeq' fracs_def interv_def add_divide_distrib)
 qed
 then show False
 by (metis c non nat_neq_iff abs_minus_commute)
 qed
 then obtain a b where "a "b \ N^n" and *: "\i. i \frac (real b * \ i) - frac (real a * \ i)\ < 1/N"
 by blast
 let ?k = "b-a"
 let ?h = "\i. \b * \ i\ - \a * \ i\"
 show ?thesis
 proof
 show "int (b - a) \ int (N ^ n)"
 using \<open>b \<le> N ^ n\<close> by auto
 next
 fix i
 assume "i
 have "frac (b * \ i) - frac (a * \ i) = ?k * \ i - ?h i"
 using \<open>a < b\<close> by (simp add: frac_def left_diff_distrib' of_nat_diff)
 then show "\of_int ?k * \ i - ?h i\ < 1/N"
 by (metis "*" \<open>i < n\<close> of_int_of_nat_eq)
 qed (use \<open>a < b\<close> in auto)
qed

text \<open>Theorem references below referr to Apostol,
 \emph{Modular Functions and Dirichlet Series in Number Theory}\<close>

text \<open>Theorem 7.1\<close>
corollary Dirichlet_approx:
 fixes \<theta>:: real and N:: nat
 assumes "N > 0"
 obtains h k where "0 < k" "k \ int N" "\of_int k * \ - of_int h\ < 1/N"
 by (rule Dirichlet_approx_simult [OF assms, where n=1 and \<theta>="\<lambda>_. \<theta>"]) auto

text \<open>Theorem 7.2\<close>
corollary Dirichlet_approx_coprime:
 fixes \<theta>:: real and N:: nat
 assumes "N > 0"
 obtains h k where "coprime h k" "0 < k" "k \ int N" "\of_int k * \ - of_int h\ < 1/N"
proof -
 obtain h' k' where k': "0 < k'" "k' \ int N" and *: "\of_int k' * \ - of_int h'\ < 1/N"
 by (meson Dirichlet_approx assms)
 let ?d = "gcd h' k'"
 show thesis
 proof (cases "?d = 1")
 case True
 with k' * that show ?thesis by auto
 next
 case False
 then have 1: "?d > 1"
 by (smt (verit, ccfv_threshold) \<open>k'>0\<close> gcd_pos_int)
 let ?k = "k' div ?d"
 let ?h = "h' div ?d"
 show ?thesis
 proof
 show "coprime (?h::int) ?k"
 by (metis "1" div_gcd_coprime gcd_eq_0_iff not_one_less_zero)
 show k0: "0 < ?k"
 using \<open>k'>0\<close> pos_imp_zdiv_pos_iff by force
 show "?k \ int N"
 using k' "1" int_div_less_self by fastforce
 have "\\ - of_int ?h / of_int ?k\ = \\ - of_int h' / of_int k'\"
 by (simp add: real_of_int_div)
 also have "\ < 1 / of_int (N * k')"
 using k' * by (simp add: field_simps)
 also have "\ < 1 / of_int (N * ?k)"
 using assms \<open>k'>0\<close> k0 1
 by (simp add: frac_less2 int_div_less_self)
 finally show "\of_int ?k * \ - of_int ?h\ < 1 / real N"
 using k0 k' by (simp add: field_simps)
 qed
 qed
qed

definition approx_set :: "real \ (int \ int) set"
 where "approx_set \ \
 {(h, k) | h k::int. k > 0 \<and> coprime h k \<and> \<bar>\<theta> - of_int h / of_int k\<bar> < 1/k\<^sup>2}"
 for \<theta>::real

text \<open>Theorem 7.3\<close>
lemma approx_set_nonempty: "approx_set \ \ {}"
proof -
 have "\\ - of_int \\\ / of_int 1\ < 1 / (of_int 1)\<^sup>2"
 by simp linarith
 then have "(\\\, 1) \ approx_set \"
 by (auto simp: approx_set_def)
 then show ?thesis
 by blast
qed

text \<open>Theorem 7.4(c)\<close>
theorem infinite_approx_set:
 assumes "infinite (approx_set \)"
 shows "\h k. (h,k) \ approx_set \ \ k > K"
proof (rule ccontr, simp add: not_less)
 assume Kb [rule_format]: "\h k. (h, k) \ approx_set \ \ k \ K"
 define H where "H \ 1 + \K * \\"
 have k0: "k > 0" if "(h,k) \ approx_set \" for h k
 using approx_set_def that by blast
 have Hb: "of_int \h\ < H" if "(h,k) \ approx_set \" for h k
 proof -
 have *: "\k * \ - h\ < 1"
 proof -
 have "\k * \ - h\ < 1 / k"
 using that by (auto simp: field_simps approx_set_def eval_nat_numeral)
 also have "\ \ 1"
 using divide_le_eq_1 by fastforce
 finally show ?thesis .
 qed
 have "k > 0"
 using approx_set_def that by blast
 have "of_int \h\ \ \k * \ - h\ + \k * \\"
 by force
 also have "\ < 1 + \k * \\"
 using * that by simp
 also have "\ \ H"
 using Kb [OF that] \<open>k>0\<close> by (auto simp add: H_def abs_if mult_right_mono mult_less_0_iff)
 finally show ?thesis .
 qed
 have "approx_set \ \ {-(ceiling H)..ceiling H} \ {0..K}"
 using Hb Kb k0
 apply (simp add: subset_iff)
 by (smt (verit, best) ceiling_add_of_int less_ceiling_iff)
 then have "finite (approx_set \)"
 by (meson finite_SigmaI finite_atLeastAtMost_int finite_subset)
 then show False
 using assms by blast
qed

text \<open>Theorem 7.4(b,d)\<close>
theorem rational_iff_finite_approx_set:
 shows "\ \ \ \ finite (approx_set \)"
proof
 assume "\ \ \"
 then obtain a b where eq: "\ = of_int a / of_int b" and "b>0" and "coprime a b"
 by (meson Rats_cases')
 then have ab: "(a,b) \ approx_set \"
 by (auto simp: approx_set_def)
 show "finite (approx_set \)"
 proof (rule ccontr)
 assume "infinite (approx_set \)"
 then obtain h k where "(h,k) \ approx_set \" "k > b" "k>0"
 using infinite_approx_set by (smt (verit, best))
 then have "coprime h k" and hk: "\a/b - h/k\ < 1 / (of_int k)\<^sup>2"
 by (auto simp: approx_set_def eq)
 have False if "a * k = h * b"
 proof -
 have "b dvd k"
 using that \<open>coprime a b\<close>
 by (metis coprime_commute coprime_dvd_mult_right_iff dvd_triv_right)
 then obtain d where "k = b * d"
 by (metis dvd_def)
 then have "h = a * d"
 using \<open>0 < b\<close> that by force
 then show False
 using \<open>0 < b\<close> \<open>b < k\<close> \<open>coprime h k\<close> \<open>k = b * d\<close> by auto
 qed
 then have 0: "0 < \a*k - b*h\"
 by auto
 have "\a*k - b*h\ < b/k"
 using \<open>k>0\<close> \<open>b>0\<close> hk by (simp add: field_simps eval_nat_numeral)
 also have "\ < 1"
 by (simp add: \<open>0 < k\<close> \<open>b < k\<close>)
 finally show False
 using 0 by linarith
 qed
next
 assume fin: "finite (approx_set \)"
 show "\ \ \"
 proof (rule ccontr)
 assume irr: "\ \ \"
 define A where "A \ (($h,k). \\ - h/k$ ` approx_set \)"
 let ?\<alpha> = "Min A"
 have "0 \ A"
 using irr by (auto simp: A_def approx_set_def)
 moreover have "\x\A. x\0" and A: "finite A" "A \ {}"
 using approx_set_nonempty by (auto simp: A_def fin)
 ultimately have \<alpha>: "?\<alpha> > 0"
 using Min_in by force
 then obtain N where N: "real N > 1 / ?\"
 using reals_Archimedean2 by blast
 have "0 < 1 / ?\"
 using \<alpha> by auto
 also have "\ < real N"
 by (fact N)
 finally have "N > 0"
 by simp
 from N have "1/N < ?\"
 by (simp add: \<alpha> divide_less_eq mult.commute)
 then obtain h k where "coprime h k" "0 < k" "k \ int N" "\of_int k * \ - of_int h\ < 1/N"
 by (metis Dirichlet_approx_coprime \<alpha> N divide_less_0_1_iff less_le not_less_iff_gr_or_eq of_nat_0_le_iff of_nat_le_iff of_nat_0)
 then have \<section>: "\<bar>\<theta> - h/k\<bar> < 1 / (k*N)"
 by (simp add: field_simps)
 also have "\ \ 1/k\<^sup>2"
 using \<open>k \<le> int N\<close> by (simp add: eval_nat_numeral divide_simps)
 finally have hk_in: "(h,k) \ approx_set \"
 using \<open>0 < k\<close> \<open>coprime h k\<close> by (auto simp: approx_set_def)
 then have "\\ - h/k\ \ A"
 by (auto simp: A_def)
 moreover have "1 / real_of_int (k * int N) < ?\"
 proof -
 have "1 / real_of_int (k * int N) = 1 / real N / of_int k"
 by simp
 also have "\ < ?\ / of_int k"
 using \<open>k > 0\<close> \<alpha> \<open>N > 0\<close> N by (intro divide_strict_right_mono) (auto simp: field_simps)
 also have "\ \ ?\ / 1"
 using \<alpha> \<open>k > 0\<close> by (intro divide_left_mono) auto
 finally show ?thesis
 by simp
 qed
 ultimately show False using A \<section> by auto
 qed
qed

text \<open>No formalisation of Liouville's Approximation Theorem because this is already in the AFP
as Liouville\_Numbers. Apostol's Theorem 7.5 should be exactly the theorem
liouville\_irrational\_algebraic. There is a minor discrepancy in the definition
of "Liouville number" between Apostol and Eberl: he requires the denominator to be
positive, while Eberl require it to exceed 1.\<close>

section \<open>Kronecker's Approximation Theorem: the One-dimensional Case\<close>

lemma frac_int_mult:
 assumes "m > 0" and le: "1-frac r \ 1/m"
 shows "1 - frac (of_int m * r) = m * (1 - frac r)"
proof -
 have "frac (of_int m * r) = 1 - m * (1 - frac r)"
 proof (subst frac_unique_iff, intro conjI)
 show "of_int m * r - (1 - of_int m * (1 - frac r)) \ \"
 by (simp add: algebra_simps frac_def)
 qed (use assms in \<open>auto simp: divide_simps mult_ac frac_lt_1\<close>)
 then show ?thesis
 by simp
qed

text \<open>Concrete statement of Theorem 7.7, and the real proof\<close>
theorem Kronecker_approx_1_explicit:
 fixes \<theta> :: real
 assumes "\ \ \" and \: "0 \ \" "\ \ 1" and "\ > 0"
 obtains k where "k>0" "\frac(real k * \) - \\ < \"
proof -
 obtain N::nat where "1/N < \" "N > 0"
 by (metis \<open>\<epsilon> > 0\<close> gr_zeroI inverse_eq_divide real_arch_inverse)
 then obtain h k where "0 < k" and hk: "\of_int k * \ - of_int h\ < \"
 using Dirichlet_approx that by (metis less_trans)
 have irrat: "of_int n * \ \ \ \ n = 0" for n
 by (metis Rats_divide Rats_of_int assms(1) nonzero_mult_div_cancel_left of_int_0_eq_iff)
 then consider "of_int k * \ < of_int h" | "of_int k * \ > of_int h"
 by (metis Rats_of_int \<open>0 < k\<close> less_irrefl linorder_neqE_linordered_idom)
 then show thesis
 proof cases
 case 1
 define \<xi> where "\<xi> \<equiv> 1 - frac (of_int k * \<theta>)"
 have pos: "\ > 0"
 by (simp add: \<xi>_def frac_lt_1)
 define N where "N \ \1/\\"
 have "N > 0"
 by (simp add: N_def \<xi>_def frac_lt_1)
 have False if "1/\ \ \"
 proof -
 from that of_int_ceiling
 obtain r where r: "of_int r = 1/\" by blast
 then obtain s where s: "of_int k * \ = of_int s + 1 - 1/r"
 by (simp add: \<xi>_def frac_def)
 from r pos s \<open>k > 0\<close> have "\<theta> = (of_int s + 1 - 1/r) / k"
 by (auto simp: field_simps)
 with assms show False
 by simp
 qed
 then have N0: "N < 1/\"
 unfolding N_def by (metis Ints_of_int floor_correct less_le)
 then have N2: "1/(N+1) < \"
 unfolding N_def by (smt (verit) divide_less_0_iff divide_less_eq floor_correct mult.commute pos)
 have "\ * (N+1) > 1"
 by (smt (verit) N2 \<open>0 < N\<close> of_int_1_less_iff pos_divide_less_eq)
 then have ex: "\m. int m \ N+1 \ 1-\ < m * \"
 by (smt (verit, best) \<open>0 < N\<close> \<open>0 \<le> \<alpha>\<close> floor_of_int floor_of_nat mult.commute of_nat_nat)
 define m where "m \ LEAST m. int m \ N+1 \ 1-\ < m * \"
 have m: "int m \ N+1 \ 1-\ < m * \"
 using LeastI_ex [OF ex] unfolding m_def by blast
 have "m > 0"
 using m gr0I \<open>\<alpha> \<le> 1\<close> by force
 have k\<theta>: "\<xi> < \<epsilon>"
 using hk 1 by (smt (verit, best) floor_eq_iff frac_def \<xi>_def)
 show thesis
 proof (cases "m=1")
 case True
 then have "\frac (real (nat k) * \) - \\ < \"
 using m \<open>\<alpha> \<le> 1\<close> \<open>0 < k\<close> \<xi>_def k\<theta> by force
 with \<open>0 < k\<close> zero_less_nat_eq that show thesis by blast
 next
 case False
 with \<open>0 < m\<close> have "m>1" by linarith
 have "\ < 1 / N"
 by (metis N0 \<open>0 < N\<close> mult_of_int_commute of_int_pos pos pos_less_divide_eq)
 also have "\ \ 1 / (real m - 1)"
 using \<open>m > 1\<close> m by (simp add: divide_simps)
 finally have "\ < 1 / (real m - 1)" .
 then have m1_eq: "(int m - 1) * \ = 1 - frac (of_int ((int m - 1) * k) * \)"
 using frac_int_mult [of "(int m - 1)" "k * \"] \1 < m\
 by (simp add: \<xi>_def mult.assoc)
 then
 have m1_eq': "frac (of_int ((int m - 1) * k) * \) = 1 - (int m - 1) * \"
 by simp
 moreover have "(m - Suc 0) * \ \ 1-\"
 using Least_le [where k="m-Suc 0"] m
 by (smt (verit, best) Suc_n_not_le_n Suc_pred \<open>0 < m\<close> m_def of_nat_le_iff)
 ultimately have le\<alpha>: " \<alpha> \<le> frac (of_int ((int m - 1) * k) * \<theta>)"
 by (simp add: Suc_leI \<open>0 < m\<close> of_nat_diff)
 moreover have "m * \ + frac (of_int ((int m - 1) * k) * \) = \ + 1"
 by (subst m1_eq') (simp add: \_def algebra_simps)
 ultimately have "\frac ((int (m - 1) * k) * \) - \\ < \"
 by (smt (verit, best) One_nat_def Suc_leI \<open>0 < m\<close> int_ops(2) k\<theta> m of_nat_diff)
 with that show thesis
 by (metis \<open>0 < k\<close> \<open>1 < m\<close> mult_pos_pos of_int_of_nat_eq of_nat_mult pos_int_cases zero_less_diff)
 qed
 next
 case 2
 define \<xi> where "\<xi> \<equiv> frac (of_int k * \<theta>)"
 have recip_frac: False if "1/\ \ \"
 proof -
 have "frac (of_int k * \) \ \"
 using that unfolding \<xi>_def
 by (metis Ints_cases Rats_1 Rats_divide Rats_of_int div_by_1 divide_divide_eq_right mult_cancel_right2)
 then show False
 using \<open>0 < k\<close> frac_in_Rats_iff irrat by blast
 qed
 have pos: "\ > 0"
 by (metis \<xi>_def Ints_0 division_ring_divide_zero frac_unique_iff less_le recip_frac)
 define N where "N \ \1 / \\"
 have "N > 0"
 unfolding N_def
 by (smt (verit) \<xi>_def divide_less_eq_1_pos floor_less_one frac_lt_1 pos)
 have N0: "N < 1 / \"
 unfolding N_def by (metis Ints_of_int floor_eq_iff less_le recip_frac)
 then have N2: "1/(N+1) < \"
 unfolding N_def
 by (smt (verit, best) divide_less_0_iff divide_less_eq floor_correct mult.commute pos)
 have "\ * (N+1) > 1"
 by (smt (verit) N2 \<open>0 < N\<close> of_int_1_less_iff pos_divide_less_eq)
 then have ex: "\m. int m \ N+1 \ \ < m * \"
 by (smt (verit, best) mult.commute \<open>\<alpha> \<le> 1\<close> \<open>0 < N\<close> of_int_of_nat_eq pos_int_cases)
 define m where "m \ LEAST m. int m \ N+1 \ \ < m * \"
 have m: "int m \ N+1 \ \ < m * \"
 using LeastI_ex [OF ex] unfolding m_def by blast
 have "m > 0"
 using \<open>0 \<le> \<alpha>\<close> m gr0I by force
 have k\<theta>: "\<xi> < \<epsilon>"
 using hk 2 unfolding \<xi>_def by (smt (verit, best) floor_eq_iff frac_def)
 have mk_eq: "frac (of_int (m*k) * \) = m * frac (of_int k * \)"
 if "m>0" "frac (of_int k * \) < 1/m" for m k
 proof (subst frac_unique_iff , intro conjI)
 show "real_of_int (m * k) * \ - real_of_int m * frac (real_of_int k * \) \ \"
 by (simp add: algebra_simps frac_def)
 qed (use that in \<open>auto simp: divide_simps mult_ac\<close>)
 show thesis
 proof (cases "m=1")
 case True
 then have "\frac (real (nat k) * \) - \\ < \"
 using m \<alpha> \<open>0 < k\<close> \<xi>_def k\<theta> by force
 with \<open>0 < k\<close> zero_less_nat_eq that show ?thesis by blast
 next
 case False
 with \<open>0 < m\<close> have "m>1" by linarith
 with \<open>0 < k\<close> have mk_pos:"(m - Suc 0) * nat k > 0" by force
 have "real_of_int (int m - 1) < 1 / frac (real_of_int k * \)"
 using N0 \<xi>_def m by force
 then
 have m1_eq: "(int m - 1) * \ = frac (((int m - 1) * k) * \)"
 using m mk_eq [of "int m-1" k] pos \<open>m>1\<close> by (simp add: divide_simps mult_ac \<xi>_def)
 moreover have "(m - Suc 0) * \ \ \"
 using Least_le [where k="m-Suc 0"] m
 by (smt (verit, best) Suc_n_not_le_n Suc_pred \<open>0 < m\<close> m_def of_nat_le_iff)
 ultimately have le\<alpha>: "frac (of_int ((int m - 1) * k) * \<theta>) \<le> \<alpha>"
 by (simp add: Suc_leI \<open>0 < m\<close> of_nat_diff)
 moreover have "(m * \ - frac (of_int ((int m - 1) * k) * \)) < \"
 by (metis m1_eq add_diff_cancel_left' diff_add_cancel k\ left_diff_distrib'
 mult_cancel_right2 of_int_1 of_int_diff of_int_of_nat_eq)
 ultimately have "\frac (real( (m - 1) * nat k) * \) - \\ < \"
 using \<open>0 < k\<close> \<open>0 < m\<close> by simp (smt (verit, best) One_nat_def Suc_leI m of_nat_1 of_nat_diff)
 with \<open>m > 0\<close> that show thesis
 using mk_pos One_nat_def by presburger
 qed
 qed
qed

text \<open>Theorem 7.7 expressed more abstractly using @{term closure}\<close>
corollary Kronecker_approx_1:
 fixes \<theta> :: real
 assumes "\ \ \"
 shows "closure (range (\n. frac (real n * \))) = {0..1}" (is "?C = _")
proof -
 have "\k>0. \frac(real k * \) - \\ < \" if "0 \ \" "\ \ 1" "\ > 0" for \ \
 by (meson Kronecker_approx_1_explicit assms that)
 then have "x \ ?C" if "0 \ x" "x \ 1" for x :: real
 using that by (auto simp add: closure_approachable dist_real_def)
 moreover
 have "(range (\n. frac (real n * \))) \ {0..1}"
 by (smt (verit) atLeastAtMost_iff frac_unique_iff image_subset_iff)
 then have "?C \ {0..1}"
 by (simp add: closure_minimal)
 ultimately show ?thesis by auto
qed

text \<open>The next theorem removes the restriction $0 \leq \alpha \leq 1$.\<close>

text \<open>Theorem 7.8\<close>
corollary sequence_of_fractional_parts_is_dense:
 fixes \<theta> :: real
 assumes "\ \ \" "\ > 0"
 obtains h k where "k > 0" "\of_int k * \ - of_int h - \\ < \"
proof -
 obtain k where "k>0" "\frac(real k * \) - frac \\ < \"
 by (metis Kronecker_approx_1_explicit assms frac_ge_0 frac_lt_1 less_le_not_le)
 then have "\real_of_int k * \ - real_of_int (\k * \\ - \\\) - \\ < \"
 by (auto simp: frac_def)
 then show thesis
 by (meson \<open>0 < k\<close> of_nat_0_less_iff that)
qed

section \<open>Extension of Kronecker's Theorem to Simultaneous Approximation\<close>

subsection \<open>Towards Lemma 1\<close>

lemma integral_exp:
 assumes "T \ 0" "a\0"
 shows "integral {0..T} (\t. exp(a * complex_of_real t)) = (exp(a * of_real T) - 1) / a"
proof -
 have "\t. t \ {0..T} \ ((\x. exp (a * x) / a) has_vector_derivative exp (a * t)) (at t within {0..T})"
 using assms
 by (intro derivative_eq_intros has_complex_derivative_imp_has_vector_derivative [unfolded o_def] | simp)+
 then have "((\t. exp(a * of_real t)) has_integral exp(a * complex_of_real T)/a - exp(a * of_real 0)/a) {0..T}"
 by (meson fundamental_theorem_of_calculus \<open>T \<ge> 0\<close>)
 then show ?thesis
 by (simp add: diff_divide_distrib integral_unique)
qed

lemma Kronecker_simult_aux1:
 fixes \<eta>:: "nat \<Rightarrow> real" and c:: "nat \<Rightarrow> complex" and N::nat
 assumes inj: "inj_on \ {..N}" and "k \ N"
 defines "f \ \t. \r\N. c r * exp(\ * of_real t * \ r)"
 shows "((\T. (1/T) * integral {0..T} (\t. f t * exp(-\ * of_real t * \ k))) \ c k) at_top"
proof -
 define F where "F \ \k t. f t * exp(-\ * of_real t * \ k)"
 have f: "F k = (\t. \r\N. c r * exp(\ * (\ r - \ k) * of_real t))"
 by (simp add: F_def f_def sum_distrib_left field_simps exp_diff exp_minus)
 have *: "integral {0..T} (F k)
 = c k * T + (\<Sum>r \<in> {..N}-{k}. c r * integral {0..T} (\<lambda>t. exp(\ * (\<eta> r - \<eta> k) * of_real t)))"
 if "T > 0" for T
 using \<open>k \<le> N\<close> that
 by (simp add: f integral_sum integrable_continuous_interval continuous_intros Groups_Big.sum_diff scaleR_conv_of_real)

 have **: "(1/T) * integral {0..T} (F k)
 = c k + (\<Sum>r \<in> {..N}-{k}. c r * (exp(\ * (\<eta> r - \<eta> k) * of_real T) - 1) / (\ * (\<eta> r - \<eta> k) * of_real T))"
 if "T > 0" for T
 proof -
 have I: "integral {0..T} (\t. exp (\ * (complex_of_real t * \ r) - \ * (complex_of_real t * \ k)))
 = (exp(\ * (\<eta> r - \<eta> k) * T) - 1) / (\ * (\<eta> r - \<eta> k))"
 if "r \ N" "r \ k" for r
 using that \<open>k \<le> N\<close> inj \<open>T > 0\<close> integral_exp [of T "\ * (\<eta> r - \<eta> k)"]
 by (simp add: inj_on_eq_iff algebra_simps)
 show ?thesis
 using that by (subst *) (auto simp add: algebra_simps sum_divide_distrib I)
 qed
 have "((\T. c r * (exp(\ * (\ r - \ k) * of_real T) - 1) / (\ * (\ r - \ k) * of_real T)) \ 0) at_top"
 for r
 proof -
 have "((\x. (cos ((\ r - \ k) * x) - 1) / x) \ 0) at_top"
 "((\x. sin ((\ r - \ k) * x) / x) \ 0) at_top"
 by real_asymp+
 hence "((\T. (exp (\ * (\ r - \ k) * of_real T) - 1) / of_real T) \ 0) at_top"
 by (simp add: tendsto_complex_iff Re_exp Im_exp)
 from tendsto_mult[OF this tendsto_const[of "c r / (\ * (\ r - \ k))"]] show ?thesis
 by (simp add: field_simps)
 qed
 then have "((\T. c k + (\r \ {..N}-{k}. c r * (exp(\ * (\ r - \ k) * of_real T) - 1) /
 (\ * (\<eta> r - \<eta> k) * of_real T))) \<longlongrightarrow> c k + 0) at_top"
 by (intro tendsto_add tendsto_null_sum) auto
 also have "?this \ ?thesis"
 proof (rule filterlim_cong)
 show "\\<^sub>F x in at_top. c k + (\r\{..N} - {k}. c r * (exp (\ * of_real (\ r - \ k) * of_real x) - 1) /
 (\ * of_real (\<eta> r - \<eta> k) * of_real x)) =
 1 / of_real x * integral {0..x} (\<lambda>t. f t * exp (- \ * of_real t * of_real (\<eta> k)))"
 using eventually_gt_at_top[of 0]
 proof eventually_elim
 case (elim T)
 show ?case
 using **[of T] elim by (simp add: F_def)
 qed
 qed auto
 finally show ?thesis .
qed

text \<open>the version of Lemma 1 that we actually need\<close>
lemma Kronecker_simult_aux1_strict:
 fixes \<eta>:: "nat \<Rightarrow> real" and c:: "nat \<Rightarrow> complex" and N::nat
 assumes \<eta>: "inj_on \<eta> {..<N}" "0 \<notin> \<eta> ` {..<N}" and "k < N"
 defines "f \ \t. 1 + (\r * of_real t * \ r))"
 shows "((\T. (1/T) * integral {0..T} (\t. f t * exp(-\ * of_real t * \ k))) \ c k) at_top"
proof -
 define c' where "c' \<equiv> case_nat 1 c"
 define \<eta>' where "\<eta>' \<equiv> case_nat 0 \<eta>"
 define f' where "f' \<equiv> \<lambda>t. (\<Sum>r\<le>N. c' r * exp(\ * of_real t * \<eta>' r))"
 have "inj_on \' {..N}"
 using \<eta> by (auto simp: \<eta>'_def inj_on_def split: nat.split_asm)
 moreover have "Suc k \ N"
 using \<open>k < N\<close> by auto
 ultimately have "((\T. 1 / T * integral {0..T} (\t. (\r\N. c' r * exp (\ * of_real t * \' r)) *
 exp (- \ * t * \<eta>' (Suc k)))) \<longlongrightarrow> c' (Suc k))
 at_top"
 by (intro Kronecker_simult_aux1)
 moreover have "(\r\N. c' r * exp (\ * of_real t * \' r)) = 1 + (\r * of_real t * \ r))" for t
 by (simp add: c'_def \'_def sum.atMost_shift)
 ultimately show ?thesis
 by (simp add: f_def c'_def \'_def)
qed

subsection \<open>Towards Lemma 2\<close>

lemma cos_monotone_aux: "\\2 * pi * of_int i + x\ \ y; y \ pi\ \ cos y \ cos x"
 by (metis add.commute abs_ge_zero cos_abs_real cos_monotone_0_pi_le sin_cos_eq_iff)

lemma Figure7_1:
 assumes "0 \ \" "\ \ \x\" "\x\ \ pi"
 shows "cmod (1 + exp (\ * x)) \ cmod (1 + exp (\ * \))"
proof -
 have norm_eq: "sqrt (2 * (1 + cos t)) = cmod (1 + cis t)" for t
 by (simp add: norm_complex_def power2_eq_square algebra_simps)
 have "cos \x\ \ cos \"
 by (rule cos_monotone_0_pi_le) (use assms in auto)
 hence "sqrt (2 * (1 + cos \x\)) \ sqrt (2 * (1 + cos \))"
 by simp
 also have "cos \x\ = cos x"
 by simp
 finally show ?thesis
 unfolding norm_eq by (simp add: cis_conv_exp)
qed

lemma Kronecker_simult_aux2:
 fixes \<alpha>:: "nat \<Rightarrow> real" and \<theta>:: "nat \<Rightarrow> real" and n::nat
 defines "F \ \t. 1 + (\r * of_real (2 * pi * (t * \ r - \ r))))"
 defines "L \ Sup (range (norm \ F))"
 shows "(\\>0. \t h. \rt * \ r - \ r - of_int (h r)\ < \) \ L = Suc n" (is "?lhs = _")
proof
 assume ?lhs
 then have "\k. \t h. \rt * \ r - \ r - of_int (h r)\ < 1 / (2 * pi * Suc k)"
 by simp
 then obtain t h where th: "\k r. r \t k * \ r - \ r - of_int (h k r)\ < 1 / (2 * pi * Suc k)"
 by metis
 have Fle: "\x. cmod (F x) \ real (Suc n)"
 by (force simp: F_def intro: order_trans [OF norm_triangle_ineq] order_trans [OF norm_sum])
 then have boundedF: "bounded (range F)"
 by (metis bounded_iff rangeE)
 have leL: "1 + n * cos(1 / Suc k) \ L" for k
 proof -
 have *: "cos (1 / Suc k) \ cos (2 * pi * (t k * \ r - \ r))" if "r
 proof (rule cos_monotone_aux)
 have "\2 * pi * (- h k r) + 2 * pi * (t k * \ r - \ r)\ \ \t k * \ r - \ r - h k r\ * 2 * pi"
 by (simp add: algebra_simps abs_mult_pos abs_mult_pos')
 also have "\ \ 1 / real (Suc k)"
 using th [OF that, of k] by (simp add: divide_simps)
 finally show "\2 * pi * real_of_int (- h k r) + 2 * pi * (t k * \ r - \ r)\ \ 1 / real (Suc k)" .
 have "1 / real (Suc k) \ 1"
 by auto
 then show "1 / real (Suc k) \ pi"
 using pi_ge_two by linarith
 qed
 have "1 + n * cos(1 / Suc k) = 1 + (\r
 by simp
 also have "\ \ 1 + (\r r - \ r)))"
 using * by (intro add_mono sum_mono) auto
 also have "\ \ Re (F(t k))"
 by (simp add: F_def Re_exp)
 also have "\ \ norm (F(t k))"
 by (simp add: complex_Re_le_cmod)
 also have "\ \ L"
 by (simp add: L_def boundedF bounded_norm_le_SUP_norm)
 finally show ?thesis .
 qed
 show "L = Suc n"
 proof (rule antisym)
 show "L \ Suc n"
 using Fle by (auto simp add: L_def intro: cSup_least)
 have "((\k. 1 + real n * cos (1 / real (Suc k))) \ 1 + real n) at_top"
 by real_asymp
 with LIMSEQ_le_const2 leL show "Suc n \ L"
 by fastforce
 qed
next
 assume L: "L = Suc n"
 show ?lhs
 proof (rule ccontr)
 assume "\ ?lhs"
 then obtain e0 where "e0>0" and e0: "\t h. \kt * \ k - \ k - of_int (h k)\ \ e0"
 by (force simp: not_less)
 define \<epsilon> where "\<epsilon> \<equiv> min e0 (pi/4)"
 have \<epsilon>: "\<And>t h. \<exists>k<n. \<bar>t * \<theta> k - \<alpha> k - of_int (h k)\<bar> \<ge> \<epsilon>"
 unfolding \<epsilon>_def using e0 min.coboundedI1 by blast
 have \<epsilon>_bounds: "\<epsilon> > 0" "\<epsilon> < pi" "\<epsilon> \<le> pi/4"
 using \<open>e0 > 0\<close> by (auto simp: \<epsilon>_def min_def)
 with sin_gt_zero have "sin \ > 0"
 by blast
 then have "\ collinear{0, 1, exp (\ * \)}"
 using collinear_iff_Reals cis.sel cis_conv_exp complex_is_Real_iff by force
 then have "norm (1 + exp (\ * \)) < 2"
 using norm_triangle_eq_imp_collinear
 by (smt (verit) linorder_not_le norm_exp_i_times norm_one norm_triangle_lt)
 then obtain \<delta> where "\<delta> > 0" and \<delta>: "norm (1 + exp (\ * \<epsilon>)) = 2 - \<delta>"
 by (smt (verit, best))
 have "norm (F t) \ n+1-\" for t
 proof -
 define h where "h \ \r. round (t * \ r - \ r)"
 define X where "X \ \r. t * \ r - \ r - h r"
 have "exp (\ * (of_int j * (of_real pi * 2))) = 1" for j
 by (metis add_0 exp_plus_2pin exp_zero)
 then have exp_X: "exp (\ * (2 * of_real pi * of_real (X r)))
 = exp (\ * of_real (2 * pi * (t * \<theta> r - \<alpha> r)))" for r
 by (simp add: X_def right_diff_distrib exp_add exp_diff mult.commute)
 have norm_pr_12: "X r \ {-1/2..<1/2}" for r
 apply (simp add: X_def h_def)
 by (smt (verit, best) abs_of_nonneg half_bounded_equal of_int_round_abs_le of_int_round_gt)
 obtain k where "k and 1: "\X k\ \ \"
 using X_def \<epsilon> [of t h] by auto
 have 2: "2*pi \ 1"
 using pi_ge_two by auto
 have "\2 * pi * X k\ \ \"
 using mult_mono [OF 2 1] pi_ge_zero by linarith
 moreover
 have "\2 * pi * X k\ \ pi"
 using norm_pr_12 [of k] apply (simp add: abs_if field_simps)
 by (smt (verit, best) divide_le_eq_1_pos divide_minus_left m2pi_less_pi nonzero_mult_div_cancel_left)
 ultimately
 have *: "norm (1 + exp (\ * of_real (2 * pi * X k))) \ norm (1 + exp (\ * \))"
 using Figure7_1[of \<epsilon> "2 * pi * X k"] \<epsilon>_bounds by linarith
 have "norm (F t) = norm (1 + (\r * of_real (2 * pi * (X r)))))"
 by (auto simp: F_def exp_X)
 also have "\ \ norm (1 + exp(\ * of_real (2 * pi * X k)) + (\r \ {.. * of_real (2 * pi * X r))))"
 by (simp add: comm_monoid_add_class.sum.remove [where x=k] \<open>k < n\<close> algebra_simps)
 also have "\ \ norm (1 + exp(\ * of_real (2 * pi * X k))) + (\r \ {.. * of_real (2 * pi * X r))))"
 by (intro norm_triangle_mono sum_norm_le order_refl)
 also have "\ \ (2 - \) + (n - 1)"
 using \<open>k < n\<close> \<delta>
 by simp (metis "*" mult_2 of_real_add of_real_mult)
 also have "\ = n + 1 - \"
 using \<open>k < n\<close> by simp
 finally show ?thesis .
 qed
 then have "L \ 1 + real n - \"
 by (auto simp: L_def intro: cSup_least)
 with L \<open>\<delta> > 0\<close> show False
 by linarith
 qed
qed

subsection \<open>Towards lemma 3\<close>

text \<open>The text doesn't say so, but the generated polynomial needs to be "clean":
all coefficients nonzero, and with no exponent string mentioned more than once.
And no constant terms (with all exponents zero).\<close>

text \<open>Some tools for combining integer-indexed sequences or splitting them into parts\<close>

lemma less_sum_nat_iff:
 fixes b::nat and k::nat
 shows "b < (\i (\ji b \ b < (\i
proof (induction k arbitrary: b)
 case (Suc k)
 then show ?case
 by (simp add: less_Suc_eq) (metis not_less trans_less_add1)
qed auto

lemma less_sum_nat_iff_uniq:
 fixes b::nat and k::nat
 shows "b < (\i (\!j. j (\i b \ b < (\i
 unfolding less_sum_nat_iff by (meson leD less_sum_nat_iff nat_neq_iff)

definition part :: "(nat \ nat) \ nat \ nat \ nat"
 where "part a k b \ (THE j. j (\i b \ b < (\i

lemma part:
 "b < (\i (let j = part a k b in j < k \ (\i < j. a i) \ b \ b < (\i < j. a i) + a j)"
 (is "?lhs = ?rhs")
proof
 assume ?lhs
 then show ?rhs
 unfolding less_sum_nat_iff_uniq part_def by (metis (no_types, lifting) theI')
qed (auto simp: less_sum_nat_iff Let_def)

lemma part_Suc: "part a (Suc k) b = (if sum a {.. b \ b < sum a {..
 using leD
 by (fastforce simp: part_def less_Suc_eq less_sum_nat_iff conj_disj_distribR cong: conj_cong)

text \<open>The polynomial expansions used in Lemma 3\<close>

definition gpoly :: "[nat, nat\complex, nat, nat\nat, [nat,nat]\nat] \ complex"
 where "gpoly n x N a r \ (\ki

lemma gpoly_cong:
 assumes "\k. k < N \ a' k = a k" "\k i. \k < N; i \ r' k i = r k i"
 shows "gpoly n x N a r = gpoly n x N a' r'"
 using assms by (auto simp: gpoly_def)

lemma gpoly_inc: "gpoly n x N a r = gpoly (Suc n) x N a (\k. (r k)(n:=0))"
 by (simp add: gpoly_def algebra_simps sum_distrib_left)

lemma monom_times_gpoly: "gpoly n x N a r * x n ^ q = gpoly (Suc n) x N a (\k. (r k)(n:=q))"
 by (simp add: gpoly_def algebra_simps sum_distrib_left)

lemma const_times_gpoly: "e * gpoly n x N a r = gpoly n x N ((*)e \ a) r"
 by (simp add: gpoly_def sum_distrib_left mult.assoc)

lemma one_plus_gpoly: "1 + gpoly n x N a r = gpoly n x (Suc N) (a(N:=1)) (r(N:=(\_. 0)))"
 by (simp add: gpoly_def)

lemma gpoly_add:
 "gpoly n x N a r + gpoly n x N' a' r'
= gpoly n x (N+N') (\k. if kk. if k
proof -
 have "{.. {N.. {N..
 by auto
 then show ?thesis
 by (simp add: gpoly_def sum.union_disjoint sum.atLeastLessThan_shift_0[of _ N] atLeast0LessThan)
qed

lemma gpoly_sum:
 fixes n Nf af rf p
 defines "N \ sum Nf {..
 defines "a \ \k. let q = (part Nf p k) in af q (k - sum Nf {..
 defines "r \ \k. let q = (part Nf p k) in rf q (k - sum Nf {..
 shows "(\q
 unfolding N_def a_def r_def
proof (induction p)
 case 0
 then show ?case
 by (simp add: gpoly_def)
next
 case (Suc p)
 then show ?case
 by (auto simp: gpoly_add Let_def part_Suc intro: gpoly_cong)
qed

text \<open>For excluding constant terms: with all exponents zero\<close>
definition nontriv_exponents :: "[nat, nat, [nat,nat]\nat] \ bool"
 where "nontriv_exponents n N r \ \ki 0"

lemma nontriv_exponents_add:
 "\nontriv_exponents n M r; nontriv_exponents (Suc n) N r'\ \
 nontriv_exponents (Suc n) (M + N) (\<lambda>k. if k<M then r k else r' (k-M))"
 by (force simp add: nontriv_exponents_def less_Suc_eq)

lemma nontriv_exponents_sum:
 assumes "\q. q < p \ nontriv_exponents n (N q) (r q)"
 shows "nontriv_exponents n (sum N {..k. let q = part N p k in r q (k - sum N {..
 using assms by (simp add: nontriv_exponents_def less_diff_conv2 part Let_def)

definition uniq_exponents :: "[nat, nat, [nat,nat]\nat] \ bool"
 where "uniq_exponents n N r \ \kk'i r k' i"

lemma uniq_exponents_inj: "uniq_exponents n N r \ inj_on r {..
 by (smt (verit, best) inj_on_def lessThan_iff linorder_cases uniq_exponents_def)

text \<open>All coefficients must be nonzero\<close>
definition nonzero_coeffs :: "[nat, nat\nat] \ bool"
 where "nonzero_coeffs N a \ \k 0"

text \<open>Any polynomial expansion can be cleaned up, removing zero coeffs, etc.\<close>
lemma gpoly_uniq_exponents:
 obtains N' a' r'
 where "\x. gpoly n x N a r = gpoly n x N' a' r'"
 "uniq_exponents n N' r'" "nonzero_coeffs N' a'" "N' \ N"
 "nontriv_exponents n N r \ nontriv_exponents n N' r'"
proof (cases "\k
 case True
 show thesis
 proof
 show "gpoly n x N a r = gpoly n x 0 a r" for x
 by (auto simp: gpoly_def True)
 qed (auto simp: uniq_exponents_def nonzero_coeffs_def nontriv_exponents_def)
next
 case False
 define cut where "cut f i \ if i
 define R where "R \ cut ` r ` ({.. {k. a k > 0})"
 define N' where "N' \<equiv> card R"
 define r' where "r' \<equiv> from_nat_into R"
 define a' where "a' \<equiv> \<lambda>k'. \<Sum>k<N. if r' k' = cut (r k) then a k else 0"
 have "finite R"
 using R_def by blast
 then have bij: "bij_betw r' {..
 using bij_betw_from_nat_into_finite N'_def r'_def by blast
 have 1: "card {i. i < N' \ r' i = cut (r k)} = Suc 0"
 if "k < N" "a k > 0" for k
 proof -
 have "card {i. i < N' \ r' i = cut (r k)} \ Suc 0"
 using bij by (simp add: card_le_Suc0_iff_eq bij_betw_iff_bijections Ball_def) metis
 moreover have "card {i. i < N' \ r' i = cut (r k)} > 0"
 using bij that by (auto simp: card_gt_0_iff bij_betw_iff_bijections R_def)
 ultimately show "card {i. i < N' \ r' i = cut (r k)} = Suc 0"
 using that by auto
 qed
 show thesis
 proof
 have "\i r' k' i" if "k < N'" and "k' < k" for k k'
 proof -
 have "k' < N'"
 using order.strict_trans that by blast
 then have "r' k \ r' k'"
 by (metis bij bij_betw_iff_bijections lessThan_iff nat_neq_iff that)
 moreover obtain sk sk' where "r' k = cut sk" "r' k' = cut sk'"
 by (metis R_def \<open>k < N'\<close> \<open>k' < N'\<close> bij bij_betwE image_iff lessThan_iff)
 ultimately show ?thesis
 using local.cut_def by force
 qed
 then show "uniq_exponents n N' r'"
 by (auto simp: uniq_exponents_def R_def)
 have "R \ (cut \ r) ` {..
 by (auto simp: R_def)
 then show "N' \ N"
 unfolding N'_def by (metis card_lessThan finite_lessThan surj_card_le)
 show "gpoly n x N a r = gpoly n x N' a' r'" for x
 proof -
 have "a k * (\i
 = (\<Sum>i<N'. (if r' i = cut (r k) then of_nat (a k) else of_nat 0) * (\<Prod>j<n. x j ^ r' i j))"
 if "k for k
 using that
 by (cases"a k = 0")
 (simp_all add: if_distrib [of "\v. v * _"] 1 cut_def flip: sum.inter_filter cong: if_cong)
 then show ?thesis
 by (simp add: gpoly_def a'_def sum_distrib_right sum.swap [where A="{..}"] if_distrib [of of_nat])
 qed
 show "nontriv_exponents n N' r'" if ne: "nontriv_exponents n N r"
 proof -
 have "\i
 proof -
 have "r' k' \ R"
 using bij bij_betwE that by blast
 then obtain k where "k and k: "r' k' = cut (r k)"
 using R_def by blast
 with ne obtain i where "i "r k i > 0"
 by (auto simp: nontriv_exponents_def)
 then show ?thesis
 using k local.cut_def by auto
 qed
 then show ?thesis
 by (simp add: nontriv_exponents_def)
 qed
 have "0 < a' k'" if "k' < N'" for k'
 proof -
 have "r' k' \ R"
 using bij bij_betwE that by blast
 then obtain k where "k "a k > 0" "r' k' = cut (r k)"
 using R_def by blast
 then have False if "a' k' = 0"
 using that by (force simp add: a'_def Ball_def )
 then show ?thesis
 by blast
 qed
 then show "nonzero_coeffs N' a'"
 by (auto simp: nonzero_coeffs_def)
 qed
qed

lemma Kronecker_simult_aux3:
 "\N a r. (\x. (1 + (\i Suc N \ (p+1)^n
 \<and> nontriv_exponents n N r"
proof (induction n arbitrary: p)
 case 0
 then show ?case
 by (auto simp: gpoly_def nontriv_exponents_def nonzero_coeffs_def)
next
 case (Suc n)
 then obtain Nf af rf
 where feq: "\q x. (1 + (\i
 and Nle: "\q. Suc (Nf q) \ (q+1)^n"
 and nontriv: "\q. nontriv_exponents n (Nf q) (rf q)"
 by metis
 define N where "N \ Nf p + (\q
 define a where "a \ \k. if k < Nf p then af p k
 else let q = part (\<lambda>t. Suc (Nf t)) p (k - Nf p)
 in (p choose q) *
 (if k - Nf p - (\<Sum>t<q. Suc (Nf t)) = Nf q then Suc 0
 else af q (k - Nf p - (\<Sum>t<q. Suc(Nf t))))"
 define r where "r \ \k. if k < Nf p then (rf p k)(n := 0)
 else let q = part (\<lambda>t. Suc (Nf t)) p (k - Nf p)
 in (if k - Nf p - (\<Sum>t<q. Suc (Nf t)) = Nf q then \<lambda>_. 0
 else rf q (k - Nf p - (\<Sum>t<q. Suc(Nf t)))) (n := p-q)"
 have peq: "{..p} = insert p {..
 by auto
 have "nontriv_exponents n (Nf p) (\i. (rf p i)(n := 0))"
 "\q. q
nontriv_exponents (Suc n) (Suc (Nf q)) (\k. (if k = Nf q then \_. 0 else rf q k) (n := p - q))"
 using nontriv by (fastforce simp: nontriv_exponents_def)+
 then have "nontriv_exponents (Suc n) N r"
 unfolding N_def r_def by (intro nontriv_exponents_add nontriv_exponents_sum)
 moreover
 { fix x :: "nat \ complex"
 have "(1 + (\i < Suc n. x i)) ^ p = (1 + (\i
 by (simp add: add_ac)
 also have "\ = (\q\p. (p choose q) * (1 + (\i
 by (simp add: binomial_ring)
 also have "\ = (\q\p. (p choose q) * (1 + gpoly n x (Nf q) (af q) (rf q)) * x n^(p-q))"
 by (simp add: feq)
 also have "\ = 1 + (gpoly n x (Nf p) (af p) (rf p) + (\q
 by (simp add: algebra_simps sum.distrib peq)
 also have "\ = 1 + gpoly (Suc n) x N a r"
 apply (subst one_plus_gpoly)
 apply (simp add: const_times_gpoly monom_times_gpoly gpoly_sum)
 apply (simp add: gpoly_inc [where n=n] gpoly_add N_def a_def r_def)
 done
 finally have "(1 + sum x {.. .
 }
 moreover have "Suc N \ (p + 1) ^ Suc n"
 proof -
 have "Suc N = (\q\p. Suc (Nf q))"
 by (simp add: N_def peq)
 also have "\ \ (\q\p. (q+1)^n)"
 by (meson Nle sum_mono)
 also have "\ \ (\q\p. (p+1)^n)"
 by (force intro!: sum_mono power_mono)
 also have "\ \ (p + 1) ^ Suc n"
 by simp
 finally show "Suc N \ (p + 1) ^ Suc n" .
 qed
 ultimately show ?case
 by blast
qed

lemma Kronecker_simult_aux3_uniq_exponents:
 obtains N a r where "\x. (1 + (\i (p+1)^n"
 "nontriv_exponents n N r" "uniq_exponents n N r" "nonzero_coeffs N a"
proof -
 obtain N0 a0 r0 where "\x. (1 + (\r
 and "Suc N0 \ (p+1)^n" "nontriv_exponents n N0 r0"
 using Kronecker_simult_aux3 by blast
 with le_trans Suc_le_mono gpoly_uniq_exponents [of n N0 a0 r0] that show thesis
 by (metis (no_types, lifting))
qed

subsection \<open>And finally Kroncker's theorem itself\<close>

text \<open>Statement of Theorem 7.9\<close>
theorem Kronecker_thm_1:
 fixes \<alpha> \<theta>:: "nat \<Rightarrow> real" and n:: nat
 assumes indp: "module.independent (\r. (*) (real_of_int r)) (\ ` {..
 and inj\<theta>: "inj_on \<theta> {..<n}" and "\<epsilon> > 0"
 obtains t h where "\i. i < n \ \t * \ i - of_int (h i) - \ i\ < \"
proof (cases "n>0")
 case False then show ?thesis
 using that by blast
next
 case True
 interpret Modules.module "(\r. (*) (real_of_int r))"
 by (simp add: Modules.module.intro distrib_left mult.commute)
 define F where "F \ \t. 1 + (\i * of_real (2 * pi * (t * \ i - \ i))))"
 define L where "L \ Sup (range (norm \ F))"
 have [continuous_intros]: "0 < T \ continuous_on {0..T} F" for T
 unfolding F_def by (intro continuous_intros)
 have nft_Sucn: "norm (F t) \ Suc n" for t
 unfolding F_def by (rule norm_triangle_le order_trans [OF norm_sum] | simp)+
 then have L_le: "L \ Suc n"
 by (simp add: L_def cSUP_least)
 have nft_L: "norm (F t) \ L" for t
 by (metis L_def UNIV_I bdd_aboveI2 cSUP_upper nft_Sucn o_apply)
 have "L = Suc n"
 proof -
 { fix p::nat
 assume "p>0"
 obtain N a r where 3: "\x. (1 + (\r
 and SucN: "Suc N \ (p+1)^n"
 and nontriv: "nontriv_exponents n N r" and uniq: "uniq_exponents n N r"
 and apos: "nonzero_coeffs N a"
 using Kronecker_simult_aux3_uniq_exponents by blast
 have "N \ 0"
 proof
 assume "N = 0"
 have "2^p = (1::complex)"
 using 3 [of "(\_. 0)(0:=1)"] True \p>0\ \N = 0\ by (simp add: gpoly_def)
 then have "2 ^ p = Suc 0"
 by (metis of_nat_1 One_nat_def of_nat_eq_iff of_nat_numeral of_nat_power)
 with \<open>0 < p\<close> show False by force
 qed
 define x where "x \ \t r. exp(\ * of_real (2 * pi * (t * \ r - \ r)))"
 define f where "f \ \t. (F t) ^ p"
 have feq: "f t = 1 + gpoly n (x t) N a r" for t
 unfolding f_def F_def x_def by (simp flip: 3)
 define c where "c \ \k. a k / cis (\i i * real (r k i)))))"
 define \<eta> where "\<eta> \<equiv> \<lambda>k. 2 * pi * (\<Sum>i<n. r k i * \<theta> i)"
 define INTT where "INTT \ \k T. (1/T) * integral {0..T} (\t. f t * exp(-\ * of_real t * \ k))"
 have "a k * (\i * t * \ k)" if "k
 apply (simp add: x_def \<eta>_def sum_distrib_left flip: exp_of_nat_mult exp_sum)
 apply (simp add: algebra_simps sum_subtractf exp_diff c_def sum_distrib_left cis_conv_exp)
 done
 then have fdef: "f t = 1 + (\k * of_real t * \ k))" for t
 by (simp add: feq gpoly_def)
 have nzero: "\ i \ 0" if "i
 using indp that local.dependent_zero by force
 have ind_disj: "\u. (\x x) = 0) \ (\v \ \`{.. 0"
 using indp by (auto simp: dependent_finite)
 have inj\<eta>: "inj_on \<eta> {..<N}"
 proof
 fix k k'
 assume k: "k \ {.. {.. k = \ k'"
 then have eq: "(\i i) = (\i i)"
 by (auto simp: \<eta>_def)
 define f where "f \ \z. let i = inv_into {.. z in int (r k i) - int (r k' i)"
 show "k = k'"
 using ind_disj [of f] inj\<theta> uniq eq k
 apply (simp add: f_def Let_def sum.reindex sum_subtractf algebra_simps uniq_exponents_def)
 by (metis not_less_iff_gr_or_eq)
 qed
 moreover have "0 \ \ ` {..
 unfolding \<eta>_def
 proof clarsimp
 fix k
 assume *: "(\i i) = 0" "k < N"
 define f where "f \ \z. let i = inv_into {.. z in int (r k i)"
 obtain i where "i and "r k i > 0"
 by (meson \<open>k < N\<close> nontriv nontriv_exponents_def zero_less_iff_neq_zero)
 with * nzero show False
 using ind_disj [of f] inj\<theta> by (simp add: f_def sum.reindex)
 qed
 ultimately have 15: "(INTT k \ c k) at_top" if "k
 unfolding fdef INTT_def using Kronecker_simult_aux1_strict that by presburger
 have norm_c: "norm (c k) \ L^p" if "k
 proof (intro tendsto_le [of _ "\_. L^p"])
 show "((norm \ INTT k) \ cmod (c k)) at_top"
 using that 15 by (simp add: o_def tendsto_norm)
 have "norm (INTT k T) \ L^p" if "T \ 0" for T::real
 proof -
 have "0 \ L ^ p"
 by (meson nft_L norm_ge_zero order_trans zero_le_power)
 have "norm (integral {0..T} (\t. f t * exp (- (\ * t * \ k))))
 \<le> integral {0..T} (\<lambda>t. L^p)" (is "?L \<le> ?R") if "T>0"
 proof -
 have "?L \ integral {0..T} (\t. norm (f t * exp (- (\ * t * \ k))))"
 unfolding f_def by (intro continuous_on_imp_absolutely_integrable_on continuous_intros that)
 also have "\ \ ?R"
 unfolding f_def
 by (intro integral_le continuous_intros integrable_continuous_interval that
 | simp add: nft_L norm_mult norm_power power_mono)+
 finally show ?thesis .
 qed
 with \<open>T \<ge> 0\<close> have "norm (INTT k T) \<le> (1/T) * integral {0..T} (\<lambda>t. L ^ p)"
 by (auto simp add: INTT_def norm_divide divide_simps simp del: integral_const_real)
 also have "\ \ L ^ p"
 using \<open>T \<ge> 0\<close> \<open>0 \<le> L ^ p\<close> by simp
 finally show ?thesis .
 qed
 then show "\\<^sub>F x in at_top. (norm \ INTT k) x \ L ^ p"
 using eventually_at_top_linorder that by fastforce
 qed auto
 then have "(\k N * L^p"
 by (metis sum_bounded_above card_lessThan lessThan_iff)
 moreover
 have "Re((1 + (\r_. 1) N a r)"
 using 3 [of "\_. 1"] by metis
 then have 14: "1 + (\k
 by (simp add: c_def norm_divide gpoly_def)
 moreover
 have "L^p \ 1"
 using norm_c [of 0] \<open>N \<noteq> 0\<close> apos
 by (force simp add: c_def norm_divide nonzero_coeffs_def)
 ultimately have *: "(1 + real n) ^ p \ Suc N * L^p"
 by (simp add: algebra_simps)
 have [simp]: "L>0"
 using \<open>1 \<le> L ^ p\<close> \<open>0 < p\<close> by (smt (verit, best) nft_L norm_ge_zero power_eq_0_iff)
 have "Suc n ^ p \ (p+1)^n * L^p"
 by (smt (verit, best) * mult.commute \<open>1 \<le> L ^ p\<close> SucN mult_left_mono of_nat_1 of_nat_add of_nat_power_eq_of_nat_cancel_iff of_nat_power_le_of_nat_cancel_iff plus_1_eq_Suc)
 then have "(Suc n ^ p) powr (1/p) \ ((p+1)^n * L^p) powr (1/p)"
 by (simp add: powr_mono2)
 then have "(Suc n) \ ((p+1)^n) powr (1/p) * L"
 using \<open>p > 0\<close> \<open>0 < L\<close> by (simp add: powr_powr powr_mult flip: powr_realpow)
 also have "\ = ((p+1) powr n) powr (1/p) * L"
 by (simp add: powr_realpow)
 also have "\ = (p+1) powr (n/p) * L"
 by (simp add: powr_powr)
 finally have "(n + 1) / L \ (p+1) powr (n/p)"
 by (simp add: divide_simps)
 then have "ln ((n + 1) / L) \ ln (real (p + 1) powr (real n / real p))"
 by (simp add: flip: ln_powr)
 also have "\ \ (n/p) * ln(p+1)"
 by (simp add: powr_def)
 finally have "ln ((n + 1) / L) \ (n/p) * ln(p+1) \ L > 0"
 by fastforce
 } note * = this
 then have [simp]: "L > 0"
 by blast
 have 0: "(\p. (n/p) * ln(p+1)) \ 0"
 by real_asymp
 have "ln (real (n + 1) / L) \ 0"
 using * eventually_at_top_dense by (intro tendsto_lowerbound [OF 0]) auto
 then have "n+1 \ L"
 using \<open>0 < L\<close> by (simp add: ln_div)
 then show ?thesis
 using L_le by linarith
 qed
 with Kronecker_simult_aux2 [of n \<theta> \<alpha>] \<open>\<epsilon> > 0\<close> that show thesis
 by (auto simp: F_def L_def add.commute diff_diff_eq)
qed

text \<open>Theorem 7.10\<close>

corollary Kronecker_thm_2:
 fixes \<alpha> \<theta> :: "nat \<Rightarrow> real" and n :: nat
 assumes indp: "module.independent (\r x. of_int r * x) (\ ` {..n})"
 and inj\<theta>: "inj_on \<theta> {..n}" and [simp]: "\<theta> n = 1" and "\<epsilon> > 0"
 obtains k m where "\i. i < n \ \of_int k * \ i - of_int (m i) - \ i\ < \"
proof -
 interpret Modules.module "(\r. (*) (real_of_int r))"
 by (simp add: Modules.module.intro distrib_left mult.commute)
 have one_in_\<theta>: "1 \<in> \<theta> ` {..n}"
 unfolding \<open>\<theta> n = 1\<close>[symmetric] by blast

 have not_in_Ints: "\ i \ \" if i: "i < n" for i
 proof
 assume "\ i \ \"
 then obtain m where m: "\ i = of_int m"
 by (auto elim!: Ints_cases)
 have not_one: "\ i \ 1"
 using inj_onD[OF inj\<theta>, of i n] i by auto
 define u :: "real \ int" where "u = (\_. 0)(\ i := 1, 1 := -m)"
 show False
 using independentD[OF indp, of "\ ` {i, n}" u "\ i"] \i < n\ not_one one_in_\
 by (auto simp: u_def simp flip: m)
 qed

 have inj\<theta>': "inj_on (frac \<circ> \<theta>) {..n}"
 proof (rule linorder_inj_onI')
 fix i j assume ij: "i \ {..n}" "j \ {..n}" "i < j"
 show "(frac \ \) i \ (frac \ \) j"
 proof (cases "j = n")
 case True
 thus ?thesis
 using not_in_Ints[of i] ij by auto
 next
 case False
 hence "j < n"
 using ij by auto
 have "inj_on \ (set [i, j, n])"
 using inj\<theta> by (rule inj_on_subset) (use ij in auto)
 moreover have "distinct [i, j, n]"
 using \<open>j < n\<close> ij by auto
 ultimately have "distinct (map \ [i, j, n])"
 unfolding distinct_map by blast
 hence distinct: "distinct [\ i, \ j, 1]"
 by simp

 show "(frac \ \) i \ (frac \ \) j"
 proof
 assume eq: "(frac \ \) i = (frac \ \) j"
 define u :: "real \ int" where "u = (\_. 0)(\ i := 1, \ j := -1, 1 := \\ j\ - \\ i\)"
 have "(\v\{\ i, \ j, 1}. real_of_int (u v) * v) = frac (\ i) - frac (\ j)"
 using distinct by (simp add: u_def frac_def)
 also have "\ = 0"
 using eq by simp
 finally have eq0: "(\v\{\ i, \ j, 1}. real_of_int (u v) * v) = 0" .
 show False
 using independentD[OF indp _ _ eq0, of "\ i"] one_in_\ ij distinct
 by (auto simp: u_def)
 qed
 qed
 qed

 have "frac (\ n) = 0"
 by auto
 then have \<theta>no_int: "of_int r \<notin> \<theta> ` {..<n}" for r
 using inj\<theta>' frac_of_int
 apply (simp add: inj_on_def Ball_def)
 by (metis \<open>frac (\<theta> n) = 0\<close> frac_of_int imageE le_less lessThan_iff less_irrefl)
 define \<theta>' where "\<theta>' \<equiv> (frac \<circ> \<theta>)(n:=1)"
 have [simp]: "{.. {x. x \ n} = {..
 by auto
 have \<theta>image[simp]: "\<theta> ` {..n} = insert 1 (\<theta> ` {..<n})"
 using lessThan_Suc lessThan_Suc_atMost by force
 have "module.independent (\r. (*) (of_int r)) (\' ` {..
 unfolding dependent_explicit \<theta>'_def
 proof clarsimp
 fix T u v
 assume T: "T \ insert 1 ((\i. frac (\ i)) ` {..
 and "finite T"
 and uv_eq0: "(\v\T. of_int (u v) * v) = 0"
 and "v \ T"
 define invf where "invf \ inv_into {.. \)"
 have "inj_on (\x. frac (\ x)) {..
 using inj\<theta>' by (auto simp: inj_on_def)
 then have invf [simp]: "invf (frac (\ i)) = i" if "i
 using frac_lt_1 [of "\ i"] that by (auto simp: invf_def o_def inv_into_f_eq [where x=i])
 define N where "N \ invf ` (T - {1})"
 have Nsub: "N \ {..n}" and "finite N"
 using T \<open>finite T\<close> by (auto simp: N_def subset_iff)
 have inj_invf: "inj_on invf (T - {1})"
 using \<theta>no_int [of 1] \<open>\<theta> n = 1\<close> inv_into_injective T
 by (fastforce simp: inj_on_def invf_def)
 have invf_iff: "invf t = i \ (i t = frac (\ i))" if "t \ T-{1}" for i t
 using that T by auto
 have sumN: "(\i\N. f i) = (\x\T - {1}. f (invf x))" for f :: "nat \ int"
 using inj_invf T by (simp add: N_def sum.reindex)
 define T' where "T' \<equiv> insert 1 (\<theta> ` N)"
 have [simp]: "finite T'" "1 \ T'"
 using T'_def N_def \finite T\ by auto
 have T'sub: "T' \<subseteq> \<theta> ` {..n}"
 using Nsub T'_def \image by blast
 have in_N_not1: "x \ N \ \ x \ 1" for x
 using \<theta>no_int [of 1] by (metis N_def image_iff invf_iff lessThan_iff of_int_1)
 define u' where "u' = (u \<circ> frac)(1:=(if 1\<in>T then u 1 else 0) + (\<Sum>i\<in>N. - \<lfloor>\<theta> i\<rfloor> * u (frac (\<theta> i))))"
 have "(\v\T'. real_of_int (u' v) * v) = u' 1 + (\v \ \ ` N. real_of_int (u' v) * v)"
 using \<open>finite N\<close> by (simp add: T'_def image_iff in_N_not1)
 also have "\ = u' 1 + sum ((\v. real_of_int (u' v) * v) \ \) N"
 by (smt (verit) N_def \<open>finite N\<close> image_iff invf_iff sum.reindex_nontrivial)
 also have "\ = u' 1 + (\i\N. of_int ((u \ frac) (\ i)) * \ i)"
 by (auto simp add: u'_def in_N_not1)
 also have "\ = u' 1 + (\i\N. of_int ((u \ frac) (\ i)) * (floor (\ i) + frac(\ i)))"
 by (simp add: frac_def cong: if_cong)
 also have "\ = (\v\T. of_int (u v) * v)"
 proof (cases "1 \ T")
 case True
 then have T1: "(\v\T. real_of_int (u v) * v) = u 1 + (\v\T-{1}. real_of_int (u v) * v)"
 by (simp add: \<open>finite T\<close> sum.remove)
 show ?thesis
 using inj_invf True T unfolding N_def u'_def
 by (auto simp: add.assoc distrib_left sum.reindex T1 simp flip: sum.distrib intro!: sum.cong)
 next
 case False
 then show ?thesis
 using inj_invf T unfolding N_def u'_def
 by (auto simp: algebra_simps sum.reindex simp flip: sum.distrib intro!: sum.cong)
 qed
 also have "\ = 0"
 using uv_eq0 by blast
 finally have 0: "(\v\T'. real_of_int (u' v) * v) = 0" .
 have "u v = 0" if T'0: "\v. v\T' \ u' v = 0"
 proof -
 have [simp]: "u t = 0" if "t \ T - {1}" for t
 proof -
 have "\ (invf t) \ T'"
 using N_def T'_def that by blast
 then show ?thesis
 using that T'0 [of "\ (invf t)"]
 by (smt (verit, best) in_N_not1 N_def fun_upd_other imageI invf_iff o_apply u'_def)
 qed
 show ?thesis
--> --------------------

--> maximum size reached

--> --------------------

quality99%

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.