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