# Theory Sin_Cos_Bounds

```chapter ‹Sine and Cosine Upper and Lower Bounds›

theory Sin_Cos_Bounds
imports Bounds_Lemmas

begin

section‹Simple base cases›

text‹Upper bound for @{term"x≥0"}›
lemma sin_le_arg:
fixes x :: real
shows "0 ≤ x ⟹ sin x ≤ x"
by (fact sin_x_le_x)

lemma cos_ge_1_arg:
fixes x :: real
assumes "0 ≤ x"
shows "1 - x ≤ cos x"
apply (rule gen_lower_bound_increasing [OF assms])
apply (intro derivative_eq_intros, auto)
done

lemmas sin_Taylor_0_upper_bound_pos = sin_le_arg ― ‹MetiTarski bound›

lemma cos_Taylor_1_lower_bound:
fixes x :: real
assumes "0 ≤ x"
shows "(1 - x^2 / 2) ≤ cos x"
apply (rule gen_lower_bound_increasing [OF assms])
apply (intro derivative_eq_intros)
apply (rule refl | simp add: sin_le_arg)+
done

lemma sin_Taylor_1_lower_bound:
fixes x :: real
assumes "0 ≤ x"
shows "(x - x ^ 3 / 6) ≤ sin x"
apply (rule gen_lower_bound_increasing [OF assms])
apply (intro derivative_eq_intros)
apply (rule refl | simp add: cos_Taylor_1_lower_bound)+
done

section‹Taylor series approximants›

definition sinpoly :: "[nat,real] ⇒ real"
where "sinpoly n = (λx. ∑k<n. sin_coeff k * x ^ k)"

definition cospoly :: "[nat,real] ⇒ real"
where "cospoly n = (λx. ∑k<n. cos_coeff k * x ^ k)"

(*sin upper bounds have the form 4*n+2; lower bounds, 4*n
sinpoly 2 x = x                                      (upper)
sinpoly 4 x = x - (x^3)/6                            (lower)
sinpoly 6 x = x - (x^3)/6 + (x^5)/120                (upper)
sinpoly 8 x = x - (x^3)/6 + (x^5)/120 - (x^7)/5040   (lower)

cos upper bounds have the form 4*n+1; lower bounds, 4*n+3
cospoly 1 x = 1                                                             (upper)
cospoly 3 x = 1 - (x^2)/2                                                   (lower)
cospoly 5 x = 1 - (x^2)/2 + (x^4)/24 - x^6/720 + x^8/40320                  (upper)
cospoly 7 x = 1 - (x^2)/2 + (x^4)/24 - x^6/720 + x^8/40320 - x^10/3628800   (lower)
*)

lemma sinpoly_Suc: "sinpoly (Suc n) = (λx. sinpoly n x + sin_coeff n * x ^ n)"

lemma cospoly_Suc: "cospoly (Suc n) = (λx. cospoly n x + cos_coeff n * x ^ n)"

lemma sinpoly_minus [simp]: "sinpoly n (-x) = - sinpoly n x"
by (induct n) (auto simp: sinpoly_def sin_coeff_def)

lemma cospoly_minus [simp]: "cospoly n (-x) = cospoly n x"
by (induct n) (auto simp: cospoly_def cos_coeff_def)

lemma d_sinpoly_cospoly:
"(sinpoly (Suc n) has_field_derivative cospoly n x) (at x)"
proof (induction n)
case 0 show ?case
next
case (Suc n) show ?case
proof (cases "n=0")
case True then show ?thesis
by (simp add: sinpoly_def sin_coeff_def cospoly_def)
next
case False then
have xn: "x ^ (n - Suc 0) * x = x ^ n"
by (metis Suc_pred mult.commute not_gr0 power_Suc)
show ?thesis using Suc False
apply (simp add: sinpoly_Suc [of "Suc n"] cospoly_def)
apply (intro derivative_eq_intros | simp)+
apply (simp add: xn mult.assoc sin_coeff_def cos_coeff_def divide_simps del: fact_Suc)
done
qed
qed

lemma d_cospoly_sinpoly:
"(cospoly (Suc n) has_field_derivative -sinpoly n x) (at x)"
proof (induction n)
case 0 show ?case
next
case (Suc n) show ?case
proof (cases "n=0")
case True then show ?thesis
by (simp add: sinpoly_def cospoly_def cos_coeff_def)
next
case False then
have xn: "x ^ (n - Suc 0) * x = x ^ n"
by (metis Suc_pred mult.commute not_gr0 power_Suc)
have m1: "odd n ⟹ (-1 :: real) ^ ((n - Suc 0) div 2) = - ((-1) ^ (Suc n div 2))"
by (cases n) simp_all
show ?thesis using Suc False
apply (simp add: cospoly_Suc [of "Suc n"] sinpoly_def)
apply (intro derivative_eq_intros | simp)+
apply (simp add: xn mult.assoc sin_coeff_def cos_coeff_def m1 divide_simps del: fact_Suc)
done
qed
qed

section‹Inductive proof of sine inequalities›

lemma sinpoly_lb_imp_cospoly_ub:
assumes x0: "0 ≤ x" and k0: "k>0" and "⋀x. 0 ≤ x ⟹ sinpoly (k - 1) x ≤ sin x"
shows "cos x ≤ cospoly k x"
apply (rule gen_lower_bound_increasing [OF x0])
apply (intro derivative_eq_intros | simp)+
using d_cospoly_sinpoly [of "k - 1"] assms
apply auto
done

lemma cospoly_ub_imp_sinpoly_ub:
assumes x0: "0 ≤ x" and k0: "k>0" and "⋀x. 0 ≤ x ⟹ cos x ≤ cospoly (k - 1) x"
shows "sin x ≤ sinpoly k x"
apply (rule gen_lower_bound_increasing [OF x0])
apply (intro derivative_eq_intros | simp)+
using d_sinpoly_cospoly [of "k - 1"] assms
apply auto
done

lemma sinpoly_ub_imp_cospoly_lb:
assumes x0: "0 ≤ x" and k0: "k>0" and "⋀x. 0 ≤ x ⟹ sin x ≤ sinpoly (k - 1) x"
shows "cospoly k x ≤ cos x"
apply (rule gen_lower_bound_increasing [OF x0])
apply (intro derivative_eq_intros | simp)+
using d_cospoly_sinpoly [of "k - 1"] assms
apply auto
done

lemma cospoly_lb_imp_sinpoly_lb:
assumes x0: "0 ≤ x" and k0: "k>0" and "⋀x. 0 ≤ x ⟹ cospoly (k - 1) x ≤ cos x"
shows "sinpoly k x ≤ sin x"
apply (rule gen_lower_bound_increasing [OF x0])
apply (intro derivative_eq_intros | simp)+
using d_sinpoly_cospoly [of "k - 1"] assms
apply auto
done

lemma
assumes "0 ≤ x"
shows sinpoly_lower_nonneg: "sinpoly (4 * Suc n) x ≤ sin x"        (is ?th1)
and sinpoly_upper_nonneg: "sin x ≤ sinpoly (Suc (Suc (4*n))) x"  (is ?th2)
proof -
have "sinpoly (4 * Suc n) x ≤ sin x  ∧  sin x ≤ sinpoly (Suc (Suc (4*n))) x"
using assms
apply (induction n arbitrary: x)
apply (simp add: sinpoly_def sin_coeff_def sin_Taylor_1_lower_bound sin_Taylor_0_upper_bound_pos lessThan_nat_numeral fact_numeral)
apply (auto simp: cospoly_lb_imp_sinpoly_lb sinpoly_ub_imp_cospoly_lb cospoly_ub_imp_sinpoly_ub sinpoly_lb_imp_cospoly_ub)
done
then show ?th1 ?th2
using assms
by auto
qed

section‹Collecting the results›

corollary sinpoly_upper_nonpos:
"x ≤ 0 ⟹ sin x ≤ sinpoly (4 * Suc n) x"
using sinpoly_lower_nonneg [of "-x" n]
by simp

corollary sinpoly_lower_nonpos:
"x ≤ 0 ⟹ sinpoly (Suc (Suc (4*n))) x ≤ sin x"
using sinpoly_upper_nonneg [of "-x" n]
by simp

corollary cospoly_lower_nonneg:
"0 ≤ x ⟹ cospoly (Suc (Suc (Suc (4*n)))) x ≤ cos x"
by (auto simp: sinpoly_upper_nonneg sinpoly_ub_imp_cospoly_lb)

lemma cospoly_lower:
"cospoly (Suc (Suc (Suc (4*n)))) x ≤ cos x"
proof (cases rule: le_cases [of 0 x])
case le then show ?thesis
next
case ge then show ?thesis using cospoly_lower_nonneg [of "-x"]
by simp
qed

lemma cospoly_upper_nonneg:
assumes "0 ≤ x"
shows "cos x ≤ cospoly (Suc (4*n)) x"
proof (cases n)
case 0 then show ?thesis
next
case (Suc m)
then show ?thesis
using sinpoly_lower_nonneg [of _ m] assms
by (auto simp: sinpoly_lb_imp_cospoly_ub)
qed

lemma cospoly_upper:
"cos x ≤ cospoly (Suc (4*n)) x"
proof (cases rule: le_cases [of 0 x])
case le then show ?thesis