src/HOL/Transcendental.thy
author paulson <lp15@cam.ac.uk>
Mon Mar 16 15:30:00 2015 +0000 (2015-03-16)
changeset 59730 b7c394c7a619
parent 59669 de7792ea4090
child 59731 7fccaeec22f0
permissions -rw-r--r--
The factorial function, "fact", now has type "nat => 'a"
     1 (*  Title:      HOL/Transcendental.thy
     2     Author:     Jacques D. Fleuriot, University of Cambridge, University of Edinburgh
     3     Author:     Lawrence C Paulson
     4     Author:     Jeremy Avigad
     5 *)
     6 
     7 section{*Power Series, Transcendental Functions etc.*}
     8 
     9 theory Transcendental
    10 imports Binomial Series Deriv NthRoot
    11 begin
    12 
    13 lemma of_real_fact [simp]: "of_real (fact n) = fact n"
    14   by (metis of_nat_fact of_real_of_nat_eq)
    15 
    16 lemma real_fact_nat [simp]: "real (fact n :: nat) = fact n"
    17   by (simp add: real_of_nat_def)
    18 
    19 lemma root_test_convergence:
    20   fixes f :: "nat \<Rightarrow> 'a::banach"
    21   assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
    22   assumes "x < 1"
    23   shows "summable f"
    24 proof -
    25   have "0 \<le> x"
    26     by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1])
    27   from `x < 1` obtain z where z: "x < z" "z < 1"
    28     by (metis dense)
    29   from f `x < z`
    30   have "eventually (\<lambda>n. root n (norm (f n)) < z) sequentially"
    31     by (rule order_tendstoD)
    32   then have "eventually (\<lambda>n. norm (f n) \<le> z^n) sequentially"
    33     using eventually_ge_at_top
    34   proof eventually_elim
    35     fix n assume less: "root n (norm (f n)) < z" and n: "1 \<le> n"
    36     from power_strict_mono[OF less, of n] n
    37     show "norm (f n) \<le> z ^ n"
    38       by simp
    39   qed
    40   then show "summable f"
    41     unfolding eventually_sequentially
    42     using z `0 \<le> x` by (auto intro!: summable_comparison_test[OF _  summable_geometric])
    43 qed
    44 
    45 subsection {* Properties of Power Series *}
    46 
    47 lemma lemma_realpow_diff:
    48   fixes y :: "'a::monoid_mult"
    49   shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
    50 proof -
    51   assume "p \<le> n"
    52   hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le)
    53   thus ?thesis by (simp add: power_commutes)
    54 qed
    55 
    56 lemma lemma_realpow_diff_sumr2:
    57   fixes y :: "'a::{comm_ring,monoid_mult}"
    58   shows
    59     "x ^ (Suc n) - y ^ (Suc n) =
    60       (x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))"
    61 proof (induct n)
    62   case (Suc n)
    63   have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x^n) - y * (y * y ^ n)"
    64     by simp
    65   also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)"
    66     by (simp add: algebra_simps)
    67   also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
    68     by (simp only: Suc)
    69   also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
    70     by (simp only: mult.left_commute)
    71   also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
    72     by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
    73   finally show ?case .
    74 qed simp
    75 
    76 corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *}
    77   fixes x :: "'a::{comm_ring,monoid_mult}"
    78   shows   "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
    79 using lemma_realpow_diff_sumr2[of x "n - 1" y]
    80 by (cases "n = 0") (simp_all add: field_simps)
    81 
    82 lemma lemma_realpow_rev_sumr:
    83    "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
    84     (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
    85   by (subst nat_diff_setsum_reindex[symmetric]) simp
    86 
    87 lemma power_diff_1_eq:
    88   fixes x :: "'a::{comm_ring,monoid_mult}"
    89   shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i<n. (x^i))"
    90 using lemma_realpow_diff_sumr2 [of x _ 1]
    91   by (cases n) auto
    92 
    93 lemma one_diff_power_eq':
    94   fixes x :: "'a::{comm_ring,monoid_mult}"
    95   shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^(n - Suc i))"
    96 using lemma_realpow_diff_sumr2 [of 1 _ x]
    97   by (cases n) auto
    98 
    99 lemma one_diff_power_eq:
   100   fixes x :: "'a::{comm_ring,monoid_mult}"
   101   shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
   102 by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
   103 
   104 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
   105   x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
   106 
   107 lemma powser_insidea:
   108   fixes x z :: "'a::real_normed_div_algebra"
   109   assumes 1: "summable (\<lambda>n. f n * x^n)"
   110     and 2: "norm z < norm x"
   111   shows "summable (\<lambda>n. norm (f n * z ^ n))"
   112 proof -
   113   from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
   114   from 1 have "(\<lambda>n. f n * x^n) ----> 0"
   115     by (rule summable_LIMSEQ_zero)
   116   hence "convergent (\<lambda>n. f n * x^n)"
   117     by (rule convergentI)
   118   hence "Cauchy (\<lambda>n. f n * x^n)"
   119     by (rule convergent_Cauchy)
   120   hence "Bseq (\<lambda>n. f n * x^n)"
   121     by (rule Cauchy_Bseq)
   122   then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x^n) \<le> K"
   123     by (simp add: Bseq_def, safe)
   124   have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
   125                    K * norm (z ^ n) * inverse (norm (x^n))"
   126   proof (intro exI allI impI)
   127     fix n::nat
   128     assume "0 \<le> n"
   129     have "norm (norm (f n * z ^ n)) * norm (x^n) =
   130           norm (f n * x^n) * norm (z ^ n)"
   131       by (simp add: norm_mult abs_mult)
   132     also have "\<dots> \<le> K * norm (z ^ n)"
   133       by (simp only: mult_right_mono 4 norm_ge_zero)
   134     also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x^n)) * norm (x^n))"
   135       by (simp add: x_neq_0)
   136     also have "\<dots> = K * norm (z ^ n) * inverse (norm (x^n)) * norm (x^n)"
   137       by (simp only: mult.assoc)
   138     finally show "norm (norm (f n * z ^ n)) \<le>
   139                   K * norm (z ^ n) * inverse (norm (x^n))"
   140       by (simp add: mult_le_cancel_right x_neq_0)
   141   qed
   142   moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))"
   143   proof -
   144     from 2 have "norm (norm (z * inverse x)) < 1"
   145       using x_neq_0
   146       by (simp add: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric])
   147     hence "summable (\<lambda>n. norm (z * inverse x) ^ n)"
   148       by (rule summable_geometric)
   149     hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
   150       by (rule summable_mult)
   151     thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))"
   152       using x_neq_0
   153       by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
   154                     power_inverse norm_power mult.assoc)
   155   qed
   156   ultimately show "summable (\<lambda>n. norm (f n * z ^ n))"
   157     by (rule summable_comparison_test)
   158 qed
   159 
   160 lemma powser_inside:
   161   fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   162   shows
   163     "summable (\<lambda>n. f n * (x^n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
   164       summable (\<lambda>n. f n * (z ^ n))"
   165   by (rule powser_insidea [THEN summable_norm_cancel])
   166 
   167 lemma sum_split_even_odd:
   168   fixes f :: "nat \<Rightarrow> real"
   169   shows
   170     "(\<Sum>i<2 * n. if even i then f i else g i) =
   171      (\<Sum>i<n. f (2 * i)) + (\<Sum>i<n. g (2 * i + 1))"
   172 proof (induct n)
   173   case 0
   174   then show ?case by simp
   175 next
   176   case (Suc n)
   177   have "(\<Sum>i<2 * Suc n. if even i then f i else g i) =
   178     (\<Sum>i<n. f (2 * i)) + (\<Sum>i<n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
   179     using Suc.hyps unfolding One_nat_def by auto
   180   also have "\<dots> = (\<Sum>i<Suc n. f (2 * i)) + (\<Sum>i<Suc n. g (2 * i + 1))"
   181     by auto
   182   finally show ?case .
   183 qed
   184 
   185 lemma sums_if':
   186   fixes g :: "nat \<Rightarrow> real"
   187   assumes "g sums x"
   188   shows "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x"
   189   unfolding sums_def
   190 proof (rule LIMSEQ_I)
   191   fix r :: real
   192   assume "0 < r"
   193   from `g sums x`[unfolded sums_def, THEN LIMSEQ_D, OF this]
   194   obtain no where no_eq: "\<And> n. n \<ge> no \<Longrightarrow> (norm (setsum g {..<n} - x) < r)" by blast
   195 
   196   let ?SUM = "\<lambda> m. \<Sum>i<m. if even i then 0 else g ((i - 1) div 2)"
   197   {
   198     fix m
   199     assume "m \<ge> 2 * no"
   200     hence "m div 2 \<ge> no" by auto
   201     have sum_eq: "?SUM (2 * (m div 2)) = setsum g {..< m div 2}"
   202       using sum_split_even_odd by auto
   203     hence "(norm (?SUM (2 * (m div 2)) - x) < r)"
   204       using no_eq unfolding sum_eq using `m div 2 \<ge> no` by auto
   205     moreover
   206     have "?SUM (2 * (m div 2)) = ?SUM m"
   207     proof (cases "even m")
   208       case True
   209       then show ?thesis by (auto simp add: even_two_times_div_two)
   210     next
   211       case False
   212       then have eq: "Suc (2 * (m div 2)) = m" by simp
   213       hence "even (2 * (m div 2))" using `odd m` by auto
   214       have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
   215       also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto
   216       finally show ?thesis by auto
   217     qed
   218     ultimately have "(norm (?SUM m - x) < r)" by auto
   219   }
   220   thus "\<exists> no. \<forall> m \<ge> no. norm (?SUM m - x) < r" by blast
   221 qed
   222 
   223 lemma sums_if:
   224   fixes g :: "nat \<Rightarrow> real"
   225   assumes "g sums x" and "f sums y"
   226   shows "(\<lambda> n. if even n then f (n div 2) else g ((n - 1) div 2)) sums (x + y)"
   227 proof -
   228   let ?s = "\<lambda> n. if even n then 0 else f ((n - 1) div 2)"
   229   {
   230     fix B T E
   231     have "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)"
   232       by (cases B) auto
   233   } note if_sum = this
   234   have g_sums: "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x"
   235     using sums_if'[OF `g sums x`] .
   236   {
   237     have if_eq: "\<And>B T E. (if \<not> B then T else E) = (if B then E else T)" by auto
   238 
   239     have "?s sums y" using sums_if'[OF `f sums y`] .
   240     from this[unfolded sums_def, THEN LIMSEQ_Suc]
   241     have "(\<lambda> n. if even n then f (n div 2) else 0) sums y"
   242       by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum.reindex if_eq sums_def cong del: if_cong)
   243   }
   244   from sums_add[OF g_sums this] show ?thesis unfolding if_sum .
   245 qed
   246 
   247 subsection {* Alternating series test / Leibniz formula *}
   248 
   249 lemma sums_alternating_upper_lower:
   250   fixes a :: "nat \<Rightarrow> real"
   251   assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0"
   252   shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. (- 1)^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. (- 1)^i*a i) ----> l) \<and>
   253              ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. (- 1)^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. (- 1)^i*a i) ----> l)"
   254   (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
   255 proof (rule nested_sequence_unique)
   256   have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
   257 
   258   show "\<forall>n. ?f n \<le> ?f (Suc n)"
   259   proof
   260     fix n
   261     show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto
   262   qed
   263   show "\<forall>n. ?g (Suc n) \<le> ?g n"
   264   proof
   265     fix n
   266     show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"]
   267       unfolding One_nat_def by auto
   268   qed
   269   show "\<forall>n. ?f n \<le> ?g n"
   270   proof
   271     fix n
   272     show "?f n \<le> ?g n" using fg_diff a_pos
   273       unfolding One_nat_def by auto
   274   qed
   275   show "(\<lambda>n. ?f n - ?g n) ----> 0" unfolding fg_diff
   276   proof (rule LIMSEQ_I)
   277     fix r :: real
   278     assume "0 < r"
   279     with `a ----> 0`[THEN LIMSEQ_D] obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n - 0) < r"
   280       by auto
   281     hence "\<forall>n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
   282     thus "\<exists>N. \<forall>n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
   283   qed
   284 qed
   285 
   286 lemma summable_Leibniz':
   287   fixes a :: "nat \<Rightarrow> real"
   288   assumes a_zero: "a ----> 0"
   289     and a_pos: "\<And> n. 0 \<le> a n"
   290     and a_monotone: "\<And> n. a (Suc n) \<le> a n"
   291   shows summable: "summable (\<lambda> n. (-1)^n * a n)"
   292     and "\<And>n. (\<Sum>i<2*n. (-1)^i*a i) \<le> (\<Sum>i. (-1)^i*a i)"
   293     and "(\<lambda>n. \<Sum>i<2*n. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
   294     and "\<And>n. (\<Sum>i. (-1)^i*a i) \<le> (\<Sum>i<2*n+1. (-1)^i*a i)"
   295     and "(\<lambda>n. \<Sum>i<2*n+1. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
   296 proof -
   297   let ?S = "\<lambda>n. (-1)^n * a n"
   298   let ?P = "\<lambda>n. \<Sum>i<n. ?S i"
   299   let ?f = "\<lambda>n. ?P (2 * n)"
   300   let ?g = "\<lambda>n. ?P (2 * n + 1)"
   301   obtain l :: real
   302     where below_l: "\<forall> n. ?f n \<le> l"
   303       and "?f ----> l"
   304       and above_l: "\<forall> n. l \<le> ?g n"
   305       and "?g ----> l"
   306     using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast
   307 
   308   let ?Sa = "\<lambda>m. \<Sum>n<m. ?S n"
   309   have "?Sa ----> l"
   310   proof (rule LIMSEQ_I)
   311     fix r :: real
   312     assume "0 < r"
   313     with `?f ----> l`[THEN LIMSEQ_D]
   314     obtain f_no where f: "\<And> n. n \<ge> f_no \<Longrightarrow> norm (?f n - l) < r" by auto
   315 
   316     from `0 < r` `?g ----> l`[THEN LIMSEQ_D]
   317     obtain g_no where g: "\<And> n. n \<ge> g_no \<Longrightarrow> norm (?g n - l) < r" by auto
   318 
   319     {
   320       fix n :: nat
   321       assume "n \<ge> (max (2 * f_no) (2 * g_no))"
   322       hence "n \<ge> 2 * f_no" and "n \<ge> 2 * g_no" by auto
   323       have "norm (?Sa n - l) < r"
   324       proof (cases "even n")
   325         case True
   326         then have n_eq: "2 * (n div 2) = n" by (simp add: even_two_times_div_two)
   327         with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no"
   328           by auto
   329         from f[OF this] show ?thesis
   330           unfolding n_eq atLeastLessThanSuc_atLeastAtMost .
   331       next
   332         case False
   333         hence "even (n - 1)" by simp
   334         then have n_eq: "2 * ((n - 1) div 2) = n - 1"
   335           by (simp add: even_two_times_div_two)
   336         hence range_eq: "n - 1 + 1 = n"
   337           using odd_pos[OF False] by auto
   338 
   339         from n_eq `n \<ge> 2 * g_no` have "(n - 1) div 2 \<ge> g_no"
   340           by auto
   341         from g[OF this] show ?thesis
   342           unfolding n_eq range_eq .
   343       qed
   344     }
   345     thus "\<exists>no. \<forall>n \<ge> no. norm (?Sa n - l) < r" by blast
   346   qed
   347   hence sums_l: "(\<lambda>i. (-1)^i * a i) sums l"
   348     unfolding sums_def .
   349   thus "summable ?S" using summable_def by auto
   350 
   351   have "l = suminf ?S" using sums_unique[OF sums_l] .
   352 
   353   fix n
   354   show "suminf ?S \<le> ?g n"
   355     unfolding sums_unique[OF sums_l, symmetric] using above_l by auto
   356   show "?f n \<le> suminf ?S"
   357     unfolding sums_unique[OF sums_l, symmetric] using below_l by auto
   358   show "?g ----> suminf ?S"
   359     using `?g ----> l` `l = suminf ?S` by auto
   360   show "?f ----> suminf ?S"
   361     using `?f ----> l` `l = suminf ?S` by auto
   362 qed
   363 
   364 theorem summable_Leibniz:
   365   fixes a :: "nat \<Rightarrow> real"
   366   assumes a_zero: "a ----> 0" and "monoseq a"
   367   shows "summable (\<lambda> n. (-1)^n * a n)" (is "?summable")
   368     and "0 < a 0 \<longrightarrow>
   369       (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n. (- 1)^i * a i .. \<Sum>i<2*n+1. (- 1)^i * a i})" (is "?pos")
   370     and "a 0 < 0 \<longrightarrow>
   371       (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n+1. (- 1)^i * a i .. \<Sum>i<2*n. (- 1)^i * a i})" (is "?neg")
   372     and "(\<lambda>n. \<Sum>i<2*n. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?f")
   373     and "(\<lambda>n. \<Sum>i<2*n+1. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?g")
   374 proof -
   375   have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g"
   376   proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)")
   377     case True
   378     hence ord: "\<And>n m. m \<le> n \<Longrightarrow> a n \<le> a m" and ge0: "\<And> n. 0 \<le> a n"
   379       by auto
   380     {
   381       fix n
   382       have "a (Suc n) \<le> a n"
   383         using ord[where n="Suc n" and m=n] by auto
   384     } note mono = this
   385     note leibniz = summable_Leibniz'[OF `a ----> 0` ge0]
   386     from leibniz[OF mono]
   387     show ?thesis using `0 \<le> a 0` by auto
   388   next
   389     let ?a = "\<lambda> n. - a n"
   390     case False
   391     with monoseq_le[OF `monoseq a` `a ----> 0`]
   392     have "(\<forall> n. a n \<le> 0) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)" by auto
   393     hence ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n"
   394       by auto
   395     {
   396       fix n
   397       have "?a (Suc n) \<le> ?a n" using ord[where n="Suc n" and m=n]
   398         by auto
   399     } note monotone = this
   400     note leibniz =
   401       summable_Leibniz'[OF _ ge0, of "\<lambda>x. x",
   402         OF tendsto_minus[OF `a ----> 0`, unfolded minus_zero] monotone]
   403     have "summable (\<lambda> n. (-1)^n * ?a n)"
   404       using leibniz(1) by auto
   405     then obtain l where "(\<lambda> n. (-1)^n * ?a n) sums l"
   406       unfolding summable_def by auto
   407     from this[THEN sums_minus] have "(\<lambda> n. (-1)^n * a n) sums -l"
   408       by auto
   409     hence ?summable unfolding summable_def by auto
   410     moreover
   411     have "\<And>a b :: real. \<bar>- a - - b\<bar> = \<bar>a - b\<bar>"
   412       unfolding minus_diff_minus by auto
   413 
   414     from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus]
   415     have move_minus: "(\<Sum>n. - ((- 1) ^ n * a n)) = - (\<Sum>n. (- 1) ^ n * a n)"
   416       by auto
   417 
   418     have ?pos using `0 \<le> ?a 0` by auto
   419     moreover have ?neg
   420       using leibniz(2,4)
   421       unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le
   422       by auto
   423     moreover have ?f and ?g
   424       using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel]
   425       by auto
   426     ultimately show ?thesis by auto
   427   qed
   428   then show ?summable and ?pos and ?neg and ?f and ?g
   429     by safe
   430 qed
   431 
   432 subsection {* Term-by-Term Differentiability of Power Series *}
   433 
   434 definition diffs :: "(nat \<Rightarrow> 'a::ring_1) \<Rightarrow> nat \<Rightarrow> 'a"
   435   where "diffs c = (\<lambda>n. of_nat (Suc n) * c (Suc n))"
   436 
   437 text{*Lemma about distributing negation over it*}
   438 lemma diffs_minus: "diffs (\<lambda>n. - c n) = (\<lambda>n. - diffs c n)"
   439   by (simp add: diffs_def)
   440 
   441 lemma sums_Suc_imp:
   442   "(f::nat \<Rightarrow> 'a::real_normed_vector) 0 = 0 \<Longrightarrow> (\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
   443   using sums_Suc_iff[of f] by simp
   444 
   445 lemma diffs_equiv:
   446   fixes x :: "'a::{real_normed_vector, ring_1}"
   447   shows "summable (\<lambda>n. diffs c n * x^n) \<Longrightarrow>
   448       (\<lambda>n. of_nat n * c n * x^(n - Suc 0)) sums (\<Sum>n. diffs c n * x^n)"
   449   unfolding diffs_def
   450   by (simp add: summable_sums sums_Suc_imp)
   451 
   452 lemma lemma_termdiff1:
   453   fixes z :: "'a :: {monoid_mult,comm_ring}" shows
   454   "(\<Sum>p<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
   455    (\<Sum>p<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
   456   by (auto simp add: algebra_simps power_add [symmetric])
   457 
   458 lemma sumr_diff_mult_const2:
   459   "setsum f {..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i<n. f i - r)"
   460   by (simp add: setsum_subtractf)
   461 
   462 lemma lemma_termdiff2:
   463   fixes h :: "'a :: {field}"
   464   assumes h: "h \<noteq> 0"
   465   shows
   466     "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
   467      h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p.
   468           (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs")
   469   apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h)
   470   apply (simp add: right_diff_distrib diff_divide_distrib h)
   471   apply (simp add: mult.assoc [symmetric])
   472   apply (cases "n", simp)
   473   apply (simp add: lemma_realpow_diff_sumr2 h
   474                    right_diff_distrib [symmetric] mult.assoc
   475               del: power_Suc setsum_lessThan_Suc of_nat_Suc)
   476   apply (subst lemma_realpow_rev_sumr)
   477   apply (subst sumr_diff_mult_const2)
   478   apply simp
   479   apply (simp only: lemma_termdiff1 setsum_right_distrib)
   480   apply (rule setsum.cong [OF refl])
   481   apply (simp add: less_iff_Suc_add)
   482   apply (clarify)
   483   apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 ac_simps
   484               del: setsum_lessThan_Suc power_Suc)
   485   apply (subst mult.assoc [symmetric], subst power_add [symmetric])
   486   apply (simp add: ac_simps)
   487   done
   488 
   489 lemma real_setsum_nat_ivl_bounded2:
   490   fixes K :: "'a::linordered_semidom"
   491   assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
   492     and K: "0 \<le> K"
   493   shows "setsum f {..<n-k} \<le> of_nat n * K"
   494   apply (rule order_trans [OF setsum_mono])
   495   apply (rule f, simp)
   496   apply (simp add: mult_right_mono K)
   497   done
   498 
   499 lemma lemma_termdiff3:
   500   fixes h z :: "'a::{real_normed_field}"
   501   assumes 1: "h \<noteq> 0"
   502     and 2: "norm z \<le> K"
   503     and 3: "norm (z + h) \<le> K"
   504   shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0))
   505           \<le> of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
   506 proof -
   507   have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) =
   508         norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p.
   509           (z + h) ^ q * z ^ (n - 2 - q)) * norm h"
   510     by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult.commute norm_mult)
   511   also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
   512   proof (rule mult_right_mono [OF _ norm_ge_zero])
   513     from norm_ge_zero 2 have K: "0 \<le> K"
   514       by (rule order_trans)
   515     have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n"
   516       apply (erule subst)
   517       apply (simp only: norm_mult norm_power power_add)
   518       apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
   519       done
   520     show "norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))
   521           \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
   522       apply (intro
   523          order_trans [OF norm_setsum]
   524          real_setsum_nat_ivl_bounded2
   525          mult_nonneg_nonneg
   526          of_nat_0_le_iff
   527          zero_le_power K)
   528       apply (rule le_Kn, simp)
   529       done
   530   qed
   531   also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
   532     by (simp only: mult.assoc)
   533   finally show ?thesis .
   534 qed
   535 
   536 lemma lemma_termdiff4:
   537   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   538   assumes k: "0 < (k::real)"
   539     and le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
   540   shows "f -- 0 --> 0"
   541 proof (rule tendsto_norm_zero_cancel)
   542   show "(\<lambda>h. norm (f h)) -- 0 --> 0"
   543   proof (rule real_tendsto_sandwich)
   544     show "eventually (\<lambda>h. 0 \<le> norm (f h)) (at 0)"
   545       by simp
   546     show "eventually (\<lambda>h. norm (f h) \<le> K * norm h) (at 0)"
   547       using k by (auto simp add: eventually_at dist_norm le)
   548     show "(\<lambda>h. 0) -- (0::'a) --> (0::real)"
   549       by (rule tendsto_const)
   550     have "(\<lambda>h. K * norm h) -- (0::'a) --> K * norm (0::'a)"
   551       by (intro tendsto_intros)
   552     then show "(\<lambda>h. K * norm h) -- (0::'a) --> 0"
   553       by simp
   554   qed
   555 qed
   556 
   557 lemma lemma_termdiff5:
   558   fixes g :: "'a::real_normed_vector \<Rightarrow> nat \<Rightarrow> 'b::banach"
   559   assumes k: "0 < (k::real)"
   560   assumes f: "summable f"
   561   assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h"
   562   shows "(\<lambda>h. suminf (g h)) -- 0 --> 0"
   563 proof (rule lemma_termdiff4 [OF k])
   564   fix h::'a
   565   assume "h \<noteq> 0" and "norm h < k"
   566   hence A: "\<forall>n. norm (g h n) \<le> f n * norm h"
   567     by (simp add: le)
   568   hence "\<exists>N. \<forall>n\<ge>N. norm (norm (g h n)) \<le> f n * norm h"
   569     by simp
   570   moreover from f have B: "summable (\<lambda>n. f n * norm h)"
   571     by (rule summable_mult2)
   572   ultimately have C: "summable (\<lambda>n. norm (g h n))"
   573     by (rule summable_comparison_test)
   574   hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))"
   575     by (rule summable_norm)
   576   also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)"
   577     by (rule suminf_le)
   578   also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h"
   579     by (rule suminf_mult2 [symmetric])
   580   finally show "norm (suminf (g h)) \<le> suminf f * norm h" .
   581 qed
   582 
   583 
   584 text{* FIXME: Long proofs*}
   585 
   586 lemma termdiffs_aux:
   587   fixes x :: "'a::{real_normed_field,banach}"
   588   assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
   589     and 2: "norm x < norm K"
   590   shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h
   591              - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   592 proof -
   593   from dense [OF 2]
   594   obtain r where r1: "norm x < r" and r2: "r < norm K" by fast
   595   from norm_ge_zero r1 have r: "0 < r"
   596     by (rule order_le_less_trans)
   597   hence r_neq_0: "r \<noteq> 0" by simp
   598   show ?thesis
   599   proof (rule lemma_termdiff5)
   600     show "0 < r - norm x" using r1 by simp
   601     from r r2 have "norm (of_real r::'a) < norm K"
   602       by simp
   603     with 1 have "summable (\<lambda>n. norm (diffs (diffs c) n * (of_real r ^ n)))"
   604       by (rule powser_insidea)
   605     hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. norm (c n))) n * r ^ n)"
   606       using r
   607       by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc)
   608     hence "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))"
   609       by (rule diffs_equiv [THEN sums_summable])
   610     also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0)) =
   611       (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
   612       apply (rule ext)
   613       apply (simp add: diffs_def)
   614       apply (case_tac n, simp_all add: r_neq_0)
   615       done
   616     finally have "summable
   617       (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
   618       by (rule diffs_equiv [THEN sums_summable])
   619     also have
   620       "(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) *
   621            r ^ (n - Suc 0)) =
   622        (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
   623       apply (rule ext)
   624       apply (case_tac "n", simp)
   625       apply (rename_tac nat)
   626       apply (case_tac "nat", simp)
   627       apply (simp add: r_neq_0)
   628       done
   629     finally
   630     show "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
   631   next
   632     fix h::'a and n::nat
   633     assume h: "h \<noteq> 0"
   634     assume "norm h < r - norm x"
   635     hence "norm x + norm h < r" by simp
   636     with norm_triangle_ineq have xh: "norm (x + h) < r"
   637       by (rule order_le_less_trans)
   638     show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))
   639           \<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
   640       apply (simp only: norm_mult mult.assoc)
   641       apply (rule mult_left_mono [OF _ norm_ge_zero])
   642       apply (simp add: mult.assoc [symmetric])
   643       apply (metis h lemma_termdiff3 less_eq_real_def r1 xh)
   644       done
   645   qed
   646 qed
   647 
   648 lemma termdiffs:
   649   fixes K x :: "'a::{real_normed_field,banach}"
   650   assumes 1: "summable (\<lambda>n. c n * K ^ n)"
   651       and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
   652       and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
   653       and 4: "norm x < norm K"
   654   shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. (diffs c) n * x^n)"
   655   unfolding DERIV_def
   656 proof (rule LIM_zero_cancel)
   657   show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x^n)) / h
   658             - suminf (\<lambda>n. diffs c n * x^n)) -- 0 --> 0"
   659   proof (rule LIM_equal2)
   660     show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
   661   next
   662     fix h :: 'a
   663     assume "norm (h - 0) < norm K - norm x"
   664     hence "norm x + norm h < norm K" by simp
   665     hence 5: "norm (x + h) < norm K"
   666       by (rule norm_triangle_ineq [THEN order_le_less_trans])
   667     have "summable (\<lambda>n. c n * x^n)"
   668       and "summable (\<lambda>n. c n * (x + h) ^ n)"
   669       and "summable (\<lambda>n. diffs c n * x^n)"
   670       using 1 2 4 5 by (auto elim: powser_inside)
   671     then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x^n)) / h - (\<Sum>n. diffs c n * x^n) =
   672           (\<Sum>n. (c n * (x + h) ^ n - c n * x^n) / h - of_nat n * c n * x ^ (n - Suc 0))"
   673       by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums)
   674     then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x^n)) / h - (\<Sum>n. diffs c n * x^n) =
   675           (\<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))"
   676       by (simp add: algebra_simps)
   677   next
   678     show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   679       by (rule termdiffs_aux [OF 3 4])
   680   qed
   681 qed
   682 
   683 
   684 subsection {* Derivability of power series *}
   685 
   686 lemma DERIV_series':
   687   fixes f :: "real \<Rightarrow> nat \<Rightarrow> real"
   688   assumes DERIV_f: "\<And> n. DERIV (\<lambda> x. f x n) x0 :> (f' x0 n)"
   689     and allf_summable: "\<And> x. x \<in> {a <..< b} \<Longrightarrow> summable (f x)" and x0_in_I: "x0 \<in> {a <..< b}"
   690     and "summable (f' x0)"
   691     and "summable L"
   692     and L_def: "\<And>n x y. \<lbrakk> x \<in> { a <..< b} ; y \<in> { a <..< b} \<rbrakk> \<Longrightarrow> \<bar>f x n - f y n\<bar> \<le> L n * \<bar>x - y\<bar>"
   693   shows "DERIV (\<lambda> x. suminf (f x)) x0 :> (suminf (f' x0))"
   694   unfolding DERIV_def
   695 proof (rule LIM_I)
   696   fix r :: real
   697   assume "0 < r" hence "0 < r/3" by auto
   698 
   699   obtain N_L where N_L: "\<And> n. N_L \<le> n \<Longrightarrow> \<bar> \<Sum> i. L (i + n) \<bar> < r/3"
   700     using suminf_exist_split[OF `0 < r/3` `summable L`] by auto
   701 
   702   obtain N_f' where N_f': "\<And> n. N_f' \<le> n \<Longrightarrow> \<bar> \<Sum> i. f' x0 (i + n) \<bar> < r/3"
   703     using suminf_exist_split[OF `0 < r/3` `summable (f' x0)`] by auto
   704 
   705   let ?N = "Suc (max N_L N_f')"
   706   have "\<bar> \<Sum> i. f' x0 (i + ?N) \<bar> < r/3" (is "?f'_part < r/3") and
   707     L_estimate: "\<bar> \<Sum> i. L (i + ?N) \<bar> < r/3" using N_L[of "?N"] and N_f' [of "?N"] by auto
   708 
   709   let ?diff = "\<lambda>i x. (f (x0 + x) i - f x0 i) / x"
   710 
   711   let ?r = "r / (3 * real ?N)"
   712   from `0 < r` have "0 < ?r" by simp
   713 
   714   let ?s = "\<lambda>n. SOME s. 0 < s \<and> (\<forall> x. x \<noteq> 0 \<and> \<bar> x \<bar> < s \<longrightarrow> \<bar> ?diff n x - f' x0 n \<bar> < ?r)"
   715   def S' \<equiv> "Min (?s ` {..< ?N })"
   716 
   717   have "0 < S'" unfolding S'_def
   718   proof (rule iffD2[OF Min_gr_iff])
   719     show "\<forall>x \<in> (?s ` {..< ?N }). 0 < x"
   720     proof
   721       fix x
   722       assume "x \<in> ?s ` {..<?N}"
   723       then obtain n where "x = ?s n" and "n \<in> {..<?N}"
   724         using image_iff[THEN iffD1] by blast
   725       from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def]
   726       obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r)"
   727         by auto
   728       have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound)
   729       thus "0 < x" unfolding `x = ?s n` .
   730     qed
   731   qed auto
   732 
   733   def S \<equiv> "min (min (x0 - a) (b - x0)) S'"
   734   hence "0 < S" and S_a: "S \<le> x0 - a" and S_b: "S \<le> b - x0"
   735     and "S \<le> S'" using x0_in_I and `0 < S'`
   736     by auto
   737 
   738   {
   739     fix x
   740     assume "x \<noteq> 0" and "\<bar> x \<bar> < S"
   741     hence x_in_I: "x0 + x \<in> { a <..< b }"
   742       using S_a S_b by auto
   743 
   744     note diff_smbl = summable_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
   745     note div_smbl = summable_divide[OF diff_smbl]
   746     note all_smbl = summable_diff[OF div_smbl `summable (f' x0)`]
   747     note ign = summable_ignore_initial_segment[where k="?N"]
   748     note diff_shft_smbl = summable_diff[OF ign[OF allf_summable[OF x_in_I]] ign[OF allf_summable[OF x0_in_I]]]
   749     note div_shft_smbl = summable_divide[OF diff_shft_smbl]
   750     note all_shft_smbl = summable_diff[OF div_smbl ign[OF `summable (f' x0)`]]
   751 
   752     { fix n
   753       have "\<bar> ?diff (n + ?N) x \<bar> \<le> L (n + ?N) * \<bar> (x0 + x) - x0 \<bar> / \<bar> x \<bar>"
   754         using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero]
   755         unfolding abs_divide .
   756       hence "\<bar> (\<bar>?diff (n + ?N) x \<bar>) \<bar> \<le> L (n + ?N)"
   757         using `x \<noteq> 0` by auto }
   758     note 1 = this and 2 = summable_rabs_comparison_test[OF _ ign[OF `summable L`]]
   759     then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))"
   760       by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] suminf_le[OF _ 2 ign[OF `summable L`]]])
   761     then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3")
   762       using L_estimate by auto
   763 
   764     have "\<bar>\<Sum>n<?N. ?diff n x - f' x0 n \<bar> \<le> (\<Sum>n<?N. \<bar>?diff n x - f' x0 n \<bar>)" ..
   765     also have "\<dots> < (\<Sum>n<?N. ?r)"
   766     proof (rule setsum_strict_mono)
   767       fix n
   768       assume "n \<in> {..< ?N}"
   769       have "\<bar>x\<bar> < S" using `\<bar>x\<bar> < S` .
   770       also have "S \<le> S'" using `S \<le> S'` .
   771       also have "S' \<le> ?s n" unfolding S'_def
   772       proof (rule Min_le_iff[THEN iffD2])
   773         have "?s n \<in> (?s ` {..<?N}) \<and> ?s n \<le> ?s n"
   774           using `n \<in> {..< ?N}` by auto
   775         thus "\<exists> a \<in> (?s ` {..<?N}). a \<le> ?s n" by blast
   776       qed auto
   777       finally have "\<bar>x\<bar> < ?s n" .
   778 
   779       from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def diff_0_right, unfolded some_eq_ex[symmetric], THEN conjunct2]
   780       have "\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < ?s n \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r" .
   781       with `x \<noteq> 0` and `\<bar>x\<bar> < ?s n` show "\<bar>?diff n x - f' x0 n\<bar> < ?r"
   782         by blast
   783     qed auto
   784     also have "\<dots> = of_nat (card {..<?N}) * ?r"
   785       by (rule setsum_constant)
   786     also have "\<dots> = real ?N * ?r"
   787       unfolding real_eq_of_nat by auto
   788     also have "\<dots> = r/3" by auto
   789     finally have "\<bar>\<Sum>n<?N. ?diff n x - f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") .
   790 
   791     from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
   792     have "\<bar>(suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0)\<bar> =
   793         \<bar>\<Sum>n. ?diff n x - f' x0 n\<bar>"
   794       unfolding suminf_diff[OF div_smbl `summable (f' x0)`, symmetric]
   795       using suminf_divide[OF diff_smbl, symmetric] by auto
   796     also have "\<dots> \<le> ?diff_part + \<bar> (\<Sum>n. ?diff (n + ?N) x) - (\<Sum> n. f' x0 (n + ?N)) \<bar>"
   797       unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"]
   798       unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]]
   799       apply (subst (5) add.commute)
   800       by (rule abs_triangle_ineq)
   801     also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part"
   802       using abs_triangle_ineq4 by auto
   803     also have "\<dots> < r /3 + r/3 + r/3"
   804       using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3`
   805       by (rule add_strict_mono [OF add_less_le_mono])
   806     finally have "\<bar>(suminf (f (x0 + x)) - suminf (f x0)) / x - suminf (f' x0)\<bar> < r"
   807       by auto
   808   }
   809   thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x - 0) < s \<longrightarrow>
   810       norm (((\<Sum>n. f (x0 + x) n) - (\<Sum>n. f x0 n)) / x - (\<Sum>n. f' x0 n)) < r"
   811     using `0 < S` unfolding real_norm_def diff_0_right by blast
   812 qed
   813 
   814 lemma DERIV_power_series':
   815   fixes f :: "nat \<Rightarrow> real"
   816   assumes converges: "\<And> x. x \<in> {-R <..< R} \<Longrightarrow> summable (\<lambda> n. f n * real (Suc n) * x^n)"
   817     and x0_in_I: "x0 \<in> {-R <..< R}" and "0 < R"
   818   shows "DERIV (\<lambda> x. (\<Sum> n. f n * x^(Suc n))) x0 :> (\<Sum> n. f n * real (Suc n) * x0^n)"
   819   (is "DERIV (\<lambda> x. (suminf (?f x))) x0 :> (suminf (?f' x0))")
   820 proof -
   821   {
   822     fix R'
   823     assume "0 < R'" and "R' < R" and "-R' < x0" and "x0 < R'"
   824     hence "x0 \<in> {-R' <..< R'}" and "R' \<in> {-R <..< R}" and "x0 \<in> {-R <..< R}"
   825       by auto
   826     have "DERIV (\<lambda> x. (suminf (?f x))) x0 :> (suminf (?f' x0))"
   827     proof (rule DERIV_series')
   828       show "summable (\<lambda> n. \<bar>f n * real (Suc n) * R'^n\<bar>)"
   829       proof -
   830         have "(R' + R) / 2 < R" and "0 < (R' + R) / 2"
   831           using `0 < R'` `0 < R` `R' < R` by auto
   832         hence in_Rball: "(R' + R) / 2 \<in> {-R <..< R}"
   833           using `R' < R` by auto
   834         have "norm R' < norm ((R' + R) / 2)"
   835           using `0 < R'` `0 < R` `R' < R` by auto
   836         from powser_insidea[OF converges[OF in_Rball] this] show ?thesis
   837           by auto
   838       qed
   839       {
   840         fix n x y
   841         assume "x \<in> {-R' <..< R'}" and "y \<in> {-R' <..< R'}"
   842         show "\<bar>?f x n - ?f y n\<bar> \<le> \<bar>f n * real (Suc n) * R'^n\<bar> * \<bar>x-y\<bar>"
   843         proof -
   844           have "\<bar>f n * x ^ (Suc n) - f n * y ^ (Suc n)\<bar> =
   845             (\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar>"
   846             unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult
   847             by auto
   848           also have "\<dots> \<le> (\<bar>f n\<bar> * \<bar>x-y\<bar>) * (\<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>)"
   849           proof (rule mult_left_mono)
   850             have "\<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> (\<Sum>p<Suc n. \<bar>x ^ p * y ^ (n - p)\<bar>)"
   851               by (rule setsum_abs)
   852             also have "\<dots> \<le> (\<Sum>p<Suc n. R' ^ n)"
   853             proof (rule setsum_mono)
   854               fix p
   855               assume "p \<in> {..<Suc n}"
   856               hence "p \<le> n" by auto
   857               {
   858                 fix n
   859                 fix x :: real
   860                 assume "x \<in> {-R'<..<R'}"
   861                 hence "\<bar>x\<bar> \<le> R'"  by auto
   862                 hence "\<bar>x^n\<bar> \<le> R'^n"
   863                   unfolding power_abs by (rule power_mono, auto)
   864               }
   865               from mult_mono[OF this[OF `x \<in> {-R'<..<R'}`, of p] this[OF `y \<in> {-R'<..<R'}`, of "n-p"]] `0 < R'`
   866               have "\<bar>x^p * y^(n-p)\<bar> \<le> R'^p * R'^(n-p)"
   867                 unfolding abs_mult by auto
   868               thus "\<bar>x^p * y^(n-p)\<bar> \<le> R'^n"
   869                 unfolding power_add[symmetric] using `p \<le> n` by auto
   870             qed
   871             also have "\<dots> = real (Suc n) * R' ^ n"
   872               unfolding setsum_constant card_atLeastLessThan real_of_nat_def by auto
   873             finally show "\<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>"
   874               unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] .
   875             show "0 \<le> \<bar>f n\<bar> * \<bar>x - y\<bar>"
   876               unfolding abs_mult[symmetric] by auto
   877           qed
   878           also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>"
   879             unfolding abs_mult mult.assoc[symmetric] by algebra
   880           finally show ?thesis .
   881         qed
   882       }
   883       {
   884         fix n
   885         show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
   886           by (auto intro!: derivative_eq_intros simp del: power_Suc simp: real_of_nat_def)
   887       }
   888       {
   889         fix x
   890         assume "x \<in> {-R' <..< R'}"
   891         hence "R' \<in> {-R <..< R}" and "norm x < norm R'"
   892           using assms `R' < R` by auto
   893         have "summable (\<lambda> n. f n * x^n)"
   894         proof (rule summable_comparison_test, intro exI allI impI)
   895           fix n
   896           have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)"
   897             by (rule mult_left_mono) auto
   898           show "norm (f n * x^n) \<le> norm (f n * real (Suc n) * x^n)"
   899             unfolding real_norm_def abs_mult
   900             by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right])
   901         qed (rule powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`])
   902         from this[THEN summable_mult2[where c=x], unfolded mult.assoc, unfolded mult.commute]
   903         show "summable (?f x)" by auto
   904       }
   905       show "summable (?f' x0)"
   906         using converges[OF `x0 \<in> {-R <..< R}`] .
   907       show "x0 \<in> {-R' <..< R'}"
   908         using `x0 \<in> {-R' <..< R'}` .
   909     qed
   910   } note for_subinterval = this
   911   let ?R = "(R + \<bar>x0\<bar>) / 2"
   912   have "\<bar>x0\<bar> < ?R" using assms by auto
   913   hence "- ?R < x0"
   914   proof (cases "x0 < 0")
   915     case True
   916     hence "- x0 < ?R" using `\<bar>x0\<bar> < ?R` by auto
   917     thus ?thesis unfolding neg_less_iff_less[symmetric, of "- x0"] by auto
   918   next
   919     case False
   920     have "- ?R < 0" using assms by auto
   921     also have "\<dots> \<le> x0" using False by auto
   922     finally show ?thesis .
   923   qed
   924   hence "0 < ?R" "?R < R" "- ?R < x0" and "x0 < ?R"
   925     using assms by auto
   926   from for_subinterval[OF this]
   927   show ?thesis .
   928 qed
   929 
   930 
   931 subsection {* Exponential Function *}
   932 
   933 definition exp :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
   934   where "exp = (\<lambda>x. \<Sum>n. x^n /\<^sub>R fact n)"
   935 
   936 lemma summable_exp_generic:
   937   fixes x :: "'a::{real_normed_algebra_1,banach}"
   938   defines S_def: "S \<equiv> \<lambda>n. x^n /\<^sub>R fact n"
   939   shows "summable S"
   940 proof -
   941   have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R (Suc n)"
   942     unfolding S_def by (simp del: mult_Suc)
   943   obtain r :: real where r0: "0 < r" and r1: "r < 1"
   944     using dense [OF zero_less_one] by fast
   945   obtain N :: nat where N: "norm x < real N * r"
   946     using reals_Archimedean3 [OF r0] by fast
   947   from r1 show ?thesis
   948   proof (rule summable_ratio_test [rule_format])
   949     fix n :: nat
   950     assume n: "N \<le> n"
   951     have "norm x \<le> real N * r"
   952       using N by (rule order_less_imp_le)
   953     also have "real N * r \<le> real (Suc n) * r"
   954       using r0 n by (simp add: mult_right_mono)
   955     finally have "norm x * norm (S n) \<le> real (Suc n) * r * norm (S n)"
   956       using norm_ge_zero by (rule mult_right_mono)
   957     hence "norm (x * S n) \<le> real (Suc n) * r * norm (S n)"
   958       by (rule order_trans [OF norm_mult_ineq])
   959     hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)"
   960       by (simp add: pos_divide_le_eq ac_simps)
   961     thus "norm (S (Suc n)) \<le> r * norm (S n)"
   962       by (simp add: S_Suc inverse_eq_divide)
   963   qed
   964 qed
   965 
   966 lemma summable_norm_exp:
   967   fixes x :: "'a::{real_normed_algebra_1,banach}"
   968   shows "summable (\<lambda>n. norm (x^n /\<^sub>R fact n))"
   969 proof (rule summable_norm_comparison_test [OF exI, rule_format])
   970   show "summable (\<lambda>n. norm x^n /\<^sub>R fact n)"
   971     by (rule summable_exp_generic)
   972   fix n
   973   show "norm (x^n /\<^sub>R fact n) \<le> norm x^n /\<^sub>R fact n"
   974     by (simp add: norm_power_ineq)
   975 qed
   976 
   977 lemma summable_exp: 
   978   fixes x :: "'a::{real_normed_field,banach}"
   979   shows "summable (\<lambda>n. inverse (fact n) * x^n)"
   980   using summable_exp_generic [where x=x]
   981   by (simp add: scaleR_conv_of_real nonzero_of_real_inverse)
   982 
   983 lemma exp_converges: "(\<lambda>n. x^n /\<^sub>R fact n) sums exp x"
   984   unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
   985 
   986 lemma exp_fdiffs:
   987   fixes XXX :: "'a::{real_normed_field,banach}"
   988   shows "diffs (\<lambda>n. inverse (fact n)) = (\<lambda>n. inverse (fact n :: 'a))"
   989   by (simp add: diffs_def mult_ac nonzero_inverse_mult_distrib nonzero_of_real_inverse
   990            del: mult_Suc of_nat_Suc)
   991 
   992 lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
   993   by (simp add: diffs_def)
   994 
   995 lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
   996   unfolding exp_def scaleR_conv_of_real
   997   apply (rule DERIV_cong)
   998   apply (rule termdiffs [where K="of_real (1 + norm x)"])
   999   apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
  1000   apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
  1001   apply (simp del: of_real_add)
  1002   done
  1003 
  1004 declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
  1005 
  1006 lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
  1007 proof -
  1008   from summable_norm[OF summable_norm_exp, of x]
  1009   have "norm (exp x) \<le> (\<Sum>n. inverse (fact n) * norm (x^n))"
  1010     by (simp add: exp_def)
  1011   also have "\<dots> \<le> exp (norm x)"
  1012     using summable_exp_generic[of "norm x"] summable_norm_exp[of x]
  1013     by (auto simp: exp_def intro!: suminf_le norm_power_ineq)
  1014   finally show ?thesis .
  1015 qed
  1016 
  1017 lemma isCont_exp:
  1018   fixes x::"'a::{real_normed_field,banach}"
  1019   shows "isCont exp x"
  1020   by (rule DERIV_exp [THEN DERIV_isCont])
  1021 
  1022 lemma isCont_exp' [simp]:
  1023   fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
  1024   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a"
  1025   by (rule isCont_o2 [OF _ isCont_exp])
  1026 
  1027 lemma tendsto_exp [tendsto_intros]:
  1028   fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
  1029   shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
  1030   by (rule isCont_tendsto_compose [OF isCont_exp])
  1031 
  1032 lemma continuous_exp [continuous_intros]:
  1033   fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
  1034   shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
  1035   unfolding continuous_def by (rule tendsto_exp)
  1036 
  1037 lemma continuous_on_exp [continuous_intros]:
  1038   fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
  1039   shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
  1040   unfolding continuous_on_def by (auto intro: tendsto_exp)
  1041 
  1042 
  1043 subsubsection {* Properties of the Exponential Function *}
  1044 
  1045 lemma powser_zero:
  1046   fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}"
  1047   shows "(\<Sum>n. f n * 0 ^ n) = f 0"
  1048 proof -
  1049   have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
  1050     by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
  1051   thus ?thesis unfolding One_nat_def by simp
  1052 qed
  1053 
  1054 lemma exp_zero [simp]: "exp 0 = 1"
  1055   unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
  1056 
  1057 lemma exp_series_add_commuting:
  1058   fixes x y :: "'a::{real_normed_algebra_1, banach}"
  1059   defines S_def: "S \<equiv> \<lambda>x n. x^n /\<^sub>R fact n"
  1060   assumes comm: "x * y = y * x"
  1061   shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n - i))"
  1062 proof (induct n)
  1063   case 0
  1064   show ?case
  1065     unfolding S_def by simp
  1066 next
  1067   case (Suc n)
  1068   have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)"
  1069     unfolding S_def by (simp del: mult_Suc)
  1070   hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)"
  1071     by simp
  1072   have S_comm: "\<And>n. S x n * y = y * S x n"
  1073     by (simp add: power_commuting_commutes comm S_def)
  1074 
  1075   have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
  1076     by (simp only: times_S)
  1077   also have "\<dots> = (x + y) * (\<Sum>i\<le>n. S x i * S y (n-i))"
  1078     by (simp only: Suc)
  1079   also have "\<dots> = x * (\<Sum>i\<le>n. S x i * S y (n-i))
  1080                 + y * (\<Sum>i\<le>n. S x i * S y (n-i))"
  1081     by (rule distrib_right)
  1082   also have "\<dots> = (\<Sum>i\<le>n. x * S x i * S y (n-i))
  1083                 + (\<Sum>i\<le>n. S x i * y * S y (n-i))"
  1084     by (simp add: setsum_right_distrib ac_simps S_comm)
  1085   also have "\<dots> = (\<Sum>i\<le>n. x * S x i * S y (n-i))
  1086                 + (\<Sum>i\<le>n. S x i * (y * S y (n-i)))"
  1087     by (simp add: ac_simps)
  1088   also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
  1089                 + (\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
  1090     by (simp add: times_S Suc_diff_le)
  1091   also have "(\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
  1092              (\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
  1093     by (subst setsum_atMost_Suc_shift) simp
  1094   also have "(\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
  1095              (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
  1096     by simp
  1097   also have "(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
  1098              (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
  1099              (\<Sum>i\<le>Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
  1100     by (simp only: setsum.distrib [symmetric] scaleR_left_distrib [symmetric]
  1101                    real_of_nat_add [symmetric]) simp
  1102   also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i\<le>Suc n. S x i * S y (Suc n-i))"
  1103     by (simp only: scaleR_right.setsum)
  1104   finally show
  1105     "S (x + y) (Suc n) = (\<Sum>i\<le>Suc n. S x i * S y (Suc n - i))"
  1106     by (simp del: setsum_cl_ivl_Suc)
  1107 qed
  1108 
  1109 lemma exp_add_commuting: "x * y = y * x \<Longrightarrow> exp (x + y) = exp x * exp y"
  1110   unfolding exp_def
  1111   by (simp only: Cauchy_product summable_norm_exp exp_series_add_commuting)
  1112 
  1113 lemma exp_add:
  1114   fixes x y::"'a::{real_normed_field,banach}"
  1115   shows "exp (x + y) = exp x * exp y"
  1116   by (rule exp_add_commuting) (simp add: ac_simps)
  1117 
  1118 lemma exp_double: "exp(2 * z) = exp z ^ 2"
  1119   by (simp add: exp_add_commuting mult_2 power2_eq_square)
  1120 
  1121 lemmas mult_exp_exp = exp_add [symmetric]
  1122 
  1123 lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
  1124   unfolding exp_def
  1125   apply (subst suminf_of_real)
  1126   apply (rule summable_exp_generic)
  1127   apply (simp add: scaleR_conv_of_real)
  1128   done
  1129 
  1130 lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
  1131 proof
  1132   have "exp x * exp (- x) = 1" by (simp add: exp_add_commuting[symmetric])
  1133   also assume "exp x = 0"
  1134   finally show "False" by simp
  1135 qed
  1136 
  1137 lemma exp_minus_inverse:
  1138   shows "exp x * exp (- x) = 1"
  1139   by (simp add: exp_add_commuting[symmetric])
  1140 
  1141 lemma exp_minus:
  1142   fixes x :: "'a::{real_normed_field, banach}"
  1143   shows "exp (- x) = inverse (exp x)"
  1144   by (intro inverse_unique [symmetric] exp_minus_inverse)
  1145 
  1146 lemma exp_diff:
  1147   fixes x :: "'a::{real_normed_field, banach}"
  1148   shows "exp (x - y) = exp x / exp y"
  1149   using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
  1150 
  1151 lemma exp_of_nat_mult:
  1152   fixes x :: "'a::{real_normed_field,banach}"
  1153   shows "exp(of_nat n * x) = exp(x) ^ n"
  1154     by (induct n) (auto simp add: distrib_left exp_add mult.commute)
  1155 
  1156 lemma exp_setsum: "finite I \<Longrightarrow> exp(setsum f I) = setprod (\<lambda>x. exp(f x)) I"
  1157   by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
  1158 
  1159 
  1160 subsubsection {* Properties of the Exponential Function on Reals *}
  1161 
  1162 text {* Comparisons of @{term "exp x"} with zero. *}
  1163 
  1164 text{*Proof: because every exponential can be seen as a square.*}
  1165 lemma exp_ge_zero [simp]: "0 \<le> exp (x::real)"
  1166 proof -
  1167   have "0 \<le> exp (x/2) * exp (x/2)" by simp
  1168   thus ?thesis by (simp add: exp_add [symmetric])
  1169 qed
  1170 
  1171 lemma exp_gt_zero [simp]: "0 < exp (x::real)"
  1172   by (simp add: order_less_le)
  1173 
  1174 lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0"
  1175   by (simp add: not_less)
  1176 
  1177 lemma not_exp_le_zero [simp]: "\<not> exp (x::real) \<le> 0"
  1178   by (simp add: not_le)
  1179 
  1180 lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
  1181   by simp
  1182 
  1183 (*FIXME: superseded by exp_of_nat_mult*)
  1184 lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
  1185   by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
  1186 
  1187 text {* Strict monotonicity of exponential. *}
  1188 
  1189 lemma exp_ge_add_one_self_aux:
  1190   assumes "0 \<le> (x::real)" shows "1+x \<le> exp(x)"
  1191 using order_le_imp_less_or_eq [OF assms]
  1192 proof
  1193   assume "0 < x"
  1194   have "1+x \<le> (\<Sum>n<2. inverse (fact n) * x^n)"
  1195     by (auto simp add: numeral_2_eq_2)
  1196   also have "... \<le> (\<Sum>n. inverse (fact n) * x^n)"
  1197     apply (rule setsum_le_suminf [OF summable_exp])
  1198     using `0 < x`
  1199     apply (auto  simp add:  zero_le_mult_iff)
  1200     done
  1201   finally show "1+x \<le> exp x"
  1202     by (simp add: exp_def)
  1203 next
  1204   assume "0 = x"
  1205   then show "1 + x \<le> exp x"
  1206     by auto
  1207 qed
  1208 
  1209 lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x"
  1210 proof -
  1211   assume x: "0 < x"
  1212   hence "1 < 1 + x" by simp
  1213   also from x have "1 + x \<le> exp x"
  1214     by (simp add: exp_ge_add_one_self_aux)
  1215   finally show ?thesis .
  1216 qed
  1217 
  1218 lemma exp_less_mono:
  1219   fixes x y :: real
  1220   assumes "x < y"
  1221   shows "exp x < exp y"
  1222 proof -
  1223   from `x < y` have "0 < y - x" by simp
  1224   hence "1 < exp (y - x)" by (rule exp_gt_one)
  1225   hence "1 < exp y / exp x" by (simp only: exp_diff)
  1226   thus "exp x < exp y" by simp
  1227 qed
  1228 
  1229 lemma exp_less_cancel: "exp (x::real) < exp y \<Longrightarrow> x < y"
  1230   unfolding linorder_not_le [symmetric]
  1231   by (auto simp add: order_le_less exp_less_mono)
  1232 
  1233 lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y"
  1234   by (auto intro: exp_less_mono exp_less_cancel)
  1235 
  1236 lemma exp_le_cancel_iff [iff]: "exp (x::real) \<le> exp y \<longleftrightarrow> x \<le> y"
  1237   by (auto simp add: linorder_not_less [symmetric])
  1238 
  1239 lemma exp_inj_iff [iff]: "exp (x::real) = exp y \<longleftrightarrow> x = y"
  1240   by (simp add: order_eq_iff)
  1241 
  1242 text {* Comparisons of @{term "exp x"} with one. *}
  1243 
  1244 lemma one_less_exp_iff [simp]: "1 < exp (x::real) \<longleftrightarrow> 0 < x"
  1245   using exp_less_cancel_iff [where x=0 and y=x] by simp
  1246 
  1247 lemma exp_less_one_iff [simp]: "exp (x::real) < 1 \<longleftrightarrow> x < 0"
  1248   using exp_less_cancel_iff [where x=x and y=0] by simp
  1249 
  1250 lemma one_le_exp_iff [simp]: "1 \<le> exp (x::real) \<longleftrightarrow> 0 \<le> x"
  1251   using exp_le_cancel_iff [where x=0 and y=x] by simp
  1252 
  1253 lemma exp_le_one_iff [simp]: "exp (x::real) \<le> 1 \<longleftrightarrow> x \<le> 0"
  1254   using exp_le_cancel_iff [where x=x and y=0] by simp
  1255 
  1256 lemma exp_eq_one_iff [simp]: "exp (x::real) = 1 \<longleftrightarrow> x = 0"
  1257   using exp_inj_iff [where x=x and y=0] by simp
  1258 
  1259 lemma lemma_exp_total: "1 \<le> y \<Longrightarrow> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y"
  1260 proof (rule IVT)
  1261   assume "1 \<le> y"
  1262   hence "0 \<le> y - 1" by simp
  1263   hence "1 + (y - 1) \<le> exp (y - 1)" by (rule exp_ge_add_one_self_aux)
  1264   thus "y \<le> exp (y - 1)" by simp
  1265 qed (simp_all add: le_diff_eq)
  1266 
  1267 lemma exp_total: "0 < (y::real) \<Longrightarrow> \<exists>x. exp x = y"
  1268 proof (rule linorder_le_cases [of 1 y])
  1269   assume "1 \<le> y"
  1270   thus "\<exists>x. exp x = y" by (fast dest: lemma_exp_total)
  1271 next
  1272   assume "0 < y" and "y \<le> 1"
  1273   hence "1 \<le> inverse y" by (simp add: one_le_inverse_iff)
  1274   then obtain x where "exp x = inverse y" by (fast dest: lemma_exp_total)
  1275   hence "exp (- x) = y" by (simp add: exp_minus)
  1276   thus "\<exists>x. exp x = y" ..
  1277 qed
  1278 
  1279 
  1280 subsection {* Natural Logarithm *}
  1281 
  1282 definition ln :: "real \<Rightarrow> real"
  1283   where "ln x = (THE u. exp u = x)"
  1284 
  1285 lemma ln_exp [simp]: "ln (exp x) = x"
  1286   by (simp add: ln_def)
  1287 
  1288 lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
  1289   by (auto dest: exp_total)
  1290 
  1291 lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
  1292   by (metis exp_gt_zero exp_ln)
  1293 
  1294 lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
  1295   by (erule subst, rule ln_exp)
  1296 
  1297 lemma ln_one [simp]: "ln 1 = 0"
  1298   by (rule ln_unique) simp
  1299 
  1300 lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
  1301   by (rule ln_unique) (simp add: exp_add)
  1302 
  1303 lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
  1304   by (rule ln_unique) (simp add: exp_minus)
  1305 
  1306 lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
  1307   by (rule ln_unique) (simp add: exp_diff)
  1308 
  1309 lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
  1310   by (rule ln_unique) (simp add: exp_real_of_nat_mult)
  1311 
  1312 lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
  1313   by (subst exp_less_cancel_iff [symmetric]) simp
  1314 
  1315 lemma ln_le_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
  1316   by (simp add: linorder_not_less [symmetric])
  1317 
  1318 lemma ln_inj_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
  1319   by (simp add: order_eq_iff)
  1320 
  1321 lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
  1322   apply (rule exp_le_cancel_iff [THEN iffD1])
  1323   apply (simp add: exp_ge_add_one_self_aux)
  1324   done
  1325 
  1326 lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
  1327   by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
  1328 
  1329 lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
  1330   using ln_le_cancel_iff [of 1 x] by simp
  1331 
  1332 lemma ln_ge_zero_imp_ge_one: "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
  1333   using ln_le_cancel_iff [of 1 x] by simp
  1334 
  1335 lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
  1336   using ln_le_cancel_iff [of 1 x] by simp
  1337 
  1338 lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
  1339   using ln_less_cancel_iff [of x 1] by simp
  1340 
  1341 lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
  1342   using ln_less_cancel_iff [of 1 x] by simp
  1343 
  1344 lemma ln_gt_zero_imp_gt_one: "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
  1345   using ln_less_cancel_iff [of 1 x] by simp
  1346 
  1347 lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
  1348   using ln_less_cancel_iff [of 1 x] by simp
  1349 
  1350 lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
  1351   using ln_inj_iff [of x 1] by simp
  1352 
  1353 lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
  1354   by simp
  1355 
  1356 lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
  1357   by (auto simp add: ln_def intro!: arg_cong[where f=The])
  1358 
  1359 lemma isCont_ln: assumes "x \<noteq> 0" shows "isCont ln x"
  1360 proof cases
  1361   assume "0 < x"
  1362   moreover then have "isCont ln (exp (ln x))"
  1363     by (intro isCont_inv_fun[where d="\<bar>x\<bar>" and f=exp]) auto
  1364   ultimately show ?thesis
  1365     by simp
  1366 next
  1367   assume "\<not> 0 < x" with `x \<noteq> 0` show "isCont ln x"
  1368     unfolding isCont_def
  1369     by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
  1370        (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
  1371                 intro!: exI[of _ "\<bar>x\<bar>"])
  1372 qed
  1373 
  1374 lemma tendsto_ln [tendsto_intros]:
  1375   "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
  1376   by (rule isCont_tendsto_compose [OF isCont_ln])
  1377 
  1378 lemma continuous_ln:
  1379   "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
  1380   unfolding continuous_def by (rule tendsto_ln)
  1381 
  1382 lemma isCont_ln' [continuous_intros]:
  1383   "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
  1384   unfolding continuous_at by (rule tendsto_ln)
  1385 
  1386 lemma continuous_within_ln [continuous_intros]:
  1387   "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
  1388   unfolding continuous_within by (rule tendsto_ln)
  1389 
  1390 lemma continuous_on_ln [continuous_intros]:
  1391   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
  1392   unfolding continuous_on_def by (auto intro: tendsto_ln)
  1393 
  1394 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
  1395   apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
  1396   apply (auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln)
  1397   done
  1398 
  1399 lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
  1400   by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
  1401 
  1402 declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
  1403 
  1404 lemma ln_series:
  1405   assumes "0 < x" and "x < 2"
  1406   shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))"
  1407   (is "ln x = suminf (?f (x - 1))")
  1408 proof -
  1409   let ?f' = "\<lambda>x n. (-1)^n * (x - 1)^n"
  1410 
  1411   have "ln x - suminf (?f (x - 1)) = ln 1 - suminf (?f (1 - 1))"
  1412   proof (rule DERIV_isconst3[where x=x])
  1413     fix x :: real
  1414     assume "x \<in> {0 <..< 2}"
  1415     hence "0 < x" and "x < 2" by auto
  1416     have "norm (1 - x) < 1"
  1417       using `0 < x` and `x < 2` by auto
  1418     have "1 / x = 1 / (1 - (1 - x))" by auto
  1419     also have "\<dots> = (\<Sum> n. (1 - x)^n)"
  1420       using geometric_sums[OF `norm (1 - x) < 1`] by (rule sums_unique)
  1421     also have "\<dots> = suminf (?f' x)"
  1422       unfolding power_mult_distrib[symmetric]
  1423       by (rule arg_cong[where f=suminf], rule arg_cong[where f="op ^"], auto)
  1424     finally have "DERIV ln x :> suminf (?f' x)"
  1425       using DERIV_ln[OF `0 < x`] unfolding divide_inverse by auto
  1426     moreover
  1427     have repos: "\<And> h x :: real. h - 1 + x = h + x - 1" by auto
  1428     have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :>
  1429       (\<Sum>n. (-1)^n * (1 / real (n + 1)) * real (Suc n) * (x - 1) ^ n)"
  1430     proof (rule DERIV_power_series')
  1431       show "x - 1 \<in> {- 1<..<1}" and "(0 :: real) < 1"
  1432         using `0 < x` `x < 2` by auto
  1433       fix x :: real
  1434       assume "x \<in> {- 1<..<1}"
  1435       hence "norm (-x) < 1" by auto
  1436       show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)"
  1437         unfolding One_nat_def
  1438         by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
  1439     qed
  1440     hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
  1441       unfolding One_nat_def by auto
  1442     hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)"
  1443       unfolding DERIV_def repos .
  1444     ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
  1445       by (rule DERIV_diff)
  1446     thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
  1447   qed (auto simp add: assms)
  1448   thus ?thesis by auto
  1449 qed
  1450 
  1451 lemma exp_first_two_terms:
  1452   fixes x :: "'a::{real_normed_field,banach}"
  1453   shows "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
  1454 proof -
  1455   have "exp x = suminf (\<lambda>n. inverse(fact n) * (x^n))"
  1456     by (simp add: exp_def scaleR_conv_of_real nonzero_of_real_inverse)
  1457   also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) +
  1458     (\<Sum> n::nat<2. inverse(fact n) * (x^n))" (is "_ = _ + ?a")
  1459     by (rule suminf_split_initial_segment)
  1460   also have "?a = 1 + x"
  1461     by (simp add: numeral_2_eq_2)
  1462   finally show ?thesis
  1463     by simp
  1464 qed
  1465 
  1466 lemma exp_bound: "0 <= (x::real) \<Longrightarrow> x <= 1 \<Longrightarrow> exp x <= 1 + x + x\<^sup>2"
  1467 proof -
  1468   assume a: "0 <= x"
  1469   assume b: "x <= 1"
  1470   {
  1471     fix n :: nat
  1472     have "(2::nat) * 2 ^ n \<le> fact (n + 2)"
  1473       by (induct n) simp_all
  1474     hence "real ((2::nat) * 2 ^ n) \<le> real_of_nat (fact (n + 2))"
  1475       by (simp only: real_of_nat_le_iff)
  1476     hence "((2::real) * 2 ^ n) \<le> fact (n + 2)"
  1477       unfolding of_nat_fact real_of_nat_def
  1478       by (simp add: of_nat_mult of_nat_power)
  1479     hence "inverse (fact (n + 2)) \<le> inverse ((2::real) * 2 ^ n)"
  1480       by (rule le_imp_inverse_le) simp
  1481     hence "inverse (fact (n + 2)) \<le> 1/(2::real) * (1/2)^n"
  1482       by (simp add: power_inverse)
  1483     hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
  1484       by (rule mult_mono)
  1485         (rule mult_mono, simp_all add: power_le_one a b)
  1486     hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
  1487       unfolding power_add by (simp add: ac_simps del: fact.simps) }
  1488   note aux1 = this
  1489   have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
  1490     by (intro sums_mult geometric_sums, simp)
  1491   hence aux2: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2"
  1492     by simp
  1493   have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <= x\<^sup>2"
  1494   proof -
  1495     have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <=
  1496         suminf (\<lambda>n. (x\<^sup>2/2) * ((1/2)^n))"
  1497       apply (rule suminf_le)
  1498       apply (rule allI, rule aux1)
  1499       apply (rule summable_exp [THEN summable_ignore_initial_segment])
  1500       by (rule sums_summable, rule aux2)
  1501     also have "... = x\<^sup>2"
  1502       by (rule sums_unique [THEN sym], rule aux2)
  1503     finally show ?thesis .
  1504   qed
  1505   thus ?thesis unfolding exp_first_two_terms by auto
  1506 qed
  1507 
  1508 corollary exp_half_le2: "exp(1/2) \<le> (2::real)"
  1509   using exp_bound [of "1/2"]
  1510   by (simp add: field_simps)
  1511 
  1512 lemma exp_bound_half: "norm(z) \<le> 1/2 \<Longrightarrow> norm(exp z) \<le> 2"
  1513   by (blast intro: order_trans intro!: exp_half_le2 norm_exp)
  1514 
  1515 lemma exp_bound_lemma:
  1516   assumes "norm(z) \<le> 1/2" shows "norm(exp z) \<le> 1 + 2 * norm(z)"
  1517 proof -
  1518   have n: "(norm z)\<^sup>2 \<le> norm z * 1"
  1519     unfolding power2_eq_square
  1520     apply (rule mult_left_mono)
  1521     using assms
  1522     apply (auto simp: )
  1523     done
  1524   show ?thesis
  1525     apply (rule order_trans [OF norm_exp])
  1526     apply (rule order_trans [OF exp_bound])
  1527     using assms n
  1528     apply (auto simp: )
  1529     done
  1530 qed
  1531 
  1532 lemma real_exp_bound_lemma:
  1533   fixes x :: real
  1534   shows "0 \<le> x \<Longrightarrow> x \<le> 1/2 \<Longrightarrow> exp(x) \<le> 1 + 2 * x"
  1535 using exp_bound_lemma [of x]
  1536 by simp
  1537 
  1538 lemma ln_one_minus_pos_upper_bound: "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
  1539 proof -
  1540   assume a: "0 <= (x::real)" and b: "x < 1"
  1541   have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)"
  1542     by (simp add: algebra_simps power2_eq_square power3_eq_cube)
  1543   also have "... <= 1"
  1544     by (auto simp add: a)
  1545   finally have "(1 - x) * (1 + x + x\<^sup>2) <= 1" .
  1546   moreover have c: "0 < 1 + x + x\<^sup>2"
  1547     by (simp add: add_pos_nonneg a)
  1548   ultimately have "1 - x <= 1 / (1 + x + x\<^sup>2)"
  1549     by (elim mult_imp_le_div_pos)
  1550   also have "... <= 1 / exp x"
  1551     by (metis a abs_one b exp_bound exp_gt_zero frac_le less_eq_real_def real_sqrt_abs
  1552               real_sqrt_pow2_iff real_sqrt_power)
  1553   also have "... = exp (-x)"
  1554     by (auto simp add: exp_minus divide_inverse)
  1555   finally have "1 - x <= exp (- x)" .
  1556   also have "1 - x = exp (ln (1 - x))"
  1557     by (metis b diff_0 exp_ln_iff less_iff_diff_less_0 minus_diff_eq)
  1558   finally have "exp (ln (1 - x)) <= exp (- x)" .
  1559   thus ?thesis by (auto simp only: exp_le_cancel_iff)
  1560 qed
  1561 
  1562 lemma exp_ge_add_one_self [simp]: "1 + (x::real) <= exp x"
  1563   apply (case_tac "0 <= x")
  1564   apply (erule exp_ge_add_one_self_aux)
  1565   apply (case_tac "x <= -1")
  1566   apply (subgoal_tac "1 + x <= 0")
  1567   apply (erule order_trans)
  1568   apply simp
  1569   apply simp
  1570   apply (subgoal_tac "1 + x = exp(ln (1 + x))")
  1571   apply (erule ssubst)
  1572   apply (subst exp_le_cancel_iff)
  1573   apply (subgoal_tac "ln (1 - (- x)) <= - (- x)")
  1574   apply simp
  1575   apply (rule ln_one_minus_pos_upper_bound)
  1576   apply auto
  1577 done
  1578 
  1579 lemma ln_one_plus_pos_lower_bound: "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> x - x\<^sup>2 <= ln (1 + x)"
  1580 proof -
  1581   assume a: "0 <= x" and b: "x <= 1"
  1582   have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)"
  1583     by (rule exp_diff)
  1584   also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)"
  1585     by (metis a b divide_right_mono exp_bound exp_ge_zero)
  1586   also have "... <= (1 + x + x\<^sup>2) / (1 + x\<^sup>2)"
  1587     by (simp add: a divide_left_mono add_pos_nonneg)
  1588   also from a have "... <= 1 + x"
  1589     by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
  1590   finally have "exp (x - x\<^sup>2) <= 1 + x" .
  1591   also have "... = exp (ln (1 + x))"
  1592   proof -
  1593     from a have "0 < 1 + x" by auto
  1594     thus ?thesis
  1595       by (auto simp only: exp_ln_iff [THEN sym])
  1596   qed
  1597   finally have "exp (x - x\<^sup>2) <= exp (ln (1 + x))" .
  1598   thus ?thesis
  1599     by (metis exp_le_cancel_iff)
  1600 qed
  1601 
  1602 lemma ln_one_minus_pos_lower_bound:
  1603   "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
  1604 proof -
  1605   assume a: "0 <= x" and b: "x <= (1 / 2)"
  1606   from b have c: "x < 1" by auto
  1607   then have "ln (1 - x) = - ln (1 + x / (1 - x))"
  1608     apply (subst ln_inverse [symmetric])
  1609     apply (simp add: field_simps)
  1610     apply (rule arg_cong [where f=ln])
  1611     apply (simp add: field_simps)
  1612     done
  1613   also have "- (x / (1 - x)) <= ..."
  1614   proof -
  1615     have "ln (1 + x / (1 - x)) <= x / (1 - x)"
  1616       using a c by (intro ln_add_one_self_le_self) auto
  1617     thus ?thesis
  1618       by auto
  1619   qed
  1620   also have "- (x / (1 - x)) = -x / (1 - x)"
  1621     by auto
  1622   finally have d: "- x / (1 - x) <= ln (1 - x)" .
  1623   have "0 < 1 - x" using a b by simp
  1624   hence e: "-x - 2 * x\<^sup>2 <= - x / (1 - x)"
  1625     using mult_right_le_one_le[of "x*x" "2*x"] a b
  1626     by (simp add: field_simps power2_eq_square)
  1627   from e d show "- x - 2 * x\<^sup>2 <= ln (1 - x)"
  1628     by (rule order_trans)
  1629 qed
  1630 
  1631 lemma ln_add_one_self_le_self2: "-1 < x \<Longrightarrow> ln(1 + x) <= x"
  1632   apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp)
  1633   apply (subst ln_le_cancel_iff)
  1634   apply auto
  1635   done
  1636 
  1637 lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
  1638   "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
  1639 proof -
  1640   assume x: "0 <= x"
  1641   assume x1: "x <= 1"
  1642   from x have "ln (1 + x) <= x"
  1643     by (rule ln_add_one_self_le_self)
  1644   then have "ln (1 + x) - x <= 0"
  1645     by simp
  1646   then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
  1647     by (rule abs_of_nonpos)
  1648   also have "... = x - ln (1 + x)"
  1649     by simp
  1650   also have "... <= x\<^sup>2"
  1651   proof -
  1652     from x x1 have "x - x\<^sup>2 <= ln (1 + x)"
  1653       by (intro ln_one_plus_pos_lower_bound)
  1654     thus ?thesis
  1655       by simp
  1656   qed
  1657   finally show ?thesis .
  1658 qed
  1659 
  1660 lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
  1661   "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  1662 proof -
  1663   assume a: "-(1 / 2) <= x"
  1664   assume b: "x <= 0"
  1665   have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
  1666     apply (subst abs_of_nonpos)
  1667     apply simp
  1668     apply (rule ln_add_one_self_le_self2)
  1669     using a apply auto
  1670     done
  1671   also have "... <= 2 * x\<^sup>2"
  1672     apply (subgoal_tac "- (-x) - 2 * (-x)\<^sup>2 <= ln (1 - (-x))")
  1673     apply (simp add: algebra_simps)
  1674     apply (rule ln_one_minus_pos_lower_bound)
  1675     using a b apply auto
  1676     done
  1677   finally show ?thesis .
  1678 qed
  1679 
  1680 lemma abs_ln_one_plus_x_minus_x_bound:
  1681     "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  1682   apply (case_tac "0 <= x")
  1683   apply (rule order_trans)
  1684   apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
  1685   apply auto
  1686   apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos)
  1687   apply auto
  1688   done
  1689 
  1690 lemma ln_x_over_x_mono: "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
  1691 proof -
  1692   assume x: "exp 1 <= x" "x <= y"
  1693   moreover have "0 < exp (1::real)" by simp
  1694   ultimately have a: "0 < x" and b: "0 < y"
  1695     by (fast intro: less_le_trans order_trans)+
  1696   have "x * ln y - x * ln x = x * (ln y - ln x)"
  1697     by (simp add: algebra_simps)
  1698   also have "... = x * ln(y / x)"
  1699     by (simp only: ln_div a b)
  1700   also have "y / x = (x + (y - x)) / x"
  1701     by simp
  1702   also have "... = 1 + (y - x) / x"
  1703     using x a by (simp add: field_simps)
  1704   also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
  1705     using x a
  1706     by (intro mult_left_mono ln_add_one_self_le_self) simp_all
  1707   also have "... = y - x" using a by simp
  1708   also have "... = (y - x) * ln (exp 1)" by simp
  1709   also have "... <= (y - x) * ln x"
  1710     apply (rule mult_left_mono)
  1711     apply (subst ln_le_cancel_iff)
  1712     apply fact
  1713     apply (rule a)
  1714     apply (rule x)
  1715     using x apply simp
  1716     done
  1717   also have "... = y * ln x - x * ln x"
  1718     by (rule left_diff_distrib)
  1719   finally have "x * ln y <= y * ln x"
  1720     by arith
  1721   then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps)
  1722   also have "... = y * (ln x / x)" by simp
  1723   finally show ?thesis using b by (simp add: field_simps)
  1724 qed
  1725 
  1726 lemma ln_le_minus_one: "0 < x \<Longrightarrow> ln x \<le> x - 1"
  1727   using exp_ge_add_one_self[of "ln x"] by simp
  1728 
  1729 lemma ln_eq_minus_one:
  1730   assumes "0 < x" "ln x = x - 1"
  1731   shows "x = 1"
  1732 proof -
  1733   let ?l = "\<lambda>y. ln y - y + 1"
  1734   have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
  1735     by (auto intro!: derivative_eq_intros)
  1736 
  1737   show ?thesis
  1738   proof (cases rule: linorder_cases)
  1739     assume "x < 1"
  1740     from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast
  1741     from `x < a` have "?l x < ?l a"
  1742     proof (rule DERIV_pos_imp_increasing, safe)
  1743       fix y
  1744       assume "x \<le> y" "y \<le> a"
  1745       with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y"
  1746         by (auto simp: field_simps)
  1747       with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
  1748         by auto
  1749     qed
  1750     also have "\<dots> \<le> 0"
  1751       using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps)
  1752     finally show "x = 1" using assms by auto
  1753   next
  1754     assume "1 < x"
  1755     from dense[OF this] obtain a where "1 < a" "a < x" by blast
  1756     from `a < x` have "?l x < ?l a"
  1757     proof (rule DERIV_neg_imp_decreasing, safe)
  1758       fix y
  1759       assume "a \<le> y" "y \<le> x"
  1760       with `1 < a` have "1 / y - 1 < 0" "0 < y"
  1761         by (auto simp: field_simps)
  1762       with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0"
  1763         by blast
  1764     qed
  1765     also have "\<dots> \<le> 0"
  1766       using ln_le_minus_one `1 < a` by (auto simp: field_simps)
  1767     finally show "x = 1" using assms by auto
  1768   next
  1769     assume "x = 1"
  1770     then show ?thesis by simp
  1771   qed
  1772 qed
  1773 
  1774 lemma exp_at_bot: "(exp ---> (0::real)) at_bot"
  1775   unfolding tendsto_Zfun_iff
  1776 proof (rule ZfunI, simp add: eventually_at_bot_dense)
  1777   fix r :: real assume "0 < r"
  1778   {
  1779     fix x
  1780     assume "x < ln r"
  1781     then have "exp x < exp (ln r)"
  1782       by simp
  1783     with `0 < r` have "exp x < r"
  1784       by simp
  1785   }
  1786   then show "\<exists>k. \<forall>n<k. exp n < r" by auto
  1787 qed
  1788 
  1789 lemma exp_at_top: "LIM x at_top. exp x :: real :> at_top"
  1790   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"])
  1791      (auto intro: eventually_gt_at_top)
  1792 
  1793 lemma lim_exp_minus_1:
  1794   fixes x :: "'a::{real_normed_field,banach}"
  1795   shows "((\<lambda>z::'a. (exp(z) - 1) / z) ---> 1) (at 0)"
  1796 proof -
  1797   have "((\<lambda>z::'a. exp(z) - 1) has_field_derivative 1) (at 0)"
  1798     by (intro derivative_eq_intros | simp)+
  1799   then show ?thesis
  1800     by (simp add: Deriv.DERIV_iff2)
  1801 qed
  1802 
  1803 lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
  1804   by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  1805      (auto simp: eventually_at_filter)
  1806 
  1807 lemma ln_at_top: "LIM x at_top. ln x :> at_top"
  1808   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  1809      (auto intro: eventually_gt_at_top)
  1810 
  1811 lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
  1812 proof (induct k)
  1813   case 0
  1814   show "((\<lambda>x. x ^ 0 / exp x) ---> (0::real)) at_top"
  1815     by (simp add: inverse_eq_divide[symmetric])
  1816        (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono
  1817               at_top_le_at_infinity order_refl)
  1818 next
  1819   case (Suc k)
  1820   show ?case
  1821   proof (rule lhospital_at_top_at_top)
  1822     show "eventually (\<lambda>x. DERIV (\<lambda>x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top"
  1823       by eventually_elim (intro derivative_eq_intros, auto)
  1824     show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top"
  1825       by eventually_elim auto
  1826     show "eventually (\<lambda>x. exp x \<noteq> 0) at_top"
  1827       by auto
  1828     from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
  1829     show "((\<lambda>x. real (Suc k) * x ^ k / exp x) ---> 0) at_top"
  1830       by simp
  1831   qed (rule exp_at_top)
  1832 qed
  1833 
  1834 
  1835 definition powr :: "[real,real] => real"  (infixr "powr" 80)
  1836   -- {*exponentation with real exponent*}
  1837   where "x powr a = exp(a * ln x)"
  1838 
  1839 definition log :: "[real,real] => real"
  1840   -- {*logarithm of @{term x} to base @{term a}*}
  1841   where "log a x = ln x / ln a"
  1842 
  1843 
  1844 lemma tendsto_log [tendsto_intros]:
  1845   "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a; a \<noteq> 1; 0 < b\<rbrakk> \<Longrightarrow> ((\<lambda>x. log (f x) (g x)) ---> log a b) F"
  1846   unfolding log_def by (intro tendsto_intros) auto
  1847 
  1848 lemma continuous_log:
  1849   assumes "continuous F f"
  1850     and "continuous F g"
  1851     and "0 < f (Lim F (\<lambda>x. x))"
  1852     and "f (Lim F (\<lambda>x. x)) \<noteq> 1"
  1853     and "0 < g (Lim F (\<lambda>x. x))"
  1854   shows "continuous F (\<lambda>x. log (f x) (g x))"
  1855   using assms unfolding continuous_def by (rule tendsto_log)
  1856 
  1857 lemma continuous_at_within_log[continuous_intros]:
  1858   assumes "continuous (at a within s) f"
  1859     and "continuous (at a within s) g"
  1860     and "0 < f a"
  1861     and "f a \<noteq> 1"
  1862     and "0 < g a"
  1863   shows "continuous (at a within s) (\<lambda>x. log (f x) (g x))"
  1864   using assms unfolding continuous_within by (rule tendsto_log)
  1865 
  1866 lemma isCont_log[continuous_intros, simp]:
  1867   assumes "isCont f a" "isCont g a" "0 < f a" "f a \<noteq> 1" "0 < g a"
  1868   shows "isCont (\<lambda>x. log (f x) (g x)) a"
  1869   using assms unfolding continuous_at by (rule tendsto_log)
  1870 
  1871 lemma continuous_on_log[continuous_intros]:
  1872   assumes "continuous_on s f" "continuous_on s g"
  1873     and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
  1874   shows "continuous_on s (\<lambda>x. log (f x) (g x))"
  1875   using assms unfolding continuous_on_def by (fast intro: tendsto_log)
  1876 
  1877 lemma powr_one_eq_one [simp]: "1 powr a = 1"
  1878   by (simp add: powr_def)
  1879 
  1880 lemma powr_zero_eq_one [simp]: "x powr 0 = 1"
  1881   by (simp add: powr_def)
  1882 
  1883 lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)"
  1884   by (simp add: powr_def)
  1885 declare powr_one_gt_zero_iff [THEN iffD2, simp]
  1886 
  1887 lemma powr_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
  1888   by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
  1889 
  1890 lemma powr_gt_zero [simp]: "0 < x powr a"
  1891   by (simp add: powr_def)
  1892 
  1893 lemma powr_ge_pzero [simp]: "0 <= x powr y"
  1894   by (rule order_less_imp_le, rule powr_gt_zero)
  1895 
  1896 lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
  1897   by (simp add: powr_def)
  1898 
  1899 lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
  1900   apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
  1901   apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
  1902   done
  1903 
  1904 lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
  1905   apply (simp add: powr_def)
  1906   apply (subst exp_diff [THEN sym])
  1907   apply (simp add: left_diff_distrib)
  1908   done
  1909 
  1910 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
  1911   by (simp add: powr_def exp_add [symmetric] distrib_right)
  1912 
  1913 lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
  1914   using assms by (auto simp: powr_add)
  1915 
  1916 lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
  1917   by (simp add: powr_def)
  1918 
  1919 lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
  1920   by (simp add: powr_powr mult.commute)
  1921 
  1922 lemma powr_minus: "x powr (-a) = inverse (x powr a)"
  1923   by (simp add: powr_def exp_minus [symmetric])
  1924 
  1925 lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
  1926   by (simp add: divide_inverse powr_minus)
  1927 
  1928 lemma divide_powr_uminus: "a / b powr c = a * b powr (- c)"
  1929   by (simp add: powr_minus_divide)
  1930 
  1931 lemma powr_less_mono: "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
  1932   by (simp add: powr_def)
  1933 
  1934 lemma powr_less_cancel: "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
  1935   by (simp add: powr_def)
  1936 
  1937 lemma powr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
  1938   by (blast intro: powr_less_cancel powr_less_mono)
  1939 
  1940 lemma powr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
  1941   by (simp add: linorder_not_less [symmetric])
  1942 
  1943 lemma log_ln: "ln x = log (exp(1)) x"
  1944   by (simp add: log_def)
  1945 
  1946 lemma DERIV_log:
  1947   assumes "x > 0"
  1948   shows "DERIV (\<lambda>y. log b y) x :> 1 / (ln b * x)"
  1949 proof -
  1950   def lb \<equiv> "1 / ln b"
  1951   moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x"
  1952     using `x > 0` by (auto intro!: derivative_eq_intros)
  1953   ultimately show ?thesis
  1954     by (simp add: log_def)
  1955 qed
  1956 
  1957 lemmas DERIV_log[THEN DERIV_chain2, derivative_intros]
  1958 
  1959 lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
  1960   by (simp add: powr_def log_def)
  1961 
  1962 lemma log_powr_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log a (a powr y) = y"
  1963   by (simp add: log_def powr_def)
  1964 
  1965 lemma log_mult:
  1966   "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow>
  1967     log a (x * y) = log a x + log a y"
  1968   by (simp add: log_def ln_mult divide_inverse distrib_right)
  1969 
  1970 lemma log_eq_div_ln_mult_log:
  1971   "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow>
  1972     log a x = (ln b/ln a) * log b x"
  1973   by (simp add: log_def divide_inverse)
  1974 
  1975 text{*Base 10 logarithms*}
  1976 lemma log_base_10_eq1: "0 < x \<Longrightarrow> log 10 x = (ln (exp 1) / ln 10) * ln x"
  1977   by (simp add: log_def)
  1978 
  1979 lemma log_base_10_eq2: "0 < x \<Longrightarrow> log 10 x = (log 10 (exp 1)) * ln x"
  1980   by (simp add: log_def)
  1981 
  1982 lemma log_one [simp]: "log a 1 = 0"
  1983   by (simp add: log_def)
  1984 
  1985 lemma log_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> log a a = 1"
  1986   by (simp add: log_def)
  1987 
  1988 lemma log_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log a (inverse x) = - log a x"
  1989   apply (rule_tac a1 = "log a x" in add_left_cancel [THEN iffD1])
  1990   apply (simp add: log_mult [symmetric])
  1991   done
  1992 
  1993 lemma log_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a (x/y) = log a x - log a y"
  1994   by (simp add: log_mult divide_inverse log_inverse)
  1995 
  1996 lemma log_add_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x + y = log b (x * b powr y)"
  1997   and add_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> y + log b x = log b (b powr y * x)"
  1998   and log_minus_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x - y = log b (x * b powr -y)"
  1999   and minus_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> y - log b x = log b (b powr y / x)"
  2000   by (simp_all add: log_mult log_divide)
  2001 
  2002 lemma log_less_cancel_iff [simp]:
  2003   "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a x < log a y \<longleftrightarrow> x < y"
  2004   apply safe
  2005   apply (rule_tac [2] powr_less_cancel)
  2006   apply (drule_tac a = "log a x" in powr_less_mono, auto)
  2007   done
  2008 
  2009 lemma log_inj:
  2010   assumes "1 < b"
  2011   shows "inj_on (log b) {0 <..}"
  2012 proof (rule inj_onI, simp)
  2013   fix x y
  2014   assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
  2015   show "x = y"
  2016   proof (cases rule: linorder_cases)
  2017     assume "x = y"
  2018     then show ?thesis by simp
  2019   next
  2020     assume "x < y" hence "log b x < log b y"
  2021       using log_less_cancel_iff[OF `1 < b`] pos by simp
  2022     then show ?thesis using * by simp
  2023   next
  2024     assume "y < x" hence "log b y < log b x"
  2025       using log_less_cancel_iff[OF `1 < b`] pos by simp
  2026     then show ?thesis using * by simp
  2027   qed
  2028 qed
  2029 
  2030 lemma log_le_cancel_iff [simp]:
  2031   "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (log a x \<le> log a y) = (x \<le> y)"
  2032   by (simp add: linorder_not_less [symmetric])
  2033 
  2034 lemma zero_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < log a x \<longleftrightarrow> 1 < x"
  2035   using log_less_cancel_iff[of a 1 x] by simp
  2036 
  2037 lemma zero_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 \<le> log a x \<longleftrightarrow> 1 \<le> x"
  2038   using log_le_cancel_iff[of a 1 x] by simp
  2039 
  2040 lemma log_less_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 0 \<longleftrightarrow> x < 1"
  2041   using log_less_cancel_iff[of a x 1] by simp
  2042 
  2043 lemma log_le_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 0 \<longleftrightarrow> x \<le> 1"
  2044   using log_le_cancel_iff[of a x 1] by simp
  2045 
  2046 lemma one_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 < log a x \<longleftrightarrow> a < x"
  2047   using log_less_cancel_iff[of a a x] by simp
  2048 
  2049 lemma one_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> log a x \<longleftrightarrow> a \<le> x"
  2050   using log_le_cancel_iff[of a a x] by simp
  2051 
  2052 lemma log_less_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 1 \<longleftrightarrow> x < a"
  2053   using log_less_cancel_iff[of a x a] by simp
  2054 
  2055 lemma log_le_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 1 \<longleftrightarrow> x \<le> a"
  2056   using log_le_cancel_iff[of a x a] by simp
  2057 
  2058 lemma le_log_iff:
  2059   assumes "1 < b" "x > 0"
  2060   shows "y \<le> log b x \<longleftrightarrow> b powr y \<le> x"
  2061   by (metis assms(1) assms(2) dual_order.strict_trans powr_le_cancel_iff powr_log_cancel
  2062     powr_one_eq_one powr_one_gt_zero_iff)
  2063 
  2064 lemma less_log_iff:
  2065   assumes "1 < b" "x > 0"
  2066   shows "y < log b x \<longleftrightarrow> b powr y < x"
  2067   by (metis assms(1) assms(2) dual_order.strict_trans less_irrefl powr_less_cancel_iff
  2068     powr_log_cancel zero_less_one)
  2069 
  2070 lemma
  2071   assumes "1 < b" "x > 0"
  2072   shows log_less_iff: "log b x < y \<longleftrightarrow> x < b powr y"
  2073     and log_le_iff: "log b x \<le> y \<longleftrightarrow> x \<le> b powr y"
  2074   using le_log_iff[OF assms, of y] less_log_iff[OF assms, of y]
  2075   by auto
  2076 
  2077 lemmas powr_le_iff = le_log_iff[symmetric]
  2078   and powr_less_iff = le_log_iff[symmetric]
  2079   and less_powr_iff = log_less_iff[symmetric]
  2080   and le_powr_iff = log_le_iff[symmetric]
  2081 
  2082 lemma
  2083   floor_log_eq_powr_iff: "x > 0 \<Longrightarrow> b > 1 \<Longrightarrow> \<lfloor>log b x\<rfloor> = k \<longleftrightarrow> b powr k \<le> x \<and> x < b powr (k + 1)"
  2084   by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
  2085 
  2086 lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
  2087   apply (induct n)
  2088   apply simp
  2089   apply (subgoal_tac "real(Suc n) = real n + 1")
  2090   apply (erule ssubst)
  2091   apply (subst powr_add, simp, simp)
  2092   done
  2093 
  2094 lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
  2095   unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
  2096 
  2097 lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
  2098 by(simp add: powr_realpow_numeral)
  2099 
  2100 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
  2101   apply (case_tac "x = 0", simp, simp)
  2102   apply (rule powr_realpow [THEN sym], simp)
  2103   done
  2104 
  2105 lemma powr_int:
  2106   assumes "x > 0"
  2107   shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))"
  2108 proof (cases "i < 0")
  2109   case True
  2110   have r: "x powr i = 1 / x powr (-i)" by (simp add: powr_minus field_simps)
  2111   show ?thesis using `i < 0` `x > 0` by (simp add: r field_simps powr_realpow[symmetric])
  2112 next
  2113   case False
  2114   then show ?thesis by (simp add: assms powr_realpow[symmetric])
  2115 qed
  2116 
  2117 lemma compute_powr[code]:
  2118   fixes i::real
  2119   shows "b powr i =
  2120     (if b \<le> 0 then Code.abort (STR ''op powr with nonpositive base'') (\<lambda>_. b powr i)
  2121     else if floor i = i then (if 0 \<le> i then b ^ nat(floor i) else 1 / b ^ nat(floor (- i)))
  2122     else Code.abort (STR ''op powr with non-integer exponent'') (\<lambda>_. b powr i))"
  2123   by (auto simp: powr_int)
  2124 
  2125 lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
  2126   using powr_realpow [of x 1] by simp
  2127 
  2128 lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
  2129   by (fact powr_realpow_numeral)
  2130 
  2131 lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
  2132   using powr_int [of x "- 1"] by simp
  2133 
  2134 lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
  2135   using powr_int [of x "- numeral n"] by simp
  2136 
  2137 lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
  2138   by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
  2139 
  2140 lemma ln_powr: "ln (x powr y) = y * ln x"
  2141   by (simp add: powr_def)
  2142 
  2143 lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) =  ln b / n"
  2144 by(simp add: root_powr_inverse ln_powr)
  2145 
  2146 lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
  2147   by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult.commute)
  2148 
  2149 lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) =  log b a / n"
  2150 by(simp add: log_def ln_root)
  2151 
  2152 lemma log_powr: "log b (x powr y) = y * log b x"
  2153   by (simp add: log_def ln_powr)
  2154 
  2155 lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
  2156   by (simp add: log_powr powr_realpow [symmetric])
  2157 
  2158 lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
  2159   by (simp add: log_def)
  2160 
  2161 lemma log_base_pow: "0 < a \<Longrightarrow> log (a ^ n) x = log a x / n"
  2162   by (simp add: log_def ln_realpow)
  2163 
  2164 lemma log_base_powr: "log (a powr b) x = log a x / b"
  2165   by (simp add: log_def ln_powr)
  2166 
  2167 lemma log_base_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> log (root n b) x = n * (log b x)"
  2168 by(simp add: log_def ln_root)
  2169 
  2170 lemma ln_bound: "1 <= x ==> ln x <= x"
  2171   apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
  2172   apply simp
  2173   apply (rule ln_add_one_self_le_self, simp)
  2174   done
  2175 
  2176 lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b"
  2177   apply (cases "x = 1", simp)
  2178   apply (cases "a = b", simp)
  2179   apply (rule order_less_imp_le)
  2180   apply (rule powr_less_mono, auto)
  2181   done
  2182 
  2183 lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a"
  2184   apply (subst powr_zero_eq_one [THEN sym])
  2185   apply (rule powr_mono, assumption+)
  2186   done
  2187 
  2188 lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
  2189   apply (unfold powr_def)
  2190   apply (rule exp_less_mono)
  2191   apply (rule mult_strict_left_mono)
  2192   apply (subst ln_less_cancel_iff, assumption)
  2193   apply (rule order_less_trans)
  2194   prefer 2
  2195   apply assumption+
  2196   done
  2197 
  2198 lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
  2199   apply (unfold powr_def)
  2200   apply (rule exp_less_mono)
  2201   apply (rule mult_strict_left_mono_neg)
  2202   apply (subst ln_less_cancel_iff)
  2203   apply assumption
  2204   apply (rule order_less_trans)
  2205   prefer 2
  2206   apply assumption+
  2207   done
  2208 
  2209 lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
  2210   apply (case_tac "a = 0", simp)
  2211   apply (case_tac "x = y", simp)
  2212   apply (metis less_eq_real_def powr_less_mono2)
  2213   done
  2214 
  2215 lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
  2216   unfolding powr_def exp_inj_iff by simp
  2217 
  2218 lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
  2219   by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute
  2220             order.strict_trans2 powr_gt_zero zero_less_one)
  2221 
  2222 lemma ln_powr_bound2:
  2223   assumes "1 < x" and "0 < a"
  2224   shows "(ln x) powr a <= (a powr a) * x"
  2225 proof -
  2226   from assms have "ln x <= (x powr (1 / a)) / (1 / a)"
  2227     by (metis less_eq_real_def ln_powr_bound zero_less_divide_1_iff)
  2228   also have "... = a * (x powr (1 / a))"
  2229     by simp
  2230   finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
  2231     by (metis assms less_imp_le ln_gt_zero powr_mono2)
  2232   also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
  2233     by (metis assms(2) powr_mult powr_gt_zero)
  2234   also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
  2235     by (rule powr_powr)
  2236   also have "... = x" using assms
  2237     by auto
  2238   finally show ?thesis .
  2239 qed
  2240 
  2241 lemma tendsto_powr [tendsto_intros]:
  2242   "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
  2243   unfolding powr_def by (intro tendsto_intros)
  2244 
  2245 lemma continuous_powr:
  2246   assumes "continuous F f"
  2247     and "continuous F g"
  2248     and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
  2249   shows "continuous F (\<lambda>x. (f x) powr (g x))"
  2250   using assms unfolding continuous_def by (rule tendsto_powr)
  2251 
  2252 lemma continuous_at_within_powr[continuous_intros]:
  2253   assumes "continuous (at a within s) f"
  2254     and "continuous (at a within s) g"
  2255     and "f a \<noteq> 0"
  2256   shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
  2257   using assms unfolding continuous_within by (rule tendsto_powr)
  2258 
  2259 lemma isCont_powr[continuous_intros, simp]:
  2260   assumes "isCont f a" "isCont g a" "f a \<noteq> 0"
  2261   shows "isCont (\<lambda>x. (f x) powr g x) a"
  2262   using assms unfolding continuous_at by (rule tendsto_powr)
  2263 
  2264 lemma continuous_on_powr[continuous_intros]:
  2265   assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0"
  2266   shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
  2267   using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
  2268 
  2269 (* FIXME: generalize by replacing d by with g x and g ---> d? *)
  2270 lemma tendsto_zero_powrI:
  2271   assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
  2272     and "0 < d"
  2273   shows "((\<lambda>x. f x powr d) ---> 0) F"
  2274 proof (rule tendstoI)
  2275   fix e :: real assume "0 < e"
  2276   def Z \<equiv> "e powr (1 / d)"
  2277   with `0 < e` have "0 < Z" by simp
  2278   with assms have "eventually (\<lambda>x. 0 < f x \<and> dist (f x) 0 < Z) F"
  2279     by (intro eventually_conj tendstoD)
  2280   moreover
  2281   from assms have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> x powr d < Z powr d"
  2282     by (intro powr_less_mono2) (auto simp: dist_real_def)
  2283   with assms `0 < e` have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> dist (x powr d) 0 < e"
  2284     unfolding dist_real_def Z_def by (auto simp: powr_powr)
  2285   ultimately
  2286   show "eventually (\<lambda>x. dist (f x powr d) 0 < e) F" by (rule eventually_elim1)
  2287 qed
  2288 
  2289 lemma tendsto_neg_powr:
  2290   assumes "s < 0"
  2291     and "LIM x F. f x :> at_top"
  2292   shows "((\<lambda>x. f x powr s) ---> 0) F"
  2293 proof (rule tendstoI)
  2294   fix e :: real assume "0 < e"
  2295   def Z \<equiv> "e powr (1 / s)"
  2296   from assms have "eventually (\<lambda>x. Z < f x) F"
  2297     by (simp add: filterlim_at_top_dense)
  2298   moreover
  2299   from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
  2300     by (auto simp: Z_def intro!: powr_less_mono2_neg)
  2301   with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
  2302     by (simp add: powr_powr Z_def dist_real_def)
  2303   ultimately
  2304   show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
  2305 qed
  2306 
  2307 (* it is funny that this isn't in the library! It could go in Transcendental *)
  2308 lemma tendsto_exp_limit_at_right:
  2309   fixes x :: real
  2310   shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)"
  2311 proof cases
  2312   assume "x \<noteq> 0"
  2313 
  2314   have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
  2315     by (auto intro!: derivative_eq_intros)
  2316   then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
  2317     by (auto simp add: has_field_derivative_def field_has_derivative_at)
  2318   then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)"
  2319     by (rule tendsto_intros)
  2320   then show ?thesis
  2321   proof (rule filterlim_mono_eventually)
  2322     show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
  2323       unfolding eventually_at_right[OF zero_less_one]
  2324       using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
  2325   qed (simp_all add: at_eq_sup_left_right)
  2326 qed simp
  2327 
  2328 lemma tendsto_exp_limit_at_top:
  2329   fixes x :: real
  2330   shows "((\<lambda>y. (1 + x / y) powr y) ---> exp x) at_top"
  2331   apply (subst filterlim_at_top_to_right)
  2332   apply (simp add: inverse_eq_divide)
  2333   apply (rule tendsto_exp_limit_at_right)
  2334   done
  2335 
  2336 lemma tendsto_exp_limit_sequentially:
  2337   fixes x :: real
  2338   shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x"
  2339 proof (rule filterlim_mono_eventually)
  2340   from reals_Archimedean2 [of "abs x"] obtain n :: nat where *: "real n > abs x" ..
  2341   hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
  2342     apply (intro eventually_sequentiallyI [of n])
  2343     apply (case_tac "x \<ge> 0")
  2344     apply (rule add_pos_nonneg, auto intro: divide_nonneg_nonneg)
  2345     apply (subgoal_tac "x / real xa > -1")
  2346     apply (auto simp add: field_simps)
  2347     done
  2348   then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
  2349     by (rule eventually_elim1) (erule powr_realpow)
  2350   show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x"
  2351     by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially])
  2352 qed auto
  2353 
  2354 subsection {* Sine and Cosine *}
  2355 
  2356 definition sin_coeff :: "nat \<Rightarrow> real" where
  2357   "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / (fact n))"
  2358 
  2359 definition cos_coeff :: "nat \<Rightarrow> real" where
  2360   "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / (fact n) else 0)"
  2361 
  2362 definition sin :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
  2363   where "sin = (\<lambda>x. \<Sum>n. sin_coeff n *\<^sub>R x^n)"
  2364 
  2365 definition cos :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
  2366   where "cos = (\<lambda>x. \<Sum>n. cos_coeff n *\<^sub>R x^n)"
  2367 
  2368 lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
  2369   unfolding sin_coeff_def by simp
  2370 
  2371 lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
  2372   unfolding cos_coeff_def by simp
  2373 
  2374 lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
  2375   unfolding cos_coeff_def sin_coeff_def
  2376   by (simp del: mult_Suc)
  2377 
  2378 lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
  2379   unfolding cos_coeff_def sin_coeff_def
  2380   by (simp del: mult_Suc) (auto elim: oddE)
  2381 
  2382 lemma summable_norm_sin:
  2383   fixes x :: "'a::{real_normed_algebra_1,banach}"
  2384   shows "summable (\<lambda>n. norm (sin_coeff n *\<^sub>R x^n))"
  2385   unfolding sin_coeff_def
  2386   apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
  2387   apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  2388   done
  2389 
  2390 lemma summable_norm_cos:
  2391   fixes x :: "'a::{real_normed_algebra_1,banach}"
  2392   shows "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x^n))"
  2393   unfolding cos_coeff_def
  2394   apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
  2395   apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  2396   done
  2397 
  2398 lemma sin_converges: "(\<lambda>n. sin_coeff n *\<^sub>R x^n) sums sin(x)"
  2399 unfolding sin_def
  2400   by (metis (full_types) summable_norm_cancel summable_norm_sin summable_sums)
  2401 
  2402 lemma cos_converges: "(\<lambda>n. cos_coeff n *\<^sub>R x^n) sums cos(x)"
  2403 unfolding cos_def
  2404   by (metis (full_types) summable_norm_cancel summable_norm_cos summable_sums)
  2405 
  2406 lemma sin_of_real:
  2407   fixes x::real
  2408   shows "sin (of_real x) = of_real (sin x)"
  2409 proof -
  2410   have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R  x^n)) = (\<lambda>n. sin_coeff n *\<^sub>R  (of_real x)^n)"
  2411   proof
  2412     fix n
  2413     show "of_real (sin_coeff n *\<^sub>R  x^n) = sin_coeff n *\<^sub>R of_real x^n"
  2414       by (simp add: scaleR_conv_of_real)
  2415   qed
  2416   also have "... sums (sin (of_real x))"
  2417     by (rule sin_converges)
  2418   finally have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R x^n)) sums (sin (of_real x))" .
  2419   then show ?thesis
  2420     using sums_unique2 sums_of_real [OF sin_converges]
  2421     by blast
  2422 qed
  2423 
  2424 lemma cos_of_real:
  2425   fixes x::real
  2426   shows "cos (of_real x) = of_real (cos x)"
  2427 proof -
  2428   have "(\<lambda>n. of_real (cos_coeff n *\<^sub>R  x^n)) = (\<lambda>n. cos_coeff n *\<^sub>R  (of_real x)^n)"
  2429   proof
  2430     fix n
  2431     show "of_real (cos_coeff n *\<^sub>R  x^n) = cos_coeff n *\<^sub>R of_real x^n"
  2432       by (simp add: scaleR_conv_of_real)
  2433   qed
  2434   also have "... sums (cos (of_real x))"
  2435     by (rule cos_converges)
  2436   finally have "(\<lambda>n. of_real (cos_coeff n *\<^sub>R x^n)) sums (cos (of_real x))" .
  2437   then show ?thesis
  2438     using sums_unique2 sums_of_real [OF cos_converges]
  2439     by blast
  2440 qed
  2441 
  2442 lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff"
  2443   by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
  2444 
  2445 lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
  2446   by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
  2447 
  2448 text{*Now at last we can get the derivatives of exp, sin and cos*}
  2449 
  2450 lemma DERIV_sin [simp]:
  2451   fixes x :: "'a::{real_normed_field,banach}"
  2452   shows "DERIV sin x :> cos(x)"
  2453   unfolding sin_def cos_def scaleR_conv_of_real
  2454   apply (rule DERIV_cong)
  2455   apply (rule termdiffs [where K="of_real (norm x) + 1 :: 'a"])
  2456   apply (simp_all add: norm_less_p1 diffs_of_real diffs_sin_coeff diffs_cos_coeff
  2457               summable_minus_iff scaleR_conv_of_real [symmetric]
  2458               summable_norm_sin [THEN summable_norm_cancel]
  2459               summable_norm_cos [THEN summable_norm_cancel])
  2460   done
  2461 
  2462 declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
  2463 
  2464 lemma DERIV_cos [simp]:
  2465   fixes x :: "'a::{real_normed_field,banach}"
  2466   shows "DERIV cos x :> -sin(x)"
  2467   unfolding sin_def cos_def scaleR_conv_of_real
  2468   apply (rule DERIV_cong)
  2469   apply (rule termdiffs [where K="of_real (norm x) + 1 :: 'a"])
  2470   apply (simp_all add: norm_less_p1 diffs_of_real diffs_minus suminf_minus
  2471               diffs_sin_coeff diffs_cos_coeff
  2472               summable_minus_iff scaleR_conv_of_real [symmetric]
  2473               summable_norm_sin [THEN summable_norm_cancel]
  2474               summable_norm_cos [THEN summable_norm_cancel])
  2475   done
  2476 
  2477 declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
  2478 
  2479 lemma isCont_sin:
  2480   fixes x :: "'a::{real_normed_field,banach}"
  2481   shows "isCont sin x"
  2482   by (rule DERIV_sin [THEN DERIV_isCont])
  2483 
  2484 lemma isCont_cos:
  2485   fixes x :: "'a::{real_normed_field,banach}"
  2486   shows "isCont cos x"
  2487   by (rule DERIV_cos [THEN DERIV_isCont])
  2488 
  2489 lemma isCont_sin' [simp]:
  2490   fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
  2491   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
  2492   by (rule isCont_o2 [OF _ isCont_sin])
  2493 
  2494 (*FIXME A CONTEXT FOR F WOULD BE BETTER*)
  2495 
  2496 lemma isCont_cos' [simp]:
  2497   fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
  2498   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
  2499   by (rule isCont_o2 [OF _ isCont_cos])
  2500 
  2501 lemma tendsto_sin [tendsto_intros]:
  2502   fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
  2503   shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) ---> sin a) F"
  2504   by (rule isCont_tendsto_compose [OF isCont_sin])
  2505 
  2506 lemma tendsto_cos [tendsto_intros]:
  2507   fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
  2508   shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
  2509   by (rule isCont_tendsto_compose [OF isCont_cos])
  2510 
  2511 lemma continuous_sin [continuous_intros]:
  2512   fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
  2513   shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
  2514   unfolding continuous_def by (rule tendsto_sin)
  2515 
  2516 lemma continuous_on_sin [continuous_intros]:
  2517   fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
  2518   shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
  2519   unfolding continuous_on_def by (auto intro: tendsto_sin)
  2520 
  2521 lemma continuous_within_sin:
  2522   fixes z :: "'a::{real_normed_field,banach}"
  2523   shows "continuous (at z within s) sin"
  2524   by (simp add: continuous_within tendsto_sin)
  2525 
  2526 lemma continuous_cos [continuous_intros]:
  2527   fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
  2528   shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
  2529   unfolding continuous_def by (rule tendsto_cos)
  2530 
  2531 lemma continuous_on_cos [continuous_intros]:
  2532   fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
  2533   shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
  2534   unfolding continuous_on_def by (auto intro: tendsto_cos)
  2535 
  2536 lemma continuous_within_cos:
  2537   fixes z :: "'a::{real_normed_field,banach}"
  2538   shows "continuous (at z within s) cos"
  2539   by (simp add: continuous_within tendsto_cos)
  2540 
  2541 subsection {* Properties of Sine and Cosine *}
  2542 
  2543 lemma sin_zero [simp]: "sin 0 = 0"
  2544   unfolding sin_def sin_coeff_def by (simp add: scaleR_conv_of_real powser_zero)
  2545 
  2546 lemma cos_zero [simp]: "cos 0 = 1"
  2547   unfolding cos_def cos_coeff_def by (simp add: scaleR_conv_of_real powser_zero)
  2548 
  2549 lemma DERIV_fun_sin:
  2550      "DERIV g x :> m \<Longrightarrow> DERIV (\<lambda>x. sin(g x)) x :> cos(g x) * m"
  2551   by (auto intro!: derivative_intros)
  2552 
  2553 lemma DERIV_fun_cos:
  2554      "DERIV g x :> m \<Longrightarrow> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
  2555   by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  2556 
  2557 subsection {*Deriving the Addition Formulas*}
  2558 
  2559 text{*The the product of two cosine series*}
  2560 lemma cos_x_cos_y:
  2561   fixes x :: "'a::{real_normed_field,banach}"
  2562   shows "(\<lambda>p. \<Sum>n\<le>p.
  2563           if even p \<and> even n
  2564           then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
  2565          sums (cos x * cos y)"
  2566 proof -
  2567   { fix n p::nat
  2568     assume "n\<le>p"
  2569     then have *: "even n \<Longrightarrow> even p \<Longrightarrow> (-1) ^ (n div 2) * (-1) ^ ((p - n) div 2) = (-1 :: real) ^ (p div 2)"
  2570       by (metis div_add power_add le_add_diff_inverse odd_add)
  2571     have "(cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
  2572           (if even p \<and> even n then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
  2573     using `n\<le>p`
  2574       by (auto simp: * algebra_simps cos_coeff_def binomial_fact real_of_nat_def)
  2575   }
  2576   then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> even n
  2577                   then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
  2578              (\<lambda>p. \<Sum>n\<le>p. (cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
  2579     by simp
  2580   also have "... = (\<lambda>p. \<Sum>n\<le>p. (cos_coeff n *\<^sub>R x^n) * (cos_coeff (p - n) *\<^sub>R y^(p-n)))"
  2581     by (simp add: algebra_simps)
  2582   also have "... sums (cos x * cos y)"
  2583     using summable_norm_cos
  2584     by (auto simp: cos_def scaleR_conv_of_real intro!: Cauchy_product_sums)
  2585   finally show ?thesis .
  2586 qed
  2587 
  2588 text{*The product of two sine series*}
  2589 lemma sin_x_sin_y:
  2590   fixes x :: "'a::{real_normed_field,banach}"
  2591   shows "(\<lambda>p. \<Sum>n\<le>p.
  2592           if even p \<and> odd n
  2593                then - ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
  2594          sums (sin x * sin y)"
  2595 proof -
  2596   { fix n p::nat
  2597     assume "n\<le>p"
  2598     { assume np: "odd n" "even p"
  2599         with `n\<le>p` have "n - Suc 0 + (p - Suc n) = p - Suc (Suc 0)" "Suc (Suc 0) \<le> p"
  2600         by arith+
  2601       moreover have "(p - Suc (Suc 0)) div 2 = p div 2 - Suc 0"
  2602         by simp
  2603       ultimately have *: "(-1) ^ ((n - Suc 0) div 2) * (-1) ^ ((p - Suc n) div 2) = - ((-1 :: real) ^ (p div 2))"
  2604         using np `n\<le>p`
  2605         apply (simp add: power_add [symmetric] div_add [symmetric] del: div_add)
  2606         apply (metis (no_types) One_nat_def Suc_1 le_div_geq minus_minus mult.left_neutral mult_minus_left power.simps(2) zero_less_Suc)
  2607         done
  2608     } then
  2609     have "(sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
  2610           (if even p \<and> odd n
  2611           then -((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
  2612     using `n\<le>p`
  2613       by (auto simp:  algebra_simps sin_coeff_def binomial_fact real_of_nat_def)
  2614   }
  2615   then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> odd n
  2616                then - ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
  2617              (\<lambda>p. \<Sum>n\<le>p. (sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
  2618     by simp
  2619   also have "... = (\<lambda>p. \<Sum>n\<le>p. (sin_coeff n *\<^sub>R x^n) * (sin_coeff (p - n) *\<^sub>R y^(p-n)))"
  2620     by (simp add: algebra_simps)
  2621   also have "... sums (sin x * sin y)"
  2622     using summable_norm_sin
  2623     by (auto simp: sin_def scaleR_conv_of_real intro!: Cauchy_product_sums)
  2624   finally show ?thesis .
  2625 qed
  2626 
  2627 lemma sums_cos_x_plus_y:
  2628   fixes x :: "'a::{real_normed_field,banach}"
  2629   shows
  2630   "(\<lambda>p. \<Sum>n\<le>p. if even p
  2631                then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
  2632                else 0)
  2633         sums cos (x + y)"
  2634 proof -
  2635   { fix p::nat
  2636     have "(\<Sum>n\<le>p. if even p
  2637                   then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
  2638                   else 0) =
  2639           (if even p
  2640                   then \<Sum>n\<le>p. ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
  2641                   else 0)"
  2642       by simp
  2643     also have "... = (if even p
  2644                   then of_real ((-1) ^ (p div 2) / (fact p)) * (\<Sum>n\<le>p. (p choose n) *\<^sub>R (x^n) * y^(p-n))
  2645                   else 0)"
  2646       by (auto simp: setsum_right_distrib field_simps scaleR_conv_of_real nonzero_of_real_divide)
  2647     also have "... = cos_coeff p *\<^sub>R ((x + y) ^ p)"
  2648       by (simp add: cos_coeff_def binomial_ring [of x y]  scaleR_conv_of_real real_of_nat_def atLeast0AtMost)
  2649     finally have "(\<Sum>n\<le>p. if even p
  2650                   then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
  2651                   else 0) = cos_coeff p *\<^sub>R ((x + y) ^ p)" .
  2652   }
  2653   then have "(\<lambda>p. \<Sum>n\<le>p.
  2654                if even p
  2655                then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
  2656                else 0)
  2657         = (\<lambda>p. cos_coeff p *\<^sub>R ((x+y)^p))"
  2658         by simp
  2659    also have "... sums cos (x + y)"
  2660     by (rule cos_converges)
  2661    finally show ?thesis .
  2662 qed
  2663 
  2664 theorem cos_add:
  2665   fixes x :: "'a::{real_normed_field,banach}"
  2666   shows "cos (x + y) = cos x * cos y - sin x * sin y"
  2667 proof -
  2668   { fix n p::nat
  2669     assume "n\<le>p"
  2670     then have "(if even p \<and> even n
  2671                then ((- 1) ^ (p div 2) * int (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) -
  2672           (if even p \<and> odd n
  2673                then - ((- 1) ^ (p div 2) * int (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
  2674           = (if even p
  2675                then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
  2676       by simp
  2677   }
  2678   then have "(\<lambda>p. \<Sum>n\<le>p. (if even p
  2679                then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
  2680         sums (cos x * cos y - sin x * sin y)"
  2681     using sums_diff [OF cos_x_cos_y [of x y] sin_x_sin_y [of x y]]
  2682     by (simp add: setsum_subtractf [symmetric])
  2683   then show ?thesis
  2684     by (blast intro: sums_cos_x_plus_y sums_unique2)
  2685 qed
  2686 
  2687 lemma sin_minus_converges: "(\<lambda>n. - (sin_coeff n *\<^sub>R (-x)^n)) sums sin(x)"
  2688 proof -
  2689   have [simp]: "\<And>n. - (sin_coeff n *\<^sub>R (-x)^n) = (sin_coeff n *\<^sub>R x^n)"
  2690     by (auto simp: sin_coeff_def elim!: oddE)
  2691   show ?thesis
  2692     by (simp add: sin_def summable_norm_sin [THEN summable_norm_cancel, THEN summable_sums])
  2693 qed
  2694 
  2695 lemma sin_minus [simp]:
  2696   fixes x :: "'a::{real_normed_algebra_1,banach}"
  2697   shows "sin (-x) = -sin(x)"
  2698 using sin_minus_converges [of x]
  2699 by (auto simp: sin_def summable_norm_sin [THEN summable_norm_cancel] suminf_minus sums_iff equation_minus_iff)
  2700 
  2701 lemma cos_minus_converges: "(\<lambda>n. (cos_coeff n *\<^sub>R (-x)^n)) sums cos(x)"
  2702 proof -
  2703   have [simp]: "\<And>n. (cos_coeff n *\<^sub>R (-x)^n) = (cos_coeff n *\<^sub>R x^n)"
  2704     by (auto simp: Transcendental.cos_coeff_def elim!: evenE)
  2705   show ?thesis
  2706     by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel, THEN summable_sums])
  2707 qed
  2708 
  2709 lemma cos_minus [simp]:
  2710   fixes x :: "'a::{real_normed_algebra_1,banach}"
  2711   shows "cos (-x) = cos(x)"
  2712 using cos_minus_converges [of x]
  2713 by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel]
  2714               suminf_minus sums_iff equation_minus_iff)
  2715 
  2716 lemma sin_cos_squared_add [simp]:
  2717   fixes x :: "'a::{real_normed_field,banach}"
  2718   shows "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
  2719 using cos_add [of x "-x"]
  2720 by (simp add: power2_eq_square algebra_simps)
  2721 
  2722 lemma sin_cos_squared_add2 [simp]:
  2723   fixes x :: "'a::{real_normed_field,banach}"
  2724   shows "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
  2725   by (subst add.commute, rule sin_cos_squared_add)
  2726 
  2727 lemma sin_cos_squared_add3 [simp]:
  2728   fixes x :: "'a::{real_normed_field,banach}"
  2729   shows "cos x * cos x + sin x * sin x = 1"
  2730   using sin_cos_squared_add2 [unfolded power2_eq_square] .
  2731 
  2732 lemma sin_squared_eq:
  2733   fixes x :: "'a::{real_normed_field,banach}"
  2734   shows "(sin x)\<^sup>2 = 1 - (cos x)\<^sup>2"
  2735   unfolding eq_diff_eq by (rule sin_cos_squared_add)
  2736 
  2737 lemma cos_squared_eq:
  2738   fixes x :: "'a::{real_normed_field,banach}"
  2739   shows "(cos x)\<^sup>2 = 1 - (sin x)\<^sup>2"
  2740   unfolding eq_diff_eq by (rule sin_cos_squared_add2)
  2741 
  2742 lemma abs_sin_le_one [simp]:
  2743   fixes x :: real
  2744   shows "\<bar>sin x\<bar> \<le> 1"
  2745   by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
  2746 
  2747 lemma sin_ge_minus_one [simp]:
  2748   fixes x :: real
  2749   shows "-1 \<le> sin x"
  2750   using abs_sin_le_one [of x] unfolding abs_le_iff by simp
  2751 
  2752 lemma sin_le_one [simp]:
  2753   fixes x :: real
  2754   shows "sin x \<le> 1"
  2755   using abs_sin_le_one [of x] unfolding abs_le_iff by simp
  2756 
  2757 lemma abs_cos_le_one [simp]:
  2758   fixes x :: real
  2759   shows "\<bar>cos x\<bar> \<le> 1"
  2760   by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
  2761 
  2762 lemma cos_ge_minus_one [simp]:
  2763   fixes x :: real
  2764   shows "-1 \<le> cos x"
  2765   using abs_cos_le_one [of x] unfolding abs_le_iff by simp
  2766 
  2767 lemma cos_le_one [simp]:
  2768   fixes x :: real
  2769   shows "cos x \<le> 1"
  2770   using abs_cos_le_one [of x] unfolding abs_le_iff by simp
  2771 
  2772 lemma cos_diff:
  2773   fixes x :: "'a::{real_normed_field,banach}"
  2774   shows "cos (x - y) = cos x * cos y + sin x * sin y"
  2775   using cos_add [of x "- y"] by simp
  2776 
  2777 lemma cos_double:
  2778   fixes x :: "'a::{real_normed_field,banach}"
  2779   shows "cos(2*x) = (cos x)\<^sup>2 - (sin x)\<^sup>2"
  2780   using cos_add [where x=x and y=x]
  2781   by (simp add: power2_eq_square)
  2782 
  2783 lemma DERIV_fun_pow: "DERIV g x :> m ==>
  2784       DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
  2785   by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  2786 
  2787 lemma DERIV_fun_exp:
  2788      "DERIV g x :> m ==> DERIV (\<lambda>x. exp(g x)) x :> exp(g x) * m"
  2789   by (auto intro!: derivative_intros)
  2790 
  2791 subsection {* The Constant Pi *}
  2792 
  2793 definition pi :: real
  2794   where "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
  2795 
  2796 text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
  2797    hence define pi.*}
  2798 
  2799 lemma sin_paired:
  2800   fixes x :: real
  2801   shows "(\<lambda>n. (- 1) ^ n / (fact (2 * n + 1)) * x ^ (2 * n + 1)) sums  sin x"
  2802 proof -
  2803   have "(\<lambda>n. \<Sum>k = n*2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
  2804     apply (rule sums_group)
  2805     using sin_converges [of x, unfolded scaleR_conv_of_real]
  2806     by auto
  2807   thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: ac_simps)
  2808 qed
  2809 
  2810 lemma sin_gt_zero_02:
  2811   fixes x :: real
  2812   assumes "0 < x" and "x < 2"
  2813   shows "0 < sin x"
  2814 proof -
  2815   let ?f = "\<lambda>n::nat. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / (fact (2*k+1)) * x^(2*k+1)"
  2816   have pos: "\<forall>n. 0 < ?f n"
  2817   proof
  2818     fix n :: nat
  2819     let ?k2 = "real (Suc (Suc (4 * n)))"
  2820     let ?k3 = "real (Suc (Suc (Suc (4 * n))))"
  2821     have "x * x < ?k2 * ?k3"
  2822       using assms by (intro mult_strict_mono', simp_all)
  2823     hence "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)"
  2824       by (intro mult_strict_right_mono zero_less_power `0 < x`)
  2825     thus "0 < ?f n"
  2826       by (simp add: real_of_nat_def divide_simps mult_ac del: mult_Suc)
  2827 qed
  2828   have sums: "?f sums sin x"
  2829     by (rule sin_paired [THEN sums_group], simp)
  2830   show "0 < sin x"
  2831     unfolding sums_unique [OF sums]
  2832     using sums_summable [OF sums] pos
  2833     by (rule suminf_pos)
  2834 qed
  2835 
  2836 lemma cos_double_less_one:
  2837   fixes x :: real
  2838   shows "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
  2839   using sin_gt_zero_02 [where x = x] by (auto simp: cos_squared_eq cos_double)
  2840 
  2841 lemma cos_paired:
  2842   fixes x :: real
  2843   shows "(\<lambda>n. (- 1) ^ n / (fact (2 * n)) * x ^ (2 * n)) sums cos x"
  2844 proof -
  2845   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
  2846     apply (rule sums_group)
  2847     using cos_converges [of x, unfolded scaleR_conv_of_real]
  2848     by auto
  2849   thus ?thesis unfolding cos_coeff_def by (simp add: ac_simps)
  2850 qed
  2851 
  2852 lemmas realpow_num_eq_if = power_eq_if
  2853 
  2854 lemma sumr_pos_lt_pair:  (*FIXME A MESS, BUT THE REAL MESS IS THE NEXT THEOREM*)
  2855   fixes f :: "nat \<Rightarrow> real"
  2856   shows "\<lbrakk>summable f;
  2857         \<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
  2858       \<Longrightarrow> setsum f {..<k} < suminf f"
  2859 unfolding One_nat_def
  2860 apply (subst suminf_split_initial_segment [where k=k], assumption, simp)
  2861 apply (drule_tac k=k in summable_ignore_initial_segment)
  2862 apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
  2863 apply simp
  2864 apply (frule sums_unique)
  2865 apply (drule sums_summable, simp)
  2866 apply (erule suminf_pos)
  2867 apply (simp add: ac_simps)
  2868 done
  2869 
  2870 lemma cos_two_less_zero [simp]:
  2871   "cos 2 < (0::real)"
  2872 proof -
  2873   note fact.simps(2) [simp del]
  2874   from sums_minus [OF cos_paired]
  2875   have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / fact (2 * n))) sums - cos (2::real)"
  2876     by simp
  2877   then have **: "summable (\<lambda>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
  2878     by (rule sums_summable)
  2879   have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
  2880     by (simp add: fact_num_eq_if realpow_num_eq_if)
  2881   moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n  * 2 ^ (2 * n) / (fact (2 * n))))
  2882     < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
  2883   proof -
  2884     { fix d
  2885       have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  2886             < (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
  2887               fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  2888         unfolding real_of_nat_mult
  2889         by (rule mult_strict_mono) (simp_all add: fact_less_mono)
  2890       then have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  2891         <  (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
  2892         by (simp only: fact.simps(2) [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"] real_of_nat_def of_nat_mult of_nat_fact)
  2893       then have "(4::real) * inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))
  2894         < inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))"
  2895         by (simp add: inverse_eq_divide less_divide_eq)
  2896     }
  2897     note *** = this
  2898     have [simp]: "\<And>x y::real. 0 < x - y \<longleftrightarrow> y < x" by arith
  2899     from ** show ?thesis by (rule sumr_pos_lt_pair)
  2900       (simp add: divide_inverse mult.assoc [symmetric] ***)
  2901   qed
  2902   ultimately have "0 < (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
  2903     by (rule order_less_trans)
  2904   moreover from * have "- cos 2 = (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
  2905     by (rule sums_unique)
  2906   ultimately have "(0::real) < - cos 2" by simp
  2907   then show ?thesis by simp
  2908 qed
  2909 
  2910 lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
  2911 lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]
  2912 
  2913 lemma cos_is_zero: "EX! x::real. 0 \<le> x & x \<le> 2 \<and> cos x = 0"
  2914 proof (rule ex_ex1I)
  2915   show "\<exists>x::real. 0 \<le> x & x \<le> 2 & cos x = 0"
  2916     by (rule IVT2, simp_all)
  2917 next
  2918   fix x::real and y::real
  2919   assume x: "0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
  2920   assume y: "0 \<le> y \<and> y \<le> 2 \<and> cos y = 0"
  2921   have [simp]: "\<forall>x::real. cos differentiable (at x)"
  2922     unfolding real_differentiable_def by (auto intro: DERIV_cos)
  2923   from x y show "x = y"
  2924     apply (cut_tac less_linear [of x y], auto)
  2925     apply (drule_tac f = cos in Rolle)
  2926     apply (drule_tac [5] f = cos in Rolle)
  2927     apply (auto dest!: DERIV_cos [THEN DERIV_unique])
  2928     apply (metis order_less_le_trans less_le sin_gt_zero_02)
  2929     apply (metis order_less_le_trans less_le sin_gt_zero_02)
  2930     done
  2931 qed
  2932 
  2933 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
  2934   by (simp add: pi_def)
  2935 
  2936 lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
  2937   by (simp add: pi_half cos_is_zero [THEN theI'])
  2938 
  2939 lemma cos_of_real_pi_half [simp]:
  2940   fixes x :: "'a :: {real_field,banach,real_normed_algebra_1}"
  2941   shows "cos ((of_real pi / 2) :: 'a) = 0"
  2942 by (metis cos_pi_half cos_of_real eq_numeral_simps(4) nonzero_of_real_divide of_real_0 of_real_numeral)
  2943 
  2944 lemma pi_half_gt_zero [simp]: "0 < pi / 2"
  2945   apply (rule order_le_neq_trans)
  2946   apply (simp add: pi_half cos_is_zero [THEN theI'])
  2947   apply (metis cos_pi_half cos_zero zero_neq_one)
  2948   done
  2949 
  2950 lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
  2951 lemmas pi_half_ge_zero [simp] = pi_half_gt_zero [THEN order_less_imp_le]
  2952 
  2953 lemma pi_half_less_two [simp]: "pi / 2 < 2"
  2954   apply (rule order_le_neq_trans)
  2955   apply (simp add: pi_half cos_is_zero [THEN theI'])
  2956   apply (metis cos_pi_half cos_two_neq_zero)
  2957   done
  2958 
  2959 lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
  2960 lemmas pi_half_le_two [simp] =  pi_half_less_two [THEN order_less_imp_le]
  2961 
  2962 lemma pi_gt_zero [simp]: "0 < pi"
  2963   using pi_half_gt_zero by simp
  2964 
  2965 lemma pi_ge_zero [simp]: "0 \<le> pi"
  2966   by (rule pi_gt_zero [THEN order_less_imp_le])
  2967 
  2968 lemma pi_neq_zero [simp]: "pi \<noteq> 0"
  2969   by (rule pi_gt_zero [THEN less_imp_neq, symmetric])
  2970 
  2971 lemma pi_not_less_zero [simp]: "\<not> pi < 0"
  2972   by (simp add: linorder_not_less)
  2973 
  2974 lemma minus_pi_half_less_zero: "-(pi/2) < 0"
  2975   by simp
  2976 
  2977 lemma m2pi_less_pi: "- (2*pi) < pi"
  2978   by simp
  2979 
  2980 lemma sin_pi_half [simp]: "sin(pi/2) = 1"
  2981   using sin_cos_squared_add2 [where x = "pi/2"]
  2982   using sin_gt_zero_02 [OF pi_half_gt_zero pi_half_less_two]
  2983   by (simp add: power2_eq_1_iff)
  2984 
  2985 lemma sin_of_real_pi_half [simp]:
  2986   fixes x :: "'a :: {real_field,banach,real_normed_algebra_1}"
  2987   shows "sin ((of_real pi / 2) :: 'a) = 1"
  2988   using sin_pi_half
  2989 by (metis sin_pi_half eq_numeral_simps(4) nonzero_of_real_divide of_real_1 of_real_numeral sin_of_real)
  2990 
  2991 lemma sin_cos_eq:
  2992   fixes x :: "'a::{real_normed_field,banach}"
  2993   shows "sin x = cos (of_real pi / 2 - x)"
  2994   by (simp add: cos_diff)
  2995 
  2996 lemma minus_sin_cos_eq:
  2997   fixes x :: "'a::{real_normed_field,banach}"
  2998   shows "-sin x = cos (x + of_real pi / 2)"
  2999   by (simp add: cos_add nonzero_of_real_divide)
  3000 
  3001 lemma cos_sin_eq:
  3002   fixes x :: "'a::{real_normed_field,banach}"
  3003   shows "cos x = sin (of_real pi / 2 - x)"
  3004   using sin_cos_eq [of "of_real pi / 2 - x"]
  3005   by simp
  3006 
  3007 lemma sin_add:
  3008   fixes x :: "'a::{real_normed_field,banach}"
  3009   shows "sin (x + y) = sin x * cos y + cos x * sin y"
  3010   using cos_add [of "of_real pi / 2 - x" "-y"]
  3011   by (simp add: cos_sin_eq) (simp add: sin_cos_eq)
  3012 
  3013 lemma sin_diff:
  3014   fixes x :: "'a::{real_normed_field,banach}"
  3015   shows "sin (x - y) = sin x * cos y - cos x * sin y"
  3016   using sin_add [of x "- y"] by simp
  3017 
  3018 lemma sin_double:
  3019   fixes x :: "'a::{real_normed_field,banach}"
  3020   shows "sin(2 * x) = 2 * sin x * cos x"
  3021   using sin_add [where x=x and y=x] by simp
  3022 
  3023 
  3024 lemma cos_of_real_pi [simp]: "cos (of_real pi) = -1"
  3025   using cos_add [where x = "pi/2" and y = "pi/2"]
  3026   by (simp add: cos_of_real)
  3027 
  3028 lemma sin_of_real_pi [simp]: "sin (of_real pi) = 0"
  3029   using sin_add [where x = "pi/2" and y = "pi/2"]
  3030   by (simp add: sin_of_real)
  3031 
  3032 lemma cos_pi [simp]: "cos pi = -1"
  3033   using cos_add [where x = "pi/2" and y = "pi/2"] by simp
  3034 
  3035 lemma sin_pi [simp]: "sin pi = 0"
  3036   using sin_add [where x = "pi/2" and y = "pi/2"] by simp
  3037 
  3038 lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
  3039   by (simp add: sin_add)
  3040 
  3041 lemma sin_periodic_pi2 [simp]: "sin (pi + x) = - sin x"
  3042   by (simp add: sin_add)
  3043 
  3044 lemma cos_periodic_pi [simp]: "cos (x + pi) = - cos x"
  3045   by (simp add: cos_add)
  3046 
  3047 lemma sin_periodic [simp]: "sin (x + 2*pi) = sin x"
  3048   by (simp add: sin_add sin_double cos_double)
  3049 
  3050 lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
  3051   by (simp add: cos_add sin_double cos_double)
  3052 
  3053 lemma cos_npi [simp]: "cos (real n * pi) = (- 1) ^ n"
  3054   by (induct n) (auto simp: real_of_nat_Suc distrib_right)
  3055 
  3056 lemma cos_npi2 [simp]: "cos (pi * real n) = (- 1) ^ n"
  3057   by (metis cos_npi mult.commute)
  3058 
  3059 lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
  3060   by (induct n) (auto simp: real_of_nat_Suc distrib_right)
  3061 
  3062 lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
  3063   by (simp add: mult.commute [of pi])
  3064 
  3065 lemma cos_two_pi [simp]: "cos (2*pi) = 1"
  3066   by (simp add: cos_double)
  3067 
  3068 lemma sin_two_pi [simp]: "sin (2*pi) = 0"
  3069   by (simp add: sin_double)
  3070 
  3071 lemma sin_gt_zero2: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < sin x"
  3072   by (metis sin_gt_zero_02 order_less_trans pi_half_less_two)
  3073 
  3074 lemma sin_less_zero:
  3075   assumes "- pi/2 < x" and "x < 0"
  3076   shows "sin x < 0"
  3077 proof -
  3078   have "0 < sin (- x)" using assms by (simp only: sin_gt_zero2)
  3079   thus ?thesis by simp
  3080 qed
  3081 
  3082 lemma pi_less_4: "pi < 4"
  3083   using pi_half_less_two by auto
  3084 
  3085 lemma cos_gt_zero: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < cos x"
  3086   by (simp add: cos_sin_eq sin_gt_zero2)
  3087 
  3088 lemma cos_gt_zero_pi: "\<lbrakk>-(pi/2) < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < cos x"
  3089   using cos_gt_zero [of x] cos_gt_zero [of "-x"]
  3090   by (cases rule: linorder_cases [of x 0]) auto
  3091 
  3092 lemma cos_ge_zero: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2\<rbrakk> \<Longrightarrow> 0 \<le> cos x"
  3093   apply (auto simp: order_le_less cos_gt_zero_pi)
  3094   by (metis cos_pi_half eq_divide_eq eq_numeral_simps(4))
  3095 
  3096 lemma sin_gt_zero: "\<lbrakk>0 < x; x < pi \<rbrakk> \<Longrightarrow> 0 < sin x"
  3097   by (simp add: sin_cos_eq cos_gt_zero_pi)
  3098 
  3099 lemma sin_lt_zero: "pi < x \<Longrightarrow> x < 2*pi \<Longrightarrow> sin x < 0"
  3100   using sin_gt_zero [of "x-pi"]
  3101   by (simp add: sin_diff)
  3102 
  3103 lemma pi_ge_two: "2 \<le> pi"
  3104 proof (rule ccontr)
  3105   assume "\<not> 2 \<le> pi" hence "pi < 2" by auto
  3106   have "\<exists>y > pi. y < 2 \<and> y < 2*pi"
  3107   proof (cases "2 < 2*pi")
  3108     case True with dense[OF `pi < 2`] show ?thesis by auto
  3109   next
  3110     case False have "pi < 2*pi" by auto
  3111     from dense[OF this] and False show ?thesis by auto
  3112   qed
  3113   then obtain y where "pi < y" and "y < 2" and "y < 2*pi" by blast
  3114   hence "0 < sin y" using sin_gt_zero_02 by auto
  3115   moreover
  3116   have "sin y < 0" using sin_gt_zero[of "y - pi"] `pi < y` and `y < 2*pi` sin_periodic_pi[of "y - pi"] by auto
  3117   ultimately show False by auto
  3118 qed
  3119 
  3120 lemma sin_ge_zero: "\<lbrakk>0 \<le> x; x \<le> pi\<rbrakk> \<Longrightarrow> 0 \<le> sin x"
  3121   by (auto simp: order_le_less sin_gt_zero)
  3122 
  3123 lemma sin_le_zero: "pi \<le> x \<Longrightarrow> x < 2*pi \<Longrightarrow> sin x \<le> 0"
  3124   using sin_ge_zero [of "x-pi"]
  3125   by (simp add: sin_diff)
  3126 
  3127 text {* FIXME: This proof is almost identical to lemma @{text cos_is_zero}.
  3128   It should be possible to factor out some of the common parts. *}
  3129 
  3130 lemma cos_total: "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)"
  3131 proof (rule ex_ex1I)
  3132   assume y: "-1 \<le> y" "y \<le> 1"
  3133   show "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y"
  3134     by (rule IVT2, simp_all add: y)
  3135 next
  3136   fix a b
  3137   assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
  3138   assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
  3139   have [simp]: "\<forall>x::real. cos differentiable (at x)"
  3140     unfolding real_differentiable_def by (auto intro: DERIV_cos)
  3141   from a b show "a = b"
  3142     apply (cut_tac less_linear [of a b], auto)
  3143     apply (drule_tac f = cos in Rolle)
  3144     apply (drule_tac [5] f = cos in Rolle)
  3145     apply (auto dest!: DERIV_cos [THEN DERIV_unique])
  3146     apply (metis order_less_le_trans less_le sin_gt_zero)
  3147     apply (metis order_less_le_trans less_le sin_gt_zero)
  3148     done
  3149 qed
  3150 
  3151 lemma sin_total:
  3152   assumes y: "-1 \<le> y" "y \<le> 1"
  3153     shows "\<exists>! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"
  3154 proof -
  3155   from cos_total [OF y]
  3156   obtain x where x: "0 \<le> x" "x \<le> pi" "cos x = y"
  3157            and uniq: "\<And>x'. 0 \<le> x' \<Longrightarrow> x' \<le> pi \<Longrightarrow> cos x' = y \<Longrightarrow> x' = x "
  3158     by blast
  3159   show ?thesis
  3160     apply (simp add: sin_cos_eq)
  3161     apply (rule ex1I [where a="pi/2 - x"])
  3162     apply (cut_tac [2] x'="pi/2 - xa" in uniq)
  3163     using x
  3164     apply auto
  3165     done
  3166 qed
  3167 
  3168 lemma reals_Archimedean4:
  3169      "\<lbrakk>0 < y; 0 \<le> x\<rbrakk> \<Longrightarrow> \<exists>n. real n * y \<le> x & x < real (Suc n) * y"
  3170 apply (auto dest!: reals_Archimedean3)
  3171 apply (drule_tac x = x in spec, clarify)
  3172 apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y")
  3173  prefer 2 apply (erule LeastI)
  3174 apply (case_tac "LEAST m::nat. x < real m * y", simp)
  3175 apply (rename_tac m)
  3176 apply (subgoal_tac "~ x < real m * y")
  3177  prefer 2 apply (rule not_less_Least, simp, force)
  3178 done
  3179 
  3180 lemma cos_zero_lemma:
  3181      "\<lbrakk>0 \<le> x; cos x = 0\<rbrakk> \<Longrightarrow>
  3182       \<exists>n::nat. odd n & x = real n * (pi/2)"
  3183 apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
  3184 apply (subgoal_tac "0 \<le> x - real n * pi &
  3185                     (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
  3186 apply (auto simp: algebra_simps real_of_nat_Suc)
  3187  prefer 2 apply (simp add: cos_diff)
  3188 apply (simp add: cos_diff)
  3189 apply (subgoal_tac "EX! x. 0 \<le> x & x \<le> pi & cos x = 0")
  3190 apply (rule_tac [2] cos_total, safe)
  3191 apply (drule_tac x = "x - real n * pi" in spec)
  3192 apply (drule_tac x = "pi/2" in spec)
  3193 apply (simp add: cos_diff)
  3194 apply (rule_tac x = "Suc (2 * n)" in exI)
  3195 apply (simp add: real_of_nat_Suc algebra_simps, auto)
  3196 done
  3197 
  3198 lemma sin_zero_lemma:
  3199      "\<lbrakk>0 \<le> x; sin x = 0\<rbrakk> \<Longrightarrow>
  3200       \<exists>n::nat. even n & x = real n * (pi/2)"
  3201 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  3202  apply (clarify, rule_tac x = "n - 1" in exI)
  3203  apply (auto elim!: oddE simp add: real_of_nat_Suc field_simps)[1]
  3204  apply (rule cos_zero_lemma)
  3205  apply (auto simp: cos_add)
  3206 done
  3207 
  3208 lemma cos_zero_iff:
  3209      "(cos x = 0) =
  3210       ((\<exists>n::nat. odd n & (x = real n * (pi/2))) |
  3211        (\<exists>n::nat. odd n & (x = -(real n * (pi/2)))))"
  3212 proof -
  3213   { fix n :: nat
  3214     assume "odd n"
  3215     then obtain m where "n = 2 * m + 1" ..
  3216     then have "cos (real n * pi / 2) = 0"
  3217       by (simp add: field_simps real_of_nat_Suc) (simp add: cos_add add_divide_distrib)
  3218   } note * = this
  3219   show ?thesis
  3220   apply (rule iffI)
  3221   apply (cut_tac linorder_linear [of 0 x], safe)
  3222   apply (drule cos_zero_lemma, assumption+)
  3223   apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
  3224   apply (auto dest: *)
  3225   done
  3226 qed
  3227 
  3228 (* ditto: but to a lesser extent *)
  3229 lemma sin_zero_iff:
  3230      "(sin x = 0) =
  3231       ((\<exists>n::nat. even n & (x = real n * (pi/2))) |
  3232        (\<exists>n::nat. even n & (x = -(real n * (pi/2)))))"
  3233 apply (rule iffI)
  3234 apply (cut_tac linorder_linear [of 0 x], safe)
  3235 apply (drule sin_zero_lemma, assumption+)
  3236 apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
  3237 apply (force simp add: minus_equation_iff [of x])
  3238 apply (auto elim: evenE)
  3239 done
  3240 
  3241 
  3242 lemma cos_zero_iff_int:
  3243      "cos x = 0 \<longleftrightarrow> (\<exists>n::int. odd n & x = real n * (pi/2))"
  3244 proof safe
  3245   assume "cos x = 0"
  3246   then show "\<exists>n::int. odd n & x = real n * (pi/2)"
  3247     apply (simp add: cos_zero_iff, safe)
  3248     apply (metis even_int_iff real_of_int_of_nat_eq)
  3249     apply (rule_tac x="- (int n)" in exI, simp)
  3250     done
  3251 next
  3252   fix n::int
  3253   assume "odd n"
  3254   then show "cos (real n * (pi / 2)) = 0"
  3255     apply (simp add: cos_zero_iff)
  3256     apply (case_tac n rule: int_cases2, simp)
  3257     apply (rule disjI2)
  3258     apply (rule_tac x="nat (-n)" in exI, simp)
  3259     done
  3260 qed
  3261 
  3262 lemma sin_zero_iff_int:
  3263      "sin x = 0 \<longleftrightarrow> (\<exists>n::int. even n & (x = real n * (pi/2)))"
  3264 proof safe
  3265   assume "sin x = 0"
  3266   then show "\<exists>n::int. even n \<and> x = real n * (pi / 2)"
  3267     apply (simp add: sin_zero_iff, safe)
  3268     apply (metis even_int_iff real_of_int_of_nat_eq)
  3269     apply (rule_tac x="- (int n)" in exI, simp)
  3270     done
  3271 next
  3272   fix n::int
  3273   assume "even n"
  3274   then show "sin (real n * (pi / 2)) = 0"
  3275     apply (simp add: sin_zero_iff)
  3276     apply (case_tac n rule: int_cases2, simp)
  3277     apply (rule disjI2)
  3278     apply (rule_tac x="nat (-n)" in exI, simp)
  3279     done
  3280 qed
  3281 
  3282 lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = real n * pi)"
  3283   apply (simp only: sin_zero_iff_int)
  3284   apply (safe elim!: evenE)
  3285   apply (simp_all add: field_simps)
  3286   using dvd_triv_left by fastforce
  3287 
  3288 lemma cos_monotone_0_pi:
  3289   assumes "0 \<le> y" and "y < x" and "x \<le> pi"
  3290   shows "cos x < cos y"
  3291 proof -
  3292   have "- (x - y) < 0" using assms by auto
  3293 
  3294   from MVT2[OF `y < x` DERIV_cos[THEN impI, THEN allI]]
  3295   obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z"
  3296     by auto
  3297   hence "0 < z" and "z < pi" using assms by auto
  3298   hence "0 < sin z" using sin_gt_zero by auto
  3299   hence "cos x - cos y < 0"
  3300     unfolding cos_diff minus_mult_commute[symmetric]
  3301     using `- (x - y) < 0` by (rule mult_pos_neg2)
  3302   thus ?thesis by auto
  3303 qed
  3304 
  3305 lemma cos_monotone_0_pi':
  3306   assumes "0 \<le> y" and "y \<le> x" and "x \<le> pi"
  3307   shows "cos x \<le> cos y"
  3308 proof (cases "y < x")
  3309   case True
  3310   show ?thesis
  3311     using cos_monotone_0_pi[OF `0 \<le> y` True `x \<le> pi`] by auto
  3312 next
  3313   case False
  3314   hence "y = x" using `y \<le> x` by auto
  3315   thus ?thesis by auto
  3316 qed
  3317 
  3318 lemma cos_monotone_minus_pi_0:
  3319   assumes "-pi \<le> y" and "y < x" and "x \<le> 0"
  3320   shows "cos y < cos x"
  3321 proof -
  3322   have "0 \<le> -x" and "-x < -y" and "-y \<le> pi"
  3323     using assms by auto
  3324   from cos_monotone_0_pi[OF this] show ?thesis
  3325     unfolding cos_minus .
  3326 qed
  3327 
  3328 lemma cos_monotone_minus_pi_0':
  3329   assumes "-pi \<le> y" and "y \<le> x" and "x \<le> 0"
  3330   shows "cos y \<le> cos x"
  3331 proof (cases "y < x")
  3332   case True
  3333   show ?thesis using cos_monotone_minus_pi_0[OF `-pi \<le> y` True `x \<le> 0`]
  3334     by auto
  3335 next
  3336   case False
  3337   hence "y = x" using `y \<le> x` by auto
  3338   thus ?thesis by auto
  3339 qed
  3340 
  3341 lemma sin_monotone_2pi':
  3342   assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2"
  3343   shows "sin y \<le> sin x"
  3344 proof -
  3345   have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
  3346     using pi_ge_two and assms by auto
  3347   from cos_monotone_0_pi'[OF this] show ?thesis
  3348     unfolding minus_sin_cos_eq[symmetric]
  3349     by (metis minus_sin_cos_eq mult.right_neutral neg_le_iff_le of_real_def real_scaleR_def)
  3350 qed
  3351 
  3352 lemma sin_x_le_x:
  3353   fixes x::real assumes x: "x \<ge> 0" shows "sin x \<le> x"
  3354 proof -
  3355   let ?f = "\<lambda>x. x - sin x"
  3356   from x have "?f x \<ge> ?f 0"
  3357     apply (rule DERIV_nonneg_imp_nondecreasing)
  3358     apply (intro allI impI exI[of _ "1 - cos x" for x])
  3359     apply (auto intro!: derivative_eq_intros simp: field_simps)
  3360     done
  3361   thus "sin x \<le> x" by simp
  3362 qed
  3363 
  3364 lemma sin_x_ge_neg_x:
  3365   fixes x::real assumes x: "x \<ge> 0" shows "sin x \<ge> - x"
  3366 proof -
  3367   let ?f = "\<lambda>x. x + sin x"
  3368   from x have "?f x \<ge> ?f 0"
  3369     apply (rule DERIV_nonneg_imp_nondecreasing)
  3370     apply (intro allI impI exI[of _ "1 + cos x" for x])
  3371     apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
  3372     done
  3373   thus "sin x \<ge> -x" by simp
  3374 qed
  3375 
  3376 lemma abs_sin_x_le_abs_x:
  3377   fixes x::real shows "\<bar>sin x\<bar> \<le> \<bar>x\<bar>"
  3378   using sin_x_ge_neg_x [of x] sin_x_le_x [of x] sin_x_ge_neg_x [of "-x"] sin_x_le_x [of "-x"]
  3379   by (auto simp: abs_real_def)
  3380 
  3381 
  3382 subsection {* Tangent *}
  3383 
  3384 definition tan :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  3385   where "tan = (\<lambda>x. sin x / cos x)"
  3386 
  3387 lemma tan_zero [simp]: "tan 0 = 0"
  3388   by (simp add: tan_def)
  3389 
  3390 lemma tan_pi [simp]: "tan pi = 0"
  3391   by (simp add: tan_def)
  3392 
  3393 lemma tan_npi [simp]: "tan (real (n::nat) * pi) = 0"
  3394   by (simp add: tan_def)
  3395 
  3396 lemma tan_minus [simp]: "tan (-x) = - tan x"
  3397   by (simp add: tan_def)
  3398 
  3399 lemma tan_periodic [simp]: "tan (x + 2*pi) = tan x"
  3400   by (simp add: tan_def)
  3401 
  3402 lemma lemma_tan_add1:
  3403   "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> 1 - tan x * tan y = cos (x + y)/(cos x * cos y)"
  3404   by (simp add: tan_def cos_add field_simps)
  3405 
  3406 lemma add_tan_eq:
  3407   fixes x :: "'a::{real_normed_field,banach}"
  3408   shows "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> tan x + tan y = sin(x + y)/(cos x * cos y)"
  3409   by (simp add: tan_def sin_add field_simps)
  3410 
  3411 lemma tan_add:
  3412   fixes x :: "'a::{real_normed_field,banach}"
  3413   shows
  3414      "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0\<rbrakk>
  3415       \<Longrightarrow> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
  3416       by (simp add: add_tan_eq lemma_tan_add1 field_simps) (simp add: tan_def)
  3417 
  3418 lemma tan_double:
  3419   fixes x :: "'a::{real_normed_field,banach}"
  3420   shows
  3421      "\<lbrakk>cos x \<noteq> 0; cos (2 * x) \<noteq> 0\<rbrakk>
  3422       \<Longrightarrow> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)"
  3423   using tan_add [of x x] by (simp add: power2_eq_square)
  3424 
  3425 lemma tan_gt_zero: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < tan x"
  3426   by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
  3427 
  3428 lemma tan_less_zero:
  3429   assumes lb: "- pi/2 < x" and "x < 0"
  3430   shows "tan x < 0"
  3431 proof -
  3432   have "0 < tan (- x)" using assms by (simp only: tan_gt_zero)
  3433   thus ?thesis by simp
  3434 qed
  3435 
  3436 lemma tan_half:
  3437   fixes x :: "'a::{real_normed_field,banach,field_inverse_zero}"
  3438   shows  "tan x = sin (2 * x) / (cos (2 * x) + 1)"
  3439   unfolding tan_def sin_double cos_double sin_squared_eq
  3440   by (simp add: power2_eq_square)
  3441 
  3442 lemma DERIV_tan [simp]:
  3443   fixes x :: "'a::{real_normed_field,banach}"
  3444   shows "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
  3445   unfolding tan_def
  3446   by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
  3447 
  3448 lemma isCont_tan:
  3449   fixes x :: "'a::{real_normed_field,banach}"
  3450   shows "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
  3451   by (rule DERIV_tan [THEN DERIV_isCont])
  3452 
  3453 lemma isCont_tan' [simp,continuous_intros]:
  3454   fixes a :: "'a::{real_normed_field,banach}" and f :: "'a \<Rightarrow> 'a"
  3455   shows "\<lbrakk>isCont f a; cos (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. tan (f x)) a"
  3456   by (rule isCont_o2 [OF _ isCont_tan])
  3457 
  3458 lemma tendsto_tan [tendsto_intros]:
  3459   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  3460   shows "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
  3461   by (rule isCont_tendsto_compose [OF isCont_tan])
  3462 
  3463 lemma continuous_tan:
  3464   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  3465   shows "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
  3466   unfolding continuous_def by (rule tendsto_tan)
  3467 
  3468 lemma continuous_on_tan [continuous_intros]:
  3469   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  3470   shows "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
  3471   unfolding continuous_on_def by (auto intro: tendsto_tan)
  3472 
  3473 lemma continuous_within_tan [continuous_intros]:
  3474   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  3475   shows
  3476   "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
  3477   unfolding continuous_within by (rule tendsto_tan)
  3478 
  3479 lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) -- pi/2 --> 0"
  3480   by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
  3481 
  3482 lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
  3483   apply (cut_tac LIM_cos_div_sin)
  3484   apply (simp only: LIM_eq)
  3485   apply (drule_tac x = "inverse y" in spec, safe, force)
  3486   apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
  3487   apply (rule_tac x = "(pi/2) - e" in exI)
  3488   apply (simp (no_asm_simp))
  3489   apply (drule_tac x = "(pi/2) - e" in spec)
  3490   apply (auto simp add: tan_def sin_diff cos_diff)
  3491   apply (rule inverse_less_iff_less [THEN iffD1])
  3492   apply (auto simp add: divide_inverse)
  3493   apply (rule mult_pos_pos)
  3494   apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
  3495   apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult.commute)
  3496   done
  3497 
  3498 lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
  3499   apply (frule order_le_imp_less_or_eq, safe)
  3500    prefer 2 apply force
  3501   apply (drule lemma_tan_total, safe)
  3502   apply (cut_tac f = tan and a = 0 and b = x and y = y in IVT_objl)
  3503   apply (auto intro!: DERIV_tan [THEN DERIV_isCont])
  3504   apply (drule_tac y = xa in order_le_imp_less_or_eq)
  3505   apply (auto dest: cos_gt_zero)
  3506   done
  3507 
  3508 lemma lemma_tan_total1: "\<exists>x. -(pi/2) < x & x < (pi/2) & tan x = y"
  3509   apply (cut_tac linorder_linear [of 0 y], safe)
  3510   apply (drule tan_total_pos)
  3511   apply (cut_tac [2] y="-y" in tan_total_pos, safe)
  3512   apply (rule_tac [3] x = "-x" in exI)
  3513   apply (auto del: exI intro!: exI)
  3514   done
  3515 
  3516 lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
  3517   apply (cut_tac y = y in lemma_tan_total1, auto)
  3518   apply hypsubst_thin
  3519   apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
  3520   apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
  3521   apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
  3522   apply (rule_tac [4] Rolle)
  3523   apply (rule_tac [2] Rolle)
  3524   apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
  3525               simp add: real_differentiable_def)
  3526   txt{*Now, simulate TRYALL*}
  3527   apply (rule_tac [!] DERIV_tan asm_rl)
  3528   apply (auto dest!: DERIV_unique [OF _ DERIV_tan]
  3529               simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym])
  3530   done
  3531 
  3532 lemma tan_monotone:
  3533   assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2"
  3534   shows "tan y < tan x"
  3535 proof -
  3536   have "\<forall>x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)"
  3537   proof (rule allI, rule impI)
  3538     fix x' :: real
  3539     assume "y \<le> x' \<and> x' \<le> x"
  3540     hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto
  3541     from cos_gt_zero_pi[OF this]
  3542     have "cos x' \<noteq> 0" by auto
  3543     thus "DERIV tan x' :> inverse ((cos x')\<^sup>2)" by (rule DERIV_tan)
  3544   qed
  3545   from MVT2[OF `y < x` this]
  3546   obtain z where "y < z" and "z < x"
  3547     and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto
  3548   hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto
  3549   hence "0 < cos z" using cos_gt_zero_pi by auto
  3550   hence inv_pos: "0 < inverse ((cos z)\<^sup>2)" by auto
  3551   have "0 < x - y" using `y < x` by auto
  3552   with inv_pos have "0 < tan x - tan y" unfolding tan_diff by auto
  3553   thus ?thesis by auto
  3554 qed
  3555 
  3556 lemma tan_monotone':
  3557   assumes "- (pi / 2) < y"
  3558     and "y < pi / 2"
  3559     and "- (pi / 2) < x"
  3560     and "x < pi / 2"
  3561   shows "(y < x) = (tan y < tan x)"
  3562 proof
  3563   assume "y < x"
  3564   thus "tan y < tan x"
  3565     using tan_monotone and `- (pi / 2) < y` and `x < pi / 2` by auto
  3566 next
  3567   assume "tan y < tan x"
  3568   show "y < x"
  3569   proof (rule ccontr)
  3570     assume "\<not> y < x" hence "x \<le> y" by auto
  3571     hence "tan x \<le> tan y"
  3572     proof (cases "x = y")
  3573       case True thus ?thesis by auto
  3574     next
  3575       case False hence "x < y" using `x \<le> y` by auto
  3576       from tan_monotone[OF `- (pi/2) < x` this `y < pi / 2`] show ?thesis by auto
  3577     qed
  3578     thus False using `tan y < tan x` by auto
  3579   qed
  3580 qed
  3581 
  3582 lemma tan_inverse: "1 / (tan y) = tan (pi / 2 - y)"
  3583   unfolding tan_def sin_cos_eq[of y] cos_sin_eq[of y] by auto
  3584 
  3585 lemma tan_periodic_pi[simp]: "tan (x + pi) = tan x"
  3586   by (simp add: tan_def)
  3587 
  3588 lemma tan_periodic_nat[simp]:
  3589   fixes n :: nat
  3590   shows "tan (x + real n * pi) = tan x"
  3591 proof (induct n arbitrary: x)
  3592   case 0
  3593   then show ?case by simp
  3594 next
  3595   case (Suc n)
  3596   have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi"
  3597     unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
  3598   show ?case unfolding split_pi_off using Suc by auto
  3599 qed
  3600 
  3601 lemma tan_periodic_int[simp]: fixes i :: int shows "tan (x + real i * pi) = tan x"
  3602 proof (cases "0 \<le> i")
  3603   case True
  3604   hence i_nat: "real i = real (nat i)" by auto
  3605   show ?thesis unfolding i_nat by auto
  3606 next
  3607   case False
  3608   hence i_nat: "real i = - real (nat (-i))" by auto
  3609   have "tan x = tan (x + real i * pi - real i * pi)"
  3610     by auto
  3611   also have "\<dots> = tan (x + real i * pi)"
  3612     unfolding i_nat mult_minus_left diff_minus_eq_add by (rule tan_periodic_nat)
  3613   finally show ?thesis by auto
  3614 qed
  3615 
  3616 lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
  3617   using tan_periodic_int[of _ "numeral n" ] unfolding real_numeral .
  3618 
  3619 
  3620 subsection {* Inverse Trigonometric Functions *}
  3621 text{*STILL DEFINED FOR THE REALS ONLY*}
  3622 
  3623 definition arcsin :: "real => real"
  3624   where "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
  3625 
  3626 definition arccos :: "real => real"
  3627   where "arccos y = (THE x. 0 \<le> x & x \<le> pi & cos x = y)"
  3628 
  3629 definition arctan :: "real => real"
  3630   where "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)"
  3631 
  3632 lemma arcsin:
  3633   "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow>
  3634     -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2 & sin(arcsin y) = y"
  3635   unfolding arcsin_def by (rule theI' [OF sin_total])
  3636 
  3637 lemma arcsin_pi:
  3638   "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi & sin(arcsin y) = y"
  3639   apply (drule (1) arcsin)
  3640   apply (force intro: order_trans)
  3641   done
  3642 
  3643 lemma sin_arcsin [simp]: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> sin(arcsin y) = y"
  3644   by (blast dest: arcsin)
  3645 
  3646 lemma arcsin_bounded: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2"
  3647   by (blast dest: arcsin)
  3648 
  3649 lemma arcsin_lbound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y"
  3650   by (blast dest: arcsin)
  3651 
  3652 lemma arcsin_ubound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin y \<le> pi/2"
  3653   by (blast dest: arcsin)
  3654 
  3655 lemma arcsin_lt_bounded:
  3656      "\<lbrakk>-1 < y; y < 1\<rbrakk> \<Longrightarrow> -(pi/2) < arcsin y & arcsin y < pi/2"
  3657   apply (frule order_less_imp_le)
  3658   apply (frule_tac y = y in order_less_imp_le)
  3659   apply (frule arcsin_bounded)
  3660   apply (safe, simp)
  3661   apply (drule_tac y = "arcsin y" in order_le_imp_less_or_eq)
  3662   apply (drule_tac [2] y = "pi/2" in order_le_imp_less_or_eq, safe)
  3663   apply (drule_tac [!] f = sin in arg_cong, auto)
  3664   done
  3665 
  3666 lemma arcsin_sin: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2\<rbrakk> \<Longrightarrow> arcsin(sin x) = x"
  3667   apply (unfold arcsin_def)
  3668   apply (rule the1_equality)
  3669   apply (rule sin_total, auto)
  3670   done
  3671 
  3672 lemma arccos:
  3673      "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk>
  3674       \<Longrightarrow> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
  3675   unfolding arccos_def by (rule theI' [OF cos_total])
  3676 
  3677 lemma cos_arccos [simp]: "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> cos(arccos y) = y"
  3678   by (blast dest: arccos)
  3679 
  3680 lemma arccos_bounded: "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> arccos y & arccos y \<le> pi"
  3681   by (blast dest: arccos)
  3682 
  3683 lemma arccos_lbound: "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> arccos y"
  3684   by (blast dest: arccos)
  3685 
  3686 lemma arccos_ubound: "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> arccos y \<le> pi"
  3687   by (blast dest: arccos)
  3688 
  3689 lemma arccos_lt_bounded:
  3690      "\<lbrakk>-1 < y; y < 1\<rbrakk>
  3691       \<Longrightarrow> 0 < arccos y & arccos y < pi"
  3692   apply (frule order_less_imp_le)
  3693   apply (frule_tac y = y in order_less_imp_le)
  3694   apply (frule arccos_bounded, auto)
  3695   apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
  3696   apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
  3697   apply (drule_tac [!] f = cos in arg_cong, auto)
  3698   done
  3699 
  3700 lemma arccos_cos: "\<lbrakk>0 \<le> x; x \<le> pi\<rbrakk> \<Longrightarrow> arccos(cos x) = x"
  3701   apply (simp add: arccos_def)
  3702   apply (auto intro!: the1_equality cos_total)
  3703   done
  3704 
  3705 lemma arccos_cos2: "\<lbrakk>x \<le> 0; -pi \<le> x\<rbrakk> \<Longrightarrow> arccos(cos x) = -x"
  3706   apply (simp add: arccos_def)
  3707   apply (auto intro!: the1_equality cos_total)
  3708   done
  3709 
  3710 lemma cos_arcsin: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> cos (arcsin x) = sqrt (1 - x\<^sup>2)"
  3711   apply (subgoal_tac "x\<^sup>2 \<le> 1")
  3712   apply (rule power2_eq_imp_eq)
  3713   apply (simp add: cos_squared_eq)
  3714   apply (rule cos_ge_zero)
  3715   apply (erule (1) arcsin_lbound)
  3716   apply (erule (1) arcsin_ubound)
  3717   apply simp
  3718   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
  3719   apply (rule power_mono, simp, simp)
  3720   done
  3721 
  3722 lemma sin_arccos: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> sin (arccos x) = sqrt (1 - x\<^sup>2)"
  3723   apply (subgoal_tac "x\<^sup>2 \<le> 1")
  3724   apply (rule power2_eq_imp_eq)
  3725   apply (simp add: sin_squared_eq)
  3726   apply (rule sin_ge_zero)
  3727   apply (erule (1) arccos_lbound)
  3728   apply (erule (1) arccos_ubound)
  3729   apply simp
  3730   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
  3731   apply (rule power_mono, simp, simp)
  3732   done
  3733 
  3734 lemma arctan [simp]: "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
  3735   unfolding arctan_def by (rule theI' [OF tan_total])
  3736 
  3737 lemma tan_arctan: "tan (arctan y) = y"
  3738   by auto
  3739 
  3740 lemma arctan_bounded: "- (pi/2) < arctan y  & arctan y < pi/2"
  3741   by (auto simp only: arctan)
  3742 
  3743 lemma arctan_lbound: "- (pi/2) < arctan y"
  3744   by auto
  3745 
  3746 lemma arctan_ubound: "arctan y < pi/2"
  3747   by (auto simp only: arctan)
  3748 
  3749 lemma arctan_unique:
  3750   assumes "-(pi/2) < x"
  3751     and "x < pi/2"
  3752     and "tan x = y"
  3753   shows "arctan y = x"
  3754   using assms arctan [of y] tan_total [of y] by (fast elim: ex1E)
  3755 
  3756 lemma arctan_tan: "-(pi/2) < x \<Longrightarrow> x < pi/2 \<Longrightarrow> arctan (tan x) = x"
  3757   by (rule arctan_unique) simp_all
  3758 
  3759 lemma arctan_zero_zero [simp]: "arctan 0 = 0"
  3760   by (rule arctan_unique) simp_all
  3761 
  3762 lemma arctan_minus: "arctan (- x) = - arctan x"
  3763   apply (rule arctan_unique)
  3764   apply (simp only: neg_less_iff_less arctan_ubound)
  3765   apply (metis minus_less_iff arctan_lbound, simp)
  3766   done
  3767 
  3768 lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
  3769   by (intro less_imp_neq [symmetric] cos_gt_zero_pi
  3770     arctan_lbound arctan_ubound)
  3771 
  3772 lemma cos_arctan: "cos (arctan x) = 1 / sqrt (1 + x\<^sup>2)"
  3773 proof (rule power2_eq_imp_eq)
  3774   have "0 < 1 + x\<^sup>2" by (simp add: add_pos_nonneg)
  3775   show "0 \<le> 1 / sqrt (1 + x\<^sup>2)" by simp
  3776   show "0 \<le> cos (arctan x)"
  3777     by (intro less_imp_le cos_gt_zero_pi arctan_lbound arctan_ubound)
  3778   have "(cos (arctan x))\<^sup>2 * (1 + (tan (arctan x))\<^sup>2) = 1"
  3779     unfolding tan_def by (simp add: distrib_left power_divide)
  3780   thus "(cos (arctan x))\<^sup>2 = (1 / sqrt (1 + x\<^sup>2))\<^sup>2"
  3781     using `0 < 1 + x\<^sup>2` by (simp add: power_divide eq_divide_eq)
  3782 qed
  3783 
  3784 lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<^sup>2)"
  3785   using add_pos_nonneg [OF zero_less_one zero_le_power2 [of x]]
  3786   using tan_arctan [of x] unfolding tan_def cos_arctan
  3787   by (simp add: eq_divide_eq)
  3788 
  3789 lemma tan_sec:
  3790   fixes x :: "'a::{real_normed_field,banach,field_inverse_zero}"
  3791   shows "cos x \<noteq> 0 \<Longrightarrow> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
  3792   apply (rule power_inverse [THEN subst])
  3793   apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
  3794   apply (auto dest: field_power_not_zero
  3795           simp add: power_mult_distrib distrib_right power_divide tan_def
  3796                     mult.assoc power_inverse [symmetric])
  3797   done
  3798 
  3799 lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
  3800   by (metis tan_monotone' arctan_lbound arctan_ubound tan_arctan)
  3801 
  3802 lemma arctan_le_iff: "arctan x \<le> arctan y \<longleftrightarrow> x \<le> y"
  3803   by (simp only: not_less [symmetric] arctan_less_iff)
  3804 
  3805 lemma arctan_eq_iff: "arctan x = arctan y \<longleftrightarrow> x = y"
  3806   by (simp only: eq_iff [where 'a=real] arctan_le_iff)
  3807 
  3808 lemma zero_less_arctan_iff [simp]: "0 < arctan x \<longleftrightarrow> 0 < x"
  3809   using arctan_less_iff [of 0 x] by simp
  3810 
  3811 lemma arctan_less_zero_iff [simp]: "arctan x < 0 \<longleftrightarrow> x < 0"
  3812   using arctan_less_iff [of x 0] by simp
  3813 
  3814 lemma zero_le_arctan_iff [simp]: "0 \<le> arctan x \<longleftrightarrow> 0 \<le> x"
  3815   using arctan_le_iff [of 0 x] by simp
  3816 
  3817 lemma arctan_le_zero_iff [simp]: "arctan x \<le> 0 \<longleftrightarrow> x \<le> 0"
  3818   using arctan_le_iff [of x 0] by simp
  3819 
  3820 lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
  3821   using arctan_eq_iff [of x 0] by simp
  3822 
  3823 lemma continuous_on_arcsin': "continuous_on {-1 .. 1} arcsin"
  3824 proof -
  3825   have "continuous_on (sin ` {- pi / 2 .. pi / 2}) arcsin"
  3826     by (rule continuous_on_inv) (auto intro: continuous_intros simp: arcsin_sin)
  3827   also have "sin ` {- pi / 2 .. pi / 2} = {-1 .. 1}"
  3828   proof safe
  3829     fix x :: real
  3830     assume "x \<in> {-1..1}"
  3831     then show "x \<in> sin ` {- pi / 2..pi / 2}"
  3832       using arcsin_lbound arcsin_ubound
  3833       by (intro image_eqI[where x="arcsin x"]) auto
  3834   qed simp
  3835   finally show ?thesis .
  3836 qed
  3837 
  3838 lemma continuous_on_arcsin [continuous_intros]:
  3839   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. -1 \<le> f x \<and> f x \<le> 1) \<Longrightarrow> continuous_on s (\<lambda>x. arcsin (f x))"
  3840   using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arcsin']]
  3841   by (auto simp: comp_def subset_eq)
  3842 
  3843 lemma isCont_arcsin: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> isCont arcsin x"
  3844   using continuous_on_arcsin'[THEN continuous_on_subset, of "{ -1 <..< 1 }"]
  3845   by (auto simp: continuous_on_eq_continuous_at subset_eq)
  3846 
  3847 lemma continuous_on_arccos': "continuous_on {-1 .. 1} arccos"
  3848 proof -
  3849   have "continuous_on (cos ` {0 .. pi}) arccos"
  3850     by (rule continuous_on_inv) (auto intro: continuous_intros simp: arccos_cos)
  3851   also have "cos ` {0 .. pi} = {-1 .. 1}"
  3852   proof safe
  3853     fix x :: real
  3854     assume "x \<in> {-1..1}"
  3855     then show "x \<in> cos ` {0..pi}"
  3856       using arccos_lbound arccos_ubound
  3857       by (intro image_eqI[where x="arccos x"]) auto
  3858   qed simp
  3859   finally show ?thesis .
  3860 qed
  3861 
  3862 lemma continuous_on_arccos [continuous_intros]:
  3863   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. -1 \<le> f x \<and> f x \<le> 1) \<Longrightarrow> continuous_on s (\<lambda>x. arccos (f x))"
  3864   using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arccos']]
  3865   by (auto simp: comp_def subset_eq)
  3866 
  3867 lemma isCont_arccos: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> isCont arccos x"
  3868   using continuous_on_arccos'[THEN continuous_on_subset, of "{ -1 <..< 1 }"]
  3869   by (auto simp: continuous_on_eq_continuous_at subset_eq)
  3870 
  3871 lemma isCont_arctan: "isCont arctan x"
  3872   apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify)
  3873   apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
  3874   apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
  3875   apply (erule (1) isCont_inverse_function2 [where f=tan])
  3876   apply (metis arctan_tan order_le_less_trans order_less_le_trans)
  3877   apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
  3878   done
  3879 
  3880 lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
  3881   by (rule isCont_tendsto_compose [OF isCont_arctan])
  3882 
  3883 lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
  3884   unfolding continuous_def by (rule tendsto_arctan)
  3885 
  3886 lemma continuous_on_arctan [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
  3887   unfolding continuous_on_def by (auto intro: tendsto_arctan)
  3888 
  3889 lemma DERIV_arcsin:
  3890   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<^sup>2))"
  3891   apply (rule DERIV_inverse_function [where f=sin and a="-1" and b=1])
  3892   apply (rule DERIV_cong [OF DERIV_sin])
  3893   apply (simp add: cos_arcsin)
  3894   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  3895   apply (rule power_strict_mono, simp, simp, simp, assumption, assumption)
  3896   apply simp
  3897   apply (erule (1) isCont_arcsin)
  3898   done
  3899 
  3900 lemma DERIV_arccos:
  3901   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<^sup>2))"
  3902   apply (rule DERIV_inverse_function [where f=cos and a="-1" and b=1])
  3903   apply (rule DERIV_cong [OF DERIV_cos])
  3904   apply (simp add: sin_arccos)
  3905   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  3906   apply (rule power_strict_mono, simp, simp, simp, assumption, assumption)
  3907   apply simp
  3908   apply (erule (1) isCont_arccos)
  3909   done
  3910 
  3911 lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)"
  3912   apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
  3913   apply (rule DERIV_cong [OF DERIV_tan])
  3914   apply (rule cos_arctan_not_zero)
  3915   apply (simp add: power_inverse tan_sec [symmetric])
  3916   apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
  3917   apply (simp add: add_pos_nonneg)
  3918   apply (simp, simp, simp, rule isCont_arctan)
  3919   done
  3920 
  3921 declare
  3922   DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
  3923   DERIV_arccos[THEN DERIV_chain2, derivative_intros]
  3924   DERIV_arctan[THEN DERIV_chain2, derivative_intros]
  3925 
  3926 lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
  3927   by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
  3928      (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
  3929            intro!: tan_monotone exI[of _ "pi/2"])
  3930 
  3931 lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
  3932   by (rule filterlim_at_top_at_left[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
  3933      (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
  3934            intro!: tan_monotone exI[of _ "pi/2"])
  3935 
  3936 lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"
  3937 proof (rule tendstoI)
  3938   fix e :: real
  3939   assume "0 < e"
  3940   def y \<equiv> "pi/2 - min (pi/2) e"
  3941   then have y: "0 \<le> y" "y < pi/2" "pi/2 \<le> e + y"
  3942     using `0 < e` by auto
  3943 
  3944   show "eventually (\<lambda>x. dist (arctan x) (pi / 2) < e) at_top"
  3945   proof (intro eventually_at_top_dense[THEN iffD2] exI allI impI)
  3946     fix x
  3947     assume "tan y < x"
  3948     then have "arctan (tan y) < arctan x"
  3949       by (simp add: arctan_less_iff)
  3950     with y have "y < arctan x"
  3951       by (subst (asm) arctan_tan) simp_all
  3952     with arctan_ubound[of x, arith] y `0 < e`
  3953     show "dist (arctan x) (pi / 2) < e"
  3954       by (simp add: dist_real_def)
  3955   qed
  3956 qed
  3957 
  3958 lemma tendsto_arctan_at_bot: "(arctan ---> - (pi/2)) at_bot"
  3959   unfolding filterlim_at_bot_mirror arctan_minus
  3960   by (intro tendsto_minus tendsto_arctan_at_top)
  3961 
  3962 
  3963 subsection {* More Theorems about Sin and Cos *}
  3964 
  3965 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
  3966 proof -
  3967   let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
  3968   have nonneg: "0 \<le> ?c"
  3969     by (simp add: cos_ge_zero)
  3970   have "0 = cos (pi / 4 + pi / 4)"
  3971     by simp
  3972   also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
  3973     by (simp only: cos_add power2_eq_square)
  3974   also have "\<dots> = 2 * ?c\<^sup>2 - 1"
  3975     by (simp add: sin_squared_eq)
  3976   finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
  3977     by (simp add: power_divide)
  3978   thus ?thesis
  3979     using nonneg by (rule power2_eq_imp_eq) simp
  3980 qed
  3981 
  3982 lemma cos_30: "cos (pi / 6) = sqrt 3/2"
  3983 proof -
  3984   let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
  3985   have pos_c: "0 < ?c"
  3986     by (rule cos_gt_zero, simp, simp)
  3987   have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
  3988     by simp
  3989   also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
  3990     by (simp only: cos_add sin_add)
  3991   also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
  3992     by (simp add: algebra_simps power2_eq_square)
  3993   finally have "?c\<^sup>2 = (sqrt 3/2)\<^sup>2"
  3994     using pos_c by (simp add: sin_squared_eq power_divide)
  3995   thus ?thesis
  3996     using pos_c [THEN order_less_imp_le]
  3997     by (rule power2_eq_imp_eq) simp
  3998 qed
  3999 
  4000 lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
  4001   by (simp add: sin_cos_eq cos_45)
  4002 
  4003 lemma sin_60: "sin (pi / 3) = sqrt 3/2"
  4004   by (simp add: sin_cos_eq cos_30)
  4005 
  4006 lemma cos_60: "cos (pi / 3) = 1 / 2"
  4007   apply (rule power2_eq_imp_eq)
  4008   apply (simp add: cos_squared_eq sin_60 power_divide)
  4009   apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
  4010   done
  4011 
  4012 lemma sin_30: "sin (pi / 6) = 1 / 2"
  4013   by (simp add: sin_cos_eq cos_60)
  4014 
  4015 lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
  4016   unfolding tan_def by (simp add: sin_30 cos_30)
  4017 
  4018 lemma tan_45: "tan (pi / 4) = 1"
  4019   unfolding tan_def by (simp add: sin_45 cos_45)
  4020 
  4021 lemma tan_60: "tan (pi / 3) = sqrt 3"
  4022   unfolding tan_def by (simp add: sin_60 cos_60)
  4023 
  4024 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
  4025 proof -
  4026   have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
  4027     by (auto simp: algebra_simps sin_add)
  4028   thus ?thesis
  4029     by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
  4030                   mult.commute [of pi])
  4031 qed
  4032 
  4033 lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
  4034   by (cases "even n") (simp_all add: cos_double mult.assoc)
  4035 
  4036 lemma cos_3over2_pi [simp]: "cos (3/2*pi) = 0"
  4037   apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
  4038   apply (subst cos_add, simp)
  4039   done
  4040 
  4041 lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
  4042   by (auto simp: mult.assoc sin_double)
  4043 
  4044 lemma sin_3over2_pi [simp]: "sin (3/2*pi) = - 1"
  4045   apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
  4046   apply (subst sin_add, simp)
  4047   done
  4048 
  4049 lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
  4050 by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
  4051 
  4052 lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
  4053   by (auto intro!: derivative_eq_intros)
  4054 
  4055 lemma sin_zero_norm_cos_one:
  4056   fixes x :: "'a::{real_normed_field,banach}"
  4057   assumes "sin x = 0" shows "norm (cos x) = 1"
  4058   using sin_cos_squared_add [of x, unfolded assms]
  4059   by (simp add: square_norm_one)
  4060 
  4061 lemma sin_zero_abs_cos_one: "sin x = 0 \<Longrightarrow> \<bar>cos x\<bar> = (1::real)"
  4062   using sin_zero_norm_cos_one by fastforce
  4063 
  4064 lemma cos_one_sin_zero:
  4065   fixes x :: "'a::{real_normed_field,banach}"
  4066   assumes "cos x = 1" shows "sin x = 0"
  4067   using sin_cos_squared_add [of x, unfolded assms]
  4068   by simp
  4069 
  4070 
  4071 subsection {* Machins formula *}
  4072 
  4073 lemma arctan_one: "arctan 1 = pi / 4"
  4074   by (rule arctan_unique, simp_all add: tan_45 m2pi_less_pi)
  4075 
  4076 lemma tan_total_pi4:
  4077   assumes "\<bar>x\<bar> < 1"
  4078   shows "\<exists>z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x"
  4079 proof
  4080   show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x"
  4081     unfolding arctan_one [symmetric] arctan_minus [symmetric]
  4082     unfolding arctan_less_iff using assms by auto
  4083 qed
  4084 
  4085 lemma arctan_add:
  4086   assumes "\<bar>x\<bar> \<le> 1" and "\<bar>y\<bar> < 1"
  4087   shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))"
  4088 proof (rule arctan_unique [symmetric])
  4089   have "- (pi / 4) \<le> arctan x" and "- (pi / 4) < arctan y"
  4090     unfolding arctan_one [symmetric] arctan_minus [symmetric]
  4091     unfolding arctan_le_iff arctan_less_iff using assms by auto
  4092   from add_le_less_mono [OF this]
  4093   show 1: "- (pi / 2) < arctan x + arctan y" by simp
  4094   have "arctan x \<le> pi / 4" and "arctan y < pi / 4"
  4095     unfolding arctan_one [symmetric]
  4096     unfolding arctan_le_iff arctan_less_iff using assms by auto
  4097   from add_le_less_mono [OF this]
  4098   show 2: "arctan x + arctan y < pi / 2" by simp
  4099   show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
  4100     using cos_gt_zero_pi [OF 1 2] by (simp add: tan_add)
  4101 qed
  4102 
  4103 theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)"
  4104 proof -
  4105   have "\<bar>1 / 5\<bar> < (1 :: real)" by auto
  4106   from arctan_add[OF less_imp_le[OF this] this]
  4107   have "2 * arctan (1 / 5) = arctan (5 / 12)" by auto
  4108   moreover
  4109   have "\<bar>5 / 12\<bar> < (1 :: real)" by auto
  4110   from arctan_add[OF less_imp_le[OF this] this]
  4111   have "2 * arctan (5 / 12) = arctan (120 / 119)" by auto
  4112   moreover
  4113   have "\<bar>1\<bar> \<le> (1::real)" and "\<bar>1 / 239\<bar> < (1::real)" by auto
  4114   from arctan_add[OF this]
  4115   have "arctan 1 + arctan (1 / 239) = arctan (120 / 119)" by auto
  4116   ultimately have "arctan 1 + arctan (1 / 239) = 4 * arctan (1 / 5)" by auto
  4117   thus ?thesis unfolding arctan_one by algebra
  4118 qed
  4119 
  4120 
  4121 subsection {* Introducing the inverse tangent power series *}
  4122 
  4123 lemma monoseq_arctan_series:
  4124   fixes x :: real
  4125   assumes "\<bar>x\<bar> \<le> 1"
  4126   shows "monoseq (\<lambda> n. 1 / real (n*2+1) * x^(n*2+1))" (is "monoseq ?a")
  4127 proof (cases "x = 0")
  4128   case True
  4129   thus ?thesis unfolding monoseq_def One_nat_def by auto
  4130 next
  4131   case False
  4132   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
  4133   show "monoseq ?a"
  4134   proof -
  4135     {
  4136       fix n
  4137       fix x :: real
  4138       assume "0 \<le> x" and "x \<le> 1"
  4139       have "1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<le>
  4140         1 / real (Suc (n * 2)) * x ^ Suc (n * 2)"
  4141       proof (rule mult_mono)
  4142         show "1 / real (Suc (Suc n * 2)) \<le> 1 / real (Suc (n * 2))"
  4143           by (rule frac_le) simp_all
  4144         show "0 \<le> 1 / real (Suc (n * 2))"
  4145           by auto
  4146         show "x ^ Suc (Suc n * 2) \<le> x ^ Suc (n * 2)"
  4147           by (rule power_decreasing) (simp_all add: `0 \<le> x` `x \<le> 1`)
  4148         show "0 \<le> x ^ Suc (Suc n * 2)"
  4149           by (rule zero_le_power) (simp add: `0 \<le> x`)
  4150       qed
  4151     } note mono = this
  4152 
  4153     show ?thesis
  4154     proof (cases "0 \<le> x")
  4155       case True from mono[OF this `x \<le> 1`, THEN allI]
  4156       show ?thesis unfolding Suc_eq_plus1[symmetric]
  4157         by (rule mono_SucI2)
  4158     next
  4159       case False
  4160       hence "0 \<le> -x" and "-x \<le> 1" using `-1 \<le> x` by auto
  4161       from mono[OF this]
  4162       have "\<And>n. 1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<ge>
  4163         1 / real (Suc (n * 2)) * x ^ Suc (n * 2)" using `0 \<le> -x` by auto
  4164       thus ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI1[OF allI])
  4165     qed
  4166   qed
  4167 qed
  4168 
  4169 lemma zeroseq_arctan_series:
  4170   fixes x :: real
  4171   assumes "\<bar>x\<bar> \<le> 1"
  4172   shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
  4173 proof (cases "x = 0")
  4174   case True
  4175   thus ?thesis
  4176     unfolding One_nat_def by auto
  4177 next
  4178   case False
  4179   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
  4180   show "?a ----> 0"
  4181   proof (cases "\<bar>x\<bar> < 1")
  4182     case True
  4183     hence "norm x < 1" by auto
  4184     from tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
  4185     have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
  4186       unfolding inverse_eq_divide Suc_eq_plus1 by simp
  4187     then show ?thesis using pos2 by (rule LIMSEQ_linear)
  4188   next
  4189     case False
  4190     hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
  4191     hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x"
  4192       unfolding One_nat_def by auto
  4193     from tendsto_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] tendsto_const[of x]]
  4194     show ?thesis unfolding n_eq Suc_eq_plus1 by auto
  4195   qed
  4196 qed
  4197 
  4198 text{*FIXME: generalise from the reals via type classes?*}
  4199 lemma summable_arctan_series:
  4200   fixes x :: real and n :: nat
  4201   assumes "\<bar>x\<bar> \<le> 1"
  4202   shows "summable (\<lambda> k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
  4203   (is "summable (?c x)")
  4204   by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms])
  4205 
  4206 lemma less_one_imp_sqr_less_one:
  4207   fixes x :: real
  4208   assumes "\<bar>x\<bar> < 1"
  4209   shows "x\<^sup>2 < 1"
  4210 proof -
  4211   have "\<bar>x\<^sup>2\<bar> < 1"
  4212     by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff)
  4213   thus ?thesis using zero_le_power2 by auto
  4214 qed
  4215 
  4216 lemma DERIV_arctan_series:
  4217   assumes "\<bar> x \<bar> < 1"
  4218   shows "DERIV (\<lambda> x'. \<Sum> k. (-1)^k * (1 / real (k*2+1) * x' ^ (k*2+1))) x :> (\<Sum> k. (-1)^k * x^(k*2))"
  4219   (is "DERIV ?arctan _ :> ?Int")
  4220 proof -
  4221   let ?f = "\<lambda>n. if even n then (-1)^(n div 2) * 1 / real (Suc n) else 0"
  4222 
  4223   have n_even: "\<And>n :: nat. even n \<Longrightarrow> 2 * (n div 2) = n"
  4224     by presburger
  4225   then have if_eq: "\<And>n x'. ?f n * real (Suc n) * x'^n =
  4226     (if even n then (-1)^(n div 2) * x'^(2 * (n div 2)) else 0)"
  4227     by auto
  4228 
  4229   {
  4230     fix x :: real
  4231     assume "\<bar>x\<bar> < 1"
  4232     hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
  4233     have "summable (\<lambda> n. (- 1) ^ n * (x\<^sup>2) ^n)"
  4234       by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x\<^sup>2 < 1` order_less_imp_le[OF `x\<^sup>2 < 1`])
  4235     hence "summable (\<lambda> n. (- 1) ^ n * x^(2*n))" unfolding power_mult .
  4236   } note summable_Integral = this
  4237 
  4238   {
  4239     fix f :: "nat \<Rightarrow> real"
  4240     have "\<And>x. f sums x = (\<lambda> n. if even n then f (n div 2) else 0) sums x"
  4241     proof
  4242       fix x :: real
  4243       assume "f sums x"
  4244       from sums_if[OF sums_zero this]
  4245       show "(\<lambda>n. if even n then f (n div 2) else 0) sums x"
  4246         by auto
  4247     next
  4248       fix x :: real
  4249       assume "(\<lambda> n. if even n then f (n div 2) else 0) sums x"
  4250       from LIMSEQ_linear[OF this[unfolded sums_def] pos2, unfolded sum_split_even_odd[unfolded mult.commute]]
  4251       show "f sums x" unfolding sums_def by auto
  4252     qed
  4253     hence "op sums f = op sums (\<lambda> n. if even n then f (n div 2) else 0)" ..
  4254   } note sums_even = this
  4255 
  4256   have Int_eq: "(\<Sum>n. ?f n * real (Suc n) * x^n) = ?Int"
  4257     unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * x ^ (2 * n)", symmetric]
  4258     by auto
  4259 
  4260   {
  4261     fix x :: real
  4262     have if_eq': "\<And>n. (if even n then (- 1) ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
  4263       (if even n then (- 1) ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
  4264       using n_even by auto
  4265     have idx_eq: "\<And>n. n * 2 + 1 = Suc (2 * n)" by auto
  4266     have "(\<Sum>n. ?f n * x^(Suc n)) = ?arctan x"
  4267       unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
  4268       by auto
  4269   } note arctan_eq = this
  4270 
  4271   have "DERIV (\<lambda> x. \<Sum> n. ?f n * x^(Suc n)) x :> (\<Sum> n. ?f n * real (Suc n) * x^n)"
  4272   proof (rule DERIV_power_series')
  4273     show "x \<in> {- 1 <..< 1}" using `\<bar> x \<bar> < 1` by auto
  4274     {
  4275       fix x' :: real
  4276       assume x'_bounds: "x' \<in> {- 1 <..< 1}"
  4277       then have "\<bar>x'\<bar> < 1" by auto
  4278       then
  4279         have *: "summable (\<lambda>n. (- 1) ^ n * x' ^ (2 * n))"
  4280         by (rule summable_Integral)
  4281       let ?S = "\<Sum> n. (-1)^n * x'^(2 * n)"
  4282       show "summable (\<lambda> n. ?f n * real (Suc n) * x'^n)" unfolding if_eq
  4283         apply (rule sums_summable [where l="0 + ?S"])
  4284         apply (rule sums_if)
  4285         apply (rule sums_zero)
  4286         apply (rule summable_sums)
  4287         apply (rule *)
  4288         done
  4289     }
  4290   qed auto
  4291   thus ?thesis unfolding Int_eq arctan_eq .
  4292 qed
  4293 
  4294 lemma arctan_series:
  4295   assumes "\<bar> x \<bar> \<le> 1"
  4296   shows "arctan x = (\<Sum>k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
  4297   (is "_ = suminf (\<lambda> n. ?c x n)")
  4298 proof -
  4299   let ?c' = "\<lambda>x n. (-1)^n * x^(n*2)"
  4300 
  4301   {
  4302     fix r x :: real
  4303     assume "0 < r" and "r < 1" and "\<bar> x \<bar> < r"
  4304     have "\<bar>x\<bar> < 1" using `r < 1` and `\<bar>x\<bar> < r` by auto
  4305     from DERIV_arctan_series[OF this] have "DERIV (\<lambda> x. suminf (?c x)) x :> (suminf (?c' x))" .
  4306   } note DERIV_arctan_suminf = this
  4307 
  4308   {
  4309     fix x :: real
  4310     assume "\<bar>x\<bar> \<le> 1"
  4311     note summable_Leibniz[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]]
  4312   } note arctan_series_borders = this
  4313 
  4314   {
  4315     fix x :: real
  4316     assume "\<bar>x\<bar> < 1"
  4317     have "arctan x = (\<Sum>k. ?c x k)"
  4318     proof -
  4319       obtain r where "\<bar>x\<bar> < r" and "r < 1"
  4320         using dense[OF `\<bar>x\<bar> < 1`] by blast
  4321       hence "0 < r" and "-r < x" and "x < r" by auto
  4322 
  4323       have suminf_eq_arctan_bounded: "\<And>x a b. \<lbrakk> -r < a ; b < r ; a < b ; a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow>
  4324         suminf (?c x) - arctan x = suminf (?c a) - arctan a"
  4325       proof -
  4326         fix x a b
  4327         assume "-r < a" and "b < r" and "a < b" and "a \<le> x" and "x \<le> b"
  4328         hence "\<bar>x\<bar> < r" by auto
  4329         show "suminf (?c x) - arctan x = suminf (?c a) - arctan a"
  4330         proof (rule DERIV_isconst2[of "a" "b"])
  4331           show "a < b" and "a \<le> x" and "x \<le> b"
  4332             using `a < b` `a \<le> x` `x \<le> b` by auto
  4333           have "\<forall>x. -r < x \<and> x < r \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
  4334           proof (rule allI, rule impI)
  4335             fix x
  4336             assume "-r < x \<and> x < r"
  4337             hence "\<bar>x\<bar> < r" by auto
  4338             hence "\<bar>x\<bar> < 1" using `r < 1` by auto
  4339             have "\<bar> - (x\<^sup>2) \<bar> < 1"
  4340               using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
  4341             hence "(\<lambda> n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))"
  4342               unfolding real_norm_def[symmetric] by (rule geometric_sums)
  4343             hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))"
  4344               unfolding power_mult_distrib[symmetric] power_mult mult.commute[of _ 2] by auto
  4345             hence suminf_c'_eq_geom: "inverse (1 + x\<^sup>2) = suminf (?c' x)"
  4346               using sums_unique unfolding inverse_eq_divide by auto
  4347             have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))"
  4348               unfolding suminf_c'_eq_geom
  4349               by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
  4350             from DERIV_diff [OF this DERIV_arctan]
  4351             show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
  4352               by auto
  4353           qed
  4354           hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
  4355             using `-r < a` `b < r` by auto
  4356           thus "\<forall> y. a < y \<and> y < b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
  4357             using `\<bar>x\<bar> < r` by auto
  4358           show "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> isCont (\<lambda> x. suminf (?c x) - arctan x) y"
  4359             using DERIV_in_rball DERIV_isCont by auto
  4360         qed
  4361       qed
  4362 
  4363       have suminf_arctan_zero: "suminf (?c 0) - arctan 0 = 0"
  4364         unfolding Suc_eq_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero
  4365         by auto
  4366 
  4367       have "suminf (?c x) - arctan x = 0"
  4368       proof (cases "x = 0")
  4369         case True
  4370         thus ?thesis using suminf_arctan_zero by auto
  4371       next
  4372         case False
  4373         hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
  4374         have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
  4375         thm suminf_eq_arctan_bounded
  4376           by (rule suminf_eq_arctan_bounded[where x1="0" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>", symmetric])
  4377             (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  4378         moreover
  4379         have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
  4380           by (rule suminf_eq_arctan_bounded[where x1="x" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>"])
  4381              (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  4382         ultimately
  4383         show ?thesis using suminf_arctan_zero by auto
  4384       qed
  4385       thus ?thesis by auto
  4386     qed
  4387   } note when_less_one = this
  4388 
  4389   show "arctan x = suminf (\<lambda> n. ?c x n)"
  4390   proof (cases "\<bar>x\<bar> < 1")
  4391     case True
  4392     thus ?thesis by (rule when_less_one)
  4393   next
  4394     case False
  4395     hence "\<bar>x\<bar> = 1" using `\<bar>x\<bar> \<le> 1` by auto
  4396     let ?a = "\<lambda>x n. \<bar>1 / real (n*2+1) * x^(n*2+1)\<bar>"
  4397     let ?diff = "\<lambda> x n. \<bar> arctan x - (\<Sum> i<n. ?c x i)\<bar>"
  4398     {
  4399       fix n :: nat
  4400       have "0 < (1 :: real)" by auto
  4401       moreover
  4402       {
  4403         fix x :: real
  4404         assume "0 < x" and "x < 1"
  4405         hence "\<bar>x\<bar> \<le> 1" and "\<bar>x\<bar> < 1" by auto
  4406         from `0 < x` have "0 < 1 / real (0 * 2 + (1::nat)) * x ^ (0 * 2 + 1)"
  4407           by auto
  4408         note bounds = mp[OF arctan_series_borders(2)[OF `\<bar>x\<bar> \<le> 1`] this, unfolded when_less_one[OF `\<bar>x\<bar> < 1`, symmetric], THEN spec]
  4409         have "0 < 1 / real (n*2+1) * x^(n*2+1)"
  4410           by (rule mult_pos_pos, auto simp only: zero_less_power[OF `0 < x`], auto)
  4411         hence a_pos: "?a x n = 1 / real (n*2+1) * x^(n*2+1)"
  4412           by (rule abs_of_pos)
  4413         have "?diff x n \<le> ?a x n"
  4414         proof (cases "even n")
  4415           case True
  4416           hence sgn_pos: "(-1)^n = (1::real)" by auto
  4417           from `even n` obtain m where "n = 2 * m" ..
  4418           then have "2 * m = n" ..
  4419           from bounds[of m, unfolded this atLeastAtMost_iff]
  4420           have "\<bar>arctan x - (\<Sum>i<n. (?c x i))\<bar> \<le> (\<Sum>i<n + 1. (?c x i)) - (\<Sum>i<n. (?c x i))"
  4421             by auto
  4422           also have "\<dots> = ?c x n" unfolding One_nat_def by auto
  4423           also have "\<dots> = ?a x n" unfolding sgn_pos a_pos by auto
  4424           finally show ?thesis .
  4425         next
  4426           case False
  4427           hence sgn_neg: "(-1)^n = (-1::real)" by auto
  4428           from `odd n` obtain m where "n = 2 * m + 1" ..
  4429           then have m_def: "2 * m + 1 = n" ..
  4430           hence m_plus: "2 * (m + 1) = n + 1" by auto
  4431           from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
  4432           have "\<bar>arctan x - (\<Sum>i<n. (?c x i))\<bar> \<le> (\<Sum>i<n. (?c x i)) - (\<Sum>i<n+1. (?c x i))"
  4433             by auto
  4434           also have "\<dots> = - ?c x n" unfolding One_nat_def by auto
  4435           also have "\<dots> = ?a x n" unfolding sgn_neg a_pos by auto
  4436           finally show ?thesis .
  4437         qed
  4438         hence "0 \<le> ?a x n - ?diff x n" by auto
  4439       }
  4440       hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
  4441       moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
  4442         unfolding diff_conv_add_uminus divide_inverse
  4443         by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan
  4444           isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum
  4445           simp del: add_uminus_conv_diff)
  4446       ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
  4447         by (rule LIM_less_bound)
  4448       hence "?diff 1 n \<le> ?a 1 n" by auto
  4449     }
  4450     have "?a 1 ----> 0"
  4451       unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
  4452       by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
  4453     have "?diff 1 ----> 0"
  4454     proof (rule LIMSEQ_I)
  4455       fix r :: real
  4456       assume "0 < r"
  4457       obtain N :: nat where N_I: "\<And>n. N \<le> n \<Longrightarrow> ?a 1 n < r"
  4458         using LIMSEQ_D[OF `?a 1 ----> 0` `0 < r`] by auto
  4459       {
  4460         fix n
  4461         assume "N \<le> n" from `?diff 1 n \<le> ?a 1 n` N_I[OF this]
  4462         have "norm (?diff 1 n - 0) < r" by auto
  4463       }
  4464       thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
  4465     qed
  4466     from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
  4467     have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
  4468     hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
  4469 
  4470     show ?thesis
  4471     proof (cases "x = 1")
  4472       case True
  4473       then show ?thesis by (simp add: `arctan 1 = (\<Sum> i. ?c 1 i)`)
  4474     next
  4475       case False
  4476       hence "x = -1" using `\<bar>x\<bar> = 1` by auto
  4477 
  4478       have "- (pi / 2) < 0" using pi_gt_zero by auto
  4479       have "- (2 * pi) < 0" using pi_gt_zero by auto
  4480 
  4481       have c_minus_minus: "\<And>i. ?c (- 1) i = - ?c 1 i"
  4482         unfolding One_nat_def by auto
  4483 
  4484       have "arctan (- 1) = arctan (tan (-(pi / 4)))"
  4485         unfolding tan_45 tan_minus ..
  4486       also have "\<dots> = - (pi / 4)"
  4487         by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
  4488       also have "\<dots> = - (arctan (tan (pi / 4)))"
  4489         unfolding neg_equal_iff_equal by (rule arctan_tan[symmetric], auto simp add: order_less_trans[OF `- (2 * pi) < 0` pi_gt_zero])
  4490       also have "\<dots> = - (arctan 1)"
  4491         unfolding tan_45 ..
  4492       also have "\<dots> = - (\<Sum> i. ?c 1 i)"
  4493         using `arctan 1 = (\<Sum> i. ?c 1 i)` by auto
  4494       also have "\<dots> = (\<Sum> i. ?c (- 1) i)"
  4495         using suminf_minus[OF sums_summable[OF `(?c 1) sums (arctan 1)`]]
  4496         unfolding c_minus_minus by auto
  4497       finally show ?thesis using `x = -1` by auto
  4498     qed
  4499   qed
  4500 qed
  4501 
  4502 lemma arctan_half:
  4503   fixes x :: real
  4504   shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x\<^sup>2)))"
  4505 proof -
  4506   obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x"
  4507     using tan_total by blast
  4508   hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2"
  4509     by auto
  4510 
  4511   have "0 < cos y" using cos_gt_zero_pi[OF low high] .
  4512   hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y"
  4513     by auto
  4514 
  4515   have "1 + (tan y)\<^sup>2 = 1 + (sin y)\<^sup>2 / (cos y)\<^sup>2"
  4516     unfolding tan_def power_divide ..
  4517   also have "\<dots> = (cos y)\<^sup>2 / (cos y)\<^sup>2 + (sin y)\<^sup>2 / (cos y)\<^sup>2"
  4518     using `cos y \<noteq> 0` by auto
  4519   also have "\<dots> = 1 / (cos y)\<^sup>2"
  4520     unfolding add_divide_distrib[symmetric] sin_cos_squared_add2 ..
  4521   finally have "1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2" .
  4522 
  4523   have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)"
  4524     unfolding tan_def using `cos y \<noteq> 0` by (simp add: field_simps)
  4525   also have "\<dots> = tan y / (1 + 1 / cos y)"
  4526     using `cos y \<noteq> 0` unfolding add_divide_distrib by auto
  4527   also have "\<dots> = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))"
  4528     unfolding cos_sqrt ..
  4529   also have "\<dots> = tan y / (1 + sqrt (1 / (cos y)\<^sup>2))"
  4530     unfolding real_sqrt_divide by auto
  4531   finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)\<^sup>2))"
  4532     unfolding `1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2` .
  4533 
  4534   have "arctan x = y"
  4535     using arctan_tan low high y_eq by auto
  4536   also have "\<dots> = 2 * (arctan (tan (y/2)))"
  4537     using arctan_tan[OF low2 high2] by auto
  4538   also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))"
  4539     unfolding tan_half by auto
  4540   finally show ?thesis
  4541     unfolding eq `tan y = x` .
  4542 qed
  4543 
  4544 lemma arctan_monotone: "x < y \<Longrightarrow> arctan x < arctan y"
  4545   by (simp only: arctan_less_iff)
  4546 
  4547 lemma arctan_monotone': "x \<le> y \<Longrightarrow> arctan x \<le> arctan y"
  4548   by (simp only: arctan_le_iff)
  4549 
  4550 lemma arctan_inverse:
  4551   assumes "x \<noteq> 0"
  4552   shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
  4553 proof (rule arctan_unique)
  4554   show "- (pi / 2) < sgn x * pi / 2 - arctan x"
  4555     using arctan_bounded [of x] assms
  4556     unfolding sgn_real_def
  4557     apply (auto simp add: algebra_simps)
  4558     apply (drule zero_less_arctan_iff [THEN iffD2])
  4559     apply arith
  4560     done
  4561   show "sgn x * pi / 2 - arctan x < pi / 2"
  4562     using arctan_bounded [of "- x"] assms
  4563     unfolding sgn_real_def arctan_minus
  4564     by (auto simp add: algebra_simps)
  4565   show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
  4566     unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
  4567     unfolding sgn_real_def
  4568     by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
  4569 qed
  4570 
  4571 theorem pi_series: "pi / 4 = (\<Sum> k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM")
  4572 proof -
  4573   have "pi / 4 = arctan 1" using arctan_one by auto
  4574   also have "\<dots> = ?SUM" using arctan_series[of 1] by auto
  4575   finally show ?thesis by auto
  4576 qed
  4577 
  4578 
  4579 subsection {* Existence of Polar Coordinates *}
  4580 
  4581 lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<^sup>2 + y\<^sup>2)\<bar> \<le> 1"
  4582   apply (rule power2_le_imp_le [OF _ zero_le_one])
  4583   apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
  4584   done
  4585 
  4586 lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
  4587   by (simp add: abs_le_iff)
  4588 
  4589 lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arccos y) = sqrt (1 - y\<^sup>2)"
  4590   by (simp add: sin_arccos abs_le_iff)
  4591 
  4592 lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]
  4593 
  4594 lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
  4595 
  4596 lemma polar_Ex: "\<exists>r::real. \<exists>a. x = r * cos a & y = r * sin a"
  4597 proof -
  4598   have polar_ex1: "\<And>y. 0 < y \<Longrightarrow> \<exists>r a. x = r * cos a & y = r * sin a"
  4599     apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)
  4600     apply (rule_tac x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))" in exI)
  4601     apply (simp add: cos_arccos_lemma1 sin_arccos_lemma1 power_divide
  4602                      real_sqrt_mult [symmetric] right_diff_distrib)
  4603     done
  4604   show ?thesis
  4605   proof (cases "0::real" y rule: linorder_cases)
  4606     case less
  4607       then show ?thesis by (rule polar_ex1)
  4608   next
  4609     case equal
  4610       then show ?thesis
  4611         by (force simp add: intro!: cos_zero sin_zero)
  4612   next
  4613     case greater
  4614       then show ?thesis
  4615      using polar_ex1 [where y="-y"]
  4616     by auto (metis cos_minus minus_minus minus_mult_right sin_minus)
  4617   qed
  4618 qed
  4619 
  4620 end