src/HOL/Transcendental.thy
author immler
Wed Nov 12 17:36:25 2014 +0100 (2014-11-12)
changeset 58981 11b6c099f5f3
parent 58889 5b7a9633cfa8
child 58984 ae0c56c485ae
permissions -rw-r--r--
code equation for powr
     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 lemmas mult_exp_exp = exp_add [symmetric]
  1110 
  1111 lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
  1112   unfolding exp_def
  1113   apply (subst suminf_of_real)
  1114   apply (rule summable_exp_generic)
  1115   apply (simp add: scaleR_conv_of_real)
  1116   done
  1117 
  1118 lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
  1119 proof
  1120   have "exp x * exp (- x) = 1" by (simp add: exp_add_commuting[symmetric])
  1121   also assume "exp x = 0"
  1122   finally show "False" by simp
  1123 qed
  1124 
  1125 lemma exp_minus_inverse:
  1126   shows "exp x * exp (- x) = 1"
  1127   by (simp add: exp_add_commuting[symmetric])
  1128 
  1129 lemma exp_minus:
  1130   fixes x :: "'a::{real_normed_field, banach}"
  1131   shows "exp (- x) = inverse (exp x)"
  1132   by (intro inverse_unique [symmetric] exp_minus_inverse)
  1133 
  1134 lemma exp_diff:
  1135   fixes x :: "'a::{real_normed_field, banach}"
  1136   shows "exp (x - y) = exp x / exp y"
  1137   using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
  1138 
  1139 
  1140 subsubsection {* Properties of the Exponential Function on Reals *}
  1141 
  1142 text {* Comparisons of @{term "exp x"} with zero. *}
  1143 
  1144 text{*Proof: because every exponential can be seen as a square.*}
  1145 lemma exp_ge_zero [simp]: "0 \<le> exp (x::real)"
  1146 proof -
  1147   have "0 \<le> exp (x/2) * exp (x/2)" by simp
  1148   thus ?thesis by (simp add: exp_add [symmetric])
  1149 qed
  1150 
  1151 lemma exp_gt_zero [simp]: "0 < exp (x::real)"
  1152   by (simp add: order_less_le)
  1153 
  1154 lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0"
  1155   by (simp add: not_less)
  1156 
  1157 lemma not_exp_le_zero [simp]: "\<not> exp (x::real) \<le> 0"
  1158   by (simp add: not_le)
  1159 
  1160 lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
  1161   by simp
  1162 
  1163 lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
  1164   by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
  1165 
  1166 text {* Strict monotonicity of exponential. *}
  1167 
  1168 lemma exp_ge_add_one_self_aux: 
  1169   assumes "0 \<le> (x::real)" shows "1+x \<le> exp(x)"
  1170 using order_le_imp_less_or_eq [OF assms]
  1171 proof 
  1172   assume "0 < x"
  1173   have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
  1174     by (auto simp add: numeral_2_eq_2)
  1175   also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
  1176     apply (rule setsum_le_suminf [OF summable_exp])
  1177     using `0 < x`
  1178     apply (auto  simp add:  zero_le_mult_iff)
  1179     done
  1180   finally show "1+x \<le> exp x" 
  1181     by (simp add: exp_def)
  1182 next
  1183   assume "0 = x"
  1184   then show "1 + x \<le> exp x"
  1185     by auto
  1186 qed
  1187 
  1188 lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x"
  1189 proof -
  1190   assume x: "0 < x"
  1191   hence "1 < 1 + x" by simp
  1192   also from x have "1 + x \<le> exp x"
  1193     by (simp add: exp_ge_add_one_self_aux)
  1194   finally show ?thesis .
  1195 qed
  1196 
  1197 lemma exp_less_mono:
  1198   fixes x y :: real
  1199   assumes "x < y"
  1200   shows "exp x < exp y"
  1201 proof -
  1202   from `x < y` have "0 < y - x" by simp
  1203   hence "1 < exp (y - x)" by (rule exp_gt_one)
  1204   hence "1 < exp y / exp x" by (simp only: exp_diff)
  1205   thus "exp x < exp y" by simp
  1206 qed
  1207 
  1208 lemma exp_less_cancel: "exp (x::real) < exp y \<Longrightarrow> x < y"
  1209   unfolding linorder_not_le [symmetric]
  1210   by (auto simp add: order_le_less exp_less_mono)
  1211 
  1212 lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y"
  1213   by (auto intro: exp_less_mono exp_less_cancel)
  1214 
  1215 lemma exp_le_cancel_iff [iff]: "exp (x::real) \<le> exp y \<longleftrightarrow> x \<le> y"
  1216   by (auto simp add: linorder_not_less [symmetric])
  1217 
  1218 lemma exp_inj_iff [iff]: "exp (x::real) = exp y \<longleftrightarrow> x = y"
  1219   by (simp add: order_eq_iff)
  1220 
  1221 text {* Comparisons of @{term "exp x"} with one. *}
  1222 
  1223 lemma one_less_exp_iff [simp]: "1 < exp (x::real) \<longleftrightarrow> 0 < x"
  1224   using exp_less_cancel_iff [where x=0 and y=x] by simp
  1225 
  1226 lemma exp_less_one_iff [simp]: "exp (x::real) < 1 \<longleftrightarrow> x < 0"
  1227   using exp_less_cancel_iff [where x=x and y=0] by simp
  1228 
  1229 lemma one_le_exp_iff [simp]: "1 \<le> exp (x::real) \<longleftrightarrow> 0 \<le> x"
  1230   using exp_le_cancel_iff [where x=0 and y=x] by simp
  1231 
  1232 lemma exp_le_one_iff [simp]: "exp (x::real) \<le> 1 \<longleftrightarrow> x \<le> 0"
  1233   using exp_le_cancel_iff [where x=x and y=0] by simp
  1234 
  1235 lemma exp_eq_one_iff [simp]: "exp (x::real) = 1 \<longleftrightarrow> x = 0"
  1236   using exp_inj_iff [where x=x and y=0] by simp
  1237 
  1238 lemma lemma_exp_total: "1 \<le> y \<Longrightarrow> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y"
  1239 proof (rule IVT)
  1240   assume "1 \<le> y"
  1241   hence "0 \<le> y - 1" by simp
  1242   hence "1 + (y - 1) \<le> exp (y - 1)" by (rule exp_ge_add_one_self_aux)
  1243   thus "y \<le> exp (y - 1)" by simp
  1244 qed (simp_all add: le_diff_eq)
  1245 
  1246 lemma exp_total: "0 < (y::real) \<Longrightarrow> \<exists>x. exp x = y"
  1247 proof (rule linorder_le_cases [of 1 y])
  1248   assume "1 \<le> y"
  1249   thus "\<exists>x. exp x = y" by (fast dest: lemma_exp_total)
  1250 next
  1251   assume "0 < y" and "y \<le> 1"
  1252   hence "1 \<le> inverse y" by (simp add: one_le_inverse_iff)
  1253   then obtain x where "exp x = inverse y" by (fast dest: lemma_exp_total)
  1254   hence "exp (- x) = y" by (simp add: exp_minus)
  1255   thus "\<exists>x. exp x = y" ..
  1256 qed
  1257 
  1258 
  1259 subsection {* Natural Logarithm *}
  1260 
  1261 definition ln :: "real \<Rightarrow> real"
  1262   where "ln x = (THE u. exp u = x)"
  1263 
  1264 lemma ln_exp [simp]: "ln (exp x) = x"
  1265   by (simp add: ln_def)
  1266 
  1267 lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
  1268   by (auto dest: exp_total)
  1269 
  1270 lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
  1271   by (metis exp_gt_zero exp_ln)
  1272 
  1273 lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
  1274   by (erule subst, rule ln_exp)
  1275 
  1276 lemma ln_one [simp]: "ln 1 = 0"
  1277   by (rule ln_unique) simp
  1278 
  1279 lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
  1280   by (rule ln_unique) (simp add: exp_add)
  1281 
  1282 lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
  1283   by (rule ln_unique) (simp add: exp_minus)
  1284 
  1285 lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
  1286   by (rule ln_unique) (simp add: exp_diff)
  1287 
  1288 lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
  1289   by (rule ln_unique) (simp add: exp_real_of_nat_mult)
  1290 
  1291 lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
  1292   by (subst exp_less_cancel_iff [symmetric]) simp
  1293 
  1294 lemma ln_le_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
  1295   by (simp add: linorder_not_less [symmetric])
  1296 
  1297 lemma ln_inj_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
  1298   by (simp add: order_eq_iff)
  1299 
  1300 lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
  1301   apply (rule exp_le_cancel_iff [THEN iffD1])
  1302   apply (simp add: exp_ge_add_one_self_aux)
  1303   done
  1304 
  1305 lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
  1306   by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
  1307 
  1308 lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
  1309   using ln_le_cancel_iff [of 1 x] by simp
  1310 
  1311 lemma ln_ge_zero_imp_ge_one: "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
  1312   using ln_le_cancel_iff [of 1 x] by simp
  1313 
  1314 lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
  1315   using ln_le_cancel_iff [of 1 x] by simp
  1316 
  1317 lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
  1318   using ln_less_cancel_iff [of x 1] by simp
  1319 
  1320 lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
  1321   using ln_less_cancel_iff [of 1 x] by simp
  1322 
  1323 lemma ln_gt_zero_imp_gt_one: "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
  1324   using ln_less_cancel_iff [of 1 x] by simp
  1325 
  1326 lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
  1327   using ln_less_cancel_iff [of 1 x] by simp
  1328 
  1329 lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
  1330   using ln_inj_iff [of x 1] by simp
  1331 
  1332 lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
  1333   by simp
  1334 
  1335 lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
  1336   by (auto simp add: ln_def intro!: arg_cong[where f=The])
  1337 
  1338 lemma isCont_ln: assumes "x \<noteq> 0" shows "isCont ln x"
  1339 proof cases
  1340   assume "0 < x"
  1341   moreover then have "isCont ln (exp (ln x))"
  1342     by (intro isCont_inv_fun[where d="\<bar>x\<bar>" and f=exp]) auto
  1343   ultimately show ?thesis
  1344     by simp
  1345 next
  1346   assume "\<not> 0 < x" with `x \<noteq> 0` show "isCont ln x"
  1347     unfolding isCont_def
  1348     by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
  1349        (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
  1350                 intro!: exI[of _ "\<bar>x\<bar>"])
  1351 qed
  1352 
  1353 lemma tendsto_ln [tendsto_intros]:
  1354   "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
  1355   by (rule isCont_tendsto_compose [OF isCont_ln])
  1356 
  1357 lemma continuous_ln:
  1358   "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
  1359   unfolding continuous_def by (rule tendsto_ln)
  1360 
  1361 lemma isCont_ln' [continuous_intros]:
  1362   "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
  1363   unfolding continuous_at by (rule tendsto_ln)
  1364 
  1365 lemma continuous_within_ln [continuous_intros]:
  1366   "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
  1367   unfolding continuous_within by (rule tendsto_ln)
  1368 
  1369 lemma continuous_on_ln [continuous_intros]:
  1370   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
  1371   unfolding continuous_on_def by (auto intro: tendsto_ln)
  1372 
  1373 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
  1374   apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
  1375   apply (auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln)
  1376   done
  1377 
  1378 lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
  1379   by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
  1380 
  1381 declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
  1382 
  1383 lemma ln_series:
  1384   assumes "0 < x" and "x < 2"
  1385   shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))"
  1386   (is "ln x = suminf (?f (x - 1))")
  1387 proof -
  1388   let ?f' = "\<lambda>x n. (-1)^n * (x - 1)^n"
  1389 
  1390   have "ln x - suminf (?f (x - 1)) = ln 1 - suminf (?f (1 - 1))"
  1391   proof (rule DERIV_isconst3[where x=x])
  1392     fix x :: real
  1393     assume "x \<in> {0 <..< 2}"
  1394     hence "0 < x" and "x < 2" by auto
  1395     have "norm (1 - x) < 1"
  1396       using `0 < x` and `x < 2` by auto
  1397     have "1 / x = 1 / (1 - (1 - x))" by auto
  1398     also have "\<dots> = (\<Sum> n. (1 - x)^n)"
  1399       using geometric_sums[OF `norm (1 - x) < 1`] by (rule sums_unique)
  1400     also have "\<dots> = suminf (?f' x)"
  1401       unfolding power_mult_distrib[symmetric]
  1402       by (rule arg_cong[where f=suminf], rule arg_cong[where f="op ^"], auto)
  1403     finally have "DERIV ln x :> suminf (?f' x)"
  1404       using DERIV_ln[OF `0 < x`] unfolding divide_inverse by auto
  1405     moreover
  1406     have repos: "\<And> h x :: real. h - 1 + x = h + x - 1" by auto
  1407     have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :>
  1408       (\<Sum>n. (-1)^n * (1 / real (n + 1)) * real (Suc n) * (x - 1) ^ n)"
  1409     proof (rule DERIV_power_series')
  1410       show "x - 1 \<in> {- 1<..<1}" and "(0 :: real) < 1"
  1411         using `0 < x` `x < 2` by auto
  1412       fix x :: real
  1413       assume "x \<in> {- 1<..<1}"
  1414       hence "norm (-x) < 1" by auto
  1415       show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
  1416         unfolding One_nat_def
  1417         by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
  1418     qed
  1419     hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
  1420       unfolding One_nat_def by auto
  1421     hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)"
  1422       unfolding DERIV_def repos .
  1423     ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
  1424       by (rule DERIV_diff)
  1425     thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
  1426   qed (auto simp add: assms)
  1427   thus ?thesis by auto
  1428 qed
  1429 
  1430 lemma exp_first_two_terms: "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
  1431 proof -
  1432   have "exp x = suminf (\<lambda>n. inverse(fact n) * (x ^ n))"
  1433     by (simp add: exp_def)
  1434   also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) + 
  1435     (\<Sum> n::nat<2. inverse(fact n) * (x ^ n))" (is "_ = _ + ?a")
  1436     by (rule suminf_split_initial_segment)
  1437   also have "?a = 1 + x"
  1438     by (simp add: numeral_2_eq_2)
  1439   finally show ?thesis
  1440     by simp
  1441 qed
  1442 
  1443 lemma exp_bound: "0 <= (x::real) \<Longrightarrow> x <= 1 \<Longrightarrow> exp x <= 1 + x + x\<^sup>2"
  1444 proof -
  1445   assume a: "0 <= x"
  1446   assume b: "x <= 1"
  1447   {
  1448     fix n :: nat
  1449     have "2 * 2 ^ n \<le> fact (n + 2)"
  1450       by (induct n) simp_all
  1451     hence "real ((2::nat) * 2 ^ n) \<le> real (fact (n + 2))"
  1452       by (simp only: real_of_nat_le_iff)
  1453     hence "2 * 2 ^ n \<le> real (fact (n + 2))"
  1454       by simp
  1455     hence "inverse (fact (n + 2)) \<le> inverse (2 * 2 ^ n)"
  1456       by (rule le_imp_inverse_le) simp
  1457     hence "inverse (fact (n + 2)) \<le> 1/2 * (1/2)^n"
  1458       by (simp add: power_inverse)
  1459     hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
  1460       by (rule mult_mono)
  1461         (rule mult_mono, simp_all add: power_le_one a b)
  1462     hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
  1463       unfolding power_add by (simp add: ac_simps del: fact_Suc) }
  1464   note aux1 = this
  1465   have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
  1466     by (intro sums_mult geometric_sums, simp)
  1467   hence aux2: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2"
  1468     by simp
  1469   have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <= x\<^sup>2"
  1470   proof -
  1471     have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <=
  1472         suminf (\<lambda>n. (x\<^sup>2/2) * ((1/2)^n))"
  1473       apply (rule suminf_le)
  1474       apply (rule allI, rule aux1)
  1475       apply (rule summable_exp [THEN summable_ignore_initial_segment])
  1476       by (rule sums_summable, rule aux2)
  1477     also have "... = x\<^sup>2"
  1478       by (rule sums_unique [THEN sym], rule aux2)
  1479     finally show ?thesis .
  1480   qed
  1481   thus ?thesis unfolding exp_first_two_terms by auto
  1482 qed
  1483 
  1484 lemma ln_one_minus_pos_upper_bound: "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
  1485 proof -
  1486   assume a: "0 <= (x::real)" and b: "x < 1"
  1487   have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)"
  1488     by (simp add: algebra_simps power2_eq_square power3_eq_cube)
  1489   also have "... <= 1"
  1490     by (auto simp add: a)
  1491   finally have "(1 - x) * (1 + x + x\<^sup>2) <= 1" .
  1492   moreover have c: "0 < 1 + x + x\<^sup>2"
  1493     by (simp add: add_pos_nonneg a)
  1494   ultimately have "1 - x <= 1 / (1 + x + x\<^sup>2)"
  1495     by (elim mult_imp_le_div_pos)
  1496   also have "... <= 1 / exp x"
  1497     by (metis a abs_one b exp_bound exp_gt_zero frac_le less_eq_real_def real_sqrt_abs 
  1498               real_sqrt_pow2_iff real_sqrt_power)
  1499   also have "... = exp (-x)"
  1500     by (auto simp add: exp_minus divide_inverse)
  1501   finally have "1 - x <= exp (- x)" .
  1502   also have "1 - x = exp (ln (1 - x))"
  1503     by (metis b diff_0 exp_ln_iff less_iff_diff_less_0 minus_diff_eq)
  1504   finally have "exp (ln (1 - x)) <= exp (- x)" .
  1505   thus ?thesis by (auto simp only: exp_le_cancel_iff)
  1506 qed
  1507 
  1508 lemma exp_ge_add_one_self [simp]: "1 + (x::real) <= exp x"
  1509   apply (case_tac "0 <= x")
  1510   apply (erule exp_ge_add_one_self_aux)
  1511   apply (case_tac "x <= -1")
  1512   apply (subgoal_tac "1 + x <= 0")
  1513   apply (erule order_trans)
  1514   apply simp
  1515   apply simp
  1516   apply (subgoal_tac "1 + x = exp(ln (1 + x))")
  1517   apply (erule ssubst)
  1518   apply (subst exp_le_cancel_iff)
  1519   apply (subgoal_tac "ln (1 - (- x)) <= - (- x)")
  1520   apply simp
  1521   apply (rule ln_one_minus_pos_upper_bound)
  1522   apply auto
  1523 done
  1524 
  1525 lemma ln_one_plus_pos_lower_bound: "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> x - x\<^sup>2 <= ln (1 + x)"
  1526 proof -
  1527   assume a: "0 <= x" and b: "x <= 1"
  1528   have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)"
  1529     by (rule exp_diff)
  1530   also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)"
  1531     by (metis a b divide_right_mono exp_bound exp_ge_zero)
  1532   also have "... <= (1 + x + x\<^sup>2) / (1 + x\<^sup>2)"
  1533     by (simp add: a divide_left_mono add_pos_nonneg)
  1534   also from a have "... <= 1 + x"
  1535     by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
  1536   finally have "exp (x - x\<^sup>2) <= 1 + x" .
  1537   also have "... = exp (ln (1 + x))"
  1538   proof -
  1539     from a have "0 < 1 + x" by auto
  1540     thus ?thesis
  1541       by (auto simp only: exp_ln_iff [THEN sym])
  1542   qed
  1543   finally have "exp (x - x\<^sup>2) <= exp (ln (1 + x))" .
  1544   thus ?thesis
  1545     by (metis exp_le_cancel_iff) 
  1546 qed
  1547 
  1548 lemma ln_one_minus_pos_lower_bound:
  1549   "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
  1550 proof -
  1551   assume a: "0 <= x" and b: "x <= (1 / 2)"
  1552   from b have c: "x < 1" by auto
  1553   then have "ln (1 - x) = - ln (1 + x / (1 - x))"
  1554     apply (subst ln_inverse [symmetric])
  1555     apply (simp add: field_simps)
  1556     apply (rule arg_cong [where f=ln])
  1557     apply (simp add: field_simps)
  1558     done
  1559   also have "- (x / (1 - x)) <= ..."
  1560   proof -
  1561     have "ln (1 + x / (1 - x)) <= x / (1 - x)"
  1562       using a c by (intro ln_add_one_self_le_self) auto
  1563     thus ?thesis
  1564       by auto
  1565   qed
  1566   also have "- (x / (1 - x)) = -x / (1 - x)"
  1567     by auto
  1568   finally have d: "- x / (1 - x) <= ln (1 - x)" .
  1569   have "0 < 1 - x" using a b by simp
  1570   hence e: "-x - 2 * x\<^sup>2 <= - x / (1 - x)"
  1571     using mult_right_le_one_le[of "x*x" "2*x"] a b
  1572     by (simp add: field_simps power2_eq_square)
  1573   from e d show "- x - 2 * x\<^sup>2 <= ln (1 - x)"
  1574     by (rule order_trans)
  1575 qed
  1576 
  1577 lemma ln_add_one_self_le_self2: "-1 < x \<Longrightarrow> ln(1 + x) <= x"
  1578   apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp)
  1579   apply (subst ln_le_cancel_iff)
  1580   apply auto
  1581   done
  1582 
  1583 lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
  1584   "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
  1585 proof -
  1586   assume x: "0 <= x"
  1587   assume x1: "x <= 1"
  1588   from x have "ln (1 + x) <= x"
  1589     by (rule ln_add_one_self_le_self)
  1590   then have "ln (1 + x) - x <= 0"
  1591     by simp
  1592   then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
  1593     by (rule abs_of_nonpos)
  1594   also have "... = x - ln (1 + x)"
  1595     by simp
  1596   also have "... <= x\<^sup>2"
  1597   proof -
  1598     from x x1 have "x - x\<^sup>2 <= ln (1 + x)"
  1599       by (intro ln_one_plus_pos_lower_bound)
  1600     thus ?thesis
  1601       by simp
  1602   qed
  1603   finally show ?thesis .
  1604 qed
  1605 
  1606 lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
  1607   "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  1608 proof -
  1609   assume a: "-(1 / 2) <= x"
  1610   assume b: "x <= 0"
  1611   have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
  1612     apply (subst abs_of_nonpos)
  1613     apply simp
  1614     apply (rule ln_add_one_self_le_self2)
  1615     using a apply auto
  1616     done
  1617   also have "... <= 2 * x\<^sup>2"
  1618     apply (subgoal_tac "- (-x) - 2 * (-x)\<^sup>2 <= ln (1 - (-x))")
  1619     apply (simp add: algebra_simps)
  1620     apply (rule ln_one_minus_pos_lower_bound)
  1621     using a b apply auto
  1622     done
  1623   finally show ?thesis .
  1624 qed
  1625 
  1626 lemma abs_ln_one_plus_x_minus_x_bound:
  1627     "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  1628   apply (case_tac "0 <= x")
  1629   apply (rule order_trans)
  1630   apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
  1631   apply auto
  1632   apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos)
  1633   apply auto
  1634   done
  1635 
  1636 lemma ln_x_over_x_mono: "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
  1637 proof -
  1638   assume x: "exp 1 <= x" "x <= y"
  1639   moreover have "0 < exp (1::real)" by simp
  1640   ultimately have a: "0 < x" and b: "0 < y"
  1641     by (fast intro: less_le_trans order_trans)+
  1642   have "x * ln y - x * ln x = x * (ln y - ln x)"
  1643     by (simp add: algebra_simps)
  1644   also have "... = x * ln(y / x)"
  1645     by (simp only: ln_div a b)
  1646   also have "y / x = (x + (y - x)) / x"
  1647     by simp
  1648   also have "... = 1 + (y - x) / x"
  1649     using x a by (simp add: field_simps)
  1650   also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
  1651     using x a 
  1652     by (intro mult_left_mono ln_add_one_self_le_self) simp_all
  1653   also have "... = y - x" using a by simp
  1654   also have "... = (y - x) * ln (exp 1)" by simp
  1655   also have "... <= (y - x) * ln x"
  1656     apply (rule mult_left_mono)
  1657     apply (subst ln_le_cancel_iff)
  1658     apply fact
  1659     apply (rule a)
  1660     apply (rule x)
  1661     using x apply simp
  1662     done
  1663   also have "... = y * ln x - x * ln x"
  1664     by (rule left_diff_distrib)
  1665   finally have "x * ln y <= y * ln x"
  1666     by arith
  1667   then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps)
  1668   also have "... = y * (ln x / x)" by simp
  1669   finally show ?thesis using b by (simp add: field_simps)
  1670 qed
  1671 
  1672 lemma ln_le_minus_one: "0 < x \<Longrightarrow> ln x \<le> x - 1"
  1673   using exp_ge_add_one_self[of "ln x"] by simp
  1674 
  1675 lemma ln_eq_minus_one:
  1676   assumes "0 < x" "ln x = x - 1"
  1677   shows "x = 1"
  1678 proof -
  1679   let ?l = "\<lambda>y. ln y - y + 1"
  1680   have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
  1681     by (auto intro!: derivative_eq_intros)
  1682 
  1683   show ?thesis
  1684   proof (cases rule: linorder_cases)
  1685     assume "x < 1"
  1686     from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast
  1687     from `x < a` have "?l x < ?l a"
  1688     proof (rule DERIV_pos_imp_increasing, safe)
  1689       fix y
  1690       assume "x \<le> y" "y \<le> a"
  1691       with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y"
  1692         by (auto simp: field_simps)
  1693       with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
  1694         by auto
  1695     qed
  1696     also have "\<dots> \<le> 0"
  1697       using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps)
  1698     finally show "x = 1" using assms by auto
  1699   next
  1700     assume "1 < x"
  1701     from dense[OF this] obtain a where "1 < a" "a < x" by blast
  1702     from `a < x` have "?l x < ?l a"
  1703     proof (rule DERIV_neg_imp_decreasing, safe)
  1704       fix y
  1705       assume "a \<le> y" "y \<le> x"
  1706       with `1 < a` have "1 / y - 1 < 0" "0 < y"
  1707         by (auto simp: field_simps)
  1708       with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0"
  1709         by blast
  1710     qed
  1711     also have "\<dots> \<le> 0"
  1712       using ln_le_minus_one `1 < a` by (auto simp: field_simps)
  1713     finally show "x = 1" using assms by auto
  1714   next
  1715     assume "x = 1"
  1716     then show ?thesis by simp
  1717   qed
  1718 qed
  1719 
  1720 lemma exp_at_bot: "(exp ---> (0::real)) at_bot"
  1721   unfolding tendsto_Zfun_iff
  1722 proof (rule ZfunI, simp add: eventually_at_bot_dense)
  1723   fix r :: real assume "0 < r"
  1724   {
  1725     fix x
  1726     assume "x < ln r"
  1727     then have "exp x < exp (ln r)"
  1728       by simp
  1729     with `0 < r` have "exp x < r"
  1730       by simp
  1731   }
  1732   then show "\<exists>k. \<forall>n<k. exp n < r" by auto
  1733 qed
  1734 
  1735 lemma exp_at_top: "LIM x at_top. exp x :: real :> at_top"
  1736   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"])
  1737      (auto intro: eventually_gt_at_top)
  1738 
  1739 lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
  1740   by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  1741      (auto simp: eventually_at_filter)
  1742 
  1743 lemma ln_at_top: "LIM x at_top. ln x :> at_top"
  1744   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  1745      (auto intro: eventually_gt_at_top)
  1746 
  1747 lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
  1748 proof (induct k)
  1749   case 0
  1750   show "((\<lambda>x. x ^ 0 / exp x) ---> (0::real)) at_top"
  1751     by (simp add: inverse_eq_divide[symmetric])
  1752        (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono
  1753               at_top_le_at_infinity order_refl)
  1754 next
  1755   case (Suc k)
  1756   show ?case
  1757   proof (rule lhospital_at_top_at_top)
  1758     show "eventually (\<lambda>x. DERIV (\<lambda>x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top"
  1759       by eventually_elim (intro derivative_eq_intros, auto)
  1760     show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top"
  1761       by eventually_elim auto
  1762     show "eventually (\<lambda>x. exp x \<noteq> 0) at_top"
  1763       by auto
  1764     from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
  1765     show "((\<lambda>x. real (Suc k) * x ^ k / exp x) ---> 0) at_top"
  1766       by simp
  1767   qed (rule exp_at_top)
  1768 qed
  1769 
  1770 
  1771 definition powr :: "[real,real] => real"  (infixr "powr" 80)
  1772   -- {*exponentation with real exponent*}
  1773   where "x powr a = exp(a * ln x)"
  1774 
  1775 definition log :: "[real,real] => real"
  1776   -- {*logarithm of @{term x} to base @{term a}*}
  1777   where "log a x = ln x / ln a"
  1778 
  1779 
  1780 lemma tendsto_log [tendsto_intros]:
  1781   "\<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"
  1782   unfolding log_def by (intro tendsto_intros) auto
  1783 
  1784 lemma continuous_log:
  1785   assumes "continuous F f"
  1786     and "continuous F g"
  1787     and "0 < f (Lim F (\<lambda>x. x))"
  1788     and "f (Lim F (\<lambda>x. x)) \<noteq> 1"
  1789     and "0 < g (Lim F (\<lambda>x. x))"
  1790   shows "continuous F (\<lambda>x. log (f x) (g x))"
  1791   using assms unfolding continuous_def by (rule tendsto_log)
  1792 
  1793 lemma continuous_at_within_log[continuous_intros]:
  1794   assumes "continuous (at a within s) f"
  1795     and "continuous (at a within s) g"
  1796     and "0 < f a"
  1797     and "f a \<noteq> 1"
  1798     and "0 < g a"
  1799   shows "continuous (at a within s) (\<lambda>x. log (f x) (g x))"
  1800   using assms unfolding continuous_within by (rule tendsto_log)
  1801 
  1802 lemma isCont_log[continuous_intros, simp]:
  1803   assumes "isCont f a" "isCont g a" "0 < f a" "f a \<noteq> 1" "0 < g a"
  1804   shows "isCont (\<lambda>x. log (f x) (g x)) a"
  1805   using assms unfolding continuous_at by (rule tendsto_log)
  1806 
  1807 lemma continuous_on_log[continuous_intros]:
  1808   assumes "continuous_on s f" "continuous_on s g"
  1809     and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
  1810   shows "continuous_on s (\<lambda>x. log (f x) (g x))"
  1811   using assms unfolding continuous_on_def by (fast intro: tendsto_log)
  1812 
  1813 lemma powr_one_eq_one [simp]: "1 powr a = 1"
  1814   by (simp add: powr_def)
  1815 
  1816 lemma powr_zero_eq_one [simp]: "x powr 0 = 1"
  1817   by (simp add: powr_def)
  1818 
  1819 lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)"
  1820   by (simp add: powr_def)
  1821 declare powr_one_gt_zero_iff [THEN iffD2, simp]
  1822 
  1823 lemma powr_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
  1824   by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
  1825 
  1826 lemma powr_gt_zero [simp]: "0 < x powr a"
  1827   by (simp add: powr_def)
  1828 
  1829 lemma powr_ge_pzero [simp]: "0 <= x powr y"
  1830   by (rule order_less_imp_le, rule powr_gt_zero)
  1831 
  1832 lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
  1833   by (simp add: powr_def)
  1834 
  1835 lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
  1836   apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
  1837   apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
  1838   done
  1839 
  1840 lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
  1841   apply (simp add: powr_def)
  1842   apply (subst exp_diff [THEN sym])
  1843   apply (simp add: left_diff_distrib)
  1844   done
  1845 
  1846 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
  1847   by (simp add: powr_def exp_add [symmetric] distrib_right)
  1848 
  1849 lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
  1850   using assms by (auto simp: powr_add)
  1851 
  1852 lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
  1853   by (simp add: powr_def)
  1854 
  1855 lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
  1856   by (simp add: powr_powr mult.commute)
  1857 
  1858 lemma powr_minus: "x powr (-a) = inverse (x powr a)"
  1859   by (simp add: powr_def exp_minus [symmetric])
  1860 
  1861 lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
  1862   by (simp add: divide_inverse powr_minus)
  1863 
  1864 lemma powr_less_mono: "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
  1865   by (simp add: powr_def)
  1866 
  1867 lemma powr_less_cancel: "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
  1868   by (simp add: powr_def)
  1869 
  1870 lemma powr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
  1871   by (blast intro: powr_less_cancel powr_less_mono)
  1872 
  1873 lemma powr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
  1874   by (simp add: linorder_not_less [symmetric])
  1875 
  1876 lemma log_ln: "ln x = log (exp(1)) x"
  1877   by (simp add: log_def)
  1878 
  1879 lemma DERIV_log:
  1880   assumes "x > 0"
  1881   shows "DERIV (\<lambda>y. log b y) x :> 1 / (ln b * x)"
  1882 proof -
  1883   def lb \<equiv> "1 / ln b"
  1884   moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x"
  1885     using `x > 0` by (auto intro!: derivative_eq_intros)
  1886   ultimately show ?thesis
  1887     by (simp add: log_def)
  1888 qed
  1889 
  1890 lemmas DERIV_log[THEN DERIV_chain2, derivative_intros]
  1891 
  1892 lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
  1893   by (simp add: powr_def log_def)
  1894 
  1895 lemma log_powr_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log a (a powr y) = y"
  1896   by (simp add: log_def powr_def)
  1897 
  1898 lemma log_mult:
  1899   "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow>
  1900     log a (x * y) = log a x + log a y"
  1901   by (simp add: log_def ln_mult divide_inverse distrib_right)
  1902 
  1903 lemma log_eq_div_ln_mult_log:
  1904   "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow>
  1905     log a x = (ln b/ln a) * log b x"
  1906   by (simp add: log_def divide_inverse)
  1907 
  1908 text{*Base 10 logarithms*}
  1909 lemma log_base_10_eq1: "0 < x \<Longrightarrow> log 10 x = (ln (exp 1) / ln 10) * ln x"
  1910   by (simp add: log_def)
  1911 
  1912 lemma log_base_10_eq2: "0 < x \<Longrightarrow> log 10 x = (log 10 (exp 1)) * ln x"
  1913   by (simp add: log_def)
  1914 
  1915 lemma log_one [simp]: "log a 1 = 0"
  1916   by (simp add: log_def)
  1917 
  1918 lemma log_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> log a a = 1"
  1919   by (simp add: log_def)
  1920 
  1921 lemma log_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log a (inverse x) = - log a x"
  1922   apply (rule_tac a1 = "log a x" in add_left_cancel [THEN iffD1])
  1923   apply (simp add: log_mult [symmetric])
  1924   done
  1925 
  1926 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"
  1927   by (simp add: log_mult divide_inverse log_inverse)
  1928 
  1929 lemma log_less_cancel_iff [simp]:
  1930   "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a x < log a y \<longleftrightarrow> x < y"
  1931   apply safe
  1932   apply (rule_tac [2] powr_less_cancel)
  1933   apply (drule_tac a = "log a x" in powr_less_mono, auto)
  1934   done
  1935 
  1936 lemma log_inj:
  1937   assumes "1 < b"
  1938   shows "inj_on (log b) {0 <..}"
  1939 proof (rule inj_onI, simp)
  1940   fix x y
  1941   assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
  1942   show "x = y"
  1943   proof (cases rule: linorder_cases)
  1944     assume "x = y"
  1945     then show ?thesis by simp
  1946   next
  1947     assume "x < y" hence "log b x < log b y"
  1948       using log_less_cancel_iff[OF `1 < b`] pos by simp
  1949     then show ?thesis using * by simp
  1950   next
  1951     assume "y < x" hence "log b y < log b x"
  1952       using log_less_cancel_iff[OF `1 < b`] pos by simp
  1953     then show ?thesis using * by simp
  1954   qed
  1955 qed
  1956 
  1957 lemma log_le_cancel_iff [simp]:
  1958   "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (log a x \<le> log a y) = (x \<le> y)"
  1959   by (simp add: linorder_not_less [symmetric])
  1960 
  1961 lemma zero_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < log a x \<longleftrightarrow> 1 < x"
  1962   using log_less_cancel_iff[of a 1 x] by simp
  1963 
  1964 lemma zero_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 \<le> log a x \<longleftrightarrow> 1 \<le> x"
  1965   using log_le_cancel_iff[of a 1 x] by simp
  1966 
  1967 lemma log_less_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 0 \<longleftrightarrow> x < 1"
  1968   using log_less_cancel_iff[of a x 1] by simp
  1969 
  1970 lemma log_le_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 0 \<longleftrightarrow> x \<le> 1"
  1971   using log_le_cancel_iff[of a x 1] by simp
  1972 
  1973 lemma one_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 < log a x \<longleftrightarrow> a < x"
  1974   using log_less_cancel_iff[of a a x] by simp
  1975 
  1976 lemma one_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> log a x \<longleftrightarrow> a \<le> x"
  1977   using log_le_cancel_iff[of a a x] by simp
  1978 
  1979 lemma log_less_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 1 \<longleftrightarrow> x < a"
  1980   using log_less_cancel_iff[of a x a] by simp
  1981 
  1982 lemma log_le_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 1 \<longleftrightarrow> x \<le> a"
  1983   using log_le_cancel_iff[of a x a] by simp
  1984 
  1985 lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
  1986   apply (induct n)
  1987   apply simp
  1988   apply (subgoal_tac "real(Suc n) = real n + 1")
  1989   apply (erule ssubst)
  1990   apply (subst powr_add, simp, simp)
  1991   done
  1992 
  1993 lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
  1994   unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
  1995 
  1996 lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
  1997 by(simp add: powr_realpow_numeral)
  1998 
  1999 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
  2000   apply (case_tac "x = 0", simp, simp)
  2001   apply (rule powr_realpow [THEN sym], simp)
  2002   done
  2003 
  2004 lemma powr_int:
  2005   assumes "x > 0"
  2006   shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))"
  2007 proof (cases "i < 0")
  2008   case True
  2009   have r: "x powr i = 1 / x powr (-i)" by (simp add: powr_minus field_simps)
  2010   show ?thesis using `i < 0` `x > 0` by (simp add: r field_simps powr_realpow[symmetric])
  2011 next
  2012   case False
  2013   then show ?thesis by (simp add: assms powr_realpow[symmetric])
  2014 qed
  2015 
  2016 lemma compute_powr[code]:
  2017   fixes i::real
  2018   shows "b powr i =
  2019     (if b \<le> 0 then Code.abort (STR ''op powr with nonpositive base'') (\<lambda>_. b powr i)
  2020     else if floor i = i then (if 0 \<le> i then b ^ natfloor i else 1 / b ^ natfloor (- i))
  2021     else Code.abort (STR ''op powr with non-integer exponent'') (\<lambda>_. b powr i))"
  2022   by (auto simp: natfloor_def powr_int)
  2023 
  2024 lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
  2025   using powr_realpow [of x 1] by simp
  2026 
  2027 lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
  2028   by (fact powr_realpow_numeral)
  2029 
  2030 lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
  2031   using powr_int [of x "- 1"] by simp
  2032 
  2033 lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
  2034   using powr_int [of x "- numeral n"] by simp
  2035 
  2036 lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
  2037   by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
  2038 
  2039 lemma ln_powr: "ln (x powr y) = y * ln x"
  2040   by (simp add: powr_def)
  2041 
  2042 lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) =  ln b / n"
  2043 by(simp add: root_powr_inverse ln_powr)
  2044 
  2045 lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
  2046   by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult.commute)
  2047 
  2048 lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) =  log b a / n"
  2049 by(simp add: log_def ln_root)
  2050 
  2051 lemma log_powr: "log b (x powr y) = y * log b x"
  2052   by (simp add: log_def ln_powr)
  2053 
  2054 lemma log_nat_power: "0 < x \<Longrightarrow> log b (x ^ n) = real n * log b x"
  2055   by (simp add: log_powr powr_realpow [symmetric])
  2056 
  2057 lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
  2058   by (simp add: log_def)
  2059 
  2060 lemma log_base_pow: "0 < a \<Longrightarrow> log (a ^ n) x = log a x / n"
  2061   by (simp add: log_def ln_realpow)
  2062 
  2063 lemma log_base_powr: "log (a powr b) x = log a x / b"
  2064   by (simp add: log_def ln_powr)
  2065 
  2066 lemma log_base_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> log (root n b) x = n * (log b x)"
  2067 by(simp add: log_def ln_root)
  2068 
  2069 lemma ln_bound: "1 <= x ==> ln x <= x"
  2070   apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
  2071   apply simp
  2072   apply (rule ln_add_one_self_le_self, simp)
  2073   done
  2074 
  2075 lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b"
  2076   apply (cases "x = 1", simp)
  2077   apply (cases "a = b", simp)
  2078   apply (rule order_less_imp_le)
  2079   apply (rule powr_less_mono, auto)
  2080   done
  2081 
  2082 lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a"
  2083   apply (subst powr_zero_eq_one [THEN sym])
  2084   apply (rule powr_mono, assumption+)
  2085   done
  2086 
  2087 lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
  2088   apply (unfold powr_def)
  2089   apply (rule exp_less_mono)
  2090   apply (rule mult_strict_left_mono)
  2091   apply (subst ln_less_cancel_iff, assumption)
  2092   apply (rule order_less_trans)
  2093   prefer 2
  2094   apply assumption+
  2095   done
  2096 
  2097 lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
  2098   apply (unfold powr_def)
  2099   apply (rule exp_less_mono)
  2100   apply (rule mult_strict_left_mono_neg)
  2101   apply (subst ln_less_cancel_iff)
  2102   apply assumption
  2103   apply (rule order_less_trans)
  2104   prefer 2
  2105   apply assumption+
  2106   done
  2107 
  2108 lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
  2109   apply (case_tac "a = 0", simp)
  2110   apply (case_tac "x = y", simp)
  2111   apply (metis less_eq_real_def powr_less_mono2)
  2112   done
  2113 
  2114 lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
  2115   unfolding powr_def exp_inj_iff by simp
  2116 
  2117 lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
  2118   by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute 
  2119             order.strict_trans2 powr_gt_zero zero_less_one)
  2120 
  2121 lemma ln_powr_bound2:
  2122   assumes "1 < x" and "0 < a"
  2123   shows "(ln x) powr a <= (a powr a) * x"
  2124 proof -
  2125   from assms have "ln x <= (x powr (1 / a)) / (1 / a)"
  2126     by (metis less_eq_real_def ln_powr_bound zero_less_divide_1_iff)
  2127   also have "... = a * (x powr (1 / a))"
  2128     by simp
  2129   finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
  2130     by (metis assms less_imp_le ln_gt_zero powr_mono2)
  2131   also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
  2132     by (metis assms(2) powr_mult powr_gt_zero)
  2133   also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
  2134     by (rule powr_powr)
  2135   also have "... = x" using assms
  2136     by auto
  2137   finally show ?thesis .
  2138 qed
  2139 
  2140 lemma tendsto_powr [tendsto_intros]:
  2141   "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
  2142   unfolding powr_def by (intro tendsto_intros)
  2143 
  2144 lemma continuous_powr:
  2145   assumes "continuous F f"
  2146     and "continuous F g"
  2147     and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
  2148   shows "continuous F (\<lambda>x. (f x) powr (g x))"
  2149   using assms unfolding continuous_def by (rule tendsto_powr)
  2150 
  2151 lemma continuous_at_within_powr[continuous_intros]:
  2152   assumes "continuous (at a within s) f"
  2153     and "continuous (at a within s) g"
  2154     and "f a \<noteq> 0"
  2155   shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
  2156   using assms unfolding continuous_within by (rule tendsto_powr)
  2157 
  2158 lemma isCont_powr[continuous_intros, simp]:
  2159   assumes "isCont f a" "isCont g a" "f a \<noteq> 0"
  2160   shows "isCont (\<lambda>x. (f x) powr g x) a"
  2161   using assms unfolding continuous_at by (rule tendsto_powr)
  2162 
  2163 lemma continuous_on_powr[continuous_intros]:
  2164   assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0"
  2165   shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
  2166   using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
  2167 
  2168 (* FIXME: generalize by replacing d by with g x and g ---> d? *)
  2169 lemma tendsto_zero_powrI:
  2170   assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
  2171     and "0 < d"
  2172   shows "((\<lambda>x. f x powr d) ---> 0) F"
  2173 proof (rule tendstoI)
  2174   fix e :: real assume "0 < e"
  2175   def Z \<equiv> "e powr (1 / d)"
  2176   with `0 < e` have "0 < Z" by simp
  2177   with assms have "eventually (\<lambda>x. 0 < f x \<and> dist (f x) 0 < Z) F"
  2178     by (intro eventually_conj tendstoD)
  2179   moreover
  2180   from assms have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> x powr d < Z powr d"
  2181     by (intro powr_less_mono2) (auto simp: dist_real_def)
  2182   with assms `0 < e` have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> dist (x powr d) 0 < e"
  2183     unfolding dist_real_def Z_def by (auto simp: powr_powr)
  2184   ultimately
  2185   show "eventually (\<lambda>x. dist (f x powr d) 0 < e) F" by (rule eventually_elim1)
  2186 qed
  2187 
  2188 lemma tendsto_neg_powr:
  2189   assumes "s < 0"
  2190     and "LIM x F. f x :> at_top"
  2191   shows "((\<lambda>x. f x powr s) ---> 0) F"
  2192 proof (rule tendstoI)
  2193   fix e :: real assume "0 < e"
  2194   def Z \<equiv> "e powr (1 / s)"
  2195   from assms have "eventually (\<lambda>x. Z < f x) F"
  2196     by (simp add: filterlim_at_top_dense)
  2197   moreover
  2198   from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
  2199     by (auto simp: Z_def intro!: powr_less_mono2_neg)
  2200   with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
  2201     by (simp add: powr_powr Z_def dist_real_def)
  2202   ultimately
  2203   show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
  2204 qed
  2205 
  2206 (* it is funny that this isn't in the library! It could go in Transcendental *)
  2207 lemma tendsto_exp_limit_at_right:
  2208   fixes x :: real
  2209   shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)"
  2210 proof cases
  2211   assume "x \<noteq> 0"
  2212 
  2213   have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
  2214     by (auto intro!: derivative_eq_intros)
  2215   then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
  2216     by (auto simp add: has_field_derivative_def field_has_derivative_at) 
  2217   then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)"
  2218     by (rule tendsto_intros)
  2219   then show ?thesis
  2220   proof (rule filterlim_mono_eventually)
  2221     show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
  2222       unfolding eventually_at_right[OF zero_less_one]
  2223       using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
  2224   qed (simp_all add: at_eq_sup_left_right)
  2225 qed simp
  2226 
  2227 lemma tendsto_exp_limit_at_top:
  2228   fixes x :: real
  2229   shows "((\<lambda>y. (1 + x / y) powr y) ---> exp x) at_top"
  2230   apply (subst filterlim_at_top_to_right)
  2231   apply (simp add: inverse_eq_divide)
  2232   apply (rule tendsto_exp_limit_at_right)
  2233   done
  2234 
  2235 lemma tendsto_exp_limit_sequentially:
  2236   fixes x :: real
  2237   shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x"
  2238 proof (rule filterlim_mono_eventually)
  2239   from reals_Archimedean2 [of "abs x"] obtain n :: nat where *: "real n > abs x" ..
  2240   hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
  2241     apply (intro eventually_sequentiallyI [of n])
  2242     apply (case_tac "x \<ge> 0")
  2243     apply (rule add_pos_nonneg, auto intro: divide_nonneg_nonneg)
  2244     apply (subgoal_tac "x / real xa > -1")
  2245     apply (auto simp add: field_simps)
  2246     done
  2247   then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
  2248     by (rule eventually_elim1) (erule powr_realpow)
  2249   show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x"
  2250     by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially])
  2251 qed auto
  2252 
  2253 subsection {* Sine and Cosine *}
  2254 
  2255 definition sin_coeff :: "nat \<Rightarrow> real" where
  2256   "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n))"
  2257 
  2258 definition cos_coeff :: "nat \<Rightarrow> real" where
  2259   "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
  2260 
  2261 definition sin :: "real \<Rightarrow> real"
  2262   where "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
  2263 
  2264 definition cos :: "real \<Rightarrow> real"
  2265   where "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
  2266 
  2267 lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
  2268   unfolding sin_coeff_def by simp
  2269 
  2270 lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
  2271   unfolding cos_coeff_def by simp
  2272 
  2273 lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
  2274   unfolding cos_coeff_def sin_coeff_def
  2275   by (simp del: mult_Suc)
  2276 
  2277 lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
  2278   unfolding cos_coeff_def sin_coeff_def
  2279   by (simp del: mult_Suc) (auto elim: oddE)
  2280 
  2281 lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
  2282   unfolding sin_coeff_def
  2283   apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
  2284   apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  2285   done
  2286 
  2287 lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
  2288   unfolding cos_coeff_def
  2289   apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
  2290   apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  2291   done
  2292 
  2293 lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
  2294   unfolding sin_def by (rule summable_sin [THEN summable_sums])
  2295 
  2296 lemma cos_converges: "(\<lambda>n. cos_coeff n * x ^ n) sums cos(x)"
  2297   unfolding cos_def by (rule summable_cos [THEN summable_sums])
  2298 
  2299 lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff"
  2300   by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
  2301 
  2302 lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
  2303   by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
  2304 
  2305 text{*Now at last we can get the derivatives of exp, sin and cos*}
  2306 
  2307 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
  2308   unfolding sin_def cos_def
  2309   apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
  2310   apply (simp_all add: diffs_sin_coeff diffs_cos_coeff
  2311     summable_minus summable_sin summable_cos)
  2312   done
  2313 
  2314 declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
  2315 
  2316 lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
  2317   unfolding cos_def sin_def
  2318   apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
  2319   apply (simp_all add: diffs_sin_coeff diffs_cos_coeff diffs_minus
  2320     summable_minus summable_sin summable_cos suminf_minus)
  2321   done
  2322 
  2323 declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
  2324 
  2325 lemma isCont_sin: "isCont sin x"
  2326   by (rule DERIV_sin [THEN DERIV_isCont])
  2327 
  2328 lemma isCont_cos: "isCont cos x"
  2329   by (rule DERIV_cos [THEN DERIV_isCont])
  2330 
  2331 lemma isCont_sin' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
  2332   by (rule isCont_o2 [OF _ isCont_sin])
  2333 
  2334 lemma isCont_cos' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
  2335   by (rule isCont_o2 [OF _ isCont_cos])
  2336 
  2337 lemma tendsto_sin [tendsto_intros]:
  2338   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) ---> sin a) F"
  2339   by (rule isCont_tendsto_compose [OF isCont_sin])
  2340 
  2341 lemma tendsto_cos [tendsto_intros]:
  2342   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
  2343   by (rule isCont_tendsto_compose [OF isCont_cos])
  2344 
  2345 lemma continuous_sin [continuous_intros]:
  2346   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
  2347   unfolding continuous_def by (rule tendsto_sin)
  2348 
  2349 lemma continuous_on_sin [continuous_intros]:
  2350   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
  2351   unfolding continuous_on_def by (auto intro: tendsto_sin)
  2352 
  2353 lemma continuous_cos [continuous_intros]:
  2354   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
  2355   unfolding continuous_def by (rule tendsto_cos)
  2356 
  2357 lemma continuous_on_cos [continuous_intros]:
  2358   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
  2359   unfolding continuous_on_def by (auto intro: tendsto_cos)
  2360 
  2361 subsection {* Properties of Sine and Cosine *}
  2362 
  2363 lemma sin_zero [simp]: "sin 0 = 0"
  2364   unfolding sin_def sin_coeff_def by (simp add: powser_zero)
  2365 
  2366 lemma cos_zero [simp]: "cos 0 = 1"
  2367   unfolding cos_def cos_coeff_def by (simp add: powser_zero)
  2368 
  2369 lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
  2370 proof -
  2371   have "\<forall>x. DERIV (\<lambda>x. (sin x)\<^sup>2 + (cos x)\<^sup>2) x :> 0"
  2372     by (auto intro!: derivative_eq_intros)
  2373   hence "(sin x)\<^sup>2 + (cos x)\<^sup>2 = (sin 0)\<^sup>2 + (cos 0)\<^sup>2"
  2374     by (rule DERIV_isconst_all)
  2375   thus "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" by simp
  2376 qed
  2377 
  2378 lemma sin_cos_squared_add2 [simp]: "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
  2379   by (subst add.commute, rule sin_cos_squared_add)
  2380 
  2381 lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
  2382   using sin_cos_squared_add2 [unfolded power2_eq_square] .
  2383 
  2384 lemma sin_squared_eq: "(sin x)\<^sup>2 = 1 - (cos x)\<^sup>2"
  2385   unfolding eq_diff_eq by (rule sin_cos_squared_add)
  2386 
  2387 lemma cos_squared_eq: "(cos x)\<^sup>2 = 1 - (sin x)\<^sup>2"
  2388   unfolding eq_diff_eq by (rule sin_cos_squared_add2)
  2389 
  2390 lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
  2391   by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
  2392 
  2393 lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
  2394   using abs_sin_le_one [of x] unfolding abs_le_iff by simp
  2395 
  2396 lemma sin_le_one [simp]: "sin x \<le> 1"
  2397   using abs_sin_le_one [of x] unfolding abs_le_iff by simp
  2398 
  2399 lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
  2400   by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
  2401 
  2402 lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
  2403   using abs_cos_le_one [of x] unfolding abs_le_iff by simp
  2404 
  2405 lemma cos_le_one [simp]: "cos x \<le> 1"
  2406   using abs_cos_le_one [of x] unfolding abs_le_iff by simp
  2407 
  2408 lemma DERIV_fun_pow: "DERIV g x :> m ==>
  2409       DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
  2410   by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  2411 
  2412 lemma DERIV_fun_exp:
  2413      "DERIV g x :> m ==> DERIV (\<lambda>x. exp(g x)) x :> exp(g x) * m"
  2414   by (auto intro!: derivative_intros)
  2415 
  2416 lemma DERIV_fun_sin:
  2417      "DERIV g x :> m ==> DERIV (\<lambda>x. sin(g x)) x :> cos(g x) * m"
  2418   by (auto intro!: derivative_intros)
  2419 
  2420 lemma DERIV_fun_cos:
  2421      "DERIV g x :> m ==> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
  2422   by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  2423 
  2424 lemma sin_cos_add_lemma:
  2425   "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 +
  2426     (cos (x + y) - (cos x * cos y - sin x * sin y))\<^sup>2 = 0"
  2427   (is "?f x = 0")
  2428 proof -
  2429   have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
  2430     by (auto intro!: derivative_eq_intros simp add: algebra_simps)
  2431   hence "?f x = ?f 0"
  2432     by (rule DERIV_isconst_all)
  2433   thus ?thesis by simp
  2434 qed
  2435 
  2436 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
  2437   using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
  2438 
  2439 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
  2440   using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
  2441 
  2442 lemma sin_cos_minus_lemma:
  2443   "(sin(-x) + sin(x))\<^sup>2 + (cos(-x) - cos(x))\<^sup>2 = 0" (is "?f x = 0")
  2444 proof -
  2445   have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
  2446     by (auto intro!: derivative_eq_intros simp add: algebra_simps)
  2447   hence "?f x = ?f 0"
  2448     by (rule DERIV_isconst_all)
  2449   thus ?thesis by simp
  2450 qed
  2451 
  2452 lemma sin_minus [simp]: "sin (-x) = -sin(x)"
  2453   using sin_cos_minus_lemma [where x=x] by simp
  2454 
  2455 lemma cos_minus [simp]: "cos (-x) = cos(x)"
  2456   using sin_cos_minus_lemma [where x=x] by simp
  2457 
  2458 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
  2459   using sin_add [of x "- y"] by simp
  2460 
  2461 lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
  2462   by (simp add: sin_diff mult.commute)
  2463 
  2464 lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
  2465   using cos_add [of x "- y"] by simp
  2466 
  2467 lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
  2468   by (simp add: cos_diff mult.commute)
  2469 
  2470 lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
  2471   using sin_add [where x=x and y=x] by simp
  2472 
  2473 lemma cos_double: "cos(2* x) = ((cos x)\<^sup>2) - ((sin x)\<^sup>2)"
  2474   using cos_add [where x=x and y=x]
  2475   by (simp add: power2_eq_square)
  2476 
  2477 lemma sin_x_le_x: assumes x: "x \<ge> 0" shows "sin x \<le> x"
  2478 proof -
  2479   let ?f = "\<lambda>x. x - sin x"
  2480   from x have "?f x \<ge> ?f 0"
  2481     apply (rule DERIV_nonneg_imp_nondecreasing)
  2482     apply (intro allI impI exI[of _ "1 - cos x" for x])
  2483     apply (auto intro!: derivative_eq_intros simp: field_simps)
  2484     done
  2485   thus "sin x \<le> x" by simp
  2486 qed
  2487 
  2488 lemma sin_x_ge_neg_x: assumes x: "x \<ge> 0" shows "sin x \<ge> - x"
  2489 proof -
  2490   let ?f = "\<lambda>x. x + sin x"
  2491   from x have "?f x \<ge> ?f 0"
  2492     apply (rule DERIV_nonneg_imp_nondecreasing)
  2493     apply (intro allI impI exI[of _ "1 + cos x" for x])
  2494     apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
  2495     done
  2496   thus "sin x \<ge> -x" by simp
  2497 qed
  2498 
  2499 lemma abs_sin_x_le_abs_x: "\<bar>sin x\<bar> \<le> \<bar>x\<bar>"
  2500   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"]
  2501   by (auto simp: abs_real_def)
  2502 
  2503 subsection {* The Constant Pi *}
  2504 
  2505 definition pi :: real
  2506   where "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
  2507 
  2508 text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
  2509    hence define pi.*}
  2510 
  2511 lemma sin_paired:
  2512   "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
  2513 proof -
  2514   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
  2515     by (rule sin_converges [THEN sums_group], simp)
  2516   thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: ac_simps)
  2517 qed
  2518 
  2519 lemma sin_gt_zero:
  2520   assumes "0 < x" and "x < 2"
  2521   shows "0 < sin x"
  2522 proof -
  2523   let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / real (fact (2*k+1)) * x^(2*k+1)"
  2524   have pos: "\<forall>n. 0 < ?f n"
  2525   proof
  2526     fix n :: nat
  2527     let ?k2 = "real (Suc (Suc (4 * n)))"
  2528     let ?k3 = "real (Suc (Suc (Suc (4 * n))))"
  2529     have "x * x < ?k2 * ?k3"
  2530       using assms by (intro mult_strict_mono', simp_all)
  2531     hence "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)"
  2532       by (intro mult_strict_right_mono zero_less_power `0 < x`)
  2533     thus "0 < ?f n"
  2534       by (simp del: mult_Suc,
  2535         simp add: less_divide_eq field_simps del: mult_Suc)
  2536   qed
  2537   have sums: "?f sums sin x"
  2538     by (rule sin_paired [THEN sums_group], simp)
  2539   show "0 < sin x"
  2540     unfolding sums_unique [OF sums]
  2541     using sums_summable [OF sums] pos
  2542     by (rule suminf_pos)
  2543 qed
  2544 
  2545 lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
  2546   using sin_gt_zero [where x = x] by (auto simp add: cos_squared_eq cos_double)
  2547 
  2548 lemma cos_paired: "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
  2549 proof -
  2550   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
  2551     by (rule cos_converges [THEN sums_group], simp)
  2552   thus ?thesis unfolding cos_coeff_def by (simp add: ac_simps)
  2553 qed
  2554 
  2555 lemmas realpow_num_eq_if = power_eq_if
  2556 
  2557 lemma sumr_pos_lt_pair:
  2558   fixes f :: "nat \<Rightarrow> real"
  2559   shows "\<lbrakk>summable f;
  2560         \<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
  2561       \<Longrightarrow> setsum f {..<k} < suminf f"
  2562 unfolding One_nat_def
  2563 apply (subst suminf_split_initial_segment [where k="k"])
  2564 apply assumption
  2565 apply simp
  2566 apply (drule_tac k="k" in summable_ignore_initial_segment)
  2567 apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
  2568 apply simp
  2569 apply (frule sums_unique)
  2570 apply (drule sums_summable)
  2571 apply simp
  2572 apply (erule suminf_pos)
  2573 apply (simp add: ac_simps)
  2574 done
  2575 
  2576 lemma cos_two_less_zero [simp]:
  2577   "cos 2 < 0"
  2578 proof -
  2579   note fact_Suc [simp del]
  2580   from cos_paired
  2581   have "(\<lambda>n. - ((- 1) ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
  2582     by (rule sums_minus)
  2583   then have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
  2584     by simp
  2585   then have **: "summable (\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2586     by (rule sums_summable)
  2587   have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2588     by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
  2589   moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
  2590     < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2591   proof -
  2592     { fix d
  2593       have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  2594        < real (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
  2595            fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  2596         by (simp only: real_of_nat_mult) (auto intro!: mult_strict_mono fact_less_mono_nat)
  2597       then have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  2598         < real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
  2599         by (simp only: fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
  2600       then have "4 * inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))))
  2601         < inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  2602         by (simp add: inverse_eq_divide less_divide_eq)
  2603     }
  2604     note *** = this
  2605     have [simp]: "\<And>x y::real. 0 < x - y \<longleftrightarrow> y < x" by arith
  2606     from ** show ?thesis by (rule sumr_pos_lt_pair)
  2607       (simp add: divide_inverse mult.assoc [symmetric] ***)
  2608   qed
  2609   ultimately have "0 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2610     by (rule order_less_trans)
  2611   moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2612     by (rule sums_unique)
  2613   ultimately have "0 < - cos 2" by simp
  2614   then show ?thesis by simp
  2615 qed
  2616 
  2617 lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
  2618 lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]
  2619 
  2620 lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 \<and> cos x = 0"
  2621 proof (rule ex_ex1I)
  2622   show "\<exists>x. 0 \<le> x & x \<le> 2 & cos x = 0"
  2623     by (rule IVT2, simp_all)
  2624 next
  2625   fix x y
  2626   assume x: "0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
  2627   assume y: "0 \<le> y \<and> y \<le> 2 \<and> cos y = 0"
  2628   have [simp]: "\<forall>x. cos differentiable (at x)"
  2629     unfolding real_differentiable_def by (auto intro: DERIV_cos)
  2630   from x y show "x = y"
  2631     apply (cut_tac less_linear [of x y], auto)
  2632     apply (drule_tac f = cos in Rolle)
  2633     apply (drule_tac [5] f = cos in Rolle)
  2634     apply (auto dest!: DERIV_cos [THEN DERIV_unique])
  2635     apply (metis order_less_le_trans less_le sin_gt_zero)
  2636     apply (metis order_less_le_trans less_le sin_gt_zero)
  2637     done
  2638 qed
  2639 
  2640 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
  2641   by (simp add: pi_def)
  2642 
  2643 lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
  2644   by (simp add: pi_half cos_is_zero [THEN theI'])
  2645 
  2646 lemma pi_half_gt_zero [simp]: "0 < pi / 2"
  2647   apply (rule order_le_neq_trans)
  2648   apply (simp add: pi_half cos_is_zero [THEN theI'])
  2649   apply (metis cos_pi_half cos_zero zero_neq_one)
  2650   done
  2651 
  2652 lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
  2653 lemmas pi_half_ge_zero [simp] = pi_half_gt_zero [THEN order_less_imp_le]
  2654 
  2655 lemma pi_half_less_two [simp]: "pi / 2 < 2"
  2656   apply (rule order_le_neq_trans)
  2657   apply (simp add: pi_half cos_is_zero [THEN theI'])
  2658   apply (metis cos_pi_half cos_two_neq_zero)
  2659   done
  2660 
  2661 lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
  2662 lemmas pi_half_le_two [simp] =  pi_half_less_two [THEN order_less_imp_le]
  2663 
  2664 lemma pi_gt_zero [simp]: "0 < pi"
  2665   using pi_half_gt_zero by simp
  2666 
  2667 lemma pi_ge_zero [simp]: "0 \<le> pi"
  2668   by (rule pi_gt_zero [THEN order_less_imp_le])
  2669 
  2670 lemma pi_neq_zero [simp]: "pi \<noteq> 0"
  2671   by (rule pi_gt_zero [THEN less_imp_neq, symmetric])
  2672 
  2673 lemma pi_not_less_zero [simp]: "\<not> pi < 0"
  2674   by (simp add: linorder_not_less)
  2675 
  2676 lemma minus_pi_half_less_zero: "-(pi/2) < 0"
  2677   by simp
  2678 
  2679 lemma m2pi_less_pi: "- (2 * pi) < pi"
  2680   by simp
  2681 
  2682 lemma sin_pi_half [simp]: "sin(pi/2) = 1"
  2683   using sin_cos_squared_add2 [where x = "pi/2"]
  2684   using sin_gt_zero [OF pi_half_gt_zero pi_half_less_two]
  2685   by (simp add: power2_eq_1_iff)
  2686 
  2687 lemma cos_pi [simp]: "cos pi = -1"
  2688   using cos_add [where x = "pi/2" and y = "pi/2"] by simp
  2689 
  2690 lemma sin_pi [simp]: "sin pi = 0"
  2691   using sin_add [where x = "pi/2" and y = "pi/2"] by simp
  2692 
  2693 lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
  2694   by (simp add: cos_diff)
  2695 
  2696 lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
  2697   by (simp add: cos_add)
  2698 
  2699 lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
  2700   by (simp add: sin_diff)
  2701 
  2702 lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
  2703   by (simp add: sin_add)
  2704 
  2705 lemma sin_periodic_pi2 [simp]: "sin (pi + x) = - sin x"
  2706   by (simp add: sin_add)
  2707 
  2708 lemma cos_periodic_pi [simp]: "cos (x + pi) = - cos x"
  2709   by (simp add: cos_add)
  2710 
  2711 lemma sin_periodic [simp]: "sin (x + 2*pi) = sin x"
  2712   by (simp add: sin_add cos_double)
  2713 
  2714 lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
  2715   by (simp add: cos_add cos_double)
  2716 
  2717 lemma cos_npi [simp]: "cos (real n * pi) = (- 1) ^ n"
  2718   by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
  2719 
  2720 lemma cos_npi2 [simp]: "cos (pi * real n) = (- 1) ^ n"
  2721   by (metis cos_npi mult.commute)
  2722 
  2723 lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
  2724   by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
  2725 
  2726 lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
  2727   by (simp add: mult.commute [of pi])
  2728 
  2729 lemma cos_two_pi [simp]: "cos (2 * pi) = 1"
  2730   by (simp add: cos_double)
  2731 
  2732 lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
  2733   by simp
  2734 
  2735 lemma sin_gt_zero2: "[| 0 < x; x < pi/2 |] ==> 0 < sin x"
  2736   by (metis sin_gt_zero order_less_trans pi_half_less_two)
  2737 
  2738 lemma sin_less_zero:
  2739   assumes "- pi/2 < x" and "x < 0"
  2740   shows "sin x < 0"
  2741 proof -
  2742   have "0 < sin (- x)" using assms by (simp only: sin_gt_zero2)
  2743   thus ?thesis by simp
  2744 qed
  2745 
  2746 lemma pi_less_4: "pi < 4"
  2747   using pi_half_less_two by auto
  2748 
  2749 lemma cos_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < cos x"
  2750   apply (cut_tac pi_less_4)
  2751   apply (cut_tac f = cos and a = 0 and b = x and y = 0 in IVT2_objl, safe, simp_all)
  2752   apply (cut_tac cos_is_zero, safe)
  2753   apply (rename_tac y z)
  2754   apply (drule_tac x = y in spec)
  2755   apply (drule_tac x = "pi/2" in spec, simp)
  2756   done
  2757 
  2758 lemma cos_gt_zero_pi: "[| -(pi/2) < x; x < pi/2 |] ==> 0 < cos x"
  2759   apply (rule_tac x = x and y = 0 in linorder_cases)
  2760   apply (metis cos_gt_zero cos_minus minus_less_iff neg_0_less_iff_less)
  2761   apply (auto intro: cos_gt_zero)
  2762   done
  2763 
  2764 lemma cos_ge_zero: "[| -(pi/2) \<le> x; x \<le> pi/2 |] ==> 0 \<le> cos x"
  2765   apply (auto simp add: order_le_less cos_gt_zero_pi)
  2766   apply (subgoal_tac "x = pi/2", auto)
  2767   done
  2768 
  2769 lemma sin_gt_zero_pi: "[| 0 < x; x < pi  |] ==> 0 < sin x"
  2770   by (simp add: sin_cos_eq cos_gt_zero_pi)
  2771 
  2772 lemma pi_ge_two: "2 \<le> pi"
  2773 proof (rule ccontr)
  2774   assume "\<not> 2 \<le> pi" hence "pi < 2" by auto
  2775   have "\<exists>y > pi. y < 2 \<and> y < 2 * pi"
  2776   proof (cases "2 < 2 * pi")
  2777     case True with dense[OF `pi < 2`] show ?thesis by auto
  2778   next
  2779     case False have "pi < 2 * pi" by auto
  2780     from dense[OF this] and False show ?thesis by auto
  2781   qed
  2782   then obtain y where "pi < y" and "y < 2" and "y < 2 * pi" by blast
  2783   hence "0 < sin y" using sin_gt_zero by auto
  2784   moreover
  2785   have "sin y < 0" using sin_gt_zero_pi[of "y - pi"] `pi < y` and `y < 2 * pi` sin_periodic_pi[of "y - pi"] by auto
  2786   ultimately show False by auto
  2787 qed
  2788 
  2789 lemma sin_ge_zero: "[| 0 \<le> x; x \<le> pi |] ==> 0 \<le> sin x"
  2790   by (auto simp add: order_le_less sin_gt_zero_pi)
  2791 
  2792 text {* FIXME: This proof is almost identical to lemma @{text cos_is_zero}.
  2793   It should be possible to factor out some of the common parts. *}
  2794 
  2795 lemma cos_total: "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)"
  2796 proof (rule ex_ex1I)
  2797   assume y: "-1 \<le> y" "y \<le> 1"
  2798   show "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y"
  2799     by (rule IVT2, simp_all add: y)
  2800 next
  2801   fix a b
  2802   assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
  2803   assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
  2804   have [simp]: "\<forall>x. cos differentiable (at x)"
  2805     unfolding real_differentiable_def by (auto intro: DERIV_cos)
  2806   from a b show "a = b"
  2807     apply (cut_tac less_linear [of a b], auto)
  2808     apply (drule_tac f = cos in Rolle)
  2809     apply (drule_tac [5] f = cos in Rolle)
  2810     apply (auto dest!: DERIV_cos [THEN DERIV_unique])
  2811     apply (metis order_less_le_trans less_le sin_gt_zero_pi)
  2812     apply (metis order_less_le_trans less_le sin_gt_zero_pi)
  2813     done
  2814 qed
  2815 
  2816 lemma sin_total:
  2817      "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"
  2818 apply (rule ccontr)
  2819 apply (subgoal_tac "\<forall>x. (- (pi/2) \<le> x & x \<le> pi/2 & (sin x = y)) = (0 \<le> (x + pi/2) & (x + pi/2) \<le> pi & (cos (x + pi/2) = -y))")
  2820 apply (erule contrapos_np)
  2821 apply simp
  2822 apply (cut_tac y="-y" in cos_total, simp) apply simp
  2823 apply (erule ex1E)
  2824 apply (rule_tac a = "x - (pi/2)" in ex1I)
  2825 apply (simp (no_asm) add: add.assoc)
  2826 apply (rotate_tac 3)
  2827 apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all add: cos_add)
  2828 done
  2829 
  2830 lemma reals_Archimedean4:
  2831      "[| 0 < y; 0 \<le> x |] ==> \<exists>n. real n * y \<le> x & x < real (Suc n) * y"
  2832 apply (auto dest!: reals_Archimedean3)
  2833 apply (drule_tac x = x in spec, clarify)
  2834 apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y")
  2835  prefer 2 apply (erule LeastI)
  2836 apply (case_tac "LEAST m::nat. x < real m * y", simp)
  2837 apply (rename_tac m)
  2838 apply (subgoal_tac "~ x < real m * y")
  2839  prefer 2 apply (rule not_less_Least, simp, force)
  2840 done
  2841 
  2842 (* Pre Isabelle99-2 proof was simpler- numerals arithmetic
  2843    now causes some unwanted re-arrangements of literals!   *)
  2844 lemma cos_zero_lemma:
  2845      "[| 0 \<le> x; cos x = 0 |] ==>
  2846       \<exists>n::nat. ~even n & x = real n * (pi/2)"
  2847 apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
  2848 apply (subgoal_tac "0 \<le> x - real n * pi &
  2849                     (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
  2850 apply (auto simp add: algebra_simps real_of_nat_Suc)
  2851  prefer 2 apply (simp add: cos_diff)
  2852 apply (simp add: cos_diff)
  2853 apply (subgoal_tac "EX! x. 0 \<le> x & x \<le> pi & cos x = 0")
  2854 apply (rule_tac [2] cos_total, safe)
  2855 apply (drule_tac x = "x - real n * pi" in spec)
  2856 apply (drule_tac x = "pi/2" in spec)
  2857 apply (simp add: cos_diff)
  2858 apply (rule_tac x = "Suc (2 * n)" in exI)
  2859 apply (simp add: real_of_nat_Suc algebra_simps, auto)
  2860 done
  2861 
  2862 lemma sin_zero_lemma:
  2863      "[| 0 \<le> x; sin x = 0 |] ==>
  2864       \<exists>n::nat. even n & x = real n * (pi/2)"
  2865 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  2866  apply (clarify, rule_tac x = "n - 1" in exI)
  2867  apply (auto elim!: oddE simp add: real_of_nat_Suc field_simps)[1]
  2868  apply (rule cos_zero_lemma)
  2869  apply (auto simp add: cos_add)
  2870 done
  2871 
  2872 lemma cos_zero_iff:
  2873      "(cos x = 0) =
  2874       ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |
  2875        (\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
  2876 proof -
  2877   { fix n :: nat
  2878     assume "odd n"
  2879     then obtain m where "n = 2 * m + 1" ..
  2880     then have "cos (real n * pi / 2) = 0"
  2881       by (simp add: field_simps real_of_nat_Suc) (simp add: cos_add add_divide_distrib)
  2882   } note * = this
  2883   show ?thesis
  2884   apply (rule iffI)
  2885   apply (cut_tac linorder_linear [of 0 x], safe)
  2886   apply (drule cos_zero_lemma, assumption+)
  2887   apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
  2888   apply (auto dest: *)
  2889   done
  2890 qed
  2891 
  2892 (* ditto: but to a lesser extent *)
  2893 lemma sin_zero_iff:
  2894      "(sin x = 0) =
  2895       ((\<exists>n::nat. even n & (x = real n * (pi/2))) |
  2896        (\<exists>n::nat. even n & (x = -(real n * (pi/2)))))"
  2897 apply (rule iffI)
  2898 apply (cut_tac linorder_linear [of 0 x], safe)
  2899 apply (drule sin_zero_lemma, assumption+)
  2900 apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
  2901 apply (force simp add: minus_equation_iff [of x])
  2902 apply (auto elim: evenE)
  2903 done
  2904 
  2905 lemma cos_monotone_0_pi:
  2906   assumes "0 \<le> y" and "y < x" and "x \<le> pi"
  2907   shows "cos x < cos y"
  2908 proof -
  2909   have "- (x - y) < 0" using assms by auto
  2910 
  2911   from MVT2[OF `y < x` DERIV_cos[THEN impI, THEN allI]]
  2912   obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z"
  2913     by auto
  2914   hence "0 < z" and "z < pi" using assms by auto
  2915   hence "0 < sin z" using sin_gt_zero_pi by auto
  2916   hence "cos x - cos y < 0"
  2917     unfolding cos_diff minus_mult_commute[symmetric]
  2918     using `- (x - y) < 0` by (rule mult_pos_neg2)
  2919   thus ?thesis by auto
  2920 qed
  2921 
  2922 lemma cos_monotone_0_pi':
  2923   assumes "0 \<le> y" and "y \<le> x" and "x \<le> pi"
  2924   shows "cos x \<le> cos y"
  2925 proof (cases "y < x")
  2926   case True
  2927   show ?thesis
  2928     using cos_monotone_0_pi[OF `0 \<le> y` True `x \<le> pi`] by auto
  2929 next
  2930   case False
  2931   hence "y = x" using `y \<le> x` by auto
  2932   thus ?thesis by auto
  2933 qed
  2934 
  2935 lemma cos_monotone_minus_pi_0:
  2936   assumes "-pi \<le> y" and "y < x" and "x \<le> 0"
  2937   shows "cos y < cos x"
  2938 proof -
  2939   have "0 \<le> -x" and "-x < -y" and "-y \<le> pi"
  2940     using assms by auto
  2941   from cos_monotone_0_pi[OF this] show ?thesis
  2942     unfolding cos_minus .
  2943 qed
  2944 
  2945 lemma cos_monotone_minus_pi_0':
  2946   assumes "-pi \<le> y" and "y \<le> x" and "x \<le> 0"
  2947   shows "cos y \<le> cos x"
  2948 proof (cases "y < x")
  2949   case True
  2950   show ?thesis using cos_monotone_minus_pi_0[OF `-pi \<le> y` True `x \<le> 0`]
  2951     by auto
  2952 next
  2953   case False
  2954   hence "y = x" using `y \<le> x` by auto
  2955   thus ?thesis by auto
  2956 qed
  2957 
  2958 lemma sin_monotone_2pi':
  2959   assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2"
  2960   shows "sin y \<le> sin x"
  2961 proof -
  2962   have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
  2963     using pi_ge_two and assms by auto
  2964   from cos_monotone_0_pi'[OF this] show ?thesis
  2965     unfolding minus_sin_cos_eq[symmetric] by auto
  2966 qed
  2967 
  2968 
  2969 subsection {* Tangent *}
  2970 
  2971 definition tan :: "real \<Rightarrow> real"
  2972   where "tan = (\<lambda>x. sin x / cos x)"
  2973 
  2974 lemma tan_zero [simp]: "tan 0 = 0"
  2975   by (simp add: tan_def)
  2976 
  2977 lemma tan_pi [simp]: "tan pi = 0"
  2978   by (simp add: tan_def)
  2979 
  2980 lemma tan_npi [simp]: "tan (real (n::nat) * pi) = 0"
  2981   by (simp add: tan_def)
  2982 
  2983 lemma tan_minus [simp]: "tan (-x) = - tan x"
  2984   by (simp add: tan_def)
  2985 
  2986 lemma tan_periodic [simp]: "tan (x + 2*pi) = tan x"
  2987   by (simp add: tan_def)
  2988 
  2989 lemma lemma_tan_add1:
  2990   "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> 1 - tan x * tan y = cos (x + y)/(cos x * cos y)"
  2991   by (simp add: tan_def cos_add field_simps)
  2992 
  2993 lemma add_tan_eq:
  2994   "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> tan x + tan y = sin(x + y)/(cos x * cos y)"
  2995   by (simp add: tan_def sin_add field_simps)
  2996 
  2997 lemma tan_add:
  2998      "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]
  2999       ==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
  3000   by (simp add: add_tan_eq lemma_tan_add1, simp add: tan_def)
  3001 
  3002 lemma tan_double:
  3003      "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]
  3004       ==> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)"
  3005   using tan_add [of x x] by (simp add: power2_eq_square)
  3006 
  3007 lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
  3008   by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
  3009 
  3010 lemma tan_less_zero:
  3011   assumes lb: "- pi/2 < x" and "x < 0"
  3012   shows "tan x < 0"
  3013 proof -
  3014   have "0 < tan (- x)" using assms by (simp only: tan_gt_zero)
  3015   thus ?thesis by simp
  3016 qed
  3017 
  3018 lemma tan_half: "tan x = sin (2 * x) / (cos (2 * x) + 1)"
  3019   unfolding tan_def sin_double cos_double sin_squared_eq
  3020   by (simp add: power2_eq_square)
  3021 
  3022 lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
  3023   unfolding tan_def
  3024   by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
  3025 
  3026 lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
  3027   by (rule DERIV_tan [THEN DERIV_isCont])
  3028 
  3029 lemma isCont_tan' [simp]:
  3030   "\<lbrakk>isCont f a; cos (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. tan (f x)) a"
  3031   by (rule isCont_o2 [OF _ isCont_tan])
  3032 
  3033 lemma tendsto_tan [tendsto_intros]:
  3034   "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
  3035   by (rule isCont_tendsto_compose [OF isCont_tan])
  3036 
  3037 lemma continuous_tan:
  3038   "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
  3039   unfolding continuous_def by (rule tendsto_tan)
  3040 
  3041 lemma isCont_tan'' [continuous_intros]:
  3042   "continuous (at x) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. tan (f x))"
  3043   unfolding continuous_at by (rule tendsto_tan)
  3044 
  3045 lemma continuous_within_tan [continuous_intros]:
  3046   "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
  3047   unfolding continuous_within by (rule tendsto_tan)
  3048 
  3049 lemma continuous_on_tan [continuous_intros]:
  3050   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
  3051   unfolding continuous_on_def by (auto intro: tendsto_tan)
  3052 
  3053 lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) -- pi/2 --> 0"
  3054   by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
  3055 
  3056 lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
  3057   apply (cut_tac LIM_cos_div_sin)
  3058   apply (simp only: LIM_eq)
  3059   apply (drule_tac x = "inverse y" in spec, safe, force)
  3060   apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
  3061   apply (rule_tac x = "(pi/2) - e" in exI)
  3062   apply (simp (no_asm_simp))
  3063   apply (drule_tac x = "(pi/2) - e" in spec)
  3064   apply (auto simp add: tan_def sin_diff cos_diff)
  3065   apply (rule inverse_less_iff_less [THEN iffD1])
  3066   apply (auto simp add: divide_inverse)
  3067   apply (rule mult_pos_pos)
  3068   apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
  3069   apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult.commute)
  3070   done
  3071 
  3072 lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
  3073   apply (frule order_le_imp_less_or_eq, safe)
  3074    prefer 2 apply force
  3075   apply (drule lemma_tan_total, safe)
  3076   apply (cut_tac f = tan and a = 0 and b = x and y = y in IVT_objl)
  3077   apply (auto intro!: DERIV_tan [THEN DERIV_isCont])
  3078   apply (drule_tac y = xa in order_le_imp_less_or_eq)
  3079   apply (auto dest: cos_gt_zero)
  3080   done
  3081 
  3082 lemma lemma_tan_total1: "\<exists>x. -(pi/2) < x & x < (pi/2) & tan x = y"
  3083   apply (cut_tac linorder_linear [of 0 y], safe)
  3084   apply (drule tan_total_pos)
  3085   apply (cut_tac [2] y="-y" in tan_total_pos, safe)
  3086   apply (rule_tac [3] x = "-x" in exI)
  3087   apply (auto del: exI intro!: exI)
  3088   done
  3089 
  3090 lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
  3091   apply (cut_tac y = y in lemma_tan_total1, auto)
  3092   apply hypsubst_thin
  3093   apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
  3094   apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
  3095   apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
  3096   apply (rule_tac [4] Rolle)
  3097   apply (rule_tac [2] Rolle)
  3098   apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
  3099               simp add: real_differentiable_def)
  3100   txt{*Now, simulate TRYALL*}
  3101   apply (rule_tac [!] DERIV_tan asm_rl)
  3102   apply (auto dest!: DERIV_unique [OF _ DERIV_tan]
  3103               simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym])
  3104   done
  3105 
  3106 lemma tan_monotone:
  3107   assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2"
  3108   shows "tan y < tan x"
  3109 proof -
  3110   have "\<forall>x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)"
  3111   proof (rule allI, rule impI)
  3112     fix x' :: real
  3113     assume "y \<le> x' \<and> x' \<le> x"
  3114     hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto
  3115     from cos_gt_zero_pi[OF this]
  3116     have "cos x' \<noteq> 0" by auto
  3117     thus "DERIV tan x' :> inverse ((cos x')\<^sup>2)" by (rule DERIV_tan)
  3118   qed
  3119   from MVT2[OF `y < x` this]
  3120   obtain z where "y < z" and "z < x"
  3121     and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto
  3122   hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto
  3123   hence "0 < cos z" using cos_gt_zero_pi by auto
  3124   hence inv_pos: "0 < inverse ((cos z)\<^sup>2)" by auto
  3125   have "0 < x - y" using `y < x` by auto
  3126   with inv_pos have "0 < tan x - tan y" unfolding tan_diff by auto
  3127   thus ?thesis by auto
  3128 qed
  3129 
  3130 lemma tan_monotone':
  3131   assumes "- (pi / 2) < y"
  3132     and "y < pi / 2"
  3133     and "- (pi / 2) < x"
  3134     and "x < pi / 2"
  3135   shows "(y < x) = (tan y < tan x)"
  3136 proof
  3137   assume "y < x"
  3138   thus "tan y < tan x"
  3139     using tan_monotone and `- (pi / 2) < y` and `x < pi / 2` by auto
  3140 next
  3141   assume "tan y < tan x"
  3142   show "y < x"
  3143   proof (rule ccontr)
  3144     assume "\<not> y < x" hence "x \<le> y" by auto
  3145     hence "tan x \<le> tan y"
  3146     proof (cases "x = y")
  3147       case True thus ?thesis by auto
  3148     next
  3149       case False hence "x < y" using `x \<le> y` by auto
  3150       from tan_monotone[OF `- (pi/2) < x` this `y < pi / 2`] show ?thesis by auto
  3151     qed
  3152     thus False using `tan y < tan x` by auto
  3153   qed
  3154 qed
  3155 
  3156 lemma tan_inverse: "1 / (tan y) = tan (pi / 2 - y)"
  3157   unfolding tan_def sin_cos_eq[of y] cos_sin_eq[of y] by auto
  3158 
  3159 lemma tan_periodic_pi[simp]: "tan (x + pi) = tan x"
  3160   by (simp add: tan_def)
  3161 
  3162 lemma tan_periodic_nat[simp]:
  3163   fixes n :: nat
  3164   shows "tan (x + real n * pi) = tan x"
  3165 proof (induct n arbitrary: x)
  3166   case 0
  3167   then show ?case by simp
  3168 next
  3169   case (Suc n)
  3170   have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi"
  3171     unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
  3172   show ?case unfolding split_pi_off using Suc by auto
  3173 qed
  3174 
  3175 lemma tan_periodic_int[simp]: fixes i :: int shows "tan (x + real i * pi) = tan x"
  3176 proof (cases "0 \<le> i")
  3177   case True
  3178   hence i_nat: "real i = real (nat i)" by auto
  3179   show ?thesis unfolding i_nat by auto
  3180 next
  3181   case False
  3182   hence i_nat: "real i = - real (nat (-i))" by auto
  3183   have "tan x = tan (x + real i * pi - real i * pi)"
  3184     by auto
  3185   also have "\<dots> = tan (x + real i * pi)"
  3186     unfolding i_nat mult_minus_left diff_minus_eq_add by (rule tan_periodic_nat)
  3187   finally show ?thesis by auto
  3188 qed
  3189 
  3190 lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
  3191   using tan_periodic_int[of _ "numeral n" ] unfolding real_numeral .
  3192 
  3193 subsection {* Inverse Trigonometric Functions *}
  3194 
  3195 definition arcsin :: "real => real"
  3196   where "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
  3197 
  3198 definition arccos :: "real => real"
  3199   where "arccos y = (THE x. 0 \<le> x & x \<le> pi & cos x = y)"
  3200 
  3201 definition arctan :: "real => real"
  3202   where "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)"
  3203 
  3204 lemma arcsin:
  3205   "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow>
  3206     -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2 & sin(arcsin y) = y"
  3207   unfolding arcsin_def by (rule theI' [OF sin_total])
  3208 
  3209 lemma arcsin_pi:
  3210   "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi & sin(arcsin y) = y"
  3211   apply (drule (1) arcsin)
  3212   apply (force intro: order_trans)
  3213   done
  3214 
  3215 lemma sin_arcsin [simp]: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> sin(arcsin y) = y"
  3216   by (blast dest: arcsin)
  3217 
  3218 lemma arcsin_bounded: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2"
  3219   by (blast dest: arcsin)
  3220 
  3221 lemma arcsin_lbound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y"
  3222   by (blast dest: arcsin)
  3223 
  3224 lemma arcsin_ubound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin y \<le> pi/2"
  3225   by (blast dest: arcsin)
  3226 
  3227 lemma arcsin_lt_bounded:
  3228      "[| -1 < y; y < 1 |] ==> -(pi/2) < arcsin y & arcsin y < pi/2"
  3229   apply (frule order_less_imp_le)
  3230   apply (frule_tac y = y in order_less_imp_le)
  3231   apply (frule arcsin_bounded)
  3232   apply (safe, simp)
  3233   apply (drule_tac y = "arcsin y" in order_le_imp_less_or_eq)
  3234   apply (drule_tac [2] y = "pi/2" in order_le_imp_less_or_eq, safe)
  3235   apply (drule_tac [!] f = sin in arg_cong, auto)
  3236   done
  3237 
  3238 lemma arcsin_sin: "[|-(pi/2) \<le> x; x \<le> pi/2 |] ==> arcsin(sin x) = x"
  3239   apply (unfold arcsin_def)
  3240   apply (rule the1_equality)
  3241   apply (rule sin_total, auto)
  3242   done
  3243 
  3244 lemma arccos:
  3245      "[| -1 \<le> y; y \<le> 1 |]
  3246       ==> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
  3247   unfolding arccos_def by (rule theI' [OF cos_total])
  3248 
  3249 lemma cos_arccos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arccos y) = y"
  3250   by (blast dest: arccos)
  3251 
  3252 lemma arccos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y & arccos y \<le> pi"
  3253   by (blast dest: arccos)
  3254 
  3255 lemma arccos_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y"
  3256   by (blast dest: arccos)
  3257 
  3258 lemma arccos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arccos y \<le> pi"
  3259   by (blast dest: arccos)
  3260 
  3261 lemma arccos_lt_bounded:
  3262      "[| -1 < y; y < 1 |]
  3263       ==> 0 < arccos y & arccos y < pi"
  3264   apply (frule order_less_imp_le)
  3265   apply (frule_tac y = y in order_less_imp_le)
  3266   apply (frule arccos_bounded, auto)
  3267   apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
  3268   apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
  3269   apply (drule_tac [!] f = cos in arg_cong, auto)
  3270   done
  3271 
  3272 lemma arccos_cos: "[|0 \<le> x; x \<le> pi |] ==> arccos(cos x) = x"
  3273   apply (simp add: arccos_def)
  3274   apply (auto intro!: the1_equality cos_total)
  3275   done
  3276 
  3277 lemma arccos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arccos(cos x) = -x"
  3278   apply (simp add: arccos_def)
  3279   apply (auto intro!: the1_equality cos_total)
  3280   done
  3281 
  3282 lemma cos_arcsin: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> cos (arcsin x) = sqrt (1 - x\<^sup>2)"
  3283   apply (subgoal_tac "x\<^sup>2 \<le> 1")
  3284   apply (rule power2_eq_imp_eq)
  3285   apply (simp add: cos_squared_eq)
  3286   apply (rule cos_ge_zero)
  3287   apply (erule (1) arcsin_lbound)
  3288   apply (erule (1) arcsin_ubound)
  3289   apply simp
  3290   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
  3291   apply (rule power_mono, simp, simp)
  3292   done
  3293 
  3294 lemma sin_arccos: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> sin (arccos x) = sqrt (1 - x\<^sup>2)"
  3295   apply (subgoal_tac "x\<^sup>2 \<le> 1")
  3296   apply (rule power2_eq_imp_eq)
  3297   apply (simp add: sin_squared_eq)
  3298   apply (rule sin_ge_zero)
  3299   apply (erule (1) arccos_lbound)
  3300   apply (erule (1) arccos_ubound)
  3301   apply simp
  3302   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
  3303   apply (rule power_mono, simp, simp)
  3304   done
  3305 
  3306 lemma arctan [simp]: "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
  3307   unfolding arctan_def by (rule theI' [OF tan_total])
  3308 
  3309 lemma tan_arctan: "tan (arctan y) = y"
  3310   by auto
  3311 
  3312 lemma arctan_bounded: "- (pi/2) < arctan y  & arctan y < pi/2"
  3313   by (auto simp only: arctan)
  3314 
  3315 lemma arctan_lbound: "- (pi/2) < arctan y"
  3316   by auto
  3317 
  3318 lemma arctan_ubound: "arctan y < pi/2"
  3319   by (auto simp only: arctan)
  3320 
  3321 lemma arctan_unique:
  3322   assumes "-(pi/2) < x"
  3323     and "x < pi/2"
  3324     and "tan x = y"
  3325   shows "arctan y = x"
  3326   using assms arctan [of y] tan_total [of y] by (fast elim: ex1E)
  3327 
  3328 lemma arctan_tan: "-(pi/2) < x \<Longrightarrow> x < pi/2 \<Longrightarrow> arctan (tan x) = x"
  3329   by (rule arctan_unique) simp_all
  3330 
  3331 lemma arctan_zero_zero [simp]: "arctan 0 = 0"
  3332   by (rule arctan_unique) simp_all
  3333 
  3334 lemma arctan_minus: "arctan (- x) = - arctan x"
  3335   apply (rule arctan_unique)
  3336   apply (simp only: neg_less_iff_less arctan_ubound)
  3337   apply (metis minus_less_iff arctan_lbound)
  3338   apply simp
  3339   done
  3340 
  3341 lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
  3342   by (intro less_imp_neq [symmetric] cos_gt_zero_pi
  3343     arctan_lbound arctan_ubound)
  3344 
  3345 lemma cos_arctan: "cos (arctan x) = 1 / sqrt (1 + x\<^sup>2)"
  3346 proof (rule power2_eq_imp_eq)
  3347   have "0 < 1 + x\<^sup>2" by (simp add: add_pos_nonneg)
  3348   show "0 \<le> 1 / sqrt (1 + x\<^sup>2)" by simp
  3349   show "0 \<le> cos (arctan x)"
  3350     by (intro less_imp_le cos_gt_zero_pi arctan_lbound arctan_ubound)
  3351   have "(cos (arctan x))\<^sup>2 * (1 + (tan (arctan x))\<^sup>2) = 1"
  3352     unfolding tan_def by (simp add: distrib_left power_divide)
  3353   thus "(cos (arctan x))\<^sup>2 = (1 / sqrt (1 + x\<^sup>2))\<^sup>2"
  3354     using `0 < 1 + x\<^sup>2` by (simp add: power_divide eq_divide_eq)
  3355 qed
  3356 
  3357 lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<^sup>2)"
  3358   using add_pos_nonneg [OF zero_less_one zero_le_power2 [of x]]
  3359   using tan_arctan [of x] unfolding tan_def cos_arctan
  3360   by (simp add: eq_divide_eq)
  3361 
  3362 lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
  3363   apply (rule power_inverse [THEN subst])
  3364   apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
  3365   apply (auto dest: field_power_not_zero
  3366           simp add: power_mult_distrib distrib_right power_divide tan_def
  3367                     mult.assoc power_inverse [symmetric])
  3368   done
  3369 
  3370 lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
  3371   by (metis tan_monotone' arctan_lbound arctan_ubound tan_arctan)
  3372 
  3373 lemma arctan_le_iff: "arctan x \<le> arctan y \<longleftrightarrow> x \<le> y"
  3374   by (simp only: not_less [symmetric] arctan_less_iff)
  3375 
  3376 lemma arctan_eq_iff: "arctan x = arctan y \<longleftrightarrow> x = y"
  3377   by (simp only: eq_iff [where 'a=real] arctan_le_iff)
  3378 
  3379 lemma zero_less_arctan_iff [simp]: "0 < arctan x \<longleftrightarrow> 0 < x"
  3380   using arctan_less_iff [of 0 x] by simp
  3381 
  3382 lemma arctan_less_zero_iff [simp]: "arctan x < 0 \<longleftrightarrow> x < 0"
  3383   using arctan_less_iff [of x 0] by simp
  3384 
  3385 lemma zero_le_arctan_iff [simp]: "0 \<le> arctan x \<longleftrightarrow> 0 \<le> x"
  3386   using arctan_le_iff [of 0 x] by simp
  3387 
  3388 lemma arctan_le_zero_iff [simp]: "arctan x \<le> 0 \<longleftrightarrow> x \<le> 0"
  3389   using arctan_le_iff [of x 0] by simp
  3390 
  3391 lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
  3392   using arctan_eq_iff [of x 0] by simp
  3393 
  3394 lemma continuous_on_arcsin': "continuous_on {-1 .. 1} arcsin"
  3395 proof -
  3396   have "continuous_on (sin ` {- pi / 2 .. pi / 2}) arcsin"
  3397     by (rule continuous_on_inv) (auto intro: continuous_intros simp: arcsin_sin)
  3398   also have "sin ` {- pi / 2 .. pi / 2} = {-1 .. 1}"
  3399   proof safe
  3400     fix x :: real
  3401     assume "x \<in> {-1..1}"
  3402     then show "x \<in> sin ` {- pi / 2..pi / 2}"
  3403       using arcsin_lbound arcsin_ubound
  3404       by (intro image_eqI[where x="arcsin x"]) auto
  3405   qed simp
  3406   finally show ?thesis .
  3407 qed
  3408 
  3409 lemma continuous_on_arcsin [continuous_intros]:
  3410   "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))"
  3411   using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arcsin']]
  3412   by (auto simp: comp_def subset_eq)
  3413 
  3414 lemma isCont_arcsin: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> isCont arcsin x"
  3415   using continuous_on_arcsin'[THEN continuous_on_subset, of "{ -1 <..< 1 }"]
  3416   by (auto simp: continuous_on_eq_continuous_at subset_eq)
  3417 
  3418 lemma continuous_on_arccos': "continuous_on {-1 .. 1} arccos"
  3419 proof -
  3420   have "continuous_on (cos ` {0 .. pi}) arccos"
  3421     by (rule continuous_on_inv) (auto intro: continuous_intros simp: arccos_cos)
  3422   also have "cos ` {0 .. pi} = {-1 .. 1}"
  3423   proof safe
  3424     fix x :: real
  3425     assume "x \<in> {-1..1}"
  3426     then show "x \<in> cos ` {0..pi}"
  3427       using arccos_lbound arccos_ubound
  3428       by (intro image_eqI[where x="arccos x"]) auto
  3429   qed simp
  3430   finally show ?thesis .
  3431 qed
  3432 
  3433 lemma continuous_on_arccos [continuous_intros]:
  3434   "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))"
  3435   using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arccos']]
  3436   by (auto simp: comp_def subset_eq)
  3437 
  3438 lemma isCont_arccos: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> isCont arccos x"
  3439   using continuous_on_arccos'[THEN continuous_on_subset, of "{ -1 <..< 1 }"]
  3440   by (auto simp: continuous_on_eq_continuous_at subset_eq)
  3441 
  3442 lemma isCont_arctan: "isCont arctan x"
  3443   apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify)
  3444   apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
  3445   apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
  3446   apply (erule (1) isCont_inverse_function2 [where f=tan])
  3447   apply (metis arctan_tan order_le_less_trans order_less_le_trans)
  3448   apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
  3449   done
  3450 
  3451 lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
  3452   by (rule isCont_tendsto_compose [OF isCont_arctan])
  3453 
  3454 lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
  3455   unfolding continuous_def by (rule tendsto_arctan)
  3456 
  3457 lemma continuous_on_arctan [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
  3458   unfolding continuous_on_def by (auto intro: tendsto_arctan)
  3459 
  3460 lemma DERIV_arcsin:
  3461   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<^sup>2))"
  3462   apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
  3463   apply (rule DERIV_cong [OF DERIV_sin])
  3464   apply (simp add: cos_arcsin)
  3465   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  3466   apply (rule power_strict_mono, simp, simp, simp)
  3467   apply assumption
  3468   apply assumption
  3469   apply simp
  3470   apply (erule (1) isCont_arcsin)
  3471   done
  3472 
  3473 lemma DERIV_arccos:
  3474   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<^sup>2))"
  3475   apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
  3476   apply (rule DERIV_cong [OF DERIV_cos])
  3477   apply (simp add: sin_arccos)
  3478   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  3479   apply (rule power_strict_mono, simp, simp, simp)
  3480   apply assumption
  3481   apply assumption
  3482   apply simp
  3483   apply (erule (1) isCont_arccos)
  3484   done
  3485 
  3486 lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)"
  3487   apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
  3488   apply (rule DERIV_cong [OF DERIV_tan])
  3489   apply (rule cos_arctan_not_zero)
  3490   apply (simp add: power_inverse tan_sec [symmetric])
  3491   apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
  3492   apply (simp add: add_pos_nonneg)
  3493   apply (simp, simp, simp, rule isCont_arctan)
  3494   done
  3495 
  3496 declare
  3497   DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
  3498   DERIV_arccos[THEN DERIV_chain2, derivative_intros]
  3499   DERIV_arctan[THEN DERIV_chain2, derivative_intros]
  3500 
  3501 lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
  3502   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])
  3503      (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
  3504            intro!: tan_monotone exI[of _ "pi/2"])
  3505 
  3506 lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
  3507   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])
  3508      (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
  3509            intro!: tan_monotone exI[of _ "pi/2"])
  3510 
  3511 lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"
  3512 proof (rule tendstoI)
  3513   fix e :: real
  3514   assume "0 < e"
  3515   def y \<equiv> "pi/2 - min (pi/2) e"
  3516   then have y: "0 \<le> y" "y < pi/2" "pi/2 \<le> e + y"
  3517     using `0 < e` by auto
  3518 
  3519   show "eventually (\<lambda>x. dist (arctan x) (pi / 2) < e) at_top"
  3520   proof (intro eventually_at_top_dense[THEN iffD2] exI allI impI)
  3521     fix x
  3522     assume "tan y < x"
  3523     then have "arctan (tan y) < arctan x"
  3524       by (simp add: arctan_less_iff)
  3525     with y have "y < arctan x"
  3526       by (subst (asm) arctan_tan) simp_all
  3527     with arctan_ubound[of x, arith] y `0 < e`
  3528     show "dist (arctan x) (pi / 2) < e"
  3529       by (simp add: dist_real_def)
  3530   qed
  3531 qed
  3532 
  3533 lemma tendsto_arctan_at_bot: "(arctan ---> - (pi/2)) at_bot"
  3534   unfolding filterlim_at_bot_mirror arctan_minus
  3535   by (intro tendsto_minus tendsto_arctan_at_top)
  3536 
  3537 
  3538 subsection {* More Theorems about Sin and Cos *}
  3539 
  3540 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
  3541 proof -
  3542   let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
  3543   have nonneg: "0 \<le> ?c"
  3544     by (simp add: cos_ge_zero)
  3545   have "0 = cos (pi / 4 + pi / 4)"
  3546     by simp
  3547   also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
  3548     by (simp only: cos_add power2_eq_square)
  3549   also have "\<dots> = 2 * ?c\<^sup>2 - 1"
  3550     by (simp add: sin_squared_eq)
  3551   finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
  3552     by (simp add: power_divide)
  3553   thus ?thesis
  3554     using nonneg by (rule power2_eq_imp_eq) simp
  3555 qed
  3556 
  3557 lemma cos_30: "cos (pi / 6) = sqrt 3 / 2"
  3558 proof -
  3559   let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
  3560   have pos_c: "0 < ?c"
  3561     by (rule cos_gt_zero, simp, simp)
  3562   have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
  3563     by simp
  3564   also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
  3565     by (simp only: cos_add sin_add)
  3566   also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
  3567     by (simp add: algebra_simps power2_eq_square)
  3568   finally have "?c\<^sup>2 = (sqrt 3 / 2)\<^sup>2"
  3569     using pos_c by (simp add: sin_squared_eq power_divide)
  3570   thus ?thesis
  3571     using pos_c [THEN order_less_imp_le]
  3572     by (rule power2_eq_imp_eq) simp
  3573 qed
  3574 
  3575 lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
  3576   by (simp add: sin_cos_eq cos_45)
  3577 
  3578 lemma sin_60: "sin (pi / 3) = sqrt 3 / 2"
  3579   by (simp add: sin_cos_eq cos_30)
  3580 
  3581 lemma cos_60: "cos (pi / 3) = 1 / 2"
  3582   apply (rule power2_eq_imp_eq)
  3583   apply (simp add: cos_squared_eq sin_60 power_divide)
  3584   apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
  3585   done
  3586 
  3587 lemma sin_30: "sin (pi / 6) = 1 / 2"
  3588   by (simp add: sin_cos_eq cos_60)
  3589 
  3590 lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
  3591   unfolding tan_def by (simp add: sin_30 cos_30)
  3592 
  3593 lemma tan_45: "tan (pi / 4) = 1"
  3594   unfolding tan_def by (simp add: sin_45 cos_45)
  3595 
  3596 lemma tan_60: "tan (pi / 3) = sqrt 3"
  3597   unfolding tan_def by (simp add: sin_60 cos_60)
  3598 
  3599 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
  3600 proof -
  3601   have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
  3602     by (auto simp add: algebra_simps sin_add)
  3603   thus ?thesis
  3604     by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
  3605                   mult.commute [of pi])
  3606 qed
  3607 
  3608 lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
  3609   by (cases "even n") (simp_all add: cos_double mult.assoc)
  3610 
  3611 lemma cos_3over2_pi [simp]: "cos (3 / 2 * pi) = 0"
  3612   apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
  3613   apply (subst cos_add, simp)
  3614   done
  3615 
  3616 lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
  3617   by (auto simp add: mult.assoc)
  3618 
  3619 lemma sin_3over2_pi [simp]: "sin (3 / 2 * pi) = - 1"
  3620   apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
  3621   apply (subst sin_add, simp)
  3622   done
  3623 
  3624 lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
  3625   apply (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib)
  3626   apply auto
  3627   done
  3628 
  3629 lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
  3630   by (auto intro!: derivative_eq_intros)
  3631 
  3632 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
  3633   by (auto simp add: sin_zero_iff elim: evenE)
  3634 
  3635 lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0"
  3636   using sin_cos_squared_add3 [where x = x] by auto
  3637 
  3638 
  3639 subsection {* Machins formula *}
  3640 
  3641 lemma arctan_one: "arctan 1 = pi / 4"
  3642   by (rule arctan_unique, simp_all add: tan_45 m2pi_less_pi)
  3643 
  3644 lemma tan_total_pi4:
  3645   assumes "\<bar>x\<bar> < 1"
  3646   shows "\<exists>z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x"
  3647 proof
  3648   show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x"
  3649     unfolding arctan_one [symmetric] arctan_minus [symmetric]
  3650     unfolding arctan_less_iff using assms by auto
  3651 qed
  3652 
  3653 lemma arctan_add:
  3654   assumes "\<bar>x\<bar> \<le> 1" and "\<bar>y\<bar> < 1"
  3655   shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))"
  3656 proof (rule arctan_unique [symmetric])
  3657   have "- (pi / 4) \<le> arctan x" and "- (pi / 4) < arctan y"
  3658     unfolding arctan_one [symmetric] arctan_minus [symmetric]
  3659     unfolding arctan_le_iff arctan_less_iff using assms by auto
  3660   from add_le_less_mono [OF this]
  3661   show 1: "- (pi / 2) < arctan x + arctan y" by simp
  3662   have "arctan x \<le> pi / 4" and "arctan y < pi / 4"
  3663     unfolding arctan_one [symmetric]
  3664     unfolding arctan_le_iff arctan_less_iff using assms by auto
  3665   from add_le_less_mono [OF this]
  3666   show 2: "arctan x + arctan y < pi / 2" by simp
  3667   show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
  3668     using cos_gt_zero_pi [OF 1 2] by (simp add: tan_add)
  3669 qed
  3670 
  3671 theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)"
  3672 proof -
  3673   have "\<bar>1 / 5\<bar> < (1 :: real)" by auto
  3674   from arctan_add[OF less_imp_le[OF this] this]
  3675   have "2 * arctan (1 / 5) = arctan (5 / 12)" by auto
  3676   moreover
  3677   have "\<bar>5 / 12\<bar> < (1 :: real)" by auto
  3678   from arctan_add[OF less_imp_le[OF this] this]
  3679   have "2 * arctan (5 / 12) = arctan (120 / 119)" by auto
  3680   moreover
  3681   have "\<bar>1\<bar> \<le> (1::real)" and "\<bar>1 / 239\<bar> < (1::real)" by auto
  3682   from arctan_add[OF this]
  3683   have "arctan 1 + arctan (1 / 239) = arctan (120 / 119)" by auto
  3684   ultimately have "arctan 1 + arctan (1 / 239) = 4 * arctan (1 / 5)" by auto
  3685   thus ?thesis unfolding arctan_one by algebra
  3686 qed
  3687 
  3688 
  3689 subsection {* Introducing the arcus tangens power series *}
  3690 
  3691 lemma monoseq_arctan_series:
  3692   fixes x :: real
  3693   assumes "\<bar>x\<bar> \<le> 1"
  3694   shows "monoseq (\<lambda> n. 1 / real (n*2+1) * x^(n*2+1))" (is "monoseq ?a")
  3695 proof (cases "x = 0")
  3696   case True
  3697   thus ?thesis unfolding monoseq_def One_nat_def by auto
  3698 next
  3699   case False
  3700   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
  3701   show "monoseq ?a"
  3702   proof -
  3703     {
  3704       fix n
  3705       fix x :: real
  3706       assume "0 \<le> x" and "x \<le> 1"
  3707       have "1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<le>
  3708         1 / real (Suc (n * 2)) * x ^ Suc (n * 2)"
  3709       proof (rule mult_mono)
  3710         show "1 / real (Suc (Suc n * 2)) \<le> 1 / real (Suc (n * 2))"
  3711           by (rule frac_le) simp_all
  3712         show "0 \<le> 1 / real (Suc (n * 2))"
  3713           by auto
  3714         show "x ^ Suc (Suc n * 2) \<le> x ^ Suc (n * 2)"
  3715           by (rule power_decreasing) (simp_all add: `0 \<le> x` `x \<le> 1`)
  3716         show "0 \<le> x ^ Suc (Suc n * 2)"
  3717           by (rule zero_le_power) (simp add: `0 \<le> x`)
  3718       qed
  3719     } note mono = this
  3720 
  3721     show ?thesis
  3722     proof (cases "0 \<le> x")
  3723       case True from mono[OF this `x \<le> 1`, THEN allI]
  3724       show ?thesis unfolding Suc_eq_plus1[symmetric]
  3725         by (rule mono_SucI2)
  3726     next
  3727       case False
  3728       hence "0 \<le> -x" and "-x \<le> 1" using `-1 \<le> x` by auto
  3729       from mono[OF this]
  3730       have "\<And>n. 1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<ge>
  3731         1 / real (Suc (n * 2)) * x ^ Suc (n * 2)" using `0 \<le> -x` by auto
  3732       thus ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI1[OF allI])
  3733     qed
  3734   qed
  3735 qed
  3736 
  3737 lemma zeroseq_arctan_series:
  3738   fixes x :: real
  3739   assumes "\<bar>x\<bar> \<le> 1"
  3740   shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
  3741 proof (cases "x = 0")
  3742   case True
  3743   thus ?thesis
  3744     unfolding One_nat_def by auto
  3745 next
  3746   case False
  3747   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
  3748   show "?a ----> 0"
  3749   proof (cases "\<bar>x\<bar> < 1")
  3750     case True
  3751     hence "norm x < 1" by auto
  3752     from tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
  3753     have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
  3754       unfolding inverse_eq_divide Suc_eq_plus1 by simp
  3755     then show ?thesis using pos2 by (rule LIMSEQ_linear)
  3756   next
  3757     case False
  3758     hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
  3759     hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x"
  3760       unfolding One_nat_def by auto
  3761     from tendsto_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] tendsto_const[of x]]
  3762     show ?thesis unfolding n_eq Suc_eq_plus1 by auto
  3763   qed
  3764 qed
  3765 
  3766 lemma summable_arctan_series:
  3767   fixes x :: real and n :: nat
  3768   assumes "\<bar>x\<bar> \<le> 1"
  3769   shows "summable (\<lambda> k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
  3770   (is "summable (?c x)")
  3771   by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms])
  3772 
  3773 lemma less_one_imp_sqr_less_one:
  3774   fixes x :: real
  3775   assumes "\<bar>x\<bar> < 1"
  3776   shows "x\<^sup>2 < 1"
  3777 proof -
  3778   have "\<bar>x\<^sup>2\<bar> < 1"
  3779     by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff) 
  3780   thus ?thesis using zero_le_power2 by auto
  3781 qed
  3782 
  3783 lemma DERIV_arctan_series:
  3784   assumes "\<bar> x \<bar> < 1"
  3785   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))"
  3786   (is "DERIV ?arctan _ :> ?Int")
  3787 proof -
  3788   let ?f = "\<lambda>n. if even n then (-1)^(n div 2) * 1 / real (Suc n) else 0"
  3789 
  3790   have n_even: "\<And>n :: nat. even n \<Longrightarrow> 2 * (n div 2) = n"
  3791     by presburger
  3792   then have if_eq: "\<And>n x'. ?f n * real (Suc n) * x'^n =
  3793     (if even n then (-1)^(n div 2) * x'^(2 * (n div 2)) else 0)"
  3794     by auto
  3795 
  3796   {
  3797     fix x :: real
  3798     assume "\<bar>x\<bar> < 1"
  3799     hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
  3800     have "summable (\<lambda> n. (- 1) ^ n * (x\<^sup>2) ^n)"
  3801       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`])
  3802     hence "summable (\<lambda> n. (- 1) ^ n * x^(2*n))" unfolding power_mult .
  3803   } note summable_Integral = this
  3804 
  3805   {
  3806     fix f :: "nat \<Rightarrow> real"
  3807     have "\<And>x. f sums x = (\<lambda> n. if even n then f (n div 2) else 0) sums x"
  3808     proof
  3809       fix x :: real
  3810       assume "f sums x"
  3811       from sums_if[OF sums_zero this]
  3812       show "(\<lambda>n. if even n then f (n div 2) else 0) sums x"
  3813         by auto
  3814     next
  3815       fix x :: real
  3816       assume "(\<lambda> n. if even n then f (n div 2) else 0) sums x"
  3817       from LIMSEQ_linear[OF this[unfolded sums_def] pos2, unfolded sum_split_even_odd[unfolded mult.commute]]
  3818       show "f sums x" unfolding sums_def by auto
  3819     qed
  3820     hence "op sums f = op sums (\<lambda> n. if even n then f (n div 2) else 0)" ..
  3821   } note sums_even = this
  3822 
  3823   have Int_eq: "(\<Sum>n. ?f n * real (Suc n) * x^n) = ?Int"
  3824     unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * x ^ (2 * n)", symmetric]
  3825     by auto
  3826 
  3827   {
  3828     fix x :: real
  3829     have if_eq': "\<And>n. (if even n then (- 1) ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
  3830       (if even n then (- 1) ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
  3831       using n_even by auto
  3832     have idx_eq: "\<And>n. n * 2 + 1 = Suc (2 * n)" by auto
  3833     have "(\<Sum>n. ?f n * x^(Suc n)) = ?arctan x"
  3834       unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
  3835       by auto
  3836   } note arctan_eq = this
  3837 
  3838   have "DERIV (\<lambda> x. \<Sum> n. ?f n * x^(Suc n)) x :> (\<Sum> n. ?f n * real (Suc n) * x^n)"
  3839   proof (rule DERIV_power_series')
  3840     show "x \<in> {- 1 <..< 1}" using `\<bar> x \<bar> < 1` by auto
  3841     {
  3842       fix x' :: real
  3843       assume x'_bounds: "x' \<in> {- 1 <..< 1}"
  3844       then have "\<bar>x'\<bar> < 1" by auto
  3845       then
  3846         have *: "summable (\<lambda>n. (- 1) ^ n * x' ^ (2 * n))"
  3847         by (rule summable_Integral)
  3848       let ?S = "\<Sum> n. (-1)^n * x'^(2 * n)"
  3849       show "summable (\<lambda> n. ?f n * real (Suc n) * x'^n)" unfolding if_eq
  3850         apply (rule sums_summable [where l="0 + ?S"])
  3851         apply (rule sums_if)
  3852         apply (rule sums_zero)
  3853         apply (rule summable_sums)
  3854         apply (rule *)
  3855         done
  3856     }
  3857   qed auto
  3858   thus ?thesis unfolding Int_eq arctan_eq .
  3859 qed
  3860 
  3861 lemma arctan_series:
  3862   assumes "\<bar> x \<bar> \<le> 1"
  3863   shows "arctan x = (\<Sum>k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
  3864   (is "_ = suminf (\<lambda> n. ?c x n)")
  3865 proof -
  3866   let ?c' = "\<lambda>x n. (-1)^n * x^(n*2)"
  3867 
  3868   {
  3869     fix r x :: real
  3870     assume "0 < r" and "r < 1" and "\<bar> x \<bar> < r"
  3871     have "\<bar>x\<bar> < 1" using `r < 1` and `\<bar>x\<bar> < r` by auto
  3872     from DERIV_arctan_series[OF this] have "DERIV (\<lambda> x. suminf (?c x)) x :> (suminf (?c' x))" .
  3873   } note DERIV_arctan_suminf = this
  3874 
  3875   {
  3876     fix x :: real
  3877     assume "\<bar>x\<bar> \<le> 1"
  3878     note summable_Leibniz[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]]
  3879   } note arctan_series_borders = this
  3880 
  3881   {
  3882     fix x :: real
  3883     assume "\<bar>x\<bar> < 1"
  3884     have "arctan x = (\<Sum>k. ?c x k)"
  3885     proof -
  3886       obtain r where "\<bar>x\<bar> < r" and "r < 1"
  3887         using dense[OF `\<bar>x\<bar> < 1`] by blast
  3888       hence "0 < r" and "-r < x" and "x < r" by auto
  3889 
  3890       have suminf_eq_arctan_bounded: "\<And>x a b. \<lbrakk> -r < a ; b < r ; a < b ; a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow>
  3891         suminf (?c x) - arctan x = suminf (?c a) - arctan a"
  3892       proof -
  3893         fix x a b
  3894         assume "-r < a" and "b < r" and "a < b" and "a \<le> x" and "x \<le> b"
  3895         hence "\<bar>x\<bar> < r" by auto
  3896         show "suminf (?c x) - arctan x = suminf (?c a) - arctan a"
  3897         proof (rule DERIV_isconst2[of "a" "b"])
  3898           show "a < b" and "a \<le> x" and "x \<le> b"
  3899             using `a < b` `a \<le> x` `x \<le> b` by auto
  3900           have "\<forall>x. -r < x \<and> x < r \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
  3901           proof (rule allI, rule impI)
  3902             fix x
  3903             assume "-r < x \<and> x < r"
  3904             hence "\<bar>x\<bar> < r" by auto
  3905             hence "\<bar>x\<bar> < 1" using `r < 1` by auto
  3906             have "\<bar> - (x\<^sup>2) \<bar> < 1"
  3907               using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
  3908             hence "(\<lambda> n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))"
  3909               unfolding real_norm_def[symmetric] by (rule geometric_sums)
  3910             hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))"
  3911               unfolding power_mult_distrib[symmetric] power_mult mult.commute[of _ 2] by auto
  3912             hence suminf_c'_eq_geom: "inverse (1 + x\<^sup>2) = suminf (?c' x)"
  3913               using sums_unique unfolding inverse_eq_divide by auto
  3914             have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))"
  3915               unfolding suminf_c'_eq_geom
  3916               by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
  3917             from DERIV_diff [OF this DERIV_arctan]
  3918             show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
  3919               by auto
  3920           qed
  3921           hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
  3922             using `-r < a` `b < r` by auto
  3923           thus "\<forall> y. a < y \<and> y < b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
  3924             using `\<bar>x\<bar> < r` by auto
  3925           show "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> isCont (\<lambda> x. suminf (?c x) - arctan x) y"
  3926             using DERIV_in_rball DERIV_isCont by auto
  3927         qed
  3928       qed
  3929 
  3930       have suminf_arctan_zero: "suminf (?c 0) - arctan 0 = 0"
  3931         unfolding Suc_eq_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero
  3932         by auto
  3933 
  3934       have "suminf (?c x) - arctan x = 0"
  3935       proof (cases "x = 0")
  3936         case True
  3937         thus ?thesis using suminf_arctan_zero by auto
  3938       next
  3939         case False
  3940         hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
  3941         have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
  3942           by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
  3943             (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  3944         moreover
  3945         have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
  3946           by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
  3947              (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  3948         ultimately
  3949         show ?thesis using suminf_arctan_zero by auto
  3950       qed
  3951       thus ?thesis by auto
  3952     qed
  3953   } note when_less_one = this
  3954 
  3955   show "arctan x = suminf (\<lambda> n. ?c x n)"
  3956   proof (cases "\<bar>x\<bar> < 1")
  3957     case True
  3958     thus ?thesis by (rule when_less_one)
  3959   next
  3960     case False
  3961     hence "\<bar>x\<bar> = 1" using `\<bar>x\<bar> \<le> 1` by auto
  3962     let ?a = "\<lambda>x n. \<bar>1 / real (n*2+1) * x^(n*2+1)\<bar>"
  3963     let ?diff = "\<lambda> x n. \<bar> arctan x - (\<Sum> i<n. ?c x i)\<bar>"
  3964     {
  3965       fix n :: nat
  3966       have "0 < (1 :: real)" by auto
  3967       moreover
  3968       {
  3969         fix x :: real
  3970         assume "0 < x" and "x < 1"
  3971         hence "\<bar>x\<bar> \<le> 1" and "\<bar>x\<bar> < 1" by auto
  3972         from `0 < x` have "0 < 1 / real (0 * 2 + (1::nat)) * x ^ (0 * 2 + 1)"
  3973           by auto
  3974         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]
  3975         have "0 < 1 / real (n*2+1) * x^(n*2+1)"
  3976           by (rule mult_pos_pos, auto simp only: zero_less_power[OF `0 < x`], auto)
  3977         hence a_pos: "?a x n = 1 / real (n*2+1) * x^(n*2+1)"
  3978           by (rule abs_of_pos)
  3979         have "?diff x n \<le> ?a x n"
  3980         proof (cases "even n")
  3981           case True
  3982           hence sgn_pos: "(-1)^n = (1::real)" by auto
  3983           from `even n` obtain m where "n = 2 * m" ..
  3984           then have "2 * m = n" ..
  3985           from bounds[of m, unfolded this atLeastAtMost_iff]
  3986           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))"
  3987             by auto
  3988           also have "\<dots> = ?c x n" unfolding One_nat_def by auto
  3989           also have "\<dots> = ?a x n" unfolding sgn_pos a_pos by auto
  3990           finally show ?thesis .
  3991         next
  3992           case False
  3993           hence sgn_neg: "(-1)^n = (-1::real)" by auto
  3994           from `odd n` obtain m where "n = 2 * m + 1" ..
  3995           then have m_def: "2 * m + 1 = n" ..
  3996           hence m_plus: "2 * (m + 1) = n + 1" by auto
  3997           from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
  3998           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))"
  3999             by auto
  4000           also have "\<dots> = - ?c x n" unfolding One_nat_def by auto
  4001           also have "\<dots> = ?a x n" unfolding sgn_neg a_pos by auto
  4002           finally show ?thesis .
  4003         qed
  4004         hence "0 \<le> ?a x n - ?diff x n" by auto
  4005       }
  4006       hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
  4007       moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
  4008         unfolding diff_conv_add_uminus divide_inverse
  4009         by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan
  4010           isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum
  4011           simp del: add_uminus_conv_diff)
  4012       ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
  4013         by (rule LIM_less_bound)
  4014       hence "?diff 1 n \<le> ?a 1 n" by auto
  4015     }
  4016     have "?a 1 ----> 0"
  4017       unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
  4018       by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
  4019     have "?diff 1 ----> 0"
  4020     proof (rule LIMSEQ_I)
  4021       fix r :: real
  4022       assume "0 < r"
  4023       obtain N :: nat where N_I: "\<And>n. N \<le> n \<Longrightarrow> ?a 1 n < r"
  4024         using LIMSEQ_D[OF `?a 1 ----> 0` `0 < r`] by auto
  4025       {
  4026         fix n
  4027         assume "N \<le> n" from `?diff 1 n \<le> ?a 1 n` N_I[OF this]
  4028         have "norm (?diff 1 n - 0) < r" by auto
  4029       }
  4030       thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
  4031     qed
  4032     from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
  4033     have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
  4034     hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
  4035 
  4036     show ?thesis
  4037     proof (cases "x = 1")
  4038       case True
  4039       then show ?thesis by (simp add: `arctan 1 = (\<Sum> i. ?c 1 i)`)
  4040     next
  4041       case False
  4042       hence "x = -1" using `\<bar>x\<bar> = 1` by auto
  4043 
  4044       have "- (pi / 2) < 0" using pi_gt_zero by auto
  4045       have "- (2 * pi) < 0" using pi_gt_zero by auto
  4046 
  4047       have c_minus_minus: "\<And>i. ?c (- 1) i = - ?c 1 i"
  4048         unfolding One_nat_def by auto
  4049 
  4050       have "arctan (- 1) = arctan (tan (-(pi / 4)))"
  4051         unfolding tan_45 tan_minus ..
  4052       also have "\<dots> = - (pi / 4)"
  4053         by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
  4054       also have "\<dots> = - (arctan (tan (pi / 4)))"
  4055         unfolding neg_equal_iff_equal by (rule arctan_tan[symmetric], auto simp add: order_less_trans[OF `- (2 * pi) < 0` pi_gt_zero])
  4056       also have "\<dots> = - (arctan 1)"
  4057         unfolding tan_45 ..
  4058       also have "\<dots> = - (\<Sum> i. ?c 1 i)"
  4059         using `arctan 1 = (\<Sum> i. ?c 1 i)` by auto
  4060       also have "\<dots> = (\<Sum> i. ?c (- 1) i)"
  4061         using suminf_minus[OF sums_summable[OF `(?c 1) sums (arctan 1)`]]
  4062         unfolding c_minus_minus by auto
  4063       finally show ?thesis using `x = -1` by auto
  4064     qed
  4065   qed
  4066 qed
  4067 
  4068 lemma arctan_half:
  4069   fixes x :: real
  4070   shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x\<^sup>2)))"
  4071 proof -
  4072   obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x"
  4073     using tan_total by blast
  4074   hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2"
  4075     by auto
  4076 
  4077   have "0 < cos y" using cos_gt_zero_pi[OF low high] .
  4078   hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y"
  4079     by auto
  4080 
  4081   have "1 + (tan y)\<^sup>2 = 1 + (sin y)\<^sup>2 / (cos y)\<^sup>2"
  4082     unfolding tan_def power_divide ..
  4083   also have "\<dots> = (cos y)\<^sup>2 / (cos y)\<^sup>2 + (sin y)\<^sup>2 / (cos y)\<^sup>2"
  4084     using `cos y \<noteq> 0` by auto
  4085   also have "\<dots> = 1 / (cos y)\<^sup>2"
  4086     unfolding add_divide_distrib[symmetric] sin_cos_squared_add2 ..
  4087   finally have "1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2" .
  4088 
  4089   have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)"
  4090     unfolding tan_def using `cos y \<noteq> 0` by (simp add: field_simps)
  4091   also have "\<dots> = tan y / (1 + 1 / cos y)"
  4092     using `cos y \<noteq> 0` unfolding add_divide_distrib by auto
  4093   also have "\<dots> = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))"
  4094     unfolding cos_sqrt ..
  4095   also have "\<dots> = tan y / (1 + sqrt (1 / (cos y)\<^sup>2))"
  4096     unfolding real_sqrt_divide by auto
  4097   finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)\<^sup>2))"
  4098     unfolding `1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2` .
  4099 
  4100   have "arctan x = y"
  4101     using arctan_tan low high y_eq by auto
  4102   also have "\<dots> = 2 * (arctan (tan (y/2)))"
  4103     using arctan_tan[OF low2 high2] by auto
  4104   also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))"
  4105     unfolding tan_half by auto
  4106   finally show ?thesis
  4107     unfolding eq `tan y = x` .
  4108 qed
  4109 
  4110 lemma arctan_monotone: "x < y \<Longrightarrow> arctan x < arctan y"
  4111   by (simp only: arctan_less_iff)
  4112 
  4113 lemma arctan_monotone': "x \<le> y \<Longrightarrow> arctan x \<le> arctan y"
  4114   by (simp only: arctan_le_iff)
  4115 
  4116 lemma arctan_inverse:
  4117   assumes "x \<noteq> 0"
  4118   shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
  4119 proof (rule arctan_unique)
  4120   show "- (pi / 2) < sgn x * pi / 2 - arctan x"
  4121     using arctan_bounded [of x] assms
  4122     unfolding sgn_real_def
  4123     apply (auto simp add: algebra_simps)
  4124     apply (drule zero_less_arctan_iff [THEN iffD2])
  4125     apply arith
  4126     done
  4127   show "sgn x * pi / 2 - arctan x < pi / 2"
  4128     using arctan_bounded [of "- x"] assms
  4129     unfolding sgn_real_def arctan_minus
  4130     by (auto simp add: algebra_simps)
  4131   show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
  4132     unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
  4133     unfolding sgn_real_def
  4134     by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
  4135 qed
  4136 
  4137 theorem pi_series: "pi / 4 = (\<Sum> k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM")
  4138 proof -
  4139   have "pi / 4 = arctan 1" using arctan_one by auto
  4140   also have "\<dots> = ?SUM" using arctan_series[of 1] by auto
  4141   finally show ?thesis by auto
  4142 qed
  4143 
  4144 
  4145 subsection {* Existence of Polar Coordinates *}
  4146 
  4147 lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<^sup>2 + y\<^sup>2)\<bar> \<le> 1"
  4148   apply (rule power2_le_imp_le [OF _ zero_le_one])
  4149   apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
  4150   done
  4151 
  4152 lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
  4153   by (simp add: abs_le_iff)
  4154 
  4155 lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arccos y) = sqrt (1 - y\<^sup>2)"
  4156   by (simp add: sin_arccos abs_le_iff)
  4157 
  4158 lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]
  4159 
  4160 lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
  4161 
  4162 lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a"
  4163 proof -
  4164   have polar_ex1: "\<And>y. 0 < y \<Longrightarrow> \<exists>r a. x = r * cos a & y = r * sin a"
  4165     apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)
  4166     apply (rule_tac x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))" in exI)
  4167     apply (simp add: cos_arccos_lemma1 sin_arccos_lemma1 power_divide
  4168                      real_sqrt_mult [symmetric] right_diff_distrib)
  4169     done
  4170   show ?thesis
  4171   proof (cases "0::real" y rule: linorder_cases)
  4172     case less 
  4173       then show ?thesis by (rule polar_ex1)
  4174   next
  4175     case equal
  4176       then show ?thesis
  4177         by (force simp add: intro!: cos_zero sin_zero)
  4178   next
  4179     case greater
  4180       then show ?thesis 
  4181      using polar_ex1 [where y="-y"]
  4182     by auto (metis cos_minus minus_minus minus_mult_right sin_minus)
  4183   qed
  4184 qed
  4185 
  4186 end