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