: "\\ - h/k\ < 1 / (k*N)" + by (simp add: field_simps) + also have "\ \ 1/k\<^sup>2" + using \k \ int N\ by (simp add: eval_nat_numeral divide_simps) + finally have hk_in: "(h,k) \ approx_set \" + using \0 < k\ \coprime h k\ by (auto simp: approx_set_def) + then have "\\ - h/k\ \ A" + by (auto simp: A_def) + moreover have "1 / real_of_int (k * int N) < ?\" + proof - + have "1 / real_of_int (k * int N) = 1 / real N / of_int k" + by simp + also have "\ < ?\ / of_int k" + using \k > 0\ \ \N > 0\ N by (intro divide_strict_right_mono) (auto simp: field_simps) + also have "\ \ ?\ / 1" + using \ \k > 0\ by (intro divide_left_mono) auto + finally show ?thesis + by simp + qed + ultimately show False using A \

by auto + qed +qed + + +text \No formalisation of Liouville's Approximation Theorem because this is already in the AFP +as Liouville\_Numbers. Apostol's Theorem 7.5 should be exactly the theorem +liouville\_irrational\_algebraic. There is a minor discrepancy in the definition +of "Liouville number" between Apostol and Eberl: he requires the denominator to be +positive, while Eberl require it to exceed 1.\ + +section \Kronecker's Approximation Theorem: the One-dimensional Case\ + +lemma frac_int_mult: + assumes "m > 0" and le: "1-frac r \ 1/m" + shows "1 - frac (of_int m * r) = m * (1 - frac r)" +proof - + have "frac (of_int m * r) = 1 - m * (1 - frac r)" + proof (subst frac_unique_iff, intro conjI) + show "of_int m * r - (1 - of_int m * (1 - frac r)) \ \" + by (simp add: algebra_simps frac_def) + qed (use assms in \auto simp: divide_simps mult_ac frac_lt_1\) + then show ?thesis + by simp +qed + +text \Concrete statement of Theorem 7.7, and the real proof\ +theorem Kronecker_approx_1_explicit: + fixes \ :: real + assumes "\ \ \" and \: "0 \ \" "\ \ 1" and "\ > 0" + obtains k where "k>0" "\frac(real k * \) - \\ < \" +proof - + obtain N::nat where "1/N < \" "N > 0" + by (metis \\ > 0\ gr_zeroI inverse_eq_divide real_arch_inverse) + then obtain h k where "0 < k" and hk: "\of_int k * \ - of_int h\ < \" + using Dirichlet_approx that by (metis less_trans) + have irrat: "of_int n * \ \ \ \ n = 0" for n + by (metis Rats_divide Rats_of_int assms(1) nonzero_mult_div_cancel_left of_int_0_eq_iff) + then consider "of_int k * \ < of_int h" | "of_int k * \ > of_int h" + by (metis Rats_of_int \0 < k\ less_irrefl linorder_neqE_linordered_idom) + then show thesis + proof cases + case 1 + define \ where "\ \ 1 - frac (of_int k * \)" + have pos: "\ > 0" + by (simp add: \_def frac_lt_1) + define N where "N \ \1/\\" + have "N > 0" + by (simp add: N_def \_def frac_lt_1) + have False if "1/\ \ \" + proof - + from that of_int_ceiling + obtain r where r: "of_int r = 1/\" by blast + then obtain s where s: "of_int k * \ = of_int s + 1 - 1/r" + by (simp add: \_def frac_def) + from r pos s \k > 0\ have "\ = (of_int s + 1 - 1/r) / k" + by (auto simp: field_simps) + with assms show False + by simp + qed + then have N0: "N < 1/\" + unfolding N_def by (metis Ints_of_int floor_correct less_le) + then have N2: "1/(N+1) < \" + unfolding N_def by (smt (verit) divide_less_0_iff divide_less_eq floor_correct mult.commute pos) + have "\ * (N+1) > 1" + by (smt (verit) N2 \0 < N\ of_int_1_less_iff pos_divide_less_eq) + then have ex: "\m. int m \ N+1 \ 1-\ < m * \" + by (smt (verit, best) \0 < N\ \0 \ \\ floor_of_int floor_of_nat mult.commute of_nat_nat) + define m where "m \ LEAST m. int m \ N+1 \ 1-\ < m * \" + have m: "int m \ N+1 \ 1-\ < m * \" + using LeastI_ex [OF ex] unfolding m_def by blast + have "m > 0" + using m gr0I \\ \ 1\ by force + have k\: "\ < \" + using hk 1 by (smt (verit, best) floor_eq_iff frac_def \_def) + show thesis + proof (cases "m=1") + case True + then have "\frac (real (nat k) * \) - \\ < \" + using m \\ \ 1\ \0 < k\ \_def k\ by force + with \0 < k\ zero_less_nat_eq that show thesis by blast + next + case False + with \0 < m\ have "m>1" by linarith + have "\ < 1 / N" + by (metis N0 \0 < N\ mult_of_int_commute of_int_pos pos pos_less_divide_eq) + also have "\ \ 1 / (real m - 1)" + using \m > 1\ m by (simp add: divide_simps) + finally have "\ < 1 / (real m - 1)" . + then have m1_eq: "(int m - 1) * \ = 1 - frac (of_int ((int m - 1) * k) * \)" + using frac_int_mult [of "(int m - 1)" "k * \"] \1 < m\ + by (simp add: \_def mult.assoc) + then + have m1_eq': "frac (of_int ((int m - 1) * k) * \) = 1 - (int m - 1) * \" + by simp + moreover have "(m - Suc 0) * \ \ 1-\" + using Least_le [where k="m-Suc 0"] m + by (smt (verit, best) Suc_n_not_le_n Suc_pred \0 < m\ m_def of_nat_le_iff) + ultimately have le\: " \ \ frac (of_int ((int m - 1) * k) * \)" + by (simp add: Suc_leI \0 < m\ of_nat_diff) + moreover have "m * \ + frac (of_int ((int m - 1) * k) * \) = \ + 1" + by (subst m1_eq') (simp add: \_def algebra_simps) + ultimately have "\frac ((int (m - 1) * k) * \) - \\ < \" + by (smt (verit, best) One_nat_def Suc_leI \0 < m\ int_ops(2) k\ m of_nat_diff) + with that show thesis + by (metis \0 < k\ \1 < m\ mult_pos_pos of_int_of_nat_eq of_nat_mult pos_int_cases zero_less_diff) + qed + next + case 2 + define \ where "\ \ frac (of_int k * \)" + have recip_frac: False if "1/\ \ \" + proof - + have "frac (of_int k * \) \ \" + using that unfolding \_def + by (metis Ints_cases Rats_1 Rats_divide Rats_of_int div_by_1 divide_divide_eq_right mult_cancel_right2) + then show False + using \0 < k\ frac_in_Rats_iff irrat by blast + qed + have pos: "\ > 0" + by (metis \_def Ints_0 division_ring_divide_zero frac_unique_iff less_le recip_frac) + define N where "N \ \1 / \\" + have "N > 0" + unfolding N_def + by (smt (verit) \_def divide_less_eq_1_pos floor_less_one frac_lt_1 pos) + have N0: "N < 1 / \" + unfolding N_def by (metis Ints_of_int floor_eq_iff less_le recip_frac) + then have N2: "1/(N+1) < \" + unfolding N_def + by (smt (verit, best) divide_less_0_iff divide_less_eq floor_correct mult.commute pos) + have "\ * (N+1) > 1" + by (smt (verit) N2 \0 < N\ of_int_1_less_iff pos_divide_less_eq) + then have ex: "\m. int m \ N+1 \ \ < m * \" + by (smt (verit, best) mult.commute \\ \ 1\ \0 < N\ of_int_of_nat_eq pos_int_cases) + define m where "m \ LEAST m. int m \ N+1 \ \ < m * \" + have m: "int m \ N+1 \ \ < m * \" + using LeastI_ex [OF ex] unfolding m_def by blast + have "m > 0" + using \0 \ \\ m gr0I by force + have k\: "\ < \" + using hk 2 unfolding \_def by (smt (verit, best) floor_eq_iff frac_def) + have mk_eq: "frac (of_int (m*k) * \) = m * frac (of_int k * \)" + if "m>0" "frac (of_int k * \) < 1/m" for m k + proof (subst frac_unique_iff , intro conjI) + show "real_of_int (m * k) * \ - real_of_int m * frac (real_of_int k * \) \ \" + by (simp add: algebra_simps frac_def) + qed (use that in \auto simp: divide_simps mult_ac\) + show thesis + proof (cases "m=1") + case True + then have "\frac (real (nat k) * \) - \\ < \" + using m \ \0 < k\ \_def k\ by force + with \0 < k\ zero_less_nat_eq that show ?thesis by blast + next + case False + with \0 < m\ have "m>1" by linarith + with \0 < k\ have mk_pos:"(m - Suc 0) * nat k > 0" by force + have "real_of_int (int m - 1) < 1 / frac (real_of_int k * \)" + using N0 \_def m by force + then + have m1_eq: "(int m - 1) * \ = frac (((int m - 1) * k) * \)" + using m mk_eq [of "int m-1" k] pos \m>1\ by (simp add: divide_simps mult_ac \_def) + moreover have "(m - Suc 0) * \ \ \" + using Least_le [where k="m-Suc 0"] m + by (smt (verit, best) Suc_n_not_le_n Suc_pred \0 < m\ m_def of_nat_le_iff) + ultimately have le\: "frac (of_int ((int m - 1) * k) * \) \ \" + by (simp add: Suc_leI \0 < m\ of_nat_diff) + moreover have "(m * \ - frac (of_int ((int m - 1) * k) * \)) < \" + by (metis m1_eq add_diff_cancel_left' diff_add_cancel k\ left_diff_distrib' + mult_cancel_right2 of_int_1 of_int_diff of_int_of_nat_eq) + ultimately have "\frac (real( (m - 1) * nat k) * \) - \\ < \" + using \0 < k\ \0 < m\ by simp (smt (verit, best) One_nat_def Suc_leI m of_nat_1 of_nat_diff) + with \m > 0\ that show thesis + using mk_pos One_nat_def by presburger + qed + qed +qed + + +text \Theorem 7.7 expressed more abstractly using @{term closure}\ +corollary Kronecker_approx_1: + fixes \ :: real + assumes "\ \ \" + shows "closure (range (\n. frac (real n * \))) = {0..1}" (is "?C = _") +proof - + have "\k>0. \frac(real k * \) - \\ < \" if "0 \ \" "\ \ 1" "\ > 0" for \ \ + by (meson Kronecker_approx_1_explicit assms that) + then have "x \ ?C" if "0 \ x" "x \ 1" for x :: real + using that by (auto simp add: closure_approachable dist_real_def) + moreover + have "(range (\n. frac (real n * \))) \ {0..1}" + by (smt (verit) atLeastAtMost_iff frac_unique_iff image_subset_iff) + then have "?C \ {0..1}" + by (simp add: closure_minimal) + ultimately show ?thesis by auto +qed + + +text \The next theorem removes the restriction $0 \leq \alpha \leq 1$.\ + +text \Theorem 7.8\ +corollary sequence_of_fractional_parts_is_dense: + fixes \ :: real + assumes "\ \ \" "\ > 0" + obtains h k where "k > 0" "\of_int k * \ - of_int h - \\ < \" +proof - + obtain k where "k>0" "\frac(real k * \) - frac \\ < \" + by (metis Kronecker_approx_1_explicit assms frac_ge_0 frac_lt_1 less_le_not_le) + then have "\real_of_int k * \ - real_of_int (\k * \\ - \\\) - \\ < \" + by (auto simp: frac_def) + then show thesis + by (meson \0 < k\ of_nat_0_less_iff that) +qed + +section \Extension of Kronecker's Theorem to Simultaneous Approximation\ + +subsection \Towards Lemma 1\ + +lemma integral_exp: + assumes "T \ 0" "a\0" + shows "integral {0..T} (\t. exp(a * complex_of_real t)) = (exp(a * of_real T) - 1) / a" +proof - + have "\t. t \ {0..T} \ ((\x. exp (a * x) / a) has_vector_derivative exp (a * t)) (at t within {0..T})" + using assms + by (intro derivative_eq_intros has_complex_derivative_imp_has_vector_derivative [unfolded o_def] | simp)+ + then have "((\t. exp(a * of_real t)) has_integral exp(a * complex_of_real T)/a - exp(a * of_real 0)/a) {0..T}" + by (meson fundamental_theorem_of_calculus \T \ 0\) + then show ?thesis + by (simp add: diff_divide_distrib integral_unique) +qed + +lemma Kronecker_simult_aux1: + fixes \:: "nat \ real" and c:: "nat \ complex" and N::nat + assumes inj: "inj_on \ {..N}" and "k \ N" + defines "f \ \t. \r\N. c r * exp(\ * of_real t * \ r)" + shows "((\T. (1/T) * integral {0..T} (\t. f t * exp(-\ * of_real t * \ k))) \ c k) at_top" +proof - + define F where "F \ \k t. f t * exp(-\ * of_real t * \ k)" + have f: "F k = (\t. \r\N. c r * exp(\ * (\ r - \ k) * of_real t))" + by (simp add: F_def f_def sum_distrib_left field_simps exp_diff exp_minus) + have *: "integral {0..T} (F k) + = c k * T + (\r \ {..N}-{k}. c r * integral {0..T} (\t. exp(\ * (\ r - \ k) * of_real t)))" + if "T > 0" for T + using \k \ N\ that + by (simp add: f integral_sum integrable_continuous_interval continuous_intros Groups_Big.sum_diff scaleR_conv_of_real) + + have **: "(1/T) * integral {0..T} (F k) + = c k + (\r \ {..N}-{k}. c r * (exp(\ * (\ r - \ k) * of_real T) - 1) / (\ * (\ r - \ k) * of_real T))" + if "T > 0" for T + proof - + have I: "integral {0..T} (\t. exp (\ * (complex_of_real t * \ r) - \ * (complex_of_real t * \ k))) + = (exp(\ * (\ r - \ k) * T) - 1) / (\ * (\ r - \ k))" + if "r \ N" "r \ k" for r + using that \k \ N\ inj \T > 0\ integral_exp [of T "\ * (\ r - \ k)"] + by (simp add: inj_on_eq_iff algebra_simps) + show ?thesis + using that by (subst *) (auto simp add: algebra_simps sum_divide_distrib I) + qed + have "((\T. c r * (exp(\ * (\ r - \ k) * of_real T) - 1) / (\ * (\ r - \ k) * of_real T)) \ 0) at_top" + for r + proof - + have "((\x. (cos ((\ r - \ k) * x) - 1) / x) \ 0) at_top" + "((\x. sin ((\ r - \ k) * x) / x) \ 0) at_top" + by real_asymp+ + hence "((\T. (exp (\ * (\ r - \ k) * of_real T) - 1) / of_real T) \ 0) at_top" + by (simp add: tendsto_complex_iff Re_exp Im_exp) + from tendsto_mult[OF this tendsto_const[of "c r / (\ * (\ r - \ k))"]] show ?thesis + by (simp add: field_simps) + qed + then have "((\T. c k + (\r \ {..N}-{k}. c r * (exp(\ * (\ r - \ k) * of_real T) - 1) / + (\ * (\ r - \ k) * of_real T))) \ c k + 0) at_top" + by (intro tendsto_add tendsto_null_sum) auto + also have "?this \ ?thesis" + proof (rule filterlim_cong) + show "\\<^sub>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 \ {.. \ ` {.. \t. 1 + (\r * of_real t * \ r))" + shows "((\T. (1/T) * integral {0..T} (\t. f t * exp(-\ * of_real t * \ k))) \ c k) at_top" +proof - + define c' where "c' \ case_nat 1 c" + define \' where "\' \ case_nat 0 \" + define f' where "f' \ \t. (\r\N. c' r * exp(\ * of_real t * \' r))" + have "inj_on \' {..N}" + using \ by (auto simp: \'_def inj_on_def split: nat.split_asm) + moreover have "Suc k \ N" + using \k < N\ by auto + ultimately have "((\T. 1 / T * integral {0..T} (\t. (\r\N. c' r * exp (\ * of_real t * \' r)) * + exp (- \ * t * \' (Suc k)))) \ c' (Suc k)) + at_top" + by (intro Kronecker_simult_aux1) + moreover have "(\r\N. c' r * exp (\ * of_real t * \' r)) = 1 + (\r * 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 * of_real (2 * pi * (t * \ r - \ r))))" + defines "L \ Sup (range (norm \ F))" + shows "(\\>0. \t h. \rt * \ r - \ r - of_int (h r)\ < \) \ L = Suc n" (is "?lhs = _") +proof + assume ?lhs + then have "\k. \t h. \rt * \ r - \ r - of_int (h r)\ < 1 / (2 * pi * Suc k)" + by simp + then obtain t h where th: "\k r. r \t k * \ r - \ r - of_int (h k r)\ < 1 / (2 * pi * Suc k)" + by metis + have Fle: "\x. cmod (F x) \ real (Suc n)" + by (force simp: F_def intro: order_trans [OF norm_triangle_ineq] order_trans [OF norm_sum]) + then have boundedF: "bounded (range F)" + by (metis bounded_iff rangeE) + have leL: "1 + n * cos(1 / Suc k) \ L" for k + proof - + have *: "cos (1 / Suc k) \ cos (2 * pi * (t k * \ r - \ r))" if "r2 * 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 \ 1 + (\r r - \ r)))" + using * by (intro add_mono sum_mono) auto + also have "\ \ Re (F(t k))" + by (simp add: F_def Re_exp) + also have "\ \ norm (F(t k))" + by (simp add: complex_Re_le_cmod) + also have "\ \ L" + by (simp add: L_def boundedF bounded_norm_le_SUP_norm) + finally show ?thesis . + qed + show "L = Suc n" + proof (rule antisym) + show "L \ Suc n" + using Fle by (auto simp add: L_def intro: cSup_least) + have "((\k. 1 + real n * cos (1 / real (Suc k))) \ 1 + real n) at_top" + by real_asymp + with LIMSEQ_le_const2 leL show "Suc n \ L" + by fastforce + qed +next + assume L: "L = Suc n" + show ?lhs + proof (rule ccontr) + assume "\ ?lhs" + then obtain e0 where "e0>0" and e0: "\t h. \kt * \ k - \ k - of_int (h k)\ \ e0" + by (force simp: not_less) + define \ where "\ \ min e0 (pi/4)" + have \: "\t h. \kt * \ 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 "kX 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 * of_real (2 * pi * (X r)))))" + by (auto simp: F_def exp_X) + also have "\ \ norm (1 + exp(\ * of_real (2 * pi * X k)) + (\r \ {.. * of_real (2 * pi * X r))))" + by (simp add: comm_monoid_add_class.sum.remove [where x=k] \k < n\ algebra_simps) + also have "\ \ norm (1 + exp(\ * of_real (2 * pi * X k))) + (\r \ {.. * of_real (2 * pi * X r))))" + by (intro norm_triangle_mono sum_norm_le order_refl) + also have "\ \ (2 - \) + (n - 1)" + using \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 (\ji b \ b < (\ii (\!j. j (\i b \ b < (\i nat) \ nat \ nat \ nat" + where "part a k b \ (THE j. j (\i b \ b < (\ii (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 {..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 \ (\kik. k < N \ a' k = a k" "\k i. \k < N; i \ r' k i = r k i" + shows "gpoly n x N a r = gpoly n x N a' r'" + using assms by (auto simp: gpoly_def) + +lemma gpoly_inc: "gpoly n x N a r = gpoly (Suc n) x N a (\k. (r k)(n:=0))" + by (simp add: gpoly_def algebra_simps sum_distrib_left) + +lemma monom_times_gpoly: "gpoly n x N a r * x n ^ q = gpoly (Suc n) x N a (\k. (r k)(n:=q))" + by (simp add: gpoly_def algebra_simps sum_distrib_left) + +lemma const_times_gpoly: "e * gpoly n x N a r = gpoly n x N ((*)e \ a) r" + by (simp add: gpoly_def sum_distrib_left mult.assoc) + +lemma one_plus_gpoly: "1 + gpoly n x N a r = gpoly n x (Suc N) (a(N:=1)) (r(N:=(\_. 0)))" + by (simp add: gpoly_def) + +lemma gpoly_add: + "gpoly n x N a r + gpoly n x N' a' r' + = gpoly n x (N+N') (\k. if kk. if k {N.. {N.. sum Nf {.. \k. let q = (part Nf p k) in af q (k - sum Nf {.. \k. let q = (part Nf p k) in rf q (k - sum Nf {..qFor excluding constant terms: with all exponents zero\ +definition nontriv_exponents :: "[nat, nat, [nat,nat]\nat] \ bool" + where "nontriv_exponents n N r \ \ki 0" + +lemma nontriv_exponents_add: + "\nontriv_exponents n M r; nontriv_exponents (Suc n) N r'\ \ + nontriv_exponents (Suc n) (M + N) (\k. if kq. q < p \ nontriv_exponents n (N q) (r q)" + shows "nontriv_exponents n (sum N {..k. let q = part N p k in r q (k - sum N {..nat] \ bool" + where "uniq_exponents n N r \ \kk'i r k' i" + +lemma uniq_exponents_inj: "uniq_exponents n N r \ inj_on r {..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 if i 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 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 < 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" + 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 * (\iijv. 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="{..i R" + using bij bij_betwE that by blast + then obtain k where "k 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 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 + (\iq. 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 \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 - (\tt \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_. 0 + else rf q (k - Nf p - (\ti. (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 = (\q\p. (p choose q) * (1 + (\i = (\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 = 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 {.. (p + 1) ^ Suc n" + proof - + have "Suc N = (\q\p. Suc (Nf q))" + by (simp add: N_def peq) + also have "\ \ (\q\p. (q+1)^n)" + by (meson Nle sum_mono) + also have "\ \ (\q\p. (p+1)^n)" + by (force intro!: sum_mono power_mono) + also have "\ \ (p + 1) ^ Suc n" + by simp + finally show "Suc N \ (p + 1) ^ Suc n" . + qed + ultimately show ?case + by blast +qed + +lemma Kronecker_simult_aux3_uniq_exponents: + obtains N a r where "\x. (1 + (\i (p+1)^n" + "nontriv_exponents n N r" "uniq_exponents n N r" "nonzero_coeffs N a" +proof - + obtain N0 a0 r0 where "\x. (1 + (\r (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)) (\ ` {..: "inj_on \ {.. > 0" + obtains t h where "\i. i < n \ \t * \ i - of_int (h i) - \ i\ < \" +proof (cases "n>0") + case False then show ?thesis + using that by blast +next + case True + interpret Modules.module "(\r. (*) (real_of_int r))" + by (simp add: Modules.module.intro distrib_left mult.commute) + define F where "F \ \t. 1 + (\i * of_real (2 * pi * (t * \ i - \ i))))" + define L where "L \ Sup (range (norm \ F))" + have [continuous_intros]: "0 < T \ continuous_on {0..T} F" for T + unfolding F_def by (intro continuous_intros) + have nft_Sucn: "norm (F t) \ Suc n" for t + unfolding F_def by (rule norm_triangle_le order_trans [OF norm_sum] | simp)+ + then have L_le: "L \ Suc n" + by (simp add: L_def cSUP_least) + have nft_L: "norm (F t) \ L" for t + by (metis L_def UNIV_I bdd_aboveI2 cSUP_upper nft_Sucn o_apply) + have "L = Suc n" + proof - + { fix p::nat + assume "p>0" + obtain N a r where 3: "\x. (1 + (\r (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 i * real (r k i)))))" + define \ where "\ \ \k. 2 * pi * (\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 * t * \ k)" if "k_def sum_distrib_left flip: exp_of_nat_mult exp_sum) + apply (simp add: algebra_simps sum_subtractf exp_diff c_def sum_distrib_left cis_conv_exp) + done + then have fdef: "f t = 1 + (\k * of_real t * \ k))" for t + by (simp add: feq gpoly_def) + have nzero: "\ i \ 0" if "iu. (\x x) = 0) \ (\v \ \`{.. 0" + using indp by (auto simp: dependent_finite) + have inj\: "inj_on \ {.. {.. {.. k = \ k'" + then have eq: "(\i i) = (\i i)" + by (auto simp: \_def) + define f where "f \ \z. let i = inv_into {.. z in int (r k i) - int (r k' i)" + show "k = k'" + using ind_disj [of f] inj\ 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 \ \ ` {.._def + proof clarsimp + fix k + assume *: "(\i i) = 0" "k < N" + define f where "f \ \z. let i = inv_into {.. z in int (r k i)" + obtain i where "i 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 L^p" if "k_. 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 "\\<^sub>F x in at_top. (norm \ INTT k) x \ L ^ p" + using eventually_at_top_linorder that by fastforce + qed auto + then have "(\k N * L^p" + by (metis sum_bounded_above card_lessThan lessThan_iff) + moreover + have "Re((1 + (\r_. 1) N a r)" + using 3 [of "\_. 1"] by metis + then have 14: "1 + (\k 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 \ \ ` {..' 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} = {..image[simp]: "\ ` {..n} = insert 1 (\ ` {..r. (*) (of_int r)) (\' ` {..'_def + proof clarsimp + fix T u v + assume T: "T \ insert 1 ((\i. frac (\ i)) ` {..v\T. of_int (u v) * v) = 0" + and "v \ T" + define invf where "invf \ inv_into {.. \)" + have "inj_on (\x. frac (\ x)) {..' by (auto simp: inj_on_def) + then have invf [simp]: "invf (frac (\ i)) = i" if "i 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 \' {..' + 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 diff -r 88eb92a52f9b -r d8045bc0544e src/HOL/Probability/Projective_Family.thy --- a/src/HOL/Probability/Projective_Family.thy Fri Nov 03 10:55:15 2023 +0100 +++ b/src/HOL/Probability/Projective_Family.thy Fri Nov 03 16:20:06 2023 +0000 @@ -9,7 +9,10 @@ imports Giry_Monad begin -lemma vimage_restrict_preseve_mono: +(** Something strange going on here regarding the syntax \(n := x) vs fun_upd \ n x + See nn_integral_eP, etc. **) + +lemma vimage_restrict_preserve_mono: assumes J: "J \ I" and sets: "A \ (\\<^sub>E i\J. S i)" "B \ (\\<^sub>E i\J. S i)" and ne: "(\\<^sub>E i\I. S i) \ {}" and eq: "(\x. restrict x J) -` A \ (\\<^sub>E i\I. S i) \ (\x. restrict x J) -` B \ (\\<^sub>E i\I. S i)" @@ -56,7 +59,7 @@ assumes "J \ L" "L \ I" and sets: "X \ sets (Pi\<^sub>M J M)" "Y \ sets (Pi\<^sub>M J M)" assumes "emb L J X \ emb L J Y" shows "X \ Y" -proof (rule vimage_restrict_preseve_mono) +proof (rule vimage_restrict_preserve_mono) show "X \ (\\<^sub>E i\J. space (M i))" "Y \ (\\<^sub>E i\J. space (M i))" using sets[THEN sets.sets_into_space] by (auto simp: space_PiM) show "(\\<^sub>E i\L. space (M i)) \ {}" @@ -286,11 +289,11 @@ lemma space_eP: "x \ space (PiM {0.. space (eP n x) = space (PiM {0.. space (PiM {0.. sets (eP n x) = sets (PiM {0.. space (PiM {0.. prob_space (eP n x)" unfolding eP_def @@ -298,13 +301,13 @@ lemma nn_integral_eP: "\ \ space (PiM {0.. f \ borel_measurable (PiM {0.. - (\\<^sup>+x. f x \eP n \) = (\\<^sup>+x. f ($n := x)) \P n $" + (\\<^sup>+x. f x \eP n \) = (\\<^sup>+x. f (fun_upd \ n x) \P n \)" unfolding eP_def by (subst nn_integral_distr) (auto intro!: measurable_fun_upd[where J="{0..[simp]: "\ \ space (PiM {0.. sets (PiM {0.. A = P n \ ((\x. $n := x)) -` A \ space (M n))" + shows "eP n \ A = P n \ ((\x. fun_upd \ n x) -` A \ space (M n))" using nn_integral_eP[of \ n "indicator A"] apply (simp add: sets_eP nn_integral_indicator[symmetric] sets_P del: nn_integral_indicator) apply (subst nn_integral_indicator[symmetric]) @@ -485,7 +488,7 @@ { fix \ n assume \: "\ \ space (PiM {0..i. ?C' i \ borel_measurable (P n $" using \[measurable, simp] measurable_fun_upd[where J="{0... ?C' (Suc i) x \ ?C' i x" for i proof (rule AE_I2) fix x assume "x \ space (P n \)" - with \ have \': "\(n := x) \ space (PiM {0.. have \': "fun_upd \ n x \ space (PiM {0..] space_PiM PiE_iff extensional_def) with \ show "?C' (Suc i) x \ ?C' i x" apply (subst emeasure_C[symmetric, of i "Suc i"]) @@ -534,7 +537,7 @@ then obtain x where "x \ space (M n)" "0 < (INF i. ?C' i x)" by (auto dest: frequently_ex) from this(2)[THEN less_INF_D, of 0] this(2) - have "\x. \(n := x) \ X (Suc n) \ 0 < (INF i. ?C' i x)" + have "\x. fun_upd \ n x \ X (Suc n) \ 0 < (INF i. ?C' i x)" by (intro exI[of _ x]) (simp split: split_indicator_asm) } note step = this diff -r 88eb92a52f9b -r d8045bc0544e src/HOL/ROOT --- a/src/HOL/ROOT Fri Nov 03 10:55:15 2023 +0100 +++ b/src/HOL/ROOT Fri Nov 03 16:20:06 2023 +0000 @@ -104,7 +104,8 @@ "HOL-Library" "HOL-Combinatorics" "HOL-Computational_Algebra" - theories + "HOL-Real_Asymp" +theories Analysis document_files "root.tex" diff -r 88eb92a52f9b -r d8045bc0544e src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Fri Nov 03 10:55:15 2023 +0100 +++ b/src/HOL/Transcendental.thy Fri Nov 03 16:20:06 2023 +0000 @@ -4547,6 +4547,19 @@ lemma sin_int_2pin [simp]: "sin ((2 * pi) * of_int n) = 0" by (metis Ints_of_int sin_integer_2pi) +lemma sin_cos_eq_iff: "sin y = sin x \ cos y = cos x \ (\n::int. y = x + 2 * pi * n)" (is "?L=?R") +proof + assume ?L + then have "cos (y-x) = 1" + using cos_add [of y "-x"] by simp + then show ?R + by (metis cos_one_2pi_int add.commute diff_add_cancel mult.assoc mult.commute) +next + assume ?R + then show ?L + by (auto simp: sin_add cos_add) +qed + lemma sincos_principal_value: "\y. (- pi < y \ y \ pi) \ (sin y = sin x \ cos y = cos x)" proof - define y where "y \ pi - (2 * pi) * frac ((pi - x) / (2 * pi))" @@ -4554,9 +4567,7 @@ by (auto simp: field_simps frac_lt_1 y_def) moreover have "sin y = sin x" "cos y = cos x" - unfolding y_def - apply (simp_all add: frac_def divide_simps sin_add cos_add) - by (metis sin_int_2pin cos_int_2pin diff_zero add.right_neutral mult.commute mult.left_neutral mult_zero_left)+ + by (simp_all add: y_def frac_def divide_simps sin_add cos_add mult_of_int_commute) ultimately show ?thesis by metis qed