chapter ‹Kronecker's Theorem with Applications› theory Kronecker_Approximation_Theorem imports Complex_Transcendental Henstock_Kurzweil_Integration "HOL-Real_Asymp.Real_Asymp" begin section ‹Dirichlet's Approximation Theorem› text ‹Simultaneous version. From Hardy and Wright, An Introduction to the Theory of Numbers, page 170.› theorem Dirichlet_approx_simult: fixes θ :: "nat ⇒ real" and N n :: nat assumes "N > 0" obtains q p where "0<q" "q ≤ int (N^n)" and "⋀i. i<n ⟹ ¦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..<n]" define X where "X ≡ fracs ` {..N^n}" define Y where "Y ≡ set (List.n_lists n (map interv [0..<N]))" 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 ⟶ ¬(∀i<n. ¦frac (real b * θ i) - frac (real a * θ i)¦ < 1/N)" proof - have "inj_on (λk. map (λi. frac (k * θ i)) [0..<n]) {..N^n}" 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<n" for i using that ‹x' ∈ X› by (auto simp: X_def fracs_def) have "f x ∈ Y" using ‹f ` X ⊆ Y› ‹x ∈ X› 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 ‹i<n› assms by (auto simp: divide_simps k_def interv_def xeq fracs_def) linarith then have k': "x'!i ∈ interv(k!i)" using ‹i<n› eq assms ge0[OF ‹i<n›] by (auto simp: k_def f_def divide_simps map_equality_iff in_interv interv_iff) with assms k show ?thesis using ‹i<n› 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" "b ≤ N^n" and *: "⋀i. i<n ⟹ ¦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 fix i assume "i<n" have "frac (b * θ i) - frac (a * θ i) = ?k * θ i - ?h i" using ‹a < b› by (simp add: frac_def left_diff_distrib' of_nat_diff) then show "¦of_int ?k * θ i - ?h i¦ < 1/N" by (metis "*" ‹i < n› of_int_of_nat_eq) qed (use ‹a < b› ‹b ≤ N^n› in auto) qed text ‹Theorem 7.1› corollary Dirichlet_approx: fixes θ:: 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 θ="λ_. θ"]) auto text ‹Theorem 7.2› corollary Dirichlet_approx_coprime: fixes θ:: 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) ‹k'>0› 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 ‹k'>0› 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 ‹k'>0› 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 ∧ coprime h k ∧ ¦θ - of_int h / of_int k¦ < 1/k⇧^{2}}" for θ::real text ‹Theorem 7.3› lemma approx_set_nonempty: "approx_set θ ≠ {}" proof - have "¦θ - of_int ⌊θ⌋ / of_int 1¦ < 1 / (of_int 1)⇧^{2}" by simp linarith then have "(⌊θ⌋, 1) ∈ approx_set θ" by (auto simp: approx_set_def) then show ?thesis by blast qed text ‹Theorem 7.4(c)› 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] ‹k>0› 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 ‹Theorem 7.4(b,d)› 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)⇧^{2}" by (auto simp: approx_set_def eq) have False if "a * k = h * b" proof - have "b dvd k" using that ‹coprime a b› 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 ‹0 < b› that by force then show False using ‹0 < b› ‹b < k› ‹coprime h k› ‹k = b * d› by auto qed then have 0: "0 < ¦a*k - b*h¦" by auto have "¦a*k - b*h¦ < b/k" using ‹k>0› ‹b>0› hk by (simp add: field_simps eval_nat_numeral) also have "… < 1" by (simp add: ‹0 < k› ‹b < k›) 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 ?α = "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 α: "?α > 0" using Min_in by force then obtain N where N: "real N > 1 / ?α" using reals_Archimedean2 by blast have "0 < 1 / ?α" using α by auto also have "… < real N" by (fact N) finally have "N > 0" by simp from N have "1/N < ?α" by (simp add: α 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 α 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 §: "¦θ - h/k¦ < 1 / (k*N)" by (simp add: field_simps) also have "… ≤ 1/k⇧^{2}" using ‹k ≤ int N› by (simp add: eval_nat_numeral divide_simps) finally have hk_in: "(h,k) ∈ approx_set θ" using ‹0 < k› ‹coprime h k› 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 ‹k > 0› α ‹N > 0› N by (intro divide_strict_right_mono) (auto simp: field_simps) also have "… ≤ ?α / 1" using α ‹k > 0› by (intro divide_left_mono) auto finally show ?thesis by simp qed ultimately show False using A § by auto qed qed text ‹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.› section ‹Kronecker's Approximation Theorem: the One-dimensional Case› 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 ‹auto simp: divide_simps mult_ac frac_lt_1›) then show ?thesis by simp qed text ‹Concrete statement of Theorem 7.7, and the real proof› theorem Kronecker_approx_1_explicit: fixes θ :: 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 ‹ε > 0› 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 ‹0 < k› less_irrefl linorder_neqE_linordered_idom) then show thesis proof cases case 1 define ξ where "ξ ≡ 1 - frac (of_int k * θ)" have pos: "ξ > 0" by (simp add: ξ_def frac_lt_1) define N where "N ≡ ⌊1/ξ⌋" have "N > 0" by (simp add: N_def ξ_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: ξ_def frac_def) from r pos s ‹k > 0› have "θ = (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 ‹0 < N› of_int_1_less_iff pos_divide_less_eq) then have ex: "∃m. int m ≤ N+1 ∧ 1-α < m * ξ" by (smt (verit, best) ‹0 < N› ‹0 ≤ α› 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 ‹α ≤ 1› by force have kθ: "ξ < ε" using hk 1 by (smt (verit, best) floor_eq_iff frac_def ξ_def) show thesis proof (cases "m=1") case True then have "¦frac (real (nat k) * θ) - α¦ < ε" using m ‹α ≤ 1› ‹0 < k› ξ_def kθ by force with ‹0 < k› zero_less_nat_eq that show thesis by blast next case False with ‹0 < m› have "m>1" by linarith have "ξ < 1 / N" by (metis N0 ‹0 < N› mult_of_int_commute of_int_pos pos pos_less_divide_eq) also have "… ≤ 1 / (real m - 1)" using ‹m > 1› 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: ξ_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 ‹0 < m› m_def of_nat_le_iff) ultimately have leα: " α ≤ frac (of_int ((int m - 1) * k) * θ)" by (simp add: Suc_leI ‹0 < m› 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 ‹0 < m› int_ops(2) kθ m of_nat_diff) with that show thesis by (metis ‹0 < k› ‹1 < m› mult_pos_pos of_int_of_nat_eq of_nat_mult pos_int_cases zero_less_diff) qed next case 2 define ξ where "ξ ≡ frac (of_int k * θ)" have recip_frac: False if "1/ξ ∈ ℤ" proof - have "frac (of_int k * θ) ∈ ℚ" using that unfolding ξ_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 ‹0 < k› frac_in_Rats_iff irrat by blast qed have pos: "ξ > 0" by (metis ξ_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) ξ_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 ‹0 < N› of_int_1_less_iff pos_divide_less_eq) then have ex: "∃m. int m ≤ N+1 ∧ α < m * ξ" by (smt (verit, best) mult.commute ‹α ≤ 1› ‹0 < N› 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 ‹0 ≤ α› m gr0I by force have kθ: "ξ < ε" using hk 2 unfolding ξ_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 ‹auto simp: divide_simps mult_ac›) show thesis proof (cases "m=1") case True then have "¦frac (real (nat k) * θ) - α¦ < ε" using m α ‹0 < k› ξ_def kθ by force with ‹0 < k› zero_less_nat_eq that show ?thesis by blast next case False with ‹0 < m› have "m>1" by linarith with ‹0 < k› 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 ξ_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 ‹m>1› by (simp add: divide_simps mult_ac ξ_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 ‹0 < m› m_def of_nat_le_iff) ultimately have leα: "frac (of_int ((int m - 1) * k) * θ) ≤ α" by (simp add: Suc_leI ‹0 < m› 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 ‹0 < k› ‹0 < m› by simp (smt (verit, best) One_nat_def Suc_leI m of_nat_1 of_nat_diff) with ‹m > 0› that show thesis using mk_pos One_nat_def by presburger qed qed qed text ‹Theorem 7.7 expressed more abstractly using @{term closure}› corollary Kronecker_approx_1: fixes θ :: 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 ‹The next theorem removes the restriction $0 \leq \alpha \leq 1$.› text ‹Theorem 7.8› corollary sequence_of_fractional_parts_is_dense: fixes θ :: 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 ‹0 < k› of_nat_0_less_iff that) qed section ‹Extension of Kronecker's Theorem to Simultaneous Approximation› subsection ‹Towards Lemma 1› 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 ‹T ≥ 0›) then show ?thesis by (simp add: diff_divide_distrib integral_unique) qed lemma Kronecker_simult_aux1: fixes η:: "nat ⇒ real" and c:: "nat ⇒ 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 + (∑r ∈ {..N}-{k}. c r * integral {0..T} (λt. exp(𝗂 * (η r - η k) * of_real t)))" if "T > 0" for T using ‹k ≤ N› 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 + (∑r ∈ {..N}-{k}. c r * (exp(𝗂 * (η r - η k) * of_real T) - 1) / (𝗂 * (η r - η 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(𝗂 * (η r - η k) * T) - 1) / (𝗂 * (η r - η k))" if "r ≤ N" "r ≠ k" for r using that ‹k ≤ N› inj ‹T > 0› integral_exp [of T "𝗂 * (η r - η 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) / (𝗂 * (η r - η k) * of_real T))) ⤏ c k + 0) at_top" by (intro tendsto_add tendsto_null_sum) auto also have "?this ⟷ ?thesis" proof (rule filterlim_cong) show "∀⇩_{F}x in at_top. c k + (∑r∈{..N} - {k}. c r * (exp (𝗂 * of_real (η r - η k) * of_real x) - 1) / (𝗂 * of_real (η r - η k) * of_real x)) = 1 / of_real x * integral {0..x} (λt. f t * exp (- 𝗂 * of_real t * of_real (η 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 ‹the version of Lemma 1 that we actually need› lemma Kronecker_simult_aux1_strict: fixes η:: "nat ⇒ real" and c:: "nat ⇒ complex" and N::nat assumes η: "inj_on η {..<N}" "0 ∉ η ` {..<N}" and "k < N" defines "f ≡ λt. 1 + (∑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 c' where "c' ≡ case_nat 1 c" define η' where "η' ≡ case_nat 0 η" define f' where "f' ≡ λt. (∑r≤N. c' r * exp(𝗂 * of_real t * η' r))" have "inj_on η' {..N}" using η by (auto simp: η'_def inj_on_def split: nat.split_asm) moreover have "Suc k ≤ N" using ‹k < N› by auto ultimately have "((λT. 1 / T * integral {0..T} (λt. (∑r≤N. c' r * exp (𝗂 * of_real t * η' r)) * exp (- 𝗂 * t * η' (Suc k)))) ⤏ c' (Suc k)) at_top" by (intro Kronecker_simult_aux1) moreover have "(∑r≤N. c' r * exp (𝗂 * of_real t * η' r)) = 1 + (∑r<N. c r * exp (𝗂 * 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 ‹Towards Lemma 2› 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 α:: "nat ⇒ real" and θ:: "nat ⇒ real" and n::nat defines "F ≡ λt. 1 + (∑r<n. exp(𝗂 * of_real (2 * pi * (t * θ r - α r))))" defines "L ≡ Sup (range (norm ∘ F))" shows "(∀ε>0. ∃t h. ∀r<n. ¦t * θ r - α r - of_int (h r)¦ < ε) ⟷ L = Suc n" (is "?lhs = _") proof assume ?lhs then have "⋀k. ∃t h. ∀r<n. ¦t * θ r - α r - of_int (h r)¦ < 1 / (2 * pi * Suc k)" by simp then obtain t h where th: "⋀k r. r<n ⟹ ¦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<n" for 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<n. cos(1 / Suc k))" by simp also have "… ≤ 1 + (∑r<n. cos (2 * pi * (t k * θ 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. ∃k<n. ¦t * θ k - α k - of_int (h k)¦ ≥ e0" by (force simp: not_less) define ε where "ε ≡ min e0 (pi/4)" have ε: "⋀t h. ∃k<n. ¦t * θ k - α k - of_int (h k)¦ ≥ ε" unfolding ε_def using e0 min.coboundedI1 by blast have ε_bounds: "ε > 0" "ε < pi" "ε ≤ pi/4" using ‹e0 > 0› by (auto simp: ε_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 δ where "δ > 0" and δ: "norm (1 + exp (𝗂 * ε)) = 2 - δ" 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 * θ r - α 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<n" and 1: "¦X k¦ ≥ ε" using X_def ε [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 ε "2 * pi * X k"] ε_bounds by linarith have "norm (F t) = norm (1 + (∑r<n. exp(𝗂 * 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 ∈ {..<n}-{k}. exp(𝗂 * of_real (2 * pi * X r))))" by (simp add: comm_monoid_add_class.sum.remove [where x=k] ‹k < n› algebra_simps) also have "… ≤ norm (1 + exp(𝗂 * of_real (2 * pi * X k))) + (∑r ∈ {..<n}-{k}. norm (exp(𝗂 * of_real (2 * pi * X r))))" by (intro norm_triangle_mono sum_norm_le order_refl) also have "… ≤ (2 - δ) + (n - 1)" using ‹k < n› δ by simp (metis "*" mult_2 of_real_add of_real_mult) also have "… = n + 1 - δ" using ‹k < n› by simp finally show ?thesis . qed then have "L ≤ 1 + real n - δ" by (auto simp: L_def intro: cSup_least) with L ‹δ > 0› show False by linarith qed qed subsection ‹Towards lemma 3› text ‹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).› text ‹Some tools for combining integer-indexed sequences or splitting them into parts› lemma less_sum_nat_iff: fixes b::nat and k::nat shows "b < (∑i<k. a i) ⟷ (∃j<k. (∑i<j. a i) ≤ b ∧ b < (∑i<j. a i) + a j)" 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<k. a i) ⟷ (∃!j. j<k ∧ (∑i<j. a i) ≤ b ∧ b < (∑i<j. a i) + a j)" 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<k ∧ (∑i<j. a i) ≤ b ∧ b < (∑i<j. a i) + a j)" lemma part: "b < (∑i<k. a 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 {..<k} ≤ b ∧ b < sum a {..<k} + a k then k else part a k b)" using leD by (fastforce simp: part_def less_Suc_eq less_sum_nat_iff conj_disj_distribR cong: conj_cong) text ‹The polynomial expansions used in Lemma 3› definition gpoly :: "[nat, nat⇒complex, nat, nat⇒nat, [nat,nat]⇒nat] ⇒ complex" where "gpoly n x N a r ≡ (∑k<N. a k * (∏i<n. x i ^ r k i))" lemma gpoly_cong: assumes "⋀k. k < N ⟹ a' k = a k" "⋀k i. ⟦k < N; i<n⟧ ⟹ 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 k<N then a k else a' (k-N)) (λk. if k<N then r k else r' (k-N))" proof - have "{..<N+N'} = {..<N} ∪ {N..<N+N'}" "{..<N} ∩ {N..<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 {..<p}" defines "a ≡ λk. let q = (part Nf p k) in af q (k - sum Nf {..<q})" defines "r ≡ λk. let q = (part Nf p k) in rf q (k - sum Nf {..<q})" shows "(∑q<p. gpoly n x (Nf q) (af q) (rf q)) = gpoly n x N a r" 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 ‹For excluding constant terms: with all exponents zero› definition nontriv_exponents :: "[nat, nat, [nat,nat]⇒nat] ⇒ bool" where "nontriv_exponents n N r ≡ ∀k<N. ∃i<n. r k i ≠ 0" lemma nontriv_exponents_add: "⟦nontriv_exponents n M r; nontriv_exponents (Suc n) N r'⟧ ⟹ nontriv_exponents (Suc n) (M + N) (λ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 {..<p}) (λk. let q = part N p k in r q (k - sum N {..<q}))" 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 ≡ ∀k<N. ∀k'<k. ∃i<n. r k i ≠ r k' i" lemma uniq_exponents_inj: "uniq_exponents n N r ⟹ inj_on r {..<N}" by (smt (verit, best) inj_on_def lessThan_iff linorder_cases uniq_exponents_def) text ‹All coefficients must be nonzero› definition nonzero_coeffs :: "[nat, nat⇒nat] ⇒ bool" where "nonzero_coeffs N a ≡ ∀k<N. a k ≠ 0" text ‹Any polynomial expansion can be cleaned up, removing zero coeffs, etc.› 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<N. a k = 0") 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<n then f i else (0::nat)" for f i define R where "R ≡ cut ` r ` ({..<N} ∩ {k. a k > 0})" define N' where "N' ≡ card R" define r' where "r' ≡ from_nat_into R" define a' where "a' ≡ λk'. ∑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' {..<N'} 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<n. r' k 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 ‹k < N'› ‹k' < N'› 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) ` {..<N}" 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<n. x i ^ r k i) = (∑i<N'. (if r' i = cut (r k) then of_nat (a k) else of_nat 0) * (∏j<n. x j ^ r' i j))" if "k<N" 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="{..<N'}"] if_distrib [of of_nat]) qed show "nontriv_exponents n N' r'" if ne: "nontriv_exponents n N r" proof - have "∃i<n. 0 < r' k' i" if "k' < N'" for k' proof - have "r' k' ∈ R" using bij bij_betwE that by blast then obtain k where "k<N" and k: "r' k' = cut (r k)" using R_def by blast with ne obtain i where "i<n" "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<N" "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<n. x i))^p = 1 + gpoly n x N a r) ∧ Suc N ≤ (p+1)^n ∧ 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<n. x i)) ^ q = 1 + gpoly n x (Nf q) (af q) (rf q)" 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<p. Suc (Nf q))" define a where "a ≡ λk. if k < Nf p then af p k else let q = part (λt. Suc (Nf t)) p (k - Nf p) in (p choose q) * (if k - Nf p - (∑t<q. Suc (Nf t)) = Nf q then Suc 0 else af q (k - Nf p - (∑t<q. Suc(Nf t))))" define r where "r ≡ λk. if k < Nf p then (rf p k)(n := 0) else let q = part (λt. Suc (Nf t)) p (k - Nf p) in (if k - Nf p - (∑t<q. Suc (Nf t)) = Nf q then λ_. 0 else rf q (k - Nf p - (∑t<q. Suc(Nf t)))) (n := p-q)" have peq: "{..p} = insert p {..<p}" by auto have "nontriv_exponents n (Nf p) (λi. (rf p i)(n := 0))" "⋀q. q<p ⟹ 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<n. x i) + x n) ^ p" by (simp add: add_ac) also have "… = (∑q≤p. (p choose q) * (1 + (∑i<n. x i))^q * x n^(p-q))" 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<p. (p choose q) * (1 + gpoly n x (Nf q) (af q) (rf q)) * x n^(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 {..<Suc n}) ^ p = 1 + gpoly (Suc n) x N a r" . } 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<n. x i))^p = 1 + gpoly n x N a r" "Suc N ≤ (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<n. x r)) ^ p = 1 + gpoly n x N0 a0 r0" 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 ‹And finally Kroncker's theorem itself› text ‹Statement of Theorem 7.9› theorem Kronecker_thm_1: fixes α θ:: "nat ⇒ real" and n:: nat assumes indp: "module.independent (λr. (*) (real_of_int r)) (θ ` {..<n})" and injθ: "inj_on θ {..<n}" and "ε > 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<n. exp(𝗂 * 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<n. x r)) ^ p = 1 + gpoly n x N a 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 ‹0 < p› 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<n. (pi * (2 * (α i * real (r k i)))))" define η where "η ≡ λk. 2 * pi * (∑i<n. r k i * θ i)" define INTT where "INTT ≡ λk T. (1/T) * integral {0..T} (λt. f t * exp(-𝗂 * of_real t * η k))" have "a k * (∏i<n. x t i ^ r k i) = c k * exp (𝗂 * t * η k)" if "k<N" for k t apply (simp add: x_def η_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<N. c k * exp(𝗂 * of_real t * η k))" for t by (simp add: feq gpoly_def) have nzero: "θ i ≠ 0" if "i<n" for i using indp that local.dependent_zero by force have ind_disj: "⋀u. (∀x<n. u (θ x) = 0) ∨ (∑v ∈ θ`{..<n}. of_int (u v) * v) ≠ 0" using indp by (auto simp: dependent_finite) have injη: "inj_on η {..<N}" proof fix k k' assume k: "k ∈ {..<N}" "k' ∈ {..<N}" and "η k = η k'" then have eq: "(∑i<n. real (r k i) * θ i) = (∑i<n. real (r k' i) * θ i)" by (auto simp: η_def) define f where "f ≡ λz. let i = inv_into {..<n} θ z in int (r k i) - int (r k' i)" show "k = k'" using ind_disj [of f] injθ 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 ∉ η ` {..<N}" unfolding η_def proof clarsimp fix k assume *: "(∑i<n. real (r k i) * θ i) = 0" "k < N" define f where "f ≡ λz. let i = inv_into {..<n} θ z in int (r k i)" obtain i where "i<n" and "r k i > 0" by (meson ‹k < N› nontriv nontriv_exponents_def zero_less_iff_neq_zero) with * nzero show False using ind_disj [of f] injθ by (simp add: f_def sum.reindex) qed ultimately have 15: "(INTT k ⤏ c k) at_top" if "k<N" for k unfolding fdef INTT_def using Kronecker_simult_aux1_strict that by presburger have norm_c: "norm (c k) ≤ L^p" if "k<N" for 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)))) ≤ integral {0..T} (λt. L^p)" (is "?L ≤ ?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 <