(* Author: Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> *) section ‹Some useful lemmas about transcendental functions› theory Missing_Transcendental imports Missing_Topology Missing_Algebraic begin subsection ‹Misc› lemma Im_Ln_eq_pi_half: "z ≠ 0 ⟹ (Im(Ln z) = pi/2 ⟷ 0 < Im(z) ∧ Re(z) = 0)" "z ≠ 0 ⟹ (Im(Ln z) = -pi/2 ⟷ Im(z) < 0 ∧ Re(z) = 0)" proof - show "z ≠ 0 ⟹ (Im(Ln z) = pi/2 ⟷ 0 < Im(z) ∧ Re(z) = 0)" by (metis Im_Ln_eq_pi Im_Ln_le_pi Im_Ln_pos_lt Re_Ln_pos_le Re_Ln_pos_lt abs_of_nonneg less_eq_real_def order_less_irrefl pi_half_gt_zero) next assume "z≠0" have "Im (Ln z) = - pi / 2 ⟹ Im z < 0 ∧ Re z = 0" by (metis Im_Ln_pos_le Re_Ln_pos_le Re_Ln_pos_lt_imp ‹z ≠ 0› abs_if add.inverse_inverse divide_minus_left less_eq_real_def linorder_not_le minus_pi_half_less_zero) moreover have "Im (Ln z) = - pi / 2" when "Im z < 0" "Re z = 0" proof - obtain r::real where "r>0" "z=r * (-𝗂)" by (metis ‹Im z < 0› ‹Re z = 0› add.commute add.inverse_inverse add.right_neutral complex_eq complex_i_mult_minus diff_0 mult.commute mult.left_commute neg_0_less_iff_less of_real_0 of_real_diff) then have "Im (Ln z) = Im (Ln (r*(-𝗂)))" by auto also have "... = Im (Ln (complex_of_real r) + Ln (- 𝗂)) " apply (subst Ln_times_of_real) using ‹r>0› by auto also have "... = - pi/2" using ‹r>0› by simp finally show "Im (Ln z) = - pi / 2" . qed ultimately show "(Im(Ln z) = -pi/2 ⟷ Im(z) < 0 ∧ Re(z) = 0)" by auto qed lemma Im_Ln_eq: assumes "z≠0" shows "Im (Ln z) = (if Re z≠0 then if Re z>0 then arctan (Im z/Re z) else if Im z≥0 then arctan (Im z/Re z) + pi else arctan (Im z/Re z) - pi else if Im z>0 then pi/2 else -pi/2)" proof - have eq_arctan_pos:"Im (Ln z) = arctan (Im z/Re z)" when "Re z>0" for z proof - define wR where "wR=Re (Ln z)" define θ where "θ = arctan (Im z/Re z)" have "z≠0" using that by auto have "exp (Complex wR θ) = z" proof (rule complex_eqI) have "Im (exp (Complex wR θ)) =exp wR * sin θ " unfolding Im_exp by simp also have "... = Im z" unfolding wR_def Re_Ln[OF ‹z≠0›] θ_def using ‹z≠0› ‹Re z>0› by (auto simp add:sin_arctan divide_simps complex_neq_0 cmod_def real_sqrt_divide) finally show "Im (exp (Complex wR θ)) = Im z" . next have "Re (exp (Complex wR θ)) = exp wR * cos θ " unfolding Re_exp by simp also have "... = Re z" unfolding wR_def Re_Ln[OF ‹z≠0›] θ_def using ‹z≠0› ‹Re z>0› by (auto simp add:cos_arctan divide_simps complex_neq_0 cmod_def real_sqrt_divide) finally show "Re (exp (Complex wR θ)) = Re z" . qed moreover have "-pi<θ" "θ≤pi" unfolding θ_def subgoal by (auto intro:order_class.order.strict_trans[OF _ arctan_lbound]) subgoal apply (rule preorder_class.less_imp_le) by (auto intro:order_class.order.strict_trans[OF arctan_ubound]) done ultimately have "Ln z = Complex wR θ" using Ln_unique by auto then show ?thesis using that unfolding θ_def by auto qed have ?thesis when "Re z=0" using Im_Ln_eq_pi_half[OF ‹z≠0›] that apply auto using assms complex.expand by auto moreover have ?thesis when "Re z>0" using eq_arctan_pos[OF that] that by auto moreover have ?thesis when "Re z<0" "Im z≥0" proof - have "Im (Ln (- z)) = arctan (Im (- z) / Re (- z))" apply (rule eq_arctan_pos) using that by auto moreover have "Ln (- z) = Ln z - 𝗂 * complex_of_real pi" apply (subst Ln_minus[OF ‹z≠0›]) using that by auto ultimately show ?thesis using that by auto qed moreover have ?thesis when "Re z<0" "Im z<0" proof - have "Im (Ln (- z)) = arctan (Im (- z) / Re (- z))" apply (rule eq_arctan_pos) using that by auto moreover have "Ln (- z) = Ln z + 𝗂 * complex_of_real pi" apply (subst Ln_minus[OF ‹z≠0›]) using that by auto ultimately show ?thesis using that by auto qed ultimately show ?thesis by linarith qed lemma exp_Arg2pi2pi_multivalue: assumes "exp (𝗂* of_real x) = z" shows "∃k::int. x = Arg2pi z + 2*k*pi" proof - define k where "k=floor( x/(2*pi))" define x' where "x'= x - (2*k*pi)" have "x'/(2*pi) ≥0" unfolding x'_def k_def by (simp add: diff_divide_distrib) moreover have "x'/(2*pi) < 1" proof - have "x/(2*pi) - k < 1" unfolding k_def by linarith thus ?thesis unfolding k_def x'_def by (auto simp add:field_simps) qed ultimately have "x'≥0" and "x'<2*pi" by (auto simp add:field_simps) moreover have "exp (𝗂 * complex_of_real x') = z" using assms x'_def by (auto simp add:field_simps ) ultimately have "Arg2pi z = x'" using Arg2pi_unique[of 1 x' z,simplified] by auto hence " x = Arg2pi z + 2*k*pi" unfolding x'_def by auto thus ?thesis by auto qed lemma cos_eq_neg_periodic_intro: assumes "x - y=2*(of_int k)*pi + pi ∨ x + y = 2*(of_int k)*pi + pi" shows "cos x = - cos y" using assms proof assume "x - y = 2 * (of_int k) * pi + pi" then have "cos x = cos ((y+ pi) + (of_int k)*(2*pi))" by (auto simp add:algebra_simps) also have "... = cos (y+pi)" using cos.periodic_simps[of "y+pi"] by (auto simp add:algebra_simps) also have "... = - cos y" by simp finally show "cos x = - cos y" by auto next assume "x + y = 2 * real_of_int k * pi + pi " then have "cos x = cos ((- y+ pi) + (of_int k)*(2*pi))" apply (intro arg_cong[where f=cos]) by (auto simp add:algebra_simps) also have "... = cos (- y +pi)" using cos.periodic_simps[of "-y+pi"] by (auto simp add:algebra_simps) also have "... = - cos y" by simp finally show "cos x = - cos y" by auto qed lemma cos_eq_periodic_intro: assumes "x - y=2*(of_int k)*pi ∨ x + y = 2*(of_int k)*pi" shows "cos x = cos y" using assms proof assume "x - y = 2 * (of_int k) * pi " then have "cos x = cos (y + (of_int k)*(2*pi))" by (auto simp add:algebra_simps) also have "... = cos y" using cos.periodic_simps[of "y"] by (auto simp add:algebra_simps) finally show "cos x = cos y" by auto next assume "x + y = 2 * of_int k * pi" then have "cos x = cos (- y + (of_int k)*(2*pi))" apply (intro arg_cong[where f=cos]) by (auto simp add:algebra_simps) also have "... = cos (- y)" using cos.periodic_simps[of "-y"] by (auto simp add:algebra_simps) also have "... = cos y" by simp finally show "cos x = cos y" by auto qed lemma sin_tan_half: "sin (2*x) = 2 * tan x / (1 + (tan x)^2)" unfolding sin_double tan_def apply (cases "cos x=0") by (auto simp add:field_simps power2_eq_square) lemma cos_tan_half: "cos x ≠0 ⟹ cos (2*x) = (1 - (tan x)^2) / (1+ (tan x)^2)" unfolding cos_double tan_def by (auto simp add:field_simps ) lemma tan_eq_arctan_Ex: shows "tan x = y ⟷ (∃k::int. x = arctan y + k*pi ∨ (x = pi/2 + k*pi ∧ y=0))" proof assume asm:"tan x = y" obtain k::int where k:"-pi/2 < x-k*pi" "x-k*pi ≤ pi/2" proof - define k where "k=ceiling (x/pi - 1/2)" have "(x/pi - 1/2)≤k" unfolding k_def by auto then have "x-k*pi ≤ pi/2" by (auto simp add:field_simps) moreover have "k-1 < x/pi - 1/2" unfolding k_def by linarith then have "-pi/2 < x-k*pi" by (auto simp add:field_simps) ultimately show ?thesis using that by auto qed have "x = arctan y + of_int k * pi" when "x ≠ pi/2 + k*pi" proof - have "tan (x - k * pi) = y" using asm tan_periodic_int[of _ "-k"] by auto then have "arctan y = x - real_of_int k * pi" apply (intro arctan_unique) using k that by (auto simp add:field_simps) then show ?thesis by auto qed moreover have "y=0" when "x = pi/2 + k*pi" using asm that by auto (simp add: tan_def) ultimately show "∃k. x = arctan y + of_int k * pi ∨ (x = pi/2 + k*pi ∧ y=0)" using k by auto next assume "∃k::int. x = arctan y + k * pi ∨ x = pi / 2 + k * pi ∧ y = 0" then show "tan x = y" by (metis arctan_unique cos_pi_half division_ring_divide_zero tan_def tan_periodic_int tan_total) qed lemma arccos_unique: assumes "0 ≤ x" and "x ≤ pi" and "cos x = y" shows "arccos y = x" using arccos_cos assms(1) assms(2) assms(3) by blast lemma cos_eq_arccos_Ex: "cos x = y ⟷ -1≤y ∧ y≤1 ∧ (∃k::int. x = arccos y + 2*k*pi ∨ x = - arccos y + 2*k*pi)" proof assume asm:"-1≤y ∧ y≤1 ∧ (∃k::int. x = arccos y + 2*k*pi ∨ x = - arccos y + 2*k*pi)" then obtain k::int where "x = arccos y + 2*k*pi ∨ x = - arccos y + 2*k*pi" by auto moreover have "cos x = y" when "x = arccos y + 2*k*pi" proof - have "cos x = cos (arccos y + k*(2*pi))" using that by (auto simp add:algebra_simps) also have "... = cos (arccos y)" using cos.periodic_simps(3)[of "arccos y" k] by auto also have "... = y" using asm by auto finally show ?thesis . qed moreover have "cos x = y" when "x = -arccos y + 2*k*pi" proof - have "cos x = cos (- arccos y + k*2*pi)" unfolding that by (auto simp add:algebra_simps) also have "... = cos (arccos y - k*2*pi)" by (metis cos_minus minus_diff_eq uminus_add_conv_diff) also have "... = cos (arccos y)" using cos.periodic_simps(3)[of "arccos y" "-k"] by (auto simp add:algebra_simps) also have "... = y" using asm by auto finally show ?thesis . qed ultimately show "cos x = y" by auto next assume asm:"cos x =y" let ?goal = "(∃k::int. x = arccos y + 2*k*pi ∨ x = - arccos y + 2*k*pi)" obtain k::int where k:"-pi < x-k*2*pi" "x-k*2*pi ≤ pi" proof - define k where "k=ceiling (x/(2*pi) - 1/2)" have "(x/(2*pi) - 1/2)≤k" unfolding k_def by auto then have "x-k*2*pi ≤ pi" by (auto simp add:field_simps) moreover have "k-1 < x/(2*pi) - 1/2" unfolding k_def by linarith then have "-pi < x-k*2*pi" by (auto simp add:field_simps) ultimately show ?thesis using that by auto qed have ?goal when "x-k*2*pi≥0" proof - have "cos (x - k * 2*pi) = y" using cos.periodic_simps(3)[of x "-k"] asm by (auto simp add:field_simps) then have "arccos y = x - k * 2*pi" apply (intro arccos_unique) using k that by auto then show ?goal by auto qed moreover have ?goal when "¬ x-k*2*pi ≥0" proof - have "cos (x - k * 2*pi) = y" using cos.periodic_simps(3)[of x "-k"] asm by (auto simp add:field_simps) then have "cos (k * 2*pi - x) = y" by (metis cos_minus minus_diff_eq) then have "arccos y = k * 2*pi - x" apply (intro arccos_unique) using k that by auto then show ?goal by auto qed ultimately have ?goal by auto moreover have "-1≤y ∧ y≤1" using asm by auto ultimately show "-1≤y ∧ y≤1 ∧ ?goal" by auto qed lemma uniform_discrete_tan_eq: "uniform_discrete {x::real. tan x = y}" proof - have "x1=x2" when dist:"dist x1 x2<pi/2" and "tan x1=y" "tan x2=y" for x1 x2 proof - obtain k1::int where x1:"x1 = arctan y + k1*pi ∨ (x1 = pi/2 + k1*pi ∧ y=0)" using tan_eq_arctan_Ex ‹tan x1=y› by auto obtain k2::int where x2:"x2 = arctan y + k2*pi ∨ (x2 = pi/2 + k2*pi ∧ y=0)" using tan_eq_arctan_Ex ‹tan x2=y› by auto let ?xk1="x1 = arctan y + k1*pi" and ?xk1'="x1 = pi/2 + k1*pi ∧ y=0" let ?xk2="x2 = arctan y + k2*pi" and ?xk2'="x2 = pi/2 + k2*pi ∧ y=0" have ?thesis when "(?xk1 ∧ ?xk2) ∨ (?xk1' ∧ ?xk2')" proof - have "x1-x2= (k1 - k2) *pi" when ?xk1 ?xk2 using arg_cong2[where f=minus,OF ‹?xk1› ‹?xk2›] by (auto simp add:algebra_simps) moreover have "x1-x2= (k1 - k2) *pi" when ?xk1' ?xk2' using arg_cong2[where f=minus,OF conjunct1[OF ‹?xk1'›] conjunct1[OF ‹?xk2'›]] by (auto simp add:algebra_simps) ultimately have "x1-x2= (k1 - k2) *pi" using that by auto then have "¦k1 - k2¦ < 1/2" using dist[unfolded dist_real_def] by (auto simp add:abs_mult) then have "k1=k2" by linarith then show ?thesis using that by auto qed moreover have ?thesis when ?xk1 ?xk2' proof - have "x1 = k1*pi" "x2 = pi / 2 + k2 * pi" using ‹?xk2'› ‹?xk1› by auto from arg_cong2[where f=minus,OF this] have "x1 - x2 = (k1 - k2) * pi -pi/2" by (auto simp add:algebra_simps) then have "¦(k1 - k2) * pi -pi/2¦ < pi/2" using dist[unfolded dist_real_def] by auto then have "0<k1-k2" "k1-k2<1" unfolding abs_less_iff by (auto simp add: zero_less_mult_iff) then have False by simp then show ?thesis by auto qed moreover have ?thesis when ?xk1' ?xk2 proof - have "x1 = pi / 2 + k1*pi" "x2 = k2 * pi" using ‹?xk2› ‹?xk1'› by auto from arg_cong2[where f=minus,OF this] have "x1 - x2 = (k1 - k2) * pi + pi/2" by (auto simp add:algebra_simps) then have "¦(k1 - k2) * pi + pi/2¦ < pi/2" using dist[unfolded dist_real_def] by auto then have "¦(k1 - k2 + 1/2)*pi¦ < pi/2" by (auto simp add:algebra_simps) then have "¦(k1 - k2 + 1/2)¦ < 1/2" by (auto simp add:abs_mult) then have "-1<k1-k2 ∧ k1-k2<0" unfolding abs_less_iff by linarith then have False by auto then show ?thesis by auto qed ultimately show ?thesis using x1 x2 by blast qed then show ?thesis unfolding uniform_discrete_def apply (intro exI[where x="pi/2"]) by auto qed lemma get_norm_value: fixes a::"'a::{floor_ceiling}" assumes "pp>0" obtains k::int and a1 where "a=(of_int k)*pp+a1" "a0≤a1" "a1<a0+pp" proof - define k where "k=floor ((a-a0)/pp)" define a1 where "a1=a-(of_int k)*pp" have "of_int ⌊(a - a0) / pp⌋ * pp ≤ a- a0" using assms by (meson le_divide_eq of_int_floor_le) moreover have "a-a0 < of_int (⌊(a - a0) / pp⌋+1) * pp" using assms by (meson divide_less_eq floor_correct) ultimately show ?thesis apply (intro that[of k a1]) unfolding k_def a1_def using assms by (auto simp add:algebra_simps) qed (*Is it possible to generalise or simplify this messy proof?*) lemma filtermap_tan_at_right: fixes a::real assumes "cos a≠0" shows "filtermap tan (at_right a) = at_right (tan a)" proof - obtain k::int and a1 where aa1:"a=k*pi+a1" and "-pi/2≤a1" "a1<pi/2" using get_norm_value[of pi a "-pi/2"] by auto have "-pi/2 < a1" proof (rule ccontr) assume "¬ - pi / 2 < a1" then have "a1=- pi / 2" using ‹-pi/2≤a1› by auto then have "cos a = 0" unfolding aa1 by (metis (no_types, hide_lams) add.commute add_0_left cos_pi_half diff_eq_eq mult.left_neutral mult_minus_right mult_zero_left sin_add sin_pi_half sin_zero_iff_int2 times_divide_eq_left uminus_add_conv_diff) then show False using assms by auto qed have "eventually P (at_right (tan a))" when "eventually P (filtermap tan (at_right a))" for P proof - obtain b1 where "b1>a" and b1_imp:" ∀y>a. y < b1 ⟶ P (tan y)" using ‹eventually P (filtermap tan (at_right a))› unfolding eventually_filtermap eventually_at_right by (metis eventually_at_right_field) define b2 where "b2=min b1 (k*pi+pi/4+a1/2)" define b3 where "b3=b2 - k*pi" have "-pi/2 < b3" "b3<pi/2" proof - have "a1<b3" using ‹b1>a› aa1 ‹a1<pi/2› unfolding b2_def b3_def by (auto simp add:field_simps) then show "-pi/2 < b3" using ‹-pi/2≤a1› by auto show "b3 < pi/2" unfolding b2_def b3_def apply (subst min_diff_distrib_left) apply (rule min.strict_coboundedI2) using ‹b1>a› aa1 ‹a1<pi/2› ‹-pi/2<a1› by auto qed have "tan b2 > tan a" proof - have "tan a = tan a1" using aa1 by (simp add: add.commute) also have "... < tan b3" proof - have "a1<b3" using ‹b1>a› aa1 ‹a1<pi/2› unfolding b2_def b3_def by (auto simp add:field_simps) then show ?thesis using tan_monotone ‹-pi/2 < a1› ‹b3 < pi/2› by simp qed also have "... = tan b2" unfolding b3_def by (metis Groups.mult_ac(2) add_uminus_conv_diff mult_minus_right of_int_minus tan_periodic_int) finally show ?thesis . qed moreover have "P y" when "y>tan a" "y < tan b2" for y proof - define y1 where "y1=arctan y+ k * pi" have "a<y1" proof - have "arctan (tan a) < arctan y" using ‹y>tan a› arctan_monotone by auto then have "a1<arctan y" using arctan_tan ‹-pi/2 < a1› ‹a1<pi/2› unfolding aa1 by (simp add: add.commute) then show ?thesis unfolding y1_def aa1 by auto qed moreover have "y1<b2" proof - have "arctan y < arctan (tan b2)" using ‹y < tan b2› arctan_monotone by auto moreover have "arctan (tan b2) = b3" using arctan_tan[of b3] ‹-pi/2 < b3› ‹b3<pi/2› unfolding b3_def by (metis add.inverse_inverse diff_minus_eq_add divide_minus_left mult.commute mult_minus_right of_int_minus tan_periodic_int) ultimately have "arctan y < b3" by auto then show ?thesis unfolding y1_def b3_def by auto qed moreover have "∀y>a. y < b2 ⟶ P (tan y)" using b1_imp unfolding b2_def by auto moreover have "tan y1=y" unfolding y1_def by (auto simp add:tan_arctan) ultimately show ?thesis by auto qed ultimately show "eventually P (at_right (tan a))" unfolding eventually_at_right by (metis eventually_at_right_field) qed moreover have "eventually P (filtermap tan (at_right a))" when "eventually P (at_right (tan a))" for P proof - obtain b1 where "b1>tan a" and b1_imp:"∀y>tan a. y < b1 ⟶ P y" using ‹eventually P (at_right (tan a))› unfolding eventually_at_right by (metis eventually_at_right_field) define b2 where "b2=arctan b1 + k*pi" have "a1 < arctan b1" by (metis ‹- pi / 2 < a1› ‹a1 < pi / 2› ‹tan a < b1› aa1 add.commute arctan_less_iff arctan_tan divide_minus_left tan_periodic_int) then have "b2>a" unfolding aa1 b2_def by auto moreover have "P (tan y)" when "y>a" "y < b2" for y proof - define y1 where "y1 = y - k*pi" have "a1 < y1" "y1 < arctan b1" unfolding y1_def subgoal using ‹y>a› unfolding aa1 by auto subgoal using b2_def that(2) by linarith done then have "tan a1 < tan y1" "tan y1< b1" subgoal using ‹a1>-pi/2› apply (intro tan_monotone,simp,simp) using arctan_ubound less_trans by blast subgoal by (metis ‹- pi / 2 < a1› ‹a1 < y1› ‹y1 < arctan b1› arctan_less_iff arctan_tan arctan_ubound divide_minus_left less_trans) done have "tan y>tan a" by (metis ‹tan a1 < tan y1› aa1 add.commute add_uminus_conv_diff mult.commute mult_minus_right of_int_minus tan_periodic_int y1_def) moreover have "tan y<b1" by (metis ‹tan y1 < b1› add_uminus_conv_diff mult.commute mult_minus_right of_int_minus tan_periodic_int y1_def) ultimately show ?thesis using b1_imp by auto qed ultimately show ?thesis unfolding eventually_filtermap eventually_at_right by (metis eventually_at_right_field) qed ultimately show ?thesis unfolding filter_eq_iff by blast qed lemma filtermap_tan_at_left: fixes a::real assumes "cos a≠0" shows "filtermap tan (at_left a) = at_left (tan a)" proof - have "filtermap tan (at_right (- a)) = at_right (tan (- a))" using filtermap_tan_at_right[of "-a"] assms by auto then have "filtermap (uminus o tan) (at_left a) = filtermap uminus (at_left (tan a))" unfolding at_right_minus filtermap_filtermap comp_def by auto then have "filtermap uminus (filtermap (uminus o tan) (at_left a)) = filtermap uminus (filtermap uminus (at_left (tan a)))" by auto then show ?thesis unfolding filtermap_filtermap comp_def by auto qed lemma cos_zero_iff_int2: fixes x::real shows "cos x = 0 ⟷ (∃n::int. x = n * pi + pi/2)" using sin_zero_iff_int2[of "x-pi/2"] unfolding sin_cos_eq by (auto simp add:algebra_simps) lemma filtermap_tan_at_right_inf: fixes a::real assumes "cos a=0" shows "filtermap tan (at_right a) = at_bot" proof - obtain k::int where ak:"a=k*pi + pi/2" using cos_zero_iff_int2 assms by auto have "eventually P at_bot" when "eventually P (filtermap tan (at_right a))" for P proof - obtain b1 where "b1>a" and b1_imp:"∀y>a. y < b1 ⟶ P (tan y)" using ‹eventually P (filtermap tan (at_right a))› unfolding eventually_filtermap eventually_at_right by (metis eventually_at_right_field) define b2 where "b2=min (k*pi+pi) b1" have "P y" when "y<tan b2" for y proof - define y1 where "y1=(k+1)*pi+arctan y" have "a < y1" unfolding ak y1_def using arctan_lbound[of y] by (auto simp add:field_simps) moreover have "y1 < b2" proof - define b3 where "b3=b2-(k+1) * pi" have "-pi/2 < b3" "b3<pi/2" using ‹b1>a› unfolding b3_def b2_def ak by (auto simp add:field_simps min_mult_distrib_left intro!:min.strict_coboundedI1) then have "arctan (tan b3) = b3" by (simp add: arctan_tan) then have "arctan (tan b2) = b3" unfolding b3_def by (metis diff_eq_eq tan_periodic_int) then have "arctan y < b3" using arctan_monotone[OF ‹y<tan b2›] by simp then show ?thesis unfolding y1_def b3_def by auto qed then have "y1<b1" unfolding b2_def by auto ultimately have " P (tan y1)" using b1_imp[rule_format,of y1,simplified] by auto then show ?thesis unfolding y1_def by (metis add.commute arctan tan_periodic_int) qed then show ?thesis unfolding eventually_at_bot_dense by auto qed moreover have "eventually P (filtermap tan (at_right a))" when "eventually P at_bot" for P proof - obtain b1 where b1_imp:"∀n<b1. P n" using ‹eventually P at_bot› unfolding eventually_at_bot_dense by auto define b2 where "b2=arctan b1 + (k+1)*pi" have "b2>a" unfolding ak b2_def using arctan_lbound[of b1] by (auto simp add:algebra_simps) moreover have "P (tan y)" when "a < y" " y < b2 " for y proof - define y1 where "y1=y-(k+1)*pi" have "tan y1 < tan (arctan b1)" apply (rule tan_monotone) subgoal using ‹a<y› unfolding y1_def ak by (auto simp add:algebra_simps) subgoal using ‹y < b2› unfolding y1_def b2_def by (auto simp add:algebra_simps) subgoal using arctan_ubound by auto done then have "tan y1<b1" by (simp add: arctan) then have "tan y < b1" unfolding y1_def by (metis diff_eq_eq tan_periodic_int) then show ?thesis using b1_imp by auto qed ultimately show "eventually P (filtermap tan (at_right a))" unfolding eventually_filtermap eventually_at_right by (metis eventually_at_right_field) qed ultimately show ?thesis unfolding filter_eq_iff by auto qed lemma filtermap_tan_at_left_inf: fixes a::real assumes "cos a=0" shows "filtermap tan (at_left a) = at_top" proof - have "filtermap tan (at_right (- a)) = at_bot" using filtermap_tan_at_right_inf[of "-a"] assms by auto then have "filtermap (uminus o tan) (at_left a) = at_bot" unfolding at_right_minus filtermap_filtermap comp_def by auto then have "filtermap uminus (filtermap (uminus o tan) (at_left a)) = filtermap uminus at_bot" by auto then show ?thesis unfolding filtermap_filtermap comp_def using at_top_mirror[where 'a=real] by auto qed subsection ‹Periodic set› (*Devised to characterize roots of Trigonometric equations, which are usually uniformly discrete.*) definition periodic_set:: "real set ⇒ real ⇒ bool" where "periodic_set S δ ⟷ (∃B. finite B ∧ (∀x∈S. ∃b∈B. ∃k::int. x =b + k * δ ))" lemma periodic_set_multiple: assumes "k≠0" shows "periodic_set S δ ⟷ periodic_set S (of_int k*δ)" proof assume asm:"periodic_set S δ " then obtain B1 where "finite B1" and B1_def:"∀x∈S. ∃b∈B1. (∃k::int. x = b + k * δ)" unfolding periodic_set_def by metis define B where "B = B1 ∪ {b+i*δ | b i. b∈B1 ∧ i∈{0..<¦k¦}}" have "∃b∈B. ∃k'. x = b + real_of_int k' * (real_of_int k * δ)" when "x∈S" for x proof - obtain b1 and k1::int where "b1∈B1" and x_δ:"x = b1 + k1 * δ" using B1_def[rule_format, OF ‹x∈S›] by auto define r d where "r= k1 mod ¦k¦" and "d = k1 div ¦k¦" define b kk where "b=b1+r*δ" and "kk = (if k>0 then d else -d)" have "x = b1 + (r+¦k¦*d)*δ" using x_δ unfolding r_def d_def by auto then have "x = b + kk*(k*δ)" unfolding b_def kk_def using ‹k≠0› by (auto simp add:algebra_simps) moreover have "b∈B" proof - have "r ∈ {0..<¦k¦}" unfolding r_def by (simp add: ‹k≠0›) then show ?thesis unfolding b_def B_def using ‹b1∈B1› by blast qed ultimately show ?thesis by auto qed moreover have "finite B" unfolding B_def using ‹finite B1› by (simp add: finite_image_set2) ultimately show "periodic_set S (real_of_int k * δ)" unfolding periodic_set_def by auto next assume "periodic_set S (real_of_int k * δ)" then show "periodic_set S δ" unfolding periodic_set_def by (metis mult.commute mult.left_commute of_int_mult) qed lemma periodic_set_empty[simp]: "periodic_set {} δ" unfolding periodic_set_def by auto lemma periodic_set_finite: assumes "finite S" shows "periodic_set S δ" unfolding periodic_set_def using assms mult.commute by force lemma periodic_set_subset[elim]: assumes "periodic_set S δ" "T ⊆ S" shows "periodic_set T δ" using assms unfolding periodic_set_def by (meson subsetCE) lemma periodic_set_union: assumes "periodic_set S δ" "periodic_set T δ" shows "periodic_set (S ∪ T) δ" using assms unfolding periodic_set_def by (metis Un_iff infinite_Un) lemma periodic_imp_uniform_discrete: assumes "periodic_set S δ" shows "uniform_discrete S" proof - have ?thesis when "S≠{}" "δ≠0" proof - obtain B g where "finite B" and g_def:"∀x∈S. g x∈B ∧ (∃k::int. x = g x + k * δ)" using assms unfolding periodic_set_def by metis define P where "P = ((*) δ) ` Ints" define B_diff where "B_diff = {¦x-y¦ | x y. x∈B ∧ y∈B} - P" have "finite B_diff" unfolding B_diff_def using ‹finite B› by (simp add: finite_image_set2) define e where "e = (if setdist B_diff P = 0 then ¦δ¦ else min (setdist B_diff P) (¦δ¦))" have "e>0" unfolding e_def using setdist_pos_le[unfolded order_class.le_less] ‹δ≠0› by auto moreover have "x=y" when "x∈S" "y∈S" "dist x y<e" for x y proof - obtain k1::int where k1:"x = g x + k1 * δ" and "g x∈B" using g_def ‹x∈S› by auto obtain k2::int where k2:"y = g y + k2 * δ" and "g y∈B" using g_def ‹y∈S› by auto have ?thesis when "¦g x - g y¦ ∈ P" proof - obtain k::int where k:"g x - g y = k * δ" proof - obtain k' where "k'∈Ints" and *:"¦g x - g y¦ = δ * k'" using ‹¦g x - g y¦ ∈ P› unfolding P_def image_iff by auto then obtain k where **:"k' = of_int k" using Ints_cases by auto show ?thesis apply (cases "g x - g y ≥ 0") subgoal using that[of k] * ** by simp subgoal using that[of "-k"] * ** by (auto simp add:algebra_simps) done qed have "dist x y = ¦(g x - g y)+(k1-k2)*δ¦" unfolding dist_real_def by (subst k1,subst k2,simp add:algebra_simps) also have "... = ¦(k+k1-k2)*δ¦" by (subst k,simp add:algebra_simps) also have "... = ¦k+k1-k2¦*¦δ¦" by (simp add: abs_mult) finally have *:"dist x y = ¦k+k1-k2¦*¦δ¦" . then have "¦k+k1-k2¦*¦δ¦ < e" using ‹dist x y<e› by auto then have "¦k+k1-k2¦*¦δ¦ < ¦δ¦" apply (elim order_class.dual_order.strict_trans1[rotated]) unfolding e_def by auto then have "¦k+k1-k2¦ = 0" unfolding e_def using ‹δ≠0› by force then have "dist x y=0" using * by auto then show ?thesis by auto qed moreover have ?thesis when "¦g x - g y¦ ∉ P" proof - have "¦g x - g y¦ ∈ B_diff" unfolding B_diff_def using ‹g x∈B› ‹g y∈B› that by auto have "e ≤ ¦¦g x - g y¦ - ¦(k1-k2)*δ¦¦" proof - have "¦g x - g y¦ ∈ B_diff" unfolding B_diff_def using ‹g x∈B› ‹g y∈B› that by auto moreover have "¦(k1-k2)*δ¦ ∈ P" unfolding P_def apply (intro rev_image_eqI[of "(if δ≥0 then ¦of_int(k1-k2)¦ else - ¦of_int(k1-k2)¦)"]) apply (metis Ints_minus Ints_of_int of_int_abs) by (auto simp add:abs_mult) ultimately have "¦¦g x - g y¦ - ¦(k1-k2)*δ¦¦ ≥ setdist B_diff P" using setdist_le_dist[of _ B_diff _ P] dist_real_def by auto moreover have "setdist B_diff P ≠ 0" proof - have "compact B_diff " using ‹finite B_diff› using finite_imp_compact by blast moreover have "closed P" unfolding P_def using closed_scaling[OF closed_Ints[where 'a=real], of δ] by auto moreover have "P ≠ {}" using Ints_0 unfolding P_def by blast moreover have "B_diff ∩ P = {}" unfolding B_diff_def by auto moreover have "B_diff ≠{}" unfolding B_diff_def using ‹g x∈B› ‹g y∈B› that by auto ultimately show ?thesis using setdist_eq_0_compact_closed[of B_diff P] by auto qed ultimately show ?thesis unfolding e_def by argo qed also have "... ≤ ¦(g x - g y) + (k1-k2)*δ¦" proof - define t1 where "t1=g x - g y" define t2 where "t2 = of_int (k1 - k2) * δ" show ?thesis apply (fold t1_def t2_def) by linarith qed also have "... = dist x y" unfolding dist_real_def by (subst (2) k1,subst (2) k2,simp add:algebra_simps) finally have "dist x y≥e" . then have False using ‹dist x y<e› by auto then show ?thesis by auto qed ultimately show ?thesis by auto qed ultimately show ?thesis unfolding uniform_discrete_def by auto qed moreover have ?thesis when "S={}" using that by auto moreover have ?thesis when "δ=0" proof - obtain B g where "finite B" and g_def:"∀x∈S. g x∈B ∧ (∃k::int. x = g x + k * δ)" using assms unfolding periodic_set_def by metis then have "∀x∈S. g x∈B ∧ (x = g x)" using that by fastforce then have "S ⊆ g ` B" by auto then have "finite S" using ‹finite B› by (auto elim:finite_subset) then show ?thesis using uniform_discrete_finite_iff by blast qed ultimately show ?thesis by blast qed lemma periodic_set_tan_linear: assumes "a≠0" "c≠0" shows "periodic_set (roots (λx. a*tan (x/c) + b)) (c*pi)" proof - define B where "B = { c*arctan (- b / a), c*pi/2}" have "∃b∈B. ∃k::int. x = b + k * (c*pi)" when "x∈roots (λx. a * tan (x/c) + b)" for x proof - define C1 where "C1 = (∃k::int. x = c*arctan (- b / a) + k * (c*pi))" define C2 where "C2 = (∃k::int. x = c*pi / 2 + k * (c*pi) ∧ - b / a = 0)" have "tan (x/c) = - b/a" using that ‹a≠0› unfolding roots_within_def by (auto simp add:field_simps) then have "C1 ∨ C2" unfolding C1_def C2_def using tan_eq_arctan_Ex[of "x/c" "-b/a"] ‹c≠0› by (auto simp add:field_simps) moreover have ?thesis when C1 using that unfolding C1_def B_def by blast moreover have ?thesis when C2 using that unfolding C2_def B_def by blast ultimately show ?thesis by auto qed moreover have "finite B" unfolding B_def by auto ultimately show ?thesis unfolding periodic_set_def by auto qed lemma periodic_set_cos_linear: assumes "a≠0" "c≠0" shows "periodic_set (roots (λx. a*cos (x/c) + b)) (2*c*pi)" proof - define B where "B = { c*arccos (- b / a), - c*arccos (- b / a)}" have "∃b∈B. ∃k::int. x = b + k * (2*c*pi)" when "x∈roots (λx. a * cos (x/c) + b)" for x proof - define C1 where "C1 = (∃k::int. x = c*arccos (- b / a) + k * (2*c*pi))" define C2 where "C2 = (∃k::int. x = - c*arccos (- b / a) + k * (2*c*pi))" have "cos (x/c) = - b/a" using that ‹a≠0› unfolding roots_within_def by (auto simp add:field_simps) then have "C1 ∨ C2" unfolding cos_eq_arccos_Ex ex_disj_distrib C1_def C2_def using ‹c≠0› apply (auto simp add:divide_simps) by (auto simp add:algebra_simps) moreover have ?thesis when C1 using that unfolding C1_def B_def by blast moreover have ?thesis when C2 using that unfolding C2_def B_def by blast ultimately show ?thesis by auto qed moreover have "finite B" unfolding B_def by auto ultimately show ?thesis unfolding periodic_set_def by auto qed lemma periodic_set_tan_poly: assumes "p≠0" "c≠0" shows "periodic_set (roots (λx. poly p (tan (x/c)))) (c*pi)" using assms proof (induct rule:poly_root_induct_alt) case 0 then show ?case by simp next case (no_proots p) then show ?case unfolding roots_within_def by simp next case (root a p) have "roots (λx. poly ([:- a, 1:] * p) (tan (x/c))) = roots (λx. tan (x/c) - a) ∪ roots (λx. poly p (tan (x/c)))" unfolding roots_within_def by auto moreover have "periodic_set (roots (λx. tan (x/c) - a)) (c*pi)" using periodic_set_tan_linear[OF _ ‹c≠0› ,of 1 "-a",simplified] . moreover have "periodic_set (roots (λx. poly p (tan (x/c)))) (c*pi)" using root by fastforce ultimately show ?case using periodic_set_union by simp qed lemma periodic_set_sin_cos_linear: fixes a b c ::real assumes "a≠0 ∨ b≠0 ∨ c≠0" shows "periodic_set (roots (λx. a * cos x + b * sin x + c)) (4*pi)" proof - define f where "f x= a * cos x + b * sin x + c" for x have "roots f = (roots f ∩ {x. cos (x/2) = 0}) ∪ (roots f ∩ {x. cos (x/2) ≠ 0})" by auto moreover have "periodic_set (roots f ∩ {x. cos (x/2) = 0}) (4*pi)" proof - have "periodic_set ({x. cos (x/2) = 0}) (4*pi)" using periodic_set_cos_linear[of 1 2 0,unfolded roots_within_def,simplified] by simp then show ?thesis by auto qed moreover have "periodic_set (roots f ∩ {x. cos (x/2) ≠ 0}) (4*pi)" proof - define p where "p=[:a+c,2*b,c-a:]" have "poly p (tan (x/2)) = 0 ⟷ f x=0" when "cos (x/2) ≠0" for x proof - define t where "t=tan (x/2)" define tt where "tt = 1+t^2" have "cos x = (1-t^2) / tt" unfolding tt_def t_def using cos_tan_half[OF that,simplified] by simp moreover have "sin x = 2*t / tt" unfolding tt_def t_def using sin_tan_half[of "x/2",simplified] by simp moreover have "tt≠0" unfolding tt_def by (metis power_one sum_power2_eq_zero_iff zero_neq_one) ultimately show ?thesis unfolding f_def p_def apply (fold t_def) apply simp apply (auto simp add:field_simps) by (auto simp add:algebra_simps tt_def power2_eq_square) qed then have "roots f ∩ {x. cos (x/2) ≠ 0} = roots (λx. poly p (tan (x/2))) ∩ {x. cos (x/2) ≠ 0}" unfolding roots_within_def by auto moreover have "periodic_set (roots (λx. poly p (tan (x/2))) ∩ {x. cos (x/2) ≠ 0}) (4*pi)" proof - have "p≠0" unfolding p_def using assms by auto then have "periodic_set (roots (λx. poly p (tan (x/2)))) (4*pi)" using periodic_set_tan_poly[of p 2,simplified] periodic_set_multiple[of 2 _ "2*pi",simplified] by auto then show ?thesis by auto qed ultimately show ?thesis by auto qed ultimately show "periodic_set (roots f) (4*pi)" using periodic_set_union by metis qed end