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