Theory HOL-Analysis.Kronecker_Approximation_Theorem

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 "x0" 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 "xx'" "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/k2}" 
  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 "xA. x0" 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/k2"
      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 : "ξ < ε"
      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  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)  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 : "ξ < ε"
      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  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  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" "a0"
  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. rN. 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. rN. 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. (rN. 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. (rN. c' r * exp (𝗂 * of_real t * η' r)) *
                    exp (- 𝗂 * t * η' (Suc k))))  c' (Suc k))
       at_top"
    by (intro Kronecker_simult_aux1)
  moreover have "(rN. 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, natcomplex, nat, natnat, [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, natnat]  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 " = (qp. (p choose q) * (1 + (i<n. x i))^q * x n^(p-q))"
      by (simp add: binomial_ring)
    also have " = (qp. (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 = (qp. Suc (Nf q))"
      by (simp add: N_def peq)
    also have "  (qp. (q+1)^n)"
      by (meson Nle sum_mono)
    also have "  (qp. (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 integral_le continuous_intros integrable_continuous_interval that
                  | simp add: nft_L norm_mult norm_power power_mono)+
            finally show ?thesis .
          qed
          with T  0 have "norm (INTT k T)  (1/T) * integral {0..T} (λt. L ^ p)"
            by (auto simp add: INTT_def norm_divide divide_simps simp del: integral_const_real)
          also have "  L ^ p"
            using T  0 0  L ^ p by simp
          finally show ?thesis .
        qed
        then show "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. cmod (c k))  N * L^p"
        by (metis sum_bounded_above card_lessThan lessThan_iff)
      moreover
      have "Re((1 + (r<n. 1)) ^ p) = Re (1 + gpoly n (λ_. 1) N a r)"
        using 3 [of "λ_. 1"] by metis
      then have 14: "1 + (k<N. norm (c k)) = (1 + real n) ^ p"
        by (simp add: c_def norm_divide gpoly_def)
      moreover 
      have "L^p  1"
        using norm_c [of 0] N  0 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 1  L ^ p 0 < p 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 1  L ^ p 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 p > 0 0 < L 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
      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"
      by (simp add: ln_div)
    then show ?thesis
      using L_le by linarith
  qed
  with Kronecker_simult_aux2 [of n θ α] ε > 0 that show thesis
    by (auto simp: F_def L_def add.commute diff_diff_eq)
qed


text ‹Theorem 7.10›

corollary Kronecker_thm_2:
  fixes α θ :: "nat  real" and n :: nat
  assumes indp: "module.independent (λr x. of_int r * x) (θ ` {..n})"
    and injθ: "inj_on θ {..n}" and [simp]: "θ n = 1" and "ε > 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_θ: "1  θ ` {..n}"
    unfolding θ n = 1[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θ, 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θ': "inj_on (frac  θ) {..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θ by (rule inj_on_subset) (use ij in auto)
      moreover have "distinct [i, j, n]"
        using j < n 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 θno_int: "of_int r  θ ` {..<n}" for r
    using injθ' frac_of_int  
    apply (simp add: inj_on_def Ball_def)
    by (metis frac (θ n) = 0 frac_of_int imageE le_less lessThan_iff less_irrefl)
  define θ' where "θ'  (frac  θ)(n:=1)"
  have [simp]: "{..<Suc n}  {x. x  n} = {..<n}"
    by auto
  have θimage[simp]: "θ ` {..n} = insert 1 (θ ` {..<n})"
    using lessThan_Suc lessThan_Suc_atMost by force
  have "module.independent (λr. (*) (of_int r)) (θ' ` {..<Suc n})"
    unfolding dependent_explicit θ'_def
  proof clarsimp
    fix T u v
    assume T: "T  insert 1 ((λi. frac (θ i)) ` {..<n})"
      and "finite T"
      and uv_eq0: "(vT. of_int (u v) * v) = 0"
      and "v  T"
    define invf where "invf  inv_into {..<n} (frac  θ)"
    have "inj_on (λx. frac (θ x)) {..<n}"
      using injθ' by (auto simp: inj_on_def)
    then have invf [simp]: "invf (frac (θ i)) = i" if "i<n" for 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 finite T by (auto simp: N_def subset_iff)
    have inj_invf: "inj_on invf (T - {1})"
      using θno_int [of 1] θ n = 1 inv_into_injective T
      by (fastforce simp: inj_on_def invf_def)
    have invf_iff: "invf t = i  (i<n  t = frac (θ i))" if "t  T-{1}" for i t
      using that T by auto
    have sumN: "(iN. f i) = (xT - {1}. f (invf x))" for f :: "nat  int"
      using inj_invf T  by (simp add: N_def sum.reindex)
    define T' where "T'  insert 1 (θ ` N)"
    have [simp]: "finite T'" "1  T'"
      using T'_def N_def finite T by auto
    have T'sub: "T'  θ ` {..n}"
      using Nsub T'_def θimage by blast
    have in_N_not1: "x  N  θ x  1" for x
      using θno_int [of 1] by (metis N_def image_iff invf_iff lessThan_iff of_int_1)
    define u' where "u' = (u  frac)(1:=(if 1T then u 1 else 0) + (iN. - θ i * u (frac (θ i))))"
    have "(vT'. real_of_int (u' v) * v) = u' 1 + (v  θ ` N. real_of_int (u' v) * v)"
      using finite N 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 finite N image_iff invf_iff sum.reindex_nontrivial)
    also have " = u' 1 + (iN. of_int ((u  frac) (θ i)) * θ i)"
      by (auto simp add: u'_def in_N_not1)
    also have " = u' 1 + (iN. of_int ((u  frac) (θ i)) * (floor (θ i) + frac(θ i)))"
      by (simp add: frac_def cong: if_cong)
    also have " = (vT. of_int (u v) * v)"
    proof (cases "1  T")
      case True
      then have T1: "(vT. real_of_int (u v) * v) = u 1 + (vT-{1}. real_of_int (u v) * v)"
        by (simp add: finite T 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: "(vT'. real_of_int (u' v) * v) = 0" .
    have "u v = 0" if T'0: "v. vT'  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
      proof (cases "v = 1")
        case True
        then have "1  T"
          using v  T by blast
        have "(vT. real_of_int (u v) * v) = u 1 + (vT - {1}. real_of_int (u v) * v)"
          using True finite T v  T mk_disjoint_insert by fastforce
        then have "0 = u 1"
          using uv_eq0 by auto
        with True show ?thesis by presburger
      next
        case False
        then have "θ (invf v)  θ ` N"
          using N_def v  T by blast
        then show ?thesis
          using that [of "θ (invf v)"] False v  T T by (force simp: T'_def in_N_not1 u'_def)
      qed
    qed
    with indp T'sub finite T' 0 show "u v = 0"
      unfolding dependent_explicit by blast
  qed
  moreover have "inj_on θ' {..<Suc n}"
    using injθ' 
    unfolding θ'_def inj_on_def 
    by (metis comp_def frac_lt_1 fun_upd_other fun_upd_same lessThan_Suc_atMost less_irrefl)
  ultimately obtain t h where th: "i. i < Suc n  ¦t * θ' i - of_int (h i) - (α(n:=0)) i¦ < ε/2"
    using Kronecker_thm_1 [of θ' "Suc n" "ε/2"] lessThan_Suc_atMost assms using half_gt_zero by blast
  define k where "k = h n"
  define m where "m  λi. h i + k * θ i"
  show thesis
  proof
    fix i assume "i < n"
    have "¦k * frac (θ i) - h i - α i¦ < ε" 
    proof -
      have "¦k * frac (θ i) - h i - α i¦ = ¦t * frac (θ i) - h i - α i + (k-t) * frac (θ i)¦"
        by (simp add: algebra_simps)
      also have "  ¦t * frac (θ i) - h i - α i¦ + ¦(k-t) * frac (θ i)¦"
        by linarith
      also have "  ¦t * frac (θ i) - h i - α i¦ + ¦k-t¦"
        using frac_lt_1 [of "θ i"] le_less by (fastforce simp add: abs_mult)
      also have " < ε"
        using th[of i] th[of n] i<n 
        by (simp add: k_def θ'_def) (smt (verit, best))
      finally show ?thesis .
    qed
    then show "¦k * θ i - m i - α i¦ < ε"
      by (simp add: algebra_simps frac_def m_def)
  qed
qed
(* TODO: use something like module.independent_family instead *)


end