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