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