# Theory Missing_Transcendental

theory Missing_Transcendental
imports Missing_Algebraic
```(*
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
moreover have "Im (Ln z) = - pi / 2" when "Im z < 0" "Re z = 0"
proof -
obtain r::real where "r>0" "z=r * (-𝗂)"
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))"
also have "... = cos (y+pi)"
using cos.periodic_simps[of "y+pi"]
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])
also have "... = cos (- y +pi)"
using cos.periodic_simps[of "-y+pi"]
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))"
also have "... = cos y"
using cos.periodic_simps[of "y"]
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])
also have "... = cos (- y)"
using cos.periodic_simps[of "-y"]
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")

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)"
also have "... = cos (arccos y)"
using cos.periodic_simps(3)[of "arccos y" "-k"]
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›]
moreover have "x1-x2= (k1 - k2) *pi" when ?xk1' ?xk2'
using arg_cong2[where f=minus,OF conjunct1[OF ‹?xk1'›] conjunct1[OF ‹?xk2'›]]
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"
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"
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
diff_eq_eq mult.left_neutral mult_minus_right mult_zero_left
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"
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
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"
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

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]
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"
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]
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›
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›
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›
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)*δ¦"
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)
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
then have "C1 ∨ C2" unfolding C1_def C2_def using tan_eq_arctan_Ex[of "x/c" "-b/a"]  ‹c≠0›
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
then have "C1 ∨ C2"
unfolding cos_eq_arccos_Ex ex_disj_distrib C1_def C2_def using ‹c≠0›
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
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
```