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