Quelle Kronecker_Approximation_Theorem.thy

Sprache: Isabelle

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 ≤ int (N^n)"
    and "∧i. i==> ∣of_int q * θ i - of_int(p i)∣ < 1/N"
proof -
  have lessN: "nat ⌊x * real N⌋ < N" if "0 ≤ x" "x < 1" for x
  proof -
    have "⌊x * real N⌋ < N"
      using that by (simp add: assms floor_less_iff)
    with assms show ?thesis by linarith
  qed
  define interv where "interv ≡ λk. {real k/N..< Suc k/N}"
  define fracs where "fracs ≡ λk. map (λi. frac (real k * θ i)) [0..
  define X where "X ≡ fracs ` {..N^n}"
  define Y where "Y ≡ set (List.n_lists n (map interv [0..
  have interv_iff: "interv k = interv k' ⟷ k=k'" for k k'
    using assms by (auto simp: interv_def Ico_eq_Ico divide_strict_right_mono)
  have in_interv: "x ∈ interv (nat ⌊x * real N⌋)" if "x≥0" for x
    using that assms by (simp add: interv_def divide_simps) linarith
  have False
    if non: "∀a b. b ≤ N^n ⟶ a < b ⟶ ¬(∀i∣frac (real b * θ i) - frac (real a * θ i)∣ < 1/N)"
  proof -
    have "inj_on (λk. map (λi. frac (k * θ i)) [0..
      using that assms by (intro linorder_inj_onI) fastforce+
    then have caX: "card X = Suc (N^n)"
      by (simp add: X_def fracs_def card_image)
    have caY: "card Y ≤ N^n"
      by (metis Y_def card_length diff_zero length_map length_n_lists length_upt)
    define f where "f ≡ λl. map (λx. interv (nat ⌊x * real N⌋)) l"
    have "f ` X ⊆ Y"
      by (auto simp: f_def Y_def X_def fracs_def o_def set_n_lists frac_lt_1 lessN)
    then have "¬ inj_on f X"
      using Y_def caX caY card_inj_on_le not_less_eq_eq by fastforce
    then obtain x x' where "x≠x'" "x ∈ X" "x' ∈ X" and eq: "f x = f x'"
      by (auto simp: inj_on_def)
    then obtain c c' where c: "c ≠ c'" "c ≤ N^n" "c' ≤ N^n"
            and xeq: "x = fracs c" and xeq': "x' = fracs c'"
      unfolding X_def by (metis atMost_iff image_iff)
    have [simp]: "length x' = n"
      by (auto simp: xeq' fracs_def)
    have ge0: "x'!i ≥ 0" if "i 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🚫› assms by (auto simp: divide_simps k_def interv_def xeq fracs_def) linarith
      then have k': "x'!i ∈ interv(k!i)"
        using ‹i🚫› eq assms ge0[OF ‹i🚫›]
        by (auto simp: k_def f_def divide_simps map_equality_iff in_interv interv_iff)
      with assms k show ?thesis
        using ‹i🚫› by (auto simp add: xeq xeq' fracs_def interv_def add_divide_distrib)
    qed
    then show False
      by (metis c non nat_neq_iff abs_minus_commute)
  qed
  then obtain a b where "a "b ≤ N^n" and *: "∧i. i==> ∣frac (real b * θ i) - frac (real a * θ i)∣ < 1/N"
    by blast
  let ?k = "b-a"
  let ?h = "λi. ⌊b * θ i⌋ - ⌊a * θ i⌋"
  show ?thesis
  proof
    show "int (b - a) ≤ int (N ^ n)"
      using ‹b ≤ N ^ n› by auto
  next
    fix i
    assume "i
    have "frac (b * θ i) - frac (a * θ i) = ?k * θ i - ?h i"
      using ‹a 🚫› by (simp add: frac_def left_diff_distrib' of_nat_diff)
    then show "∣of_int ?k * θ i - ?h i∣ < 1/N"
      by (metis "*" ‹i 🚫› of_int_of_nat_eq)
  qed (use ‹a 🚫› in auto)
qed

text ‹Theorem references below referr to Apostol,
\emph{Modular Functions and Dirichlet Series in Number Theory}›

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 🚫› that by force
      then show False
        using ‹0 🚫› ‹b 🚫› ‹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 🚫› ‹b 🚫›)
    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 🚫› ‹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 🚫› 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 🚫› of_int_1_less_iff pos_divide_less_eq)
    then have ex: "∃m. int m ≤ N+1 ∧ 1-α < m * ξ"
      by (smt (verit, best) ‹0 🚫› ‹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 🚫› ξ_def kθ by force
      with ‹0 🚫› zero_less_nat_eq that show thesis by blast
    next
      case False
      with ‹0 🚫› have "m>1" by linarith
      have "ξ < 1 / N"
        by (metis N0 ‹0 🚫› 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 🚫›
        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_def of_nat_le_iff)
      ultimately have leα: " α ≤ frac (of_int ((int m - 1) * k) * θ)"
        by (simp add: Suc_leI ‹0 🚫› 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 🚫› int_ops(2) kθ m of_nat_diff)
      with that show thesis
        by (metis ‹0 🚫› ‹1 🚫› 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 🚫› 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 🚫› 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 🚫› 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 🚫› ξ_def kθ by force
      with ‹0 🚫› zero_less_nat_eq that show ?thesis by blast
    next
      case False
      with ‹0 🚫› have "m>1" by linarith
      with ‹0 🚫› 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_def of_nat_le_iff)
      ultimately have leα: "frac (of_int ((int m - 1) * k) * θ) ≤ α"
        by (simp add: Suc_leI ‹0 🚫› 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 🚫› ‹0 🚫› 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 🚫› 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(i * of_real t * 🪙 r)"
  shows "((λT. (1/T) * integral {0..T} (λt. f t * exp(-i * of_real t * 🪙 k))) ---> c k) at_top"
proof -
  define F where "F ≡ λk t. f t * exp(-i * of_real t * 🪙 k)"
  have f: "F k = (λt. ∑r≤N. c r * exp(i * (🪙 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(i * (🪙 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(i * (🪙 r - 🪙 k) * of_real T) - 1) / (i * (🪙 r - 🪙 k) * of_real T))"
    if "T > 0" for T
  proof -
    have I: "integral {0..T} (λt. exp (i * (complex_of_real t * 🪙 r) - i * (complex_of_real t * 🪙 k)))
           = (exp(i * (🪙 r - 🪙 k) * T) - 1) / (i * (🪙 r - 🪙 k))"
      if "r ≤ N" "r ≠ k" for r
      using that ‹k ≤ N› inj ‹T > 0› integral_exp [of T "i * (🪙 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(i * (🪙 r - 🪙 k) * of_real T) - 1) / (i * (🪙 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 (i * (🪙 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 / (i * (🪙 r - 🪙 k))"]] show ?thesis
      by (simp add: field_simps)
  qed
  then have "((λT. c k + (∑r ∈ {..N}-{k}. c r * (exp(i * (🪙 r - 🪙 k) * of_real T) - 1) /
                  (i * (🪙 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 (i * of_real (🪙 r - 🪙 k) * of_real x) - 1) /
            (i * of_real (🪙 r - 🪙 k) * of_real x)) =
          1 / of_real x * integral {0..x} (λt. f t * exp (- i * 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 🪙 {.. "0 ∉ 🪙 ` {.. and "k < N"
  defines "f ≡ λt. 1 + (∑ri * of_real t * 🪙 r))"
  shows "((λT. (1/T) * integral {0..T} (λt. f t * exp(-i * 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(i * 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 🚫› by auto
  ultimately have "((λT. 1 / T * integral {0..T} (λt. (∑r≤N. c' r * exp (i * of_real t * 🪙' r)) *
                    exp (- i * t * 🪙' (Suc k)))) ---> c' (Suc k))
       at_top"
    by (intro Kronecker_simult_aux1)
  moreover have "(∑r≤N. c' r * exp (i * of_real t * 🪙' r)) = 1 + (∑ri * 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 (i * x)) ≤ cmod (1 + exp (i * ε))"
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 + (∑ri * of_real (2 * pi * (t * θ r - α r))))"
  defines "L ≡ Sup (range (norm ∘ F))"
  shows "(∀ε>0. ∃t h. ∀r∣t * θ r - α r - of_int (h r)∣ < ε) ⟷ L = Suc n" (is "?lhs = _")
proof
  assume ?lhs
  then have "∧k. ∃t h. ∀r∣t * θ r - α r - of_int (h r)∣ < 1 / (2 * pi * Suc k)"
    by simp
  then obtain t h where th: "∧k r. r==> ∣t k * θ r - α r - of_int (h k r)∣ < 1 / (2 * pi * Suc k)"
    by metis
  have Fle: "∧x. cmod (F x) ≤ real (Suc n)"
    by (force simp: F_def intro: order_trans [OF norm_triangle_ineq] order_trans [OF norm_sum])
  then have boundedF: "bounded (range F)"
    by (metis bounded_iff rangeE)
  have leL: "1 + n * cos(1 / Suc k) ≤ L" for k
  proof -
    have *: "cos (1 / Suc k) ≤ cos (2 * pi * (t k * θ r - α r))" if "r 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
      by simp
    also have "… ≤ 1 + (∑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∣t * θ k - α k - of_int (h k)∣ ≥ e0"
      by (force simp: not_less)
    define ε where "ε ≡ min e0 (pi/4)"
    have ε: "∧t h. ∃k∣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 (i * ε)}"
      using collinear_iff_Reals cis.sel cis_conv_exp complex_is_Real_iff by force
    then have "norm (1 + exp (i * ε)) < 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 (i * ε)) = 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 (i * (of_int j * (of_real pi * 2))) = 1" for j
        by (metis add_0 exp_plus_2pin exp_zero)
      then have exp_X: "exp (i * (2 * of_real pi * of_real (X r)))
                 = exp (i * 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 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 (i * of_real (2 * pi * X k))) ≤ norm (1 + exp (i * ε))"
        using Figure7_1[of ε "2 * pi * X k"] ε_bounds by linarith
      have "norm (F t) = norm (1 + (∑ri * of_real (2 * pi * (X r)))))"
        by (auto simp: F_def exp_X)
      also have "… ≤ norm (1 + exp(i * of_real (2 * pi * X k)) + (∑r ∈ {..i * of_real (2 * pi * X r))))"
        by (simp add: comm_monoid_add_class.sum.remove [where x=k] ‹k 🚫› algebra_simps)
      also have "… ≤ norm (1 + exp(i * of_real (2 * pi * X k))) + (∑r ∈ {..i * of_real (2 * pi * X r))))"
        by (intro norm_triangle_mono sum_norm_le order_refl)
      also have "… ≤ (2 - δ) + (n - 1)"
        using ‹k 🚫› δ
        by simp (metis "*" mult_2 of_real_add of_real_mult)
      also have "… = n + 1 - δ"
        using ‹k 🚫› 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⟷ (∃j∑i≤ b ∧ b < (∑i
proof (induction k arbitrary: b)
  case (Suc k)
  then show ?case
    by (simp add: less_Suc_eq) (metis not_less trans_less_add1)
qed auto

lemma less_sum_nat_iff_uniq:
  fixes b::nat and k::nat
  shows "b < (∑i⟷ (∃!j. j∧ (∑i≤ b ∧ b < (∑i
  unfolding less_sum_nat_iff by (meson leD less_sum_nat_iff nat_neq_iff)

definition part :: "(nat ==> nat) ==> nat ==> nat ==> nat"
  where "part a k b ≡ (THE j. j∧ (∑i≤ b ∧ b < (∑i

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

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

text ‹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∏i

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

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

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

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

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

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

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

text ‹For excluding constant terms: with all exponents zero›
definition nontriv_exponents :: "[nat, nat, [nat,nat]==>nat] ==> bool"
  where "nontriv_exponents n 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
  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 {..
  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∀k'∃i≠ r k' i"

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

text ‹All coefficients must be nonzero›
definition nonzero_coeffs :: "[nat, nat==>nat] ==> bool"
  where "nonzero_coeffs 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)
  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 for f i
  define R where "R ≡ cut ` r ` ({..∩ {k. a k > 0})"
  define N' where "N' ≡ card R"
  define r' where "r' ≡ from_nat_into R"
  define a' where "a' ≡ λk'. ∑k
  have "finite R"
    using R_def by blast
  then have bij: "bij_betw r' {..
    using bij_betw_from_nat_into_finite N'_def r'_def by blast
  have 1: "card {i. i < N' ∧ r' i = cut (r k)} = Suc 0"
    if "k < N" "a k > 0" for k
  proof -
    have "card {i. i < N' ∧ r' i = cut (r k)} ≤ Suc 0"
      using bij by (simp add: card_le_Suc0_iff_eq bij_betw_iff_bijections Ball_def) metis
    moreover have "card {i. i < N' ∧ r' i = cut (r k)} > 0"
      using bij that by (auto simp: card_gt_0_iff bij_betw_iff_bijections R_def)
    ultimately show "card {i. i < N' ∧ r' i = cut (r k)} = Suc 0"
      using that by auto
  qed
  show thesis
  proof
    have "∃i≠ r' k' i" if "k < N'" and "k' < k" for k k'
    proof -
      have "k' < N'"
        using order.strict_trans that by blast
      then have "r' k ≠ r' k'"
        by (metis bij bij_betw_iff_bijections lessThan_iff nat_neq_iff that)
      moreover obtain sk sk' where "r' k = cut sk" "r' k' = cut sk'"
        by (metis R_def ‹k 🚫'› ‹k' 🚫'› bij bij_betwE image_iff lessThan_iff)
      ultimately show ?thesis
        using local.cut_def by force
    qed
    then show "uniq_exponents n N' r'"
      by (auto simp: uniq_exponents_def R_def)
    have "R ⊆ (cut ∘ r) ` {..
      by (auto simp: R_def)
    then show "N' ≤ N"
      unfolding N'_def by (metis card_lessThan finite_lessThan surj_card_le)
    show "gpoly n x N a r = gpoly n x N' a' r'" for x
    proof -
      have "a k * (∏i
          = (∑i∏j
        if "k for k
        using that
        by (cases"a k = 0")
           (simp_all add: if_distrib [of "λv. v * _"] 1 cut_def flip: sum.inter_filter cong: if_cong)
      then show ?thesis
        by (simp add: gpoly_def a'_def sum_distrib_right sum.swap [where A="{..] if_distrib [of of_nat])
    qed
    show "nontriv_exponents n N' r'" if ne: "nontriv_exponents n N r"
    proof -
      have "∃i if "k' < N'" for k'
      proof -
        have "r' k' ∈ R"
          using bij bij_betwE that by blast
        then obtain k where "k and k: "r' k' = cut (r k)"
          using R_def by blast
        with ne obtain i where "i "r k i > 0"
          by (auto simp: nontriv_exponents_def)
        then show ?thesis
          using k local.cut_def by auto
      qed
      then show ?thesis
        by (simp add: nontriv_exponents_def)
    qed
    have "0 < a' k'" if "k' < N'" for k'
    proof -
      have "r' k' ∈ R"
        using bij bij_betwE that by blast
      then obtain k where "k "a k > 0" "r' k' = cut (r k)"
        using R_def by blast
      then have False if "a' k' = 0"
        using that by (force simp add: a'_def Ball_def )
      then show ?thesis
        by blast
    qed
    then show "nonzero_coeffs N' a'"
      by (auto simp: nonzero_coeffs_def)
  qed
qed

lemma Kronecker_simult_aux3:
  "∃N a r. (∀x. (1 + (∑i∧ Suc N ≤ (p+1)^n
         ∧ nontriv_exponents n N r"
proof (induction n arbitrary: p)
  case 0
  then show ?case
    by (auto simp: gpoly_def nontriv_exponents_def nonzero_coeffs_def)
next
  case (Suc n)
  then obtain Nf af rf
    where feq: "∧q x. (1 + (∑i
      and Nle: "∧q. Suc (Nf q) ≤ (q+1)^n"
      and nontriv: "∧q. nontriv_exponents n (Nf q) (rf q)"
    by metis
  define N where "N ≡ Nf p + (∑q
  define a where "a ≡ λk. if k < Nf p then af p k
                           else let q = part (λt. Suc (Nf t)) p (k - Nf p)
                                in (p choose q) *
                                   (if k - Nf p - (∑t
                                    else af q (k - Nf p - (∑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
                                              else rf q (k - Nf p - (∑t
  have peq: "{..p} = insert p {..
    by auto
  have "nontriv_exponents n (Nf p) (λi. (rf p i)(n := 0))"
       "∧q. q

==> nontriv_exponents (Suc n) (Suc (Nf q)) (λk. (if k = Nf q then λ_. 0 else rf q k) (n := p - q))"
    using nontriv by (fastforce simp: nontriv_exponents_def)+
  then have "nontriv_exponents (Suc n) N r"
    unfolding N_def r_def by (intro nontriv_exponents_add nontriv_exponents_sum)
  moreover
  { fix x :: "nat ==> complex"
    have "(1 + (∑i < Suc n. x i)) ^ p = (1 + (∑i
      by (simp add: add_ac)
    also have "… = (∑q≤p. (p choose q) * (1 + (∑i
      by (simp add: binomial_ring)
    also have "… = (∑q≤p. (p choose q) * (1 + gpoly n x (Nf q) (af q) (rf q)) * x n^(p-q))"
      by (simp add: feq)
    also have "… = 1 + (gpoly n x (Nf p) (af p) (rf p) + (∑q
      by (simp add: algebra_simps sum.distrib peq)
    also have "… = 1 + gpoly (Suc n) x N a r"
      apply (subst one_plus_gpoly)
      apply (simp add: const_times_gpoly monom_times_gpoly gpoly_sum)
      apply (simp add: gpoly_inc [where n=n] gpoly_add N_def a_def r_def)
      done
    finally have "(1 + sum x {.. .
  }
  moreover have "Suc N ≤ (p + 1) ^ Suc n"
  proof -
    have "Suc N = (∑q≤p. Suc (Nf q))"
      by (simp add: N_def peq)
    also have "… ≤ (∑q≤p. (q+1)^n)"
      by (meson Nle sum_mono)
    also have "… ≤ (∑q≤p. (p+1)^n)"
      by (force intro!: sum_mono power_mono)
    also have "… ≤ (p + 1) ^ Suc n"
      by simp
    finally show "Suc N ≤ (p + 1) ^ Suc n" .
  qed
  ultimately show ?case
    by blast
qed

lemma Kronecker_simult_aux3_uniq_exponents:
  obtains N a r where "∧x. (1 + (∑i "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
    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)) (θ ` {..
    and injθ: "inj_on θ {.. 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 + (∑ii * of_real (2 * pi * (t * θ i - α i))))"
  define L where "L ≡ Sup (range (norm ∘ F))"
  have [continuous_intros]: "0 < T ==> continuous_on {0..T} F" for T
    unfolding F_def by (intro continuous_intros)
  have nft_Sucn: "norm (F t) ≤ Suc n" for t
    unfolding F_def by (rule norm_triangle_le order_trans [OF norm_sum] | simp)+
  then have L_le: "L ≤ Suc n"
    by (simp add: L_def cSUP_least)
  have nft_L: "norm (F t) ≤ L" for t
    by (metis L_def UNIV_I bdd_aboveI2 cSUP_upper nft_Sucn o_apply)
  have "L = Suc n"
  proof -
    { fix p::nat
      assume "p>0"
      obtain N a r where 3: "∧x. (1 + (∑r
             and SucN: "Suc N ≤ (p+1)^n"
             and nontriv: "nontriv_exponents n N r" and uniq: "uniq_exponents n N r"
             and apos: "nonzero_coeffs N a"
        using Kronecker_simult_aux3_uniq_exponents by blast
      have "N ≠ 0"
      proof
        assume "N = 0"
        have "2^p = (1::complex)"
          using 3 [of "(λ_. 0)(0:=1)"] True ‹p>0› ‹N = 0› by (simp add: gpoly_def)
        then have "2 ^ p = Suc 0"
          by (metis of_nat_1 One_nat_def of_nat_eq_iff of_nat_numeral of_nat_power)
        with ‹0 🚫› show False by force
      qed
      define x where "x ≡ λt r. exp(i * 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
      define 🪙 where "🪙 ≡ λk. 2 * pi * (∑i
      define INTT where "INTT ≡ λk T. (1/T) * integral {0..T} (λt. f t * exp(-i * of_real t * 🪙 k))"
      have "a k * (∏ii * t * 🪙 k)" if "k 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 + (∑ki * of_real t * 🪙 k))" for t
        by (simp add: feq gpoly_def)
      have nzero: "θ i ≠ 0" if "i for i
        using indp that local.dependent_zero by force
      have ind_disj: "∧u. (∀x∨ (∑v ∈ θ`{..≠ 0"
        using indp by (auto simp: dependent_finite)
      have inj🪙: "inj_on 🪙 {..
      proof
        fix k k'
        assume k: "k ∈ {.. "k' ∈ {.. and "🪙 k = 🪙 k'"
        then have eq: "(∑i∑i
          by (auto simp: 🪙_def)
        define f where "f ≡ λz. let i = inv_into {..
        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 ∉ 🪙 ` {..
        unfolding 🪙_def
      proof clarsimp
        fix k
        assume *: "(∑i "k < N"
        define f where "f ≡ λz. let i = inv_into {..
        obtain i where "i and "r k i > 0"
          by (meson ‹k 🚫› 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 for k
        unfolding fdef INTT_def using Kronecker_simult_aux1_strict that by presburger
      have norm_c: "norm (c k) ≤ L^p" if "k 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 (- (i * 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 (- (i * 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 * L^p"
        by (metis sum_bounded_above card_lessThan lessThan_iff)
      moreover
      have "Re((1 + (∑r
        using 3 [of "λ_. 1"] by metis
      then have 14: "1 + (∑k
        by (simp add: c_def norm_divide gpoly_def)
      moreover
      have "L^p ≥ 1"
        using norm_c [of 0] ‹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 🚫› 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 🚫› by (simp add: powr_powr powr_mult flip: powr_realpow)
      also have "… = ((p+1) powr n) powr (1/p) * L"
        by (simp add: powr_realpow)
      also have "… = (p+1) powr (n/p) * L"
        by (simp add: powr_powr)
      finally have "(n + 1) / L ≤ (p+1) powr (n/p)"
        by (simp add: divide_simps)
      then have "ln ((n + 1) / L) ≤ ln (real (p + 1) powr (real n / real p))"
        by (simp add: flip: ln_powr)
      also have "… ≤ (n/p) * ln(p+1)"
        by (simp add: powr_def)
      finally have "ln ((n + 1) / L) ≤ (n/p) * ln(p+1) ∧ L > 0"
        by fastforce
    } note * = this
    then have [simp]: "L > 0"
      by blast
    have 0: "(λp. (n/p) * ln(p+1)) <---- 0"
      by real_asymp
    have "ln (real (n + 1) / L) ≤ 0"
      using * eventually_at_top_dense by (intro tendsto_lowerbound [OF 0]) auto
    then have "n+1 ≤ L"
      using ‹0 🚫› 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 🚫› 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 🚫› 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 ∉ θ ` {.. 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]: "{..∩ {x. x ≠ n} = {..
    by auto
  have θimage[simp]: "θ ` {..n} = insert 1 (θ ` {..
    using lessThan_Suc lessThan_Suc_atMost by force
  have "module.independent (λr. (*) (of_int r)) (θ' ` {..
    unfolding dependent_explicit θ'_def
  proof clarsimp
    fix T u v
    assume T: "T ⊆ insert 1 ((λi. frac (θ i)) ` {..
      and "finite T"
      and uv_eq0: "(∑v∈T. of_int (u v) * v) = 0"
      and "v ∈ T"
    define invf where "invf ≡ inv_into {..∘ θ)"
    have "inj_on (λx. frac (θ x)) {..
      using injθ' by (auto simp: inj_on_def)
    then have invf [simp]: "invf (frac (θ i)) = i" if "i 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∧ t = frac (θ i))" if "t ∈ T-{1}" for i t
      using that T by auto
    have sumN: "(∑i∈N. f i) = (∑x∈T - {1}. f (invf x))" for f :: "nat ==> int"
      using inj_invf T  by (simp add: N_def sum.reindex)
    define T' where "T' ≡ 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 1∈T then u 1 else 0) + (∑i∈N. - ⌊θ i⌋ * u (frac (θ i))))"
    have "(∑v∈T'. 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 + (∑i∈N. of_int ((u ∘ frac) (θ i)) * θ i)"
      by (auto simp add: u'_def in_N_not1)
    also have "… = u' 1 + (∑i∈N. of_int ((u ∘ frac) (θ i)) * (floor (θ i) + frac(θ i)))"
      by (simp add: frac_def cong: if_cong)
    also have "… = (∑v∈T. of_int (u v) * v)"
    proof (cases "1 ∈ T")
      case True
      then have T1: "(∑v∈T. real_of_int (u v) * v) = u 1 + (∑v∈T-{1}. real_of_int (u v) * v)"
        by (simp add: ‹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: "(∑v∈T'. real_of_int (u' v) * v) = 0" .
    have "u v = 0" if T'0: "∧v. v∈T' ==> u' v = 0"
    proof -
      have [simp]: "u t = 0" if "t ∈ T - {1}" for t
      proof -
        have "θ (invf t) ∈ T'"
          using N_def T'_def that by blast
        then show ?thesis
          using that T'0 [of "θ (invf t)"]
          by (smt (verit, best) in_N_not1 N_def fun_upd_other imageI invf_iff o_apply u'_def)
      qed
      show ?thesis
      proof (cases "v = 1")
        case True
        then have "1 ∈ T"
          using ‹v ∈ T› by blast
        have "(∑v∈T. real_of_int (u v) * v) = u 1 + (∑v∈T - {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 θ' {..
    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🚫›
        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

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet am 2026-04-26) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.