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