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