src/HOL/Transcendental.thy
author nipkow
Tue May 13 22:14:12 2014 +0200 (2014-05-13)
changeset 56952 efa2a83d548b
parent 56571 f4635657d66f
child 57025 e7fd64f82876
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/Transcendental.thy
     2     Author:     Jacques D. Fleuriot, University of Cambridge, University of Edinburgh
     3     Author:     Lawrence C Paulson
     4     Author:     Jeremy Avigad
     5 *)
     6 
     7 header{*Power Series, Transcendental Functions etc.*}
     8 
     9 theory Transcendental
    10 imports Fact Series Deriv NthRoot
    11 begin
    12 
    13 subsection {* Properties of Power Series *}
    14 
    15 lemma lemma_realpow_diff:
    16   fixes y :: "'a::monoid_mult"
    17   shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
    18 proof -
    19   assume "p \<le> n"
    20   hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le)
    21   thus ?thesis by (simp add: power_commutes)
    22 qed
    23 
    24 lemma lemma_realpow_diff_sumr2:
    25   fixes y :: "'a::{comm_ring,monoid_mult}"
    26   shows
    27     "x ^ (Suc n) - y ^ (Suc n) =
    28       (x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))"
    29 proof (induct n)
    30   case (Suc n)
    31   have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x ^ n) - y * (y * y ^ n)"
    32     by simp
    33   also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x ^ n)"
    34     by (simp add: algebra_simps)
    35   also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    36     by (simp only: Suc)
    37   also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    38     by (simp only: mult_left_commute)
    39   also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
    40     by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
    41   finally show ?case .
    42 qed simp
    43 
    44 corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *}
    45   fixes x :: "'a::{comm_ring,monoid_mult}"
    46   shows   "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
    47 using lemma_realpow_diff_sumr2[of x "n - 1" y]
    48 by (cases "n = 0") (simp_all add: field_simps)
    49 
    50 lemma lemma_realpow_rev_sumr:
    51    "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
    52     (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
    53   apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
    54   apply (auto simp: image_iff Bex_def intro!: inj_onI)
    55   apply arith
    56   done
    57 
    58 lemma power_diff_1_eq:
    59   fixes x :: "'a::{comm_ring,monoid_mult}"
    60   shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i<n. (x^i))"
    61 using lemma_realpow_diff_sumr2 [of x _ 1] 
    62   by (cases n) auto
    63 
    64 lemma one_diff_power_eq':
    65   fixes x :: "'a::{comm_ring,monoid_mult}"
    66   shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^(n - Suc i))"
    67 using lemma_realpow_diff_sumr2 [of 1 _ x] 
    68   by (cases n) auto
    69 
    70 lemma one_diff_power_eq:
    71   fixes x :: "'a::{comm_ring,monoid_mult}"
    72   shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
    73 by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
    74 
    75 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
    76   x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
    77 
    78 lemma powser_insidea:
    79   fixes x z :: "'a::real_normed_div_algebra"
    80   assumes 1: "summable (\<lambda>n. f n * x ^ n)"
    81     and 2: "norm z < norm x"
    82   shows "summable (\<lambda>n. norm (f n * z ^ n))"
    83 proof -
    84   from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
    85   from 1 have "(\<lambda>n. f n * x ^ n) ----> 0"
    86     by (rule summable_LIMSEQ_zero)
    87   hence "convergent (\<lambda>n. f n * x ^ n)"
    88     by (rule convergentI)
    89   hence "Cauchy (\<lambda>n. f n * x ^ n)"
    90     by (rule convergent_Cauchy)
    91   hence "Bseq (\<lambda>n. f n * x ^ n)"
    92     by (rule Cauchy_Bseq)
    93   then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K"
    94     by (simp add: Bseq_def, safe)
    95   have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
    96                    K * norm (z ^ n) * inverse (norm (x ^ n))"
    97   proof (intro exI allI impI)
    98     fix n::nat
    99     assume "0 \<le> n"
   100     have "norm (norm (f n * z ^ n)) * norm (x ^ n) =
   101           norm (f n * x ^ n) * norm (z ^ n)"
   102       by (simp add: norm_mult abs_mult)
   103     also have "\<dots> \<le> K * norm (z ^ n)"
   104       by (simp only: mult_right_mono 4 norm_ge_zero)
   105     also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))"
   106       by (simp add: x_neq_0)
   107     also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)"
   108       by (simp only: mult_assoc)
   109     finally show "norm (norm (f n * z ^ n)) \<le>
   110                   K * norm (z ^ n) * inverse (norm (x ^ n))"
   111       by (simp add: mult_le_cancel_right x_neq_0)
   112   qed
   113   moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
   114   proof -
   115     from 2 have "norm (norm (z * inverse x)) < 1"
   116       using x_neq_0
   117       by (simp add: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric])
   118     hence "summable (\<lambda>n. norm (z * inverse x) ^ n)"
   119       by (rule summable_geometric)
   120     hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
   121       by (rule summable_mult)
   122     thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
   123       using x_neq_0
   124       by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
   125                     power_inverse norm_power mult_assoc)
   126   qed
   127   ultimately show "summable (\<lambda>n. norm (f n * z ^ n))"
   128     by (rule summable_comparison_test)
   129 qed
   130 
   131 lemma powser_inside:
   132   fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   133   shows
   134     "summable (\<lambda>n. f n * (x ^ n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
   135       summable (\<lambda>n. f n * (z ^ n))"
   136   by (rule powser_insidea [THEN summable_norm_cancel])
   137 
   138 lemma sum_split_even_odd:
   139   fixes f :: "nat \<Rightarrow> real"
   140   shows
   141     "(\<Sum>i<2 * n. if even i then f i else g i) =
   142      (\<Sum>i<n. f (2 * i)) + (\<Sum>i<n. g (2 * i + 1))"
   143 proof (induct n)
   144   case 0
   145   then show ?case by simp
   146 next
   147   case (Suc n)
   148   have "(\<Sum>i<2 * Suc n. if even i then f i else g i) =
   149     (\<Sum>i<n. f (2 * i)) + (\<Sum>i<n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
   150     using Suc.hyps unfolding One_nat_def by auto
   151   also have "\<dots> = (\<Sum>i<Suc n. f (2 * i)) + (\<Sum>i<Suc n. g (2 * i + 1))"
   152     by auto
   153   finally show ?case .
   154 qed
   155 
   156 lemma sums_if':
   157   fixes g :: "nat \<Rightarrow> real"
   158   assumes "g sums x"
   159   shows "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x"
   160   unfolding sums_def
   161 proof (rule LIMSEQ_I)
   162   fix r :: real
   163   assume "0 < r"
   164   from `g sums x`[unfolded sums_def, THEN LIMSEQ_D, OF this]
   165   obtain no where no_eq: "\<And> n. n \<ge> no \<Longrightarrow> (norm (setsum g {..<n} - x) < r)" by blast
   166 
   167   let ?SUM = "\<lambda> m. \<Sum>i<m. if even i then 0 else g ((i - 1) div 2)"
   168   {
   169     fix m
   170     assume "m \<ge> 2 * no"
   171     hence "m div 2 \<ge> no" by auto
   172     have sum_eq: "?SUM (2 * (m div 2)) = setsum g {..< m div 2}"
   173       using sum_split_even_odd by auto
   174     hence "(norm (?SUM (2 * (m div 2)) - x) < r)"
   175       using no_eq unfolding sum_eq using `m div 2 \<ge> no` by auto
   176     moreover
   177     have "?SUM (2 * (m div 2)) = ?SUM m"
   178     proof (cases "even m")
   179       case True
   180       show ?thesis
   181         unfolding even_nat_div_two_times_two[OF True, unfolded numeral_2_eq_2[symmetric]] ..
   182     next
   183       case False
   184       hence "even (Suc m)" by auto
   185       from even_nat_div_two_times_two[OF this, unfolded numeral_2_eq_2[symmetric]]
   186         odd_nat_plus_one_div_two[OF False, unfolded numeral_2_eq_2[symmetric]]
   187       have eq: "Suc (2 * (m div 2)) = m" by auto
   188       hence "even (2 * (m div 2))" using `odd m` by auto
   189       have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
   190       also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto
   191       finally show ?thesis by auto
   192     qed
   193     ultimately have "(norm (?SUM m - x) < r)" by auto
   194   }
   195   thus "\<exists> no. \<forall> m \<ge> no. norm (?SUM m - x) < r" by blast
   196 qed
   197 
   198 lemma sums_if:
   199   fixes g :: "nat \<Rightarrow> real"
   200   assumes "g sums x" and "f sums y"
   201   shows "(\<lambda> n. if even n then f (n div 2) else g ((n - 1) div 2)) sums (x + y)"
   202 proof -
   203   let ?s = "\<lambda> n. if even n then 0 else f ((n - 1) div 2)"
   204   {
   205     fix B T E
   206     have "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)"
   207       by (cases B) auto
   208   } note if_sum = this
   209   have g_sums: "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x"
   210     using sums_if'[OF `g sums x`] .
   211   {
   212     have if_eq: "\<And>B T E. (if \<not> B then T else E) = (if B then E else T)" by auto
   213 
   214     have "?s sums y" using sums_if'[OF `f sums y`] .
   215     from this[unfolded sums_def, THEN LIMSEQ_Suc]
   216     have "(\<lambda> n. if even n then f (n div 2) else 0) sums y"
   217       by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum_reindex if_eq sums_def cong del: if_cong)
   218   }
   219   from sums_add[OF g_sums this] show ?thesis unfolding if_sum .
   220 qed
   221 
   222 subsection {* Alternating series test / Leibniz formula *}
   223 
   224 lemma sums_alternating_upper_lower:
   225   fixes a :: "nat \<Rightarrow> real"
   226   assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0"
   227   shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. -1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. -1^i*a i) ----> l) \<and>
   228              ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. -1^i*a i) ----> l)"
   229   (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
   230 proof (rule nested_sequence_unique)
   231   have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
   232 
   233   show "\<forall>n. ?f n \<le> ?f (Suc n)"
   234   proof
   235     fix n
   236     show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto
   237   qed
   238   show "\<forall>n. ?g (Suc n) \<le> ?g n"
   239   proof
   240     fix n
   241     show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"]
   242       unfolding One_nat_def by auto
   243   qed
   244   show "\<forall>n. ?f n \<le> ?g n"
   245   proof
   246     fix n
   247     show "?f n \<le> ?g n" using fg_diff a_pos
   248       unfolding One_nat_def by auto
   249   qed
   250   show "(\<lambda>n. ?f n - ?g n) ----> 0" unfolding fg_diff
   251   proof (rule LIMSEQ_I)
   252     fix r :: real
   253     assume "0 < r"
   254     with `a ----> 0`[THEN LIMSEQ_D] obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n - 0) < r"
   255       by auto
   256     hence "\<forall>n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
   257     thus "\<exists>N. \<forall>n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
   258   qed
   259 qed
   260 
   261 lemma summable_Leibniz':
   262   fixes a :: "nat \<Rightarrow> real"
   263   assumes a_zero: "a ----> 0"
   264     and a_pos: "\<And> n. 0 \<le> a n"
   265     and a_monotone: "\<And> n. a (Suc n) \<le> a n"
   266   shows summable: "summable (\<lambda> n. (-1)^n * a n)"
   267     and "\<And>n. (\<Sum>i<2*n. (-1)^i*a i) \<le> (\<Sum>i. (-1)^i*a i)"
   268     and "(\<lambda>n. \<Sum>i<2*n. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
   269     and "\<And>n. (\<Sum>i. (-1)^i*a i) \<le> (\<Sum>i<2*n+1. (-1)^i*a i)"
   270     and "(\<lambda>n. \<Sum>i<2*n+1. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
   271 proof -
   272   let ?S = "\<lambda>n. (-1)^n * a n"
   273   let ?P = "\<lambda>n. \<Sum>i<n. ?S i"
   274   let ?f = "\<lambda>n. ?P (2 * n)"
   275   let ?g = "\<lambda>n. ?P (2 * n + 1)"
   276   obtain l :: real
   277     where below_l: "\<forall> n. ?f n \<le> l"
   278       and "?f ----> l"
   279       and above_l: "\<forall> n. l \<le> ?g n"
   280       and "?g ----> l"
   281     using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast
   282 
   283   let ?Sa = "\<lambda>m. \<Sum>n<m. ?S n"
   284   have "?Sa ----> l"
   285   proof (rule LIMSEQ_I)
   286     fix r :: real
   287     assume "0 < r"
   288     with `?f ----> l`[THEN LIMSEQ_D]
   289     obtain f_no where f: "\<And> n. n \<ge> f_no \<Longrightarrow> norm (?f n - l) < r" by auto
   290 
   291     from `0 < r` `?g ----> l`[THEN LIMSEQ_D]
   292     obtain g_no where g: "\<And> n. n \<ge> g_no \<Longrightarrow> norm (?g n - l) < r" by auto
   293 
   294     {
   295       fix n :: nat
   296       assume "n \<ge> (max (2 * f_no) (2 * g_no))"
   297       hence "n \<ge> 2 * f_no" and "n \<ge> 2 * g_no" by auto
   298       have "norm (?Sa n - l) < r"
   299       proof (cases "even n")
   300         case True
   301         from even_nat_div_two_times_two[OF this]
   302         have n_eq: "2 * (n div 2) = n"
   303           unfolding numeral_2_eq_2[symmetric] by auto
   304         with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no"
   305           by auto
   306         from f[OF this] show ?thesis
   307           unfolding n_eq atLeastLessThanSuc_atLeastAtMost .
   308       next
   309         case False
   310         hence "even (n - 1)" by simp
   311         from even_nat_div_two_times_two[OF this]
   312         have n_eq: "2 * ((n - 1) div 2) = n - 1"
   313           unfolding numeral_2_eq_2[symmetric] by auto
   314         hence range_eq: "n - 1 + 1 = n"
   315           using odd_pos[OF False] by auto
   316 
   317         from n_eq `n \<ge> 2 * g_no` have "(n - 1) div 2 \<ge> g_no"
   318           by auto
   319         from g[OF this] show ?thesis
   320           unfolding n_eq range_eq .
   321       qed
   322     }
   323     thus "\<exists>no. \<forall>n \<ge> no. norm (?Sa n - l) < r" by blast
   324   qed
   325   hence sums_l: "(\<lambda>i. (-1)^i * a i) sums l"
   326     unfolding sums_def .
   327   thus "summable ?S" using summable_def by auto
   328 
   329   have "l = suminf ?S" using sums_unique[OF sums_l] .
   330 
   331   fix n
   332   show "suminf ?S \<le> ?g n"
   333     unfolding sums_unique[OF sums_l, symmetric] using above_l by auto
   334   show "?f n \<le> suminf ?S"
   335     unfolding sums_unique[OF sums_l, symmetric] using below_l by auto
   336   show "?g ----> suminf ?S"
   337     using `?g ----> l` `l = suminf ?S` by auto
   338   show "?f ----> suminf ?S"
   339     using `?f ----> l` `l = suminf ?S` by auto
   340 qed
   341 
   342 theorem summable_Leibniz:
   343   fixes a :: "nat \<Rightarrow> real"
   344   assumes a_zero: "a ----> 0" and "monoseq a"
   345   shows "summable (\<lambda> n. (-1)^n * a n)" (is "?summable")
   346     and "0 < a 0 \<longrightarrow>
   347       (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i<2*n. -1^i * a i .. \<Sum>i<2*n+1. -1^i * a i})" (is "?pos")
   348     and "a 0 < 0 \<longrightarrow>
   349       (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i<2*n+1. -1^i * a i .. \<Sum>i<2*n. -1^i * a i})" (is "?neg")
   350     and "(\<lambda>n. \<Sum>i<2*n. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?f")
   351     and "(\<lambda>n. \<Sum>i<2*n+1. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?g")
   352 proof -
   353   have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g"
   354   proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)")
   355     case True
   356     hence ord: "\<And>n m. m \<le> n \<Longrightarrow> a n \<le> a m" and ge0: "\<And> n. 0 \<le> a n"
   357       by auto
   358     {
   359       fix n
   360       have "a (Suc n) \<le> a n"
   361         using ord[where n="Suc n" and m=n] by auto
   362     } note mono = this
   363     note leibniz = summable_Leibniz'[OF `a ----> 0` ge0]
   364     from leibniz[OF mono]
   365     show ?thesis using `0 \<le> a 0` by auto
   366   next
   367     let ?a = "\<lambda> n. - a n"
   368     case False
   369     with monoseq_le[OF `monoseq a` `a ----> 0`]
   370     have "(\<forall> n. a n \<le> 0) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)" by auto
   371     hence ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n"
   372       by auto
   373     {
   374       fix n
   375       have "?a (Suc n) \<le> ?a n" using ord[where n="Suc n" and m=n]
   376         by auto
   377     } note monotone = this
   378     note leibniz =
   379       summable_Leibniz'[OF _ ge0, of "\<lambda>x. x",
   380         OF tendsto_minus[OF `a ----> 0`, unfolded minus_zero] monotone]
   381     have "summable (\<lambda> n. (-1)^n * ?a n)"
   382       using leibniz(1) by auto
   383     then obtain l where "(\<lambda> n. (-1)^n * ?a n) sums l"
   384       unfolding summable_def by auto
   385     from this[THEN sums_minus] have "(\<lambda> n. (-1)^n * a n) sums -l"
   386       by auto
   387     hence ?summable unfolding summable_def by auto
   388     moreover
   389     have "\<And>a b :: real. \<bar>- a - - b\<bar> = \<bar>a - b\<bar>"
   390       unfolding minus_diff_minus by auto
   391 
   392     from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus]
   393     have move_minus: "(\<Sum>n. - (-1 ^ n * a n)) = - (\<Sum>n. -1 ^ n * a n)"
   394       by auto
   395 
   396     have ?pos using `0 \<le> ?a 0` by auto
   397     moreover have ?neg
   398       using leibniz(2,4)
   399       unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le
   400       by auto
   401     moreover have ?f and ?g
   402       using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel]
   403       by auto
   404     ultimately show ?thesis by auto
   405   qed
   406   then show ?summable and ?pos and ?neg and ?f and ?g 
   407     by safe
   408 qed
   409 
   410 subsection {* Term-by-Term Differentiability of Power Series *}
   411 
   412 definition diffs :: "(nat \<Rightarrow> 'a::ring_1) \<Rightarrow> nat \<Rightarrow> 'a"
   413   where "diffs c = (\<lambda>n. of_nat (Suc n) * c (Suc n))"
   414 
   415 text{*Lemma about distributing negation over it*}
   416 lemma diffs_minus: "diffs (\<lambda>n. - c n) = (\<lambda>n. - diffs c n)"
   417   by (simp add: diffs_def)
   418 
   419 lemma sums_Suc_imp:
   420   "(f::nat \<Rightarrow> 'a::real_normed_vector) 0 = 0 \<Longrightarrow> (\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
   421   using sums_Suc_iff[of f] by simp
   422 
   423 lemma diffs_equiv:
   424   fixes x :: "'a::{real_normed_vector, ring_1}"
   425   shows "summable (\<lambda>n. diffs c n * x^n) \<Longrightarrow>
   426       (\<lambda>n. of_nat n * c n * x^(n - Suc 0)) sums (\<Sum>n. diffs c n * x^n)"
   427   unfolding diffs_def
   428   by (simp add: summable_sums sums_Suc_imp)
   429 
   430 lemma lemma_termdiff1:
   431   fixes z :: "'a :: {monoid_mult,comm_ring}" shows
   432   "(\<Sum>p<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
   433    (\<Sum>p<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
   434   by (auto simp add: algebra_simps power_add [symmetric])
   435 
   436 lemma sumr_diff_mult_const2:
   437   "setsum f {..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i<n. f i - r)"
   438   by (simp add: setsum_subtractf)
   439 
   440 lemma lemma_termdiff2:
   441   fixes h :: "'a :: {field}"
   442   assumes h: "h \<noteq> 0"
   443   shows
   444     "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
   445      h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p.
   446           (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs")
   447   apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h)
   448   apply (simp add: right_diff_distrib diff_divide_distrib h)
   449   apply (simp add: mult_assoc [symmetric])
   450   apply (cases "n", simp)
   451   apply (simp add: lemma_realpow_diff_sumr2 h
   452                    right_diff_distrib [symmetric] mult_assoc
   453               del: power_Suc setsum_lessThan_Suc of_nat_Suc)
   454   apply (subst lemma_realpow_rev_sumr)
   455   apply (subst sumr_diff_mult_const2)
   456   apply simp
   457   apply (simp only: lemma_termdiff1 setsum_right_distrib)
   458   apply (rule setsum_cong [OF refl])
   459   apply (simp add: less_iff_Suc_add)
   460   apply (clarify)
   461   apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
   462               del: setsum_lessThan_Suc power_Suc)
   463   apply (subst mult_assoc [symmetric], subst power_add [symmetric])
   464   apply (simp add: mult_ac)
   465   done
   466 
   467 lemma real_setsum_nat_ivl_bounded2:
   468   fixes K :: "'a::linordered_semidom"
   469   assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
   470     and K: "0 \<le> K"
   471   shows "setsum f {..<n-k} \<le> of_nat n * K"
   472   apply (rule order_trans [OF setsum_mono])
   473   apply (rule f, simp)
   474   apply (simp add: mult_right_mono K)
   475   done
   476 
   477 lemma lemma_termdiff3:
   478   fixes h z :: "'a::{real_normed_field}"
   479   assumes 1: "h \<noteq> 0"
   480     and 2: "norm z \<le> K"
   481     and 3: "norm (z + h) \<le> K"
   482   shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0))
   483           \<le> of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
   484 proof -
   485   have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) =
   486         norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p.
   487           (z + h) ^ q * z ^ (n - 2 - q)) * norm h"
   488     by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult_commute norm_mult)
   489   also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
   490   proof (rule mult_right_mono [OF _ norm_ge_zero])
   491     from norm_ge_zero 2 have K: "0 \<le> K"
   492       by (rule order_trans)
   493     have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n"
   494       apply (erule subst)
   495       apply (simp only: norm_mult norm_power power_add)
   496       apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
   497       done
   498     show "norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))
   499           \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
   500       apply (intro
   501          order_trans [OF norm_setsum]
   502          real_setsum_nat_ivl_bounded2
   503          mult_nonneg_nonneg
   504          of_nat_0_le_iff
   505          zero_le_power K)
   506       apply (rule le_Kn, simp)
   507       done
   508   qed
   509   also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
   510     by (simp only: mult_assoc)
   511   finally show ?thesis .
   512 qed
   513 
   514 lemma lemma_termdiff4:
   515   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   516   assumes k: "0 < (k::real)"
   517     and le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
   518   shows "f -- 0 --> 0"
   519 proof (rule tendsto_norm_zero_cancel)
   520   show "(\<lambda>h. norm (f h)) -- 0 --> 0"
   521   proof (rule real_tendsto_sandwich)
   522     show "eventually (\<lambda>h. 0 \<le> norm (f h)) (at 0)"
   523       by simp
   524     show "eventually (\<lambda>h. norm (f h) \<le> K * norm h) (at 0)"
   525       using k by (auto simp add: eventually_at dist_norm le)
   526     show "(\<lambda>h. 0) -- (0::'a) --> (0::real)"
   527       by (rule tendsto_const)
   528     have "(\<lambda>h. K * norm h) -- (0::'a) --> K * norm (0::'a)"
   529       by (intro tendsto_intros)
   530     then show "(\<lambda>h. K * norm h) -- (0::'a) --> 0"
   531       by simp
   532   qed
   533 qed
   534 
   535 lemma lemma_termdiff5:
   536   fixes g :: "'a::real_normed_vector \<Rightarrow> nat \<Rightarrow> 'b::banach"
   537   assumes k: "0 < (k::real)"
   538   assumes f: "summable f"
   539   assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h"
   540   shows "(\<lambda>h. suminf (g h)) -- 0 --> 0"
   541 proof (rule lemma_termdiff4 [OF k])
   542   fix h::'a
   543   assume "h \<noteq> 0" and "norm h < k"
   544   hence A: "\<forall>n. norm (g h n) \<le> f n * norm h"
   545     by (simp add: le)
   546   hence "\<exists>N. \<forall>n\<ge>N. norm (norm (g h n)) \<le> f n * norm h"
   547     by simp
   548   moreover from f have B: "summable (\<lambda>n. f n * norm h)"
   549     by (rule summable_mult2)
   550   ultimately have C: "summable (\<lambda>n. norm (g h n))"
   551     by (rule summable_comparison_test)
   552   hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))"
   553     by (rule summable_norm)
   554   also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)"
   555     by (rule suminf_le)
   556   also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h"
   557     by (rule suminf_mult2 [symmetric])
   558   finally show "norm (suminf (g h)) \<le> suminf f * norm h" .
   559 qed
   560 
   561 
   562 text{* FIXME: Long proofs*}
   563 
   564 lemma termdiffs_aux:
   565   fixes x :: "'a::{real_normed_field,banach}"
   566   assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
   567     and 2: "norm x < norm K"
   568   shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
   569              - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   570 proof -
   571   from dense [OF 2]
   572   obtain r where r1: "norm x < r" and r2: "r < norm K" by fast
   573   from norm_ge_zero r1 have r: "0 < r"
   574     by (rule order_le_less_trans)
   575   hence r_neq_0: "r \<noteq> 0" by simp
   576   show ?thesis
   577   proof (rule lemma_termdiff5)
   578     show "0 < r - norm x" using r1 by simp
   579     from r r2 have "norm (of_real r::'a) < norm K"
   580       by simp
   581     with 1 have "summable (\<lambda>n. norm (diffs (diffs c) n * (of_real r ^ n)))"
   582       by (rule powser_insidea)
   583     hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. norm (c n))) n * r ^ n)"
   584       using r
   585       by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc)
   586     hence "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))"
   587       by (rule diffs_equiv [THEN sums_summable])
   588     also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0)) =
   589       (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
   590       apply (rule ext)
   591       apply (simp add: diffs_def)
   592       apply (case_tac n, simp_all add: r_neq_0)
   593       done
   594     finally have "summable
   595       (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
   596       by (rule diffs_equiv [THEN sums_summable])
   597     also have
   598       "(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) *
   599            r ^ (n - Suc 0)) =
   600        (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
   601       apply (rule ext)
   602       apply (case_tac "n", simp)
   603       apply (rename_tac nat)
   604       apply (case_tac "nat", simp)
   605       apply (simp add: r_neq_0)
   606       done
   607     finally
   608     show "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
   609   next
   610     fix h::'a and n::nat
   611     assume h: "h \<noteq> 0"
   612     assume "norm h < r - norm x"
   613     hence "norm x + norm h < r" by simp
   614     with norm_triangle_ineq have xh: "norm (x + h) < r"
   615       by (rule order_le_less_trans)
   616     show "norm (c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))
   617           \<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
   618       apply (simp only: norm_mult mult_assoc)
   619       apply (rule mult_left_mono [OF _ norm_ge_zero])
   620       apply (simp add: mult_assoc [symmetric])
   621       apply (metis h lemma_termdiff3 less_eq_real_def r1 xh)
   622       done
   623   qed
   624 qed
   625 
   626 lemma termdiffs:
   627   fixes K x :: "'a::{real_normed_field,banach}"
   628   assumes 1: "summable (\<lambda>n. c n * K ^ n)"
   629       and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
   630       and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
   631       and 4: "norm x < norm K"
   632   shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
   633   unfolding DERIV_def
   634 proof (rule LIM_zero_cancel)
   635   show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
   636             - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
   637   proof (rule LIM_equal2)
   638     show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
   639   next
   640     fix h :: 'a
   641     assume "norm (h - 0) < norm K - norm x"
   642     hence "norm x + norm h < norm K" by simp
   643     hence 5: "norm (x + h) < norm K"
   644       by (rule norm_triangle_ineq [THEN order_le_less_trans])
   645     have "summable (\<lambda>n. c n * x ^ n)"
   646       and "summable (\<lambda>n. c n * (x + h) ^ n)"
   647       and "summable (\<lambda>n. diffs c n * x ^ n)"
   648       using 1 2 4 5 by (auto elim: powser_inside)
   649     then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
   650           (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h - of_nat n * c n * x ^ (n - Suc 0))"
   651       by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums)
   652     then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
   653           (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
   654       by (simp add: algebra_simps)
   655   next
   656     show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   657       by (rule termdiffs_aux [OF 3 4])
   658   qed
   659 qed
   660 
   661 
   662 subsection {* Derivability of power series *}
   663 
   664 lemma DERIV_series':
   665   fixes f :: "real \<Rightarrow> nat \<Rightarrow> real"
   666   assumes DERIV_f: "\<And> n. DERIV (\<lambda> x. f x n) x0 :> (f' x0 n)"
   667     and allf_summable: "\<And> x. x \<in> {a <..< b} \<Longrightarrow> summable (f x)" and x0_in_I: "x0 \<in> {a <..< b}"
   668     and "summable (f' x0)"
   669     and "summable L"
   670     and L_def: "\<And>n x y. \<lbrakk> x \<in> { a <..< b} ; y \<in> { a <..< b} \<rbrakk> \<Longrightarrow> \<bar>f x n - f y n\<bar> \<le> L n * \<bar>x - y\<bar>"
   671   shows "DERIV (\<lambda> x. suminf (f x)) x0 :> (suminf (f' x0))"
   672   unfolding DERIV_def
   673 proof (rule LIM_I)
   674   fix r :: real
   675   assume "0 < r" hence "0 < r/3" by auto
   676 
   677   obtain N_L where N_L: "\<And> n. N_L \<le> n \<Longrightarrow> \<bar> \<Sum> i. L (i + n) \<bar> < r/3"
   678     using suminf_exist_split[OF `0 < r/3` `summable L`] by auto
   679 
   680   obtain N_f' where N_f': "\<And> n. N_f' \<le> n \<Longrightarrow> \<bar> \<Sum> i. f' x0 (i + n) \<bar> < r/3"
   681     using suminf_exist_split[OF `0 < r/3` `summable (f' x0)`] by auto
   682 
   683   let ?N = "Suc (max N_L N_f')"
   684   have "\<bar> \<Sum> i. f' x0 (i + ?N) \<bar> < r/3" (is "?f'_part < r/3") and
   685     L_estimate: "\<bar> \<Sum> i. L (i + ?N) \<bar> < r/3" using N_L[of "?N"] and N_f' [of "?N"] by auto
   686 
   687   let ?diff = "\<lambda>i x. (f (x0 + x) i - f x0 i) / x"
   688 
   689   let ?r = "r / (3 * real ?N)"
   690   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       using a c by (intro ln_add_one_self_le_self) auto
  1498     thus ?thesis
  1499       by auto
  1500   qed
  1501   also have "- (x / (1 - x)) = -x / (1 - x)"
  1502     by auto
  1503   finally have d: "- x / (1 - x) <= ln (1 - x)" .
  1504   have "0 < 1 - x" using a b by simp
  1505   hence e: "-x - 2 * x\<^sup>2 <= - x / (1 - x)"
  1506     using mult_right_le_one_le[of "x*x" "2*x"] a b
  1507     by (simp add: field_simps power2_eq_square)
  1508   from e d show "- x - 2 * x\<^sup>2 <= ln (1 - x)"
  1509     by (rule order_trans)
  1510 qed
  1511 
  1512 lemma ln_add_one_self_le_self2: "-1 < x \<Longrightarrow> ln(1 + x) <= x"
  1513   apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp)
  1514   apply (subst ln_le_cancel_iff)
  1515   apply auto
  1516   done
  1517 
  1518 lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
  1519   "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
  1520 proof -
  1521   assume x: "0 <= x"
  1522   assume x1: "x <= 1"
  1523   from x have "ln (1 + x) <= x"
  1524     by (rule ln_add_one_self_le_self)
  1525   then have "ln (1 + x) - x <= 0"
  1526     by simp
  1527   then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
  1528     by (rule abs_of_nonpos)
  1529   also have "... = x - ln (1 + x)"
  1530     by simp
  1531   also have "... <= x\<^sup>2"
  1532   proof -
  1533     from x x1 have "x - x\<^sup>2 <= ln (1 + x)"
  1534       by (intro ln_one_plus_pos_lower_bound)
  1535     thus ?thesis
  1536       by simp
  1537   qed
  1538   finally show ?thesis .
  1539 qed
  1540 
  1541 lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
  1542   "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  1543 proof -
  1544   assume a: "-(1 / 2) <= x"
  1545   assume b: "x <= 0"
  1546   have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
  1547     apply (subst abs_of_nonpos)
  1548     apply simp
  1549     apply (rule ln_add_one_self_le_self2)
  1550     using a apply auto
  1551     done
  1552   also have "... <= 2 * x\<^sup>2"
  1553     apply (subgoal_tac "- (-x) - 2 * (-x)\<^sup>2 <= ln (1 - (-x))")
  1554     apply (simp add: algebra_simps)
  1555     apply (rule ln_one_minus_pos_lower_bound)
  1556     using a b apply auto
  1557     done
  1558   finally show ?thesis .
  1559 qed
  1560 
  1561 lemma abs_ln_one_plus_x_minus_x_bound:
  1562     "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  1563   apply (case_tac "0 <= x")
  1564   apply (rule order_trans)
  1565   apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
  1566   apply auto
  1567   apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos)
  1568   apply auto
  1569   done
  1570 
  1571 lemma ln_x_over_x_mono: "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
  1572 proof -
  1573   assume x: "exp 1 <= x" "x <= y"
  1574   moreover have "0 < exp (1::real)" by simp
  1575   ultimately have a: "0 < x" and b: "0 < y"
  1576     by (fast intro: less_le_trans order_trans)+
  1577   have "x * ln y - x * ln x = x * (ln y - ln x)"
  1578     by (simp add: algebra_simps)
  1579   also have "... = x * ln(y / x)"
  1580     by (simp only: ln_div a b)
  1581   also have "y / x = (x + (y - x)) / x"
  1582     by simp
  1583   also have "... = 1 + (y - x) / x"
  1584     using x a by (simp add: field_simps)
  1585   also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
  1586     using x a 
  1587     by (intro mult_left_mono ln_add_one_self_le_self) simp_all
  1588   also have "... = y - x" using a by simp
  1589   also have "... = (y - x) * ln (exp 1)" by simp
  1590   also have "... <= (y - x) * ln x"
  1591     apply (rule mult_left_mono)
  1592     apply (subst ln_le_cancel_iff)
  1593     apply fact
  1594     apply (rule a)
  1595     apply (rule x)
  1596     using x apply simp
  1597     done
  1598   also have "... = y * ln x - x * ln x"
  1599     by (rule left_diff_distrib)
  1600   finally have "x * ln y <= y * ln x"
  1601     by arith
  1602   then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps)
  1603   also have "... = y * (ln x / x)" by simp
  1604   finally show ?thesis using b by (simp add: field_simps)
  1605 qed
  1606 
  1607 lemma ln_le_minus_one: "0 < x \<Longrightarrow> ln x \<le> x - 1"
  1608   using exp_ge_add_one_self[of "ln x"] by simp
  1609 
  1610 lemma ln_eq_minus_one:
  1611   assumes "0 < x" "ln x = x - 1"
  1612   shows "x = 1"
  1613 proof -
  1614   let ?l = "\<lambda>y. ln y - y + 1"
  1615   have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
  1616     by (auto intro!: derivative_eq_intros)
  1617 
  1618   show ?thesis
  1619   proof (cases rule: linorder_cases)
  1620     assume "x < 1"
  1621     from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast
  1622     from `x < a` have "?l x < ?l a"
  1623     proof (rule DERIV_pos_imp_increasing, safe)
  1624       fix y
  1625       assume "x \<le> y" "y \<le> a"
  1626       with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y"
  1627         by (auto simp: field_simps)
  1628       with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
  1629         by auto
  1630     qed
  1631     also have "\<dots> \<le> 0"
  1632       using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps)
  1633     finally show "x = 1" using assms by auto
  1634   next
  1635     assume "1 < x"
  1636     from dense[OF this] obtain a where "1 < a" "a < x" by blast
  1637     from `a < x` have "?l x < ?l a"
  1638     proof (rule DERIV_neg_imp_decreasing, safe)
  1639       fix y
  1640       assume "a \<le> y" "y \<le> x"
  1641       with `1 < a` have "1 / y - 1 < 0" "0 < y"
  1642         by (auto simp: field_simps)
  1643       with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0"
  1644         by blast
  1645     qed
  1646     also have "\<dots> \<le> 0"
  1647       using ln_le_minus_one `1 < a` by (auto simp: field_simps)
  1648     finally show "x = 1" using assms by auto
  1649   next
  1650     assume "x = 1"
  1651     then show ?thesis by simp
  1652   qed
  1653 qed
  1654 
  1655 lemma exp_at_bot: "(exp ---> (0::real)) at_bot"
  1656   unfolding tendsto_Zfun_iff
  1657 proof (rule ZfunI, simp add: eventually_at_bot_dense)
  1658   fix r :: real assume "0 < r"
  1659   {
  1660     fix x
  1661     assume "x < ln r"
  1662     then have "exp x < exp (ln r)"
  1663       by simp
  1664     with `0 < r` have "exp x < r"
  1665       by simp
  1666   }
  1667   then show "\<exists>k. \<forall>n<k. exp n < r" by auto
  1668 qed
  1669 
  1670 lemma exp_at_top: "LIM x at_top. exp x :: real :> at_top"
  1671   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"])
  1672      (auto intro: eventually_gt_at_top)
  1673 
  1674 lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
  1675   by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  1676      (auto simp: eventually_at_filter)
  1677 
  1678 lemma ln_at_top: "LIM x at_top. ln x :> at_top"
  1679   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  1680      (auto intro: eventually_gt_at_top)
  1681 
  1682 lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
  1683 proof (induct k)
  1684   case 0
  1685   show "((\<lambda>x. x ^ 0 / exp x) ---> (0::real)) at_top"
  1686     by (simp add: inverse_eq_divide[symmetric])
  1687        (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono
  1688               at_top_le_at_infinity order_refl)
  1689 next
  1690   case (Suc k)
  1691   show ?case
  1692   proof (rule lhospital_at_top_at_top)
  1693     show "eventually (\<lambda>x. DERIV (\<lambda>x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top"
  1694       by eventually_elim (intro derivative_eq_intros, auto)
  1695     show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top"
  1696       by eventually_elim auto
  1697     show "eventually (\<lambda>x. exp x \<noteq> 0) at_top"
  1698       by auto
  1699     from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
  1700     show "((\<lambda>x. real (Suc k) * x ^ k / exp x) ---> 0) at_top"
  1701       by simp
  1702   qed (rule exp_at_top)
  1703 qed
  1704 
  1705 
  1706 definition powr :: "[real,real] => real"  (infixr "powr" 80)
  1707   -- {*exponentation with real exponent*}
  1708   where "x powr a = exp(a * ln x)"
  1709 
  1710 definition log :: "[real,real] => real"
  1711   -- {*logarithm of @{term x} to base @{term a}*}
  1712   where "log a x = ln x / ln a"
  1713 
  1714 
  1715 lemma tendsto_log [tendsto_intros]:
  1716   "\<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"
  1717   unfolding log_def by (intro tendsto_intros) auto
  1718 
  1719 lemma continuous_log:
  1720   assumes "continuous F f"
  1721     and "continuous F g"
  1722     and "0 < f (Lim F (\<lambda>x. x))"
  1723     and "f (Lim F (\<lambda>x. x)) \<noteq> 1"
  1724     and "0 < g (Lim F (\<lambda>x. x))"
  1725   shows "continuous F (\<lambda>x. log (f x) (g x))"
  1726   using assms unfolding continuous_def by (rule tendsto_log)
  1727 
  1728 lemma continuous_at_within_log[continuous_intros]:
  1729   assumes "continuous (at a within s) f"
  1730     and "continuous (at a within s) g"
  1731     and "0 < f a"
  1732     and "f a \<noteq> 1"
  1733     and "0 < g a"
  1734   shows "continuous (at a within s) (\<lambda>x. log (f x) (g x))"
  1735   using assms unfolding continuous_within by (rule tendsto_log)
  1736 
  1737 lemma isCont_log[continuous_intros, simp]:
  1738   assumes "isCont f a" "isCont g a" "0 < f a" "f a \<noteq> 1" "0 < g a"
  1739   shows "isCont (\<lambda>x. log (f x) (g x)) a"
  1740   using assms unfolding continuous_at by (rule tendsto_log)
  1741 
  1742 lemma continuous_on_log[continuous_intros]:
  1743   assumes "continuous_on s f" "continuous_on s g"
  1744     and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
  1745   shows "continuous_on s (\<lambda>x. log (f x) (g x))"
  1746   using assms unfolding continuous_on_def by (fast intro: tendsto_log)
  1747 
  1748 lemma powr_one_eq_one [simp]: "1 powr a = 1"
  1749   by (simp add: powr_def)
  1750 
  1751 lemma powr_zero_eq_one [simp]: "x powr 0 = 1"
  1752   by (simp add: powr_def)
  1753 
  1754 lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)"
  1755   by (simp add: powr_def)
  1756 declare powr_one_gt_zero_iff [THEN iffD2, simp]
  1757 
  1758 lemma powr_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
  1759   by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
  1760 
  1761 lemma powr_gt_zero [simp]: "0 < x powr a"
  1762   by (simp add: powr_def)
  1763 
  1764 lemma powr_ge_pzero [simp]: "0 <= x powr y"
  1765   by (rule order_less_imp_le, rule powr_gt_zero)
  1766 
  1767 lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
  1768   by (simp add: powr_def)
  1769 
  1770 lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
  1771   apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
  1772   apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
  1773   done
  1774 
  1775 lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
  1776   apply (simp add: powr_def)
  1777   apply (subst exp_diff [THEN sym])
  1778   apply (simp add: left_diff_distrib)
  1779   done
  1780 
  1781 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
  1782   by (simp add: powr_def exp_add [symmetric] distrib_right)
  1783 
  1784 lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
  1785   using assms by (auto simp: powr_add)
  1786 
  1787 lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
  1788   by (simp add: powr_def)
  1789 
  1790 lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
  1791   by (simp add: powr_powr mult_commute)
  1792 
  1793 lemma powr_minus: "x powr (-a) = inverse (x powr a)"
  1794   by (simp add: powr_def exp_minus [symmetric])
  1795 
  1796 lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
  1797   by (simp add: divide_inverse powr_minus)
  1798 
  1799 lemma powr_less_mono: "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
  1800   by (simp add: powr_def)
  1801 
  1802 lemma powr_less_cancel: "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
  1803   by (simp add: powr_def)
  1804 
  1805 lemma powr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
  1806   by (blast intro: powr_less_cancel powr_less_mono)
  1807 
  1808 lemma powr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
  1809   by (simp add: linorder_not_less [symmetric])
  1810 
  1811 lemma log_ln: "ln x = log (exp(1)) x"
  1812   by (simp add: log_def)
  1813 
  1814 lemma DERIV_log:
  1815   assumes "x > 0"
  1816   shows "DERIV (\<lambda>y. log b y) x :> 1 / (ln b * x)"
  1817 proof -
  1818   def lb \<equiv> "1 / ln b"
  1819   moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x"
  1820     using `x > 0` by (auto intro!: derivative_eq_intros)
  1821   ultimately show ?thesis
  1822     by (simp add: log_def)
  1823 qed
  1824 
  1825 lemmas DERIV_log[THEN DERIV_chain2, derivative_intros]
  1826 
  1827 lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
  1828   by (simp add: powr_def log_def)
  1829 
  1830 lemma log_powr_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log a (a powr y) = y"
  1831   by (simp add: log_def powr_def)
  1832 
  1833 lemma log_mult:
  1834   "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow>
  1835     log a (x * y) = log a x + log a y"
  1836   by (simp add: log_def ln_mult divide_inverse distrib_right)
  1837 
  1838 lemma log_eq_div_ln_mult_log:
  1839   "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow>
  1840     log a x = (ln b/ln a) * log b x"
  1841   by (simp add: log_def divide_inverse)
  1842 
  1843 text{*Base 10 logarithms*}
  1844 lemma log_base_10_eq1: "0 < x \<Longrightarrow> log 10 x = (ln (exp 1) / ln 10) * ln x"
  1845   by (simp add: log_def)
  1846 
  1847 lemma log_base_10_eq2: "0 < x \<Longrightarrow> log 10 x = (log 10 (exp 1)) * ln x"
  1848   by (simp add: log_def)
  1849 
  1850 lemma log_one [simp]: "log a 1 = 0"
  1851   by (simp add: log_def)
  1852 
  1853 lemma log_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> log a a = 1"
  1854   by (simp add: log_def)
  1855 
  1856 lemma log_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log a (inverse x) = - log a x"
  1857   apply (rule_tac a1 = "log a x" in add_left_cancel [THEN iffD1])
  1858   apply (simp add: log_mult [symmetric])
  1859   done
  1860 
  1861 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"
  1862   by (simp add: log_mult divide_inverse log_inverse)
  1863 
  1864 lemma log_less_cancel_iff [simp]:
  1865   "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a x < log a y \<longleftrightarrow> x < y"
  1866   apply safe
  1867   apply (rule_tac [2] powr_less_cancel)
  1868   apply (drule_tac a = "log a x" in powr_less_mono, auto)
  1869   done
  1870 
  1871 lemma log_inj:
  1872   assumes "1 < b"
  1873   shows "inj_on (log b) {0 <..}"
  1874 proof (rule inj_onI, simp)
  1875   fix x y
  1876   assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
  1877   show "x = y"
  1878   proof (cases rule: linorder_cases)
  1879     assume "x = y"
  1880     then show ?thesis by simp
  1881   next
  1882     assume "x < y" hence "log b x < log b y"
  1883       using log_less_cancel_iff[OF `1 < b`] pos by simp
  1884     then show ?thesis using * by simp
  1885   next
  1886     assume "y < x" hence "log b y < log b x"
  1887       using log_less_cancel_iff[OF `1 < b`] pos by simp
  1888     then show ?thesis using * by simp
  1889   qed
  1890 qed
  1891 
  1892 lemma log_le_cancel_iff [simp]:
  1893   "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (log a x \<le> log a y) = (x \<le> y)"
  1894   by (simp add: linorder_not_less [symmetric])
  1895 
  1896 lemma zero_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < log a x \<longleftrightarrow> 1 < x"
  1897   using log_less_cancel_iff[of a 1 x] by simp
  1898 
  1899 lemma zero_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 \<le> log a x \<longleftrightarrow> 1 \<le> x"
  1900   using log_le_cancel_iff[of a 1 x] by simp
  1901 
  1902 lemma log_less_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 0 \<longleftrightarrow> x < 1"
  1903   using log_less_cancel_iff[of a x 1] by simp
  1904 
  1905 lemma log_le_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 0 \<longleftrightarrow> x \<le> 1"
  1906   using log_le_cancel_iff[of a x 1] by simp
  1907 
  1908 lemma one_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 < log a x \<longleftrightarrow> a < x"
  1909   using log_less_cancel_iff[of a a x] by simp
  1910 
  1911 lemma one_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> log a x \<longleftrightarrow> a \<le> x"
  1912   using log_le_cancel_iff[of a a x] by simp
  1913 
  1914 lemma log_less_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 1 \<longleftrightarrow> x < a"
  1915   using log_less_cancel_iff[of a x a] by simp
  1916 
  1917 lemma log_le_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 1 \<longleftrightarrow> x \<le> a"
  1918   using log_le_cancel_iff[of a x a] by simp
  1919 
  1920 lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
  1921   apply (induct n)
  1922   apply simp
  1923   apply (subgoal_tac "real(Suc n) = real n + 1")
  1924   apply (erule ssubst)
  1925   apply (subst powr_add, simp, simp)
  1926   done
  1927 
  1928 lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
  1929   unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
  1930 
  1931 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
  1932   apply (case_tac "x = 0", simp, simp)
  1933   apply (rule powr_realpow [THEN sym], simp)
  1934   done
  1935 
  1936 lemma powr_int:
  1937   assumes "x > 0"
  1938   shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))"
  1939 proof (cases "i < 0")
  1940   case True
  1941   have r: "x powr i = 1 / x powr (-i)" by (simp add: powr_minus field_simps)
  1942   show ?thesis using `i < 0` `x > 0` by (simp add: r field_simps powr_realpow[symmetric])
  1943 next
  1944   case False
  1945   then show ?thesis by (simp add: assms powr_realpow[symmetric])
  1946 qed
  1947 
  1948 lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
  1949   using powr_realpow [of x 1] by simp
  1950 
  1951 lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
  1952   by (fact powr_realpow_numeral)
  1953 
  1954 lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
  1955   using powr_int [of x "- 1"] by simp
  1956 
  1957 lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
  1958   using powr_int [of x "- numeral n"] by simp
  1959 
  1960 lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
  1961   by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
  1962 
  1963 lemma ln_powr: "ln (x powr y) = y * ln x"
  1964   by (simp add: powr_def)
  1965 
  1966 lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) =  ln b / n"
  1967 by(simp add: root_powr_inverse ln_powr)
  1968 
  1969 lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) =  log b a / n"
  1970 by(simp add: log_def ln_root)
  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 log_base_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> log (root n b) x = n * (log b x)"
  1988 by(simp add: log_def ln_root)
  1989 
  1990 lemma ln_bound: "1 <= x ==> ln x <= x"
  1991   apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
  1992   apply simp
  1993   apply (rule ln_add_one_self_le_self, simp)
  1994   done
  1995 
  1996 lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b"
  1997   apply (cases "x = 1", simp)
  1998   apply (cases "a = b", simp)
  1999   apply (rule order_less_imp_le)
  2000   apply (rule powr_less_mono, auto)
  2001   done
  2002 
  2003 lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a"
  2004   apply (subst powr_zero_eq_one [THEN sym])
  2005   apply (rule powr_mono, assumption+)
  2006   done
  2007 
  2008 lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
  2009   apply (unfold powr_def)
  2010   apply (rule exp_less_mono)
  2011   apply (rule mult_strict_left_mono)
  2012   apply (subst ln_less_cancel_iff, assumption)
  2013   apply (rule order_less_trans)
  2014   prefer 2
  2015   apply assumption+
  2016   done
  2017 
  2018 lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
  2019   apply (unfold powr_def)
  2020   apply (rule exp_less_mono)
  2021   apply (rule mult_strict_left_mono_neg)
  2022   apply (subst ln_less_cancel_iff)
  2023   apply assumption
  2024   apply (rule order_less_trans)
  2025   prefer 2
  2026   apply assumption+
  2027   done
  2028 
  2029 lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
  2030   apply (case_tac "a = 0", simp)
  2031   apply (case_tac "x = y", simp)
  2032   apply (metis less_eq_real_def powr_less_mono2)
  2033   done
  2034 
  2035 lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
  2036   unfolding powr_def exp_inj_iff by simp
  2037 
  2038 lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
  2039   by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult_commute 
  2040             order.strict_trans2 powr_gt_zero zero_less_one)
  2041 
  2042 lemma ln_powr_bound2:
  2043   assumes "1 < x" and "0 < a"
  2044   shows "(ln x) powr a <= (a powr a) * x"
  2045 proof -
  2046   from assms have "ln x <= (x powr (1 / a)) / (1 / a)"
  2047     by (metis less_eq_real_def ln_powr_bound zero_less_divide_1_iff)
  2048   also have "... = a * (x powr (1 / a))"
  2049     by simp
  2050   finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
  2051     by (metis assms less_imp_le ln_gt_zero powr_mono2)
  2052   also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
  2053     by (metis assms(2) powr_mult powr_gt_zero)
  2054   also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
  2055     by (rule powr_powr)
  2056   also have "... = x" using assms
  2057     by auto
  2058   finally show ?thesis .
  2059 qed
  2060 
  2061 lemma tendsto_powr [tendsto_intros]:
  2062   "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
  2063   unfolding powr_def by (intro tendsto_intros)
  2064 
  2065 lemma continuous_powr:
  2066   assumes "continuous F f"
  2067     and "continuous F g"
  2068     and "0 < f (Lim F (\<lambda>x. x))"
  2069   shows "continuous F (\<lambda>x. (f x) powr (g x))"
  2070   using assms unfolding continuous_def by (rule tendsto_powr)
  2071 
  2072 lemma continuous_at_within_powr[continuous_intros]:
  2073   assumes "continuous (at a within s) f"
  2074     and "continuous (at a within s) g"
  2075     and "0 < f a"
  2076   shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
  2077   using assms unfolding continuous_within by (rule tendsto_powr)
  2078 
  2079 lemma isCont_powr[continuous_intros, simp]:
  2080   assumes "isCont f a" "isCont g a" "0 < f a"
  2081   shows "isCont (\<lambda>x. (f x) powr g x) a"
  2082   using assms unfolding continuous_at by (rule tendsto_powr)
  2083 
  2084 lemma continuous_on_powr[continuous_intros]:
  2085   assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. 0 < f x"
  2086   shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
  2087   using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
  2088 
  2089 (* FIXME: generalize by replacing d by with g x and g ---> d? *)
  2090 lemma tendsto_zero_powrI:
  2091   assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
  2092     and "0 < d"
  2093   shows "((\<lambda>x. f x powr d) ---> 0) F"
  2094 proof (rule tendstoI)
  2095   fix e :: real assume "0 < e"
  2096   def Z \<equiv> "e powr (1 / d)"
  2097   with `0 < e` have "0 < Z" by simp
  2098   with assms have "eventually (\<lambda>x. 0 < f x \<and> dist (f x) 0 < Z) F"
  2099     by (intro eventually_conj tendstoD)
  2100   moreover
  2101   from assms have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> x powr d < Z powr d"
  2102     by (intro powr_less_mono2) (auto simp: dist_real_def)
  2103   with assms `0 < e` have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> dist (x powr d) 0 < e"
  2104     unfolding dist_real_def Z_def by (auto simp: powr_powr)
  2105   ultimately
  2106   show "eventually (\<lambda>x. dist (f x powr d) 0 < e) F" by (rule eventually_elim1)
  2107 qed
  2108 
  2109 lemma tendsto_neg_powr:
  2110   assumes "s < 0"
  2111     and "LIM x F. f x :> at_top"
  2112   shows "((\<lambda>x. f x powr s) ---> 0) F"
  2113 proof (rule tendstoI)
  2114   fix e :: real assume "0 < e"
  2115   def Z \<equiv> "e powr (1 / s)"
  2116   from assms have "eventually (\<lambda>x. Z < f x) F"
  2117     by (simp add: filterlim_at_top_dense)
  2118   moreover
  2119   from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
  2120     by (auto simp: Z_def intro!: powr_less_mono2_neg)
  2121   with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
  2122     by (simp add: powr_powr Z_def dist_real_def)
  2123   ultimately
  2124   show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
  2125 qed
  2126 
  2127 subsection {* Sine and Cosine *}
  2128 
  2129 definition sin_coeff :: "nat \<Rightarrow> real" where
  2130   "sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))"
  2131 
  2132 definition cos_coeff :: "nat \<Rightarrow> real" where
  2133   "cos_coeff = (\<lambda>n. if even n then (-1 ^ (n div 2)) / real (fact n) else 0)"
  2134 
  2135 definition sin :: "real \<Rightarrow> real"
  2136   where "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
  2137 
  2138 definition cos :: "real \<Rightarrow> real"
  2139   where "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
  2140 
  2141 lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
  2142   unfolding sin_coeff_def by simp
  2143 
  2144 lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
  2145   unfolding cos_coeff_def by simp
  2146 
  2147 lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
  2148   unfolding cos_coeff_def sin_coeff_def
  2149   by (simp del: mult_Suc)
  2150 
  2151 lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
  2152   unfolding cos_coeff_def sin_coeff_def
  2153   by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
  2154 
  2155 lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
  2156   unfolding sin_coeff_def
  2157   apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
  2158   apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  2159   done
  2160 
  2161 lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
  2162   unfolding cos_coeff_def
  2163   apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
  2164   apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  2165   done
  2166 
  2167 lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
  2168   unfolding sin_def by (rule summable_sin [THEN summable_sums])
  2169 
  2170 lemma cos_converges: "(\<lambda>n. cos_coeff n * x ^ n) sums cos(x)"
  2171   unfolding cos_def by (rule summable_cos [THEN summable_sums])
  2172 
  2173 lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff"
  2174   by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
  2175 
  2176 lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
  2177   by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
  2178 
  2179 text{*Now at last we can get the derivatives of exp, sin and cos*}
  2180 
  2181 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
  2182   unfolding sin_def cos_def
  2183   apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
  2184   apply (simp_all add: diffs_sin_coeff diffs_cos_coeff
  2185     summable_minus summable_sin summable_cos)
  2186   done
  2187 
  2188 declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
  2189 
  2190 lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
  2191   unfolding cos_def sin_def
  2192   apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
  2193   apply (simp_all add: diffs_sin_coeff diffs_cos_coeff diffs_minus
  2194     summable_minus summable_sin summable_cos suminf_minus)
  2195   done
  2196 
  2197 declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
  2198 
  2199 lemma isCont_sin: "isCont sin x"
  2200   by (rule DERIV_sin [THEN DERIV_isCont])
  2201 
  2202 lemma isCont_cos: "isCont cos x"
  2203   by (rule DERIV_cos [THEN DERIV_isCont])
  2204 
  2205 lemma isCont_sin' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
  2206   by (rule isCont_o2 [OF _ isCont_sin])
  2207 
  2208 lemma isCont_cos' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
  2209   by (rule isCont_o2 [OF _ isCont_cos])
  2210 
  2211 lemma tendsto_sin [tendsto_intros]:
  2212   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) ---> sin a) F"
  2213   by (rule isCont_tendsto_compose [OF isCont_sin])
  2214 
  2215 lemma tendsto_cos [tendsto_intros]:
  2216   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
  2217   by (rule isCont_tendsto_compose [OF isCont_cos])
  2218 
  2219 lemma continuous_sin [continuous_intros]:
  2220   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
  2221   unfolding continuous_def by (rule tendsto_sin)
  2222 
  2223 lemma continuous_on_sin [continuous_intros]:
  2224   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
  2225   unfolding continuous_on_def by (auto intro: tendsto_sin)
  2226 
  2227 lemma continuous_cos [continuous_intros]:
  2228   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
  2229   unfolding continuous_def by (rule tendsto_cos)
  2230 
  2231 lemma continuous_on_cos [continuous_intros]:
  2232   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
  2233   unfolding continuous_on_def by (auto intro: tendsto_cos)
  2234 
  2235 subsection {* Properties of Sine and Cosine *}
  2236 
  2237 lemma sin_zero [simp]: "sin 0 = 0"
  2238   unfolding sin_def sin_coeff_def by (simp add: powser_zero)
  2239 
  2240 lemma cos_zero [simp]: "cos 0 = 1"
  2241   unfolding cos_def cos_coeff_def by (simp add: powser_zero)
  2242 
  2243 lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
  2244 proof -
  2245   have "\<forall>x. DERIV (\<lambda>x. (sin x)\<^sup>2 + (cos x)\<^sup>2) x :> 0"
  2246     by (auto intro!: derivative_eq_intros)
  2247   hence "(sin x)\<^sup>2 + (cos x)\<^sup>2 = (sin 0)\<^sup>2 + (cos 0)\<^sup>2"
  2248     by (rule DERIV_isconst_all)
  2249   thus "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" by simp
  2250 qed
  2251 
  2252 lemma sin_cos_squared_add2 [simp]: "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
  2253   by (subst add_commute, rule sin_cos_squared_add)
  2254 
  2255 lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
  2256   using sin_cos_squared_add2 [unfolded power2_eq_square] .
  2257 
  2258 lemma sin_squared_eq: "(sin x)\<^sup>2 = 1 - (cos x)\<^sup>2"
  2259   unfolding eq_diff_eq by (rule sin_cos_squared_add)
  2260 
  2261 lemma cos_squared_eq: "(cos x)\<^sup>2 = 1 - (sin x)\<^sup>2"
  2262   unfolding eq_diff_eq by (rule sin_cos_squared_add2)
  2263 
  2264 lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
  2265   by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
  2266 
  2267 lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
  2268   using abs_sin_le_one [of x] unfolding abs_le_iff by simp
  2269 
  2270 lemma sin_le_one [simp]: "sin x \<le> 1"
  2271   using abs_sin_le_one [of x] unfolding abs_le_iff by simp
  2272 
  2273 lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
  2274   by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
  2275 
  2276 lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
  2277   using abs_cos_le_one [of x] unfolding abs_le_iff by simp
  2278 
  2279 lemma cos_le_one [simp]: "cos x \<le> 1"
  2280   using abs_cos_le_one [of x] unfolding abs_le_iff by simp
  2281 
  2282 lemma DERIV_fun_pow: "DERIV g x :> m ==>
  2283       DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
  2284   by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  2285 
  2286 lemma DERIV_fun_exp:
  2287      "DERIV g x :> m ==> DERIV (\<lambda>x. exp(g x)) x :> exp(g x) * m"
  2288   by (auto intro!: derivative_intros)
  2289 
  2290 lemma DERIV_fun_sin:
  2291      "DERIV g x :> m ==> DERIV (\<lambda>x. sin(g x)) x :> cos(g x) * m"
  2292   by (auto intro!: derivative_intros)
  2293 
  2294 lemma DERIV_fun_cos:
  2295      "DERIV g x :> m ==> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
  2296   by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  2297 
  2298 lemma sin_cos_add_lemma:
  2299   "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 +
  2300     (cos (x + y) - (cos x * cos y - sin x * sin y))\<^sup>2 = 0"
  2301   (is "?f x = 0")
  2302 proof -
  2303   have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
  2304     by (auto intro!: derivative_eq_intros simp add: algebra_simps)
  2305   hence "?f x = ?f 0"
  2306     by (rule DERIV_isconst_all)
  2307   thus ?thesis by simp
  2308 qed
  2309 
  2310 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
  2311   using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
  2312 
  2313 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
  2314   using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
  2315 
  2316 lemma sin_cos_minus_lemma:
  2317   "(sin(-x) + sin(x))\<^sup>2 + (cos(-x) - cos(x))\<^sup>2 = 0" (is "?f x = 0")
  2318 proof -
  2319   have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
  2320     by (auto intro!: derivative_eq_intros simp add: algebra_simps)
  2321   hence "?f x = ?f 0"
  2322     by (rule DERIV_isconst_all)
  2323   thus ?thesis by simp
  2324 qed
  2325 
  2326 lemma sin_minus [simp]: "sin (-x) = -sin(x)"
  2327   using sin_cos_minus_lemma [where x=x] by simp
  2328 
  2329 lemma cos_minus [simp]: "cos (-x) = cos(x)"
  2330   using sin_cos_minus_lemma [where x=x] by simp
  2331 
  2332 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
  2333   using sin_add [of x "- y"] by simp
  2334 
  2335 lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
  2336   by (simp add: sin_diff mult_commute)
  2337 
  2338 lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
  2339   using cos_add [of x "- y"] by simp
  2340 
  2341 lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
  2342   by (simp add: cos_diff mult_commute)
  2343 
  2344 lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
  2345   using sin_add [where x=x and y=x] by simp
  2346 
  2347 lemma cos_double: "cos(2* x) = ((cos x)\<^sup>2) - ((sin x)\<^sup>2)"
  2348   using cos_add [where x=x and y=x]
  2349   by (simp add: power2_eq_square)
  2350 
  2351 
  2352 subsection {* The Constant Pi *}
  2353 
  2354 definition pi :: real
  2355   where "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
  2356 
  2357 text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
  2358    hence define pi.*}
  2359 
  2360 lemma sin_paired:
  2361   "(\<lambda>n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
  2362 proof -
  2363   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
  2364     by (rule sin_converges [THEN sums_group], simp)
  2365   thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: mult_ac)
  2366 qed
  2367 
  2368 lemma sin_gt_zero:
  2369   assumes "0 < x" and "x < 2"
  2370   shows "0 < sin x"
  2371 proof -
  2372   let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. -1 ^ k / real (fact (2*k+1)) * x^(2*k+1)"
  2373   have pos: "\<forall>n. 0 < ?f n"
  2374   proof
  2375     fix n :: nat
  2376     let ?k2 = "real (Suc (Suc (4 * n)))"
  2377     let ?k3 = "real (Suc (Suc (Suc (4 * n))))"
  2378     have "x * x < ?k2 * ?k3"
  2379       using assms by (intro mult_strict_mono', simp_all)
  2380     hence "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)"
  2381       by (intro mult_strict_right_mono zero_less_power `0 < x`)
  2382     thus "0 < ?f n"
  2383       by (simp del: mult_Suc,
  2384         simp add: less_divide_eq field_simps del: mult_Suc)
  2385   qed
  2386   have sums: "?f sums sin x"
  2387     by (rule sin_paired [THEN sums_group], simp)
  2388   show "0 < sin x"
  2389     unfolding sums_unique [OF sums]
  2390     using sums_summable [OF sums] pos
  2391     by (rule suminf_pos)
  2392 qed
  2393 
  2394 lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
  2395   using sin_gt_zero [where x = x] by (auto simp add: cos_squared_eq cos_double)
  2396 
  2397 lemma cos_paired: "(\<lambda>n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
  2398 proof -
  2399   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
  2400     by (rule cos_converges [THEN sums_group], simp)
  2401   thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
  2402 qed
  2403 
  2404 lemmas realpow_num_eq_if = power_eq_if
  2405 
  2406 lemma sumr_pos_lt_pair:
  2407   fixes f :: "nat \<Rightarrow> real"
  2408   shows "\<lbrakk>summable f;
  2409         \<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
  2410       \<Longrightarrow> setsum f {..<k} < suminf f"
  2411 unfolding One_nat_def
  2412 apply (subst suminf_split_initial_segment [where k="k"])
  2413 apply assumption
  2414 apply simp
  2415 apply (drule_tac k="k" in summable_ignore_initial_segment)
  2416 apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
  2417 apply simp
  2418 apply (frule sums_unique)
  2419 apply (drule sums_summable)
  2420 apply simp
  2421 apply (erule suminf_pos)
  2422 apply (simp add: add_ac)
  2423 done
  2424 
  2425 lemma cos_two_less_zero [simp]:
  2426   "cos 2 < 0"
  2427 proof -
  2428   note fact_Suc [simp del]
  2429   from cos_paired
  2430   have "(\<lambda>n. - (-1 ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
  2431     by (rule sums_minus)
  2432   then have *: "(\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
  2433     by simp
  2434   then have **: "summable (\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2435     by (rule sums_summable)
  2436   have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2437     by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
  2438   moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - (-1 ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
  2439     < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2440   proof -
  2441     { fix d
  2442       have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  2443        < real (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
  2444            fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  2445         by (simp only: real_of_nat_mult) (auto intro!: mult_strict_mono fact_less_mono_nat)
  2446       then have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  2447         < real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
  2448         by (simp only: fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
  2449       then have "4 * inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))))
  2450         < inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  2451         by (simp add: inverse_eq_divide less_divide_eq)
  2452     }
  2453     note *** = this
  2454     have [simp]: "\<And>x y::real. 0 < x - y \<longleftrightarrow> y < x" by arith
  2455     from ** show ?thesis by (rule sumr_pos_lt_pair)
  2456       (simp add: divide_inverse mult_assoc [symmetric] ***)
  2457   qed
  2458   ultimately have "0 < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2459     by (rule order_less_trans)
  2460   moreover from * have "- cos 2 = (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2461     by (rule sums_unique)
  2462   ultimately have "0 < - cos 2" by simp
  2463   then show ?thesis by simp
  2464 qed
  2465 
  2466 lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
  2467 lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]
  2468 
  2469 lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 \<and> cos x = 0"
  2470 proof (rule ex_ex1I)
  2471   show "\<exists>x. 0 \<le> x & x \<le> 2 & cos x = 0"
  2472     by (rule IVT2, simp_all)
  2473 next
  2474   fix x y
  2475   assume x: "0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
  2476   assume y: "0 \<le> y \<and> y \<le> 2 \<and> cos y = 0"
  2477   have [simp]: "\<forall>x. cos differentiable (at x)"
  2478     unfolding real_differentiable_def by (auto intro: DERIV_cos)
  2479   from x y show "x = y"
  2480     apply (cut_tac less_linear [of x y], auto)
  2481     apply (drule_tac f = cos in Rolle)
  2482     apply (drule_tac [5] f = cos in Rolle)
  2483     apply (auto dest!: DERIV_cos [THEN DERIV_unique])
  2484     apply (metis order_less_le_trans less_le sin_gt_zero)
  2485     apply (metis order_less_le_trans less_le sin_gt_zero)
  2486     done
  2487 qed
  2488 
  2489 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
  2490   by (simp add: pi_def)
  2491 
  2492 lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
  2493   by (simp add: pi_half cos_is_zero [THEN theI'])
  2494 
  2495 lemma pi_half_gt_zero [simp]: "0 < pi / 2"
  2496   apply (rule order_le_neq_trans)
  2497   apply (simp add: pi_half cos_is_zero [THEN theI'])
  2498   apply (metis cos_pi_half cos_zero zero_neq_one)
  2499   done
  2500 
  2501 lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
  2502 lemmas pi_half_ge_zero [simp] = pi_half_gt_zero [THEN order_less_imp_le]
  2503 
  2504 lemma pi_half_less_two [simp]: "pi / 2 < 2"
  2505   apply (rule order_le_neq_trans)
  2506   apply (simp add: pi_half cos_is_zero [THEN theI'])
  2507   apply (metis cos_pi_half cos_two_neq_zero)
  2508   done
  2509 
  2510 lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
  2511 lemmas pi_half_le_two [simp] =  pi_half_less_two [THEN order_less_imp_le]
  2512 
  2513 lemma pi_gt_zero [simp]: "0 < pi"
  2514   using pi_half_gt_zero by simp
  2515 
  2516 lemma pi_ge_zero [simp]: "0 \<le> pi"
  2517   by (rule pi_gt_zero [THEN order_less_imp_le])
  2518 
  2519 lemma pi_neq_zero [simp]: "pi \<noteq> 0"
  2520   by (rule pi_gt_zero [THEN less_imp_neq, symmetric])
  2521 
  2522 lemma pi_not_less_zero [simp]: "\<not> pi < 0"
  2523   by (simp add: linorder_not_less)
  2524 
  2525 lemma minus_pi_half_less_zero: "-(pi/2) < 0"
  2526   by simp
  2527 
  2528 lemma m2pi_less_pi: "- (2 * pi) < pi"
  2529   by simp
  2530 
  2531 lemma sin_pi_half [simp]: "sin(pi/2) = 1"
  2532   using sin_cos_squared_add2 [where x = "pi/2"]
  2533   using sin_gt_zero [OF pi_half_gt_zero pi_half_less_two]
  2534   by (simp add: power2_eq_1_iff)
  2535 
  2536 lemma cos_pi [simp]: "cos pi = -1"
  2537   using cos_add [where x = "pi/2" and y = "pi/2"] by simp
  2538 
  2539 lemma sin_pi [simp]: "sin pi = 0"
  2540   using sin_add [where x = "pi/2" and y = "pi/2"] by simp
  2541 
  2542 lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
  2543   by (simp add: cos_diff)
  2544 
  2545 lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
  2546   by (simp add: cos_add)
  2547 
  2548 lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
  2549   by (simp add: sin_diff)
  2550 
  2551 lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
  2552   by (simp add: sin_add)
  2553 
  2554 lemma sin_periodic_pi2 [simp]: "sin (pi + x) = - sin x"
  2555   by (simp add: sin_add)
  2556 
  2557 lemma cos_periodic_pi [simp]: "cos (x + pi) = - cos x"
  2558   by (simp add: cos_add)
  2559 
  2560 lemma sin_periodic [simp]: "sin (x + 2*pi) = sin x"
  2561   by (simp add: sin_add cos_double)
  2562 
  2563 lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
  2564   by (simp add: cos_add cos_double)
  2565 
  2566 lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
  2567   by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
  2568 
  2569 lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
  2570   by (metis cos_npi mult_commute)
  2571 
  2572 lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
  2573   by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
  2574 
  2575 lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
  2576   by (simp add: mult_commute [of pi])
  2577 
  2578 lemma cos_two_pi [simp]: "cos (2 * pi) = 1"
  2579   by (simp add: cos_double)
  2580 
  2581 lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
  2582   by simp
  2583 
  2584 lemma sin_gt_zero2: "[| 0 < x; x < pi/2 |] ==> 0 < sin x"
  2585   by (metis sin_gt_zero order_less_trans pi_half_less_two)
  2586 
  2587 lemma sin_less_zero:
  2588   assumes "- pi/2 < x" and "x < 0"
  2589   shows "sin x < 0"
  2590 proof -
  2591   have "0 < sin (- x)" using assms by (simp only: sin_gt_zero2)
  2592   thus ?thesis by simp
  2593 qed
  2594 
  2595 lemma pi_less_4: "pi < 4"
  2596   using pi_half_less_two by auto
  2597 
  2598 lemma cos_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < cos x"
  2599   apply (cut_tac pi_less_4)
  2600   apply (cut_tac f = cos and a = 0 and b = x and y = 0 in IVT2_objl, safe, simp_all)
  2601   apply (cut_tac cos_is_zero, safe)
  2602   apply (rename_tac y z)
  2603   apply (drule_tac x = y in spec)
  2604   apply (drule_tac x = "pi/2" in spec, simp)
  2605   done
  2606 
  2607 lemma cos_gt_zero_pi: "[| -(pi/2) < x; x < pi/2 |] ==> 0 < cos x"
  2608   apply (rule_tac x = x and y = 0 in linorder_cases)
  2609   apply (metis cos_gt_zero cos_minus minus_less_iff neg_0_less_iff_less)
  2610   apply (auto intro: cos_gt_zero)
  2611   done
  2612 
  2613 lemma cos_ge_zero: "[| -(pi/2) \<le> x; x \<le> pi/2 |] ==> 0 \<le> cos x"
  2614   apply (auto simp add: order_le_less cos_gt_zero_pi)
  2615   apply (subgoal_tac "x = pi/2", auto)
  2616   done
  2617 
  2618 lemma sin_gt_zero_pi: "[| 0 < x; x < pi  |] ==> 0 < sin x"
  2619   by (simp add: sin_cos_eq cos_gt_zero_pi)
  2620 
  2621 lemma pi_ge_two: "2 \<le> pi"
  2622 proof (rule ccontr)
  2623   assume "\<not> 2 \<le> pi" hence "pi < 2" by auto
  2624   have "\<exists>y > pi. y < 2 \<and> y < 2 * pi"
  2625   proof (cases "2 < 2 * pi")
  2626     case True with dense[OF `pi < 2`] show ?thesis by auto
  2627   next
  2628     case False have "pi < 2 * pi" by auto
  2629     from dense[OF this] and False show ?thesis by auto
  2630   qed
  2631   then obtain y where "pi < y" and "y < 2" and "y < 2 * pi" by blast
  2632   hence "0 < sin y" using sin_gt_zero by auto
  2633   moreover
  2634   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
  2635   ultimately show False by auto
  2636 qed
  2637 
  2638 lemma sin_ge_zero: "[| 0 \<le> x; x \<le> pi |] ==> 0 \<le> sin x"
  2639   by (auto simp add: order_le_less sin_gt_zero_pi)
  2640 
  2641 text {* FIXME: This proof is almost identical to lemma @{text cos_is_zero}.
  2642   It should be possible to factor out some of the common parts. *}
  2643 
  2644 lemma cos_total: "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)"
  2645 proof (rule ex_ex1I)
  2646   assume y: "-1 \<le> y" "y \<le> 1"
  2647   show "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y"
  2648     by (rule IVT2, simp_all add: y)
  2649 next
  2650   fix a b
  2651   assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
  2652   assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
  2653   have [simp]: "\<forall>x. cos differentiable (at x)"
  2654     unfolding real_differentiable_def by (auto intro: DERIV_cos)
  2655   from a b show "a = b"
  2656     apply (cut_tac less_linear [of a b], auto)
  2657     apply (drule_tac f = cos in Rolle)
  2658     apply (drule_tac [5] f = cos in Rolle)
  2659     apply (auto dest!: DERIV_cos [THEN DERIV_unique])
  2660     apply (metis order_less_le_trans less_le sin_gt_zero_pi)
  2661     apply (metis order_less_le_trans less_le sin_gt_zero_pi)
  2662     done
  2663 qed
  2664 
  2665 lemma sin_total:
  2666      "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"
  2667 apply (rule ccontr)
  2668 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))")
  2669 apply (erule contrapos_np)
  2670 apply simp
  2671 apply (cut_tac y="-y" in cos_total, simp) apply simp
  2672 apply (erule ex1E)
  2673 apply (rule_tac a = "x - (pi/2)" in ex1I)
  2674 apply (simp (no_asm) add: add_assoc)
  2675 apply (rotate_tac 3)
  2676 apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all add: cos_add)
  2677 done
  2678 
  2679 lemma reals_Archimedean4:
  2680      "[| 0 < y; 0 \<le> x |] ==> \<exists>n. real n * y \<le> x & x < real (Suc n) * y"
  2681 apply (auto dest!: reals_Archimedean3)
  2682 apply (drule_tac x = x in spec, clarify)
  2683 apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y")
  2684  prefer 2 apply (erule LeastI)
  2685 apply (case_tac "LEAST m::nat. x < real m * y", simp)
  2686 apply (rename_tac m)
  2687 apply (subgoal_tac "~ x < real m * y")
  2688  prefer 2 apply (rule not_less_Least, simp, force)
  2689 done
  2690 
  2691 (* Pre Isabelle99-2 proof was simpler- numerals arithmetic
  2692    now causes some unwanted re-arrangements of literals!   *)
  2693 lemma cos_zero_lemma:
  2694      "[| 0 \<le> x; cos x = 0 |] ==>
  2695       \<exists>n::nat. ~even n & x = real n * (pi/2)"
  2696 apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
  2697 apply (subgoal_tac "0 \<le> x - real n * pi &
  2698                     (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
  2699 apply (auto simp add: algebra_simps real_of_nat_Suc)
  2700  prefer 2 apply (simp add: cos_diff)
  2701 apply (simp add: cos_diff)
  2702 apply (subgoal_tac "EX! x. 0 \<le> x & x \<le> pi & cos x = 0")
  2703 apply (rule_tac [2] cos_total, safe)
  2704 apply (drule_tac x = "x - real n * pi" in spec)
  2705 apply (drule_tac x = "pi/2" in spec)
  2706 apply (simp add: cos_diff)
  2707 apply (rule_tac x = "Suc (2 * n)" in exI)
  2708 apply (simp add: real_of_nat_Suc algebra_simps, auto)
  2709 done
  2710 
  2711 lemma sin_zero_lemma:
  2712      "[| 0 \<le> x; sin x = 0 |] ==>
  2713       \<exists>n::nat. even n & x = real n * (pi/2)"
  2714 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  2715  apply (clarify, rule_tac x = "n - 1" in exI)
  2716  apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
  2717 apply (rule cos_zero_lemma)
  2718 apply (simp_all add: cos_add)
  2719 done
  2720 
  2721 
  2722 lemma cos_zero_iff:
  2723      "(cos x = 0) =
  2724       ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |
  2725        (\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
  2726 apply (rule iffI)
  2727 apply (cut_tac linorder_linear [of 0 x], safe)
  2728 apply (drule cos_zero_lemma, assumption+)
  2729 apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
  2730 apply (force simp add: minus_equation_iff [of x])
  2731 apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
  2732 apply (auto simp add: cos_diff cos_add)
  2733 done
  2734 
  2735 (* ditto: but to a lesser extent *)
  2736 lemma sin_zero_iff:
  2737      "(sin x = 0) =
  2738       ((\<exists>n::nat. even n & (x = real n * (pi/2))) |
  2739        (\<exists>n::nat. even n & (x = -(real n * (pi/2)))))"
  2740 apply (rule iffI)
  2741 apply (cut_tac linorder_linear [of 0 x], safe)
  2742 apply (drule sin_zero_lemma, assumption+)
  2743 apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
  2744 apply (force simp add: minus_equation_iff [of x])
  2745 apply (auto simp add: even_mult_two_ex)
  2746 done
  2747 
  2748 lemma cos_monotone_0_pi:
  2749   assumes "0 \<le> y" and "y < x" and "x \<le> pi"
  2750   shows "cos x < cos y"
  2751 proof -
  2752   have "- (x - y) < 0" using assms by auto
  2753 
  2754   from MVT2[OF `y < x` DERIV_cos[THEN impI, THEN allI]]
  2755   obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z"
  2756     by auto
  2757   hence "0 < z" and "z < pi" using assms by auto
  2758   hence "0 < sin z" using sin_gt_zero_pi by auto
  2759   hence "cos x - cos y < 0"
  2760     unfolding cos_diff minus_mult_commute[symmetric]
  2761     using `- (x - y) < 0` by (rule mult_pos_neg2)
  2762   thus ?thesis by auto
  2763 qed
  2764 
  2765 lemma cos_monotone_0_pi':
  2766   assumes "0 \<le> y" and "y \<le> x" and "x \<le> pi"
  2767   shows "cos x \<le> cos y"
  2768 proof (cases "y < x")
  2769   case True
  2770   show ?thesis
  2771     using cos_monotone_0_pi[OF `0 \<le> y` True `x \<le> pi`] by auto
  2772 next
  2773   case False
  2774   hence "y = x" using `y \<le> x` by auto
  2775   thus ?thesis by auto
  2776 qed
  2777 
  2778 lemma cos_monotone_minus_pi_0:
  2779   assumes "-pi \<le> y" and "y < x" and "x \<le> 0"
  2780   shows "cos y < cos x"
  2781 proof -
  2782   have "0 \<le> -x" and "-x < -y" and "-y \<le> pi"
  2783     using assms by auto
  2784   from cos_monotone_0_pi[OF this] show ?thesis
  2785     unfolding cos_minus .
  2786 qed
  2787 
  2788 lemma cos_monotone_minus_pi_0':
  2789   assumes "-pi \<le> y" and "y \<le> x" and "x \<le> 0"
  2790   shows "cos y \<le> cos x"
  2791 proof (cases "y < x")
  2792   case True
  2793   show ?thesis using cos_monotone_minus_pi_0[OF `-pi \<le> y` True `x \<le> 0`]
  2794     by auto
  2795 next
  2796   case False
  2797   hence "y = x" using `y \<le> x` by auto
  2798   thus ?thesis by auto
  2799 qed
  2800 
  2801 lemma sin_monotone_2pi':
  2802   assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2"
  2803   shows "sin y \<le> sin x"
  2804 proof -
  2805   have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
  2806     using pi_ge_two and assms by auto
  2807   from cos_monotone_0_pi'[OF this] show ?thesis
  2808     unfolding minus_sin_cos_eq[symmetric] by auto
  2809 qed
  2810 
  2811 
  2812 subsection {* Tangent *}
  2813 
  2814 definition tan :: "real \<Rightarrow> real"
  2815   where "tan = (\<lambda>x. sin x / cos x)"
  2816 
  2817 lemma tan_zero [simp]: "tan 0 = 0"
  2818   by (simp add: tan_def)
  2819 
  2820 lemma tan_pi [simp]: "tan pi = 0"
  2821   by (simp add: tan_def)
  2822 
  2823 lemma tan_npi [simp]: "tan (real (n::nat) * pi) = 0"
  2824   by (simp add: tan_def)
  2825 
  2826 lemma tan_minus [simp]: "tan (-x) = - tan x"
  2827   by (simp add: tan_def)
  2828 
  2829 lemma tan_periodic [simp]: "tan (x + 2*pi) = tan x"
  2830   by (simp add: tan_def)
  2831 
  2832 lemma lemma_tan_add1:
  2833   "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> 1 - tan x * tan y = cos (x + y)/(cos x * cos y)"
  2834   by (simp add: tan_def cos_add field_simps)
  2835 
  2836 lemma add_tan_eq:
  2837   "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> tan x + tan y = sin(x + y)/(cos x * cos y)"
  2838   by (simp add: tan_def sin_add field_simps)
  2839 
  2840 lemma tan_add:
  2841      "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]
  2842       ==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
  2843   by (simp add: add_tan_eq lemma_tan_add1, simp add: tan_def)
  2844 
  2845 lemma tan_double:
  2846      "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]
  2847       ==> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)"
  2848   using tan_add [of x x] by (simp add: power2_eq_square)
  2849 
  2850 lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
  2851   by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
  2852 
  2853 lemma tan_less_zero:
  2854   assumes lb: "- pi/2 < x" and "x < 0"
  2855   shows "tan x < 0"
  2856 proof -
  2857   have "0 < tan (- x)" using assms by (simp only: tan_gt_zero)
  2858   thus ?thesis by simp
  2859 qed
  2860 
  2861 lemma tan_half: "tan x = sin (2 * x) / (cos (2 * x) + 1)"
  2862   unfolding tan_def sin_double cos_double sin_squared_eq
  2863   by (simp add: power2_eq_square)
  2864 
  2865 lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
  2866   unfolding tan_def
  2867   by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
  2868 
  2869 lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
  2870   by (rule DERIV_tan [THEN DERIV_isCont])
  2871 
  2872 lemma isCont_tan' [simp]:
  2873   "\<lbrakk>isCont f a; cos (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. tan (f x)) a"
  2874   by (rule isCont_o2 [OF _ isCont_tan])
  2875 
  2876 lemma tendsto_tan [tendsto_intros]:
  2877   "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
  2878   by (rule isCont_tendsto_compose [OF isCont_tan])
  2879 
  2880 lemma continuous_tan:
  2881   "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
  2882   unfolding continuous_def by (rule tendsto_tan)
  2883 
  2884 lemma isCont_tan'' [continuous_intros]:
  2885   "continuous (at x) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. tan (f x))"
  2886   unfolding continuous_at by (rule tendsto_tan)
  2887 
  2888 lemma continuous_within_tan [continuous_intros]:
  2889   "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
  2890   unfolding continuous_within by (rule tendsto_tan)
  2891 
  2892 lemma continuous_on_tan [continuous_intros]:
  2893   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
  2894   unfolding continuous_on_def by (auto intro: tendsto_tan)
  2895 
  2896 lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) -- pi/2 --> 0"
  2897   by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
  2898 
  2899 lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
  2900   apply (cut_tac LIM_cos_div_sin)
  2901   apply (simp only: LIM_eq)
  2902   apply (drule_tac x = "inverse y" in spec, safe, force)
  2903   apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
  2904   apply (rule_tac x = "(pi/2) - e" in exI)
  2905   apply (simp (no_asm_simp))
  2906   apply (drule_tac x = "(pi/2) - e" in spec)
  2907   apply (auto simp add: tan_def sin_diff cos_diff)
  2908   apply (rule inverse_less_iff_less [THEN iffD1])
  2909   apply (auto simp add: divide_inverse)
  2910   apply (rule mult_pos_pos)
  2911   apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
  2912   apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult_commute)
  2913   done
  2914 
  2915 lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
  2916   apply (frule order_le_imp_less_or_eq, safe)
  2917    prefer 2 apply force
  2918   apply (drule lemma_tan_total, safe)
  2919   apply (cut_tac f = tan and a = 0 and b = x and y = y in IVT_objl)
  2920   apply (auto intro!: DERIV_tan [THEN DERIV_isCont])
  2921   apply (drule_tac y = xa in order_le_imp_less_or_eq)
  2922   apply (auto dest: cos_gt_zero)
  2923   done
  2924 
  2925 lemma lemma_tan_total1: "\<exists>x. -(pi/2) < x & x < (pi/2) & tan x = y"
  2926   apply (cut_tac linorder_linear [of 0 y], safe)
  2927   apply (drule tan_total_pos)
  2928   apply (cut_tac [2] y="-y" in tan_total_pos, safe)
  2929   apply (rule_tac [3] x = "-x" in exI)
  2930   apply (auto del: exI intro!: exI)
  2931   done
  2932 
  2933 lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
  2934   apply (cut_tac y = y in lemma_tan_total1, auto)
  2935   apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
  2936   apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
  2937   apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
  2938   apply (rule_tac [4] Rolle)
  2939   apply (rule_tac [2] Rolle)
  2940   apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
  2941               simp add: real_differentiable_def)
  2942   txt{*Now, simulate TRYALL*}
  2943   apply (rule_tac [!] DERIV_tan asm_rl)
  2944   apply (auto dest!: DERIV_unique [OF _ DERIV_tan]
  2945               simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym])
  2946   done
  2947 
  2948 lemma tan_monotone:
  2949   assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2"
  2950   shows "tan y < tan x"
  2951 proof -
  2952   have "\<forall>x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)"
  2953   proof (rule allI, rule impI)
  2954     fix x' :: real
  2955     assume "y \<le> x' \<and> x' \<le> x"
  2956     hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto
  2957     from cos_gt_zero_pi[OF this]
  2958     have "cos x' \<noteq> 0" by auto
  2959     thus "DERIV tan x' :> inverse ((cos x')\<^sup>2)" by (rule DERIV_tan)
  2960   qed
  2961   from MVT2[OF `y < x` this]
  2962   obtain z where "y < z" and "z < x"
  2963     and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto
  2964   hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto
  2965   hence "0 < cos z" using cos_gt_zero_pi by auto
  2966   hence inv_pos: "0 < inverse ((cos z)\<^sup>2)" by auto
  2967   have "0 < x - y" using `y < x` by auto
  2968   with inv_pos have "0 < tan x - tan y" unfolding tan_diff by auto
  2969   thus ?thesis by auto
  2970 qed
  2971 
  2972 lemma tan_monotone':
  2973   assumes "- (pi / 2) < y"
  2974     and "y < pi / 2"
  2975     and "- (pi / 2) < x"
  2976     and "x < pi / 2"
  2977   shows "(y < x) = (tan y < tan x)"
  2978 proof
  2979   assume "y < x"
  2980   thus "tan y < tan x"
  2981     using tan_monotone and `- (pi / 2) < y` and `x < pi / 2` by auto
  2982 next
  2983   assume "tan y < tan x"
  2984   show "y < x"
  2985   proof (rule ccontr)
  2986     assume "\<not> y < x" hence "x \<le> y" by auto
  2987     hence "tan x \<le> tan y"
  2988     proof (cases "x = y")
  2989       case True thus ?thesis by auto
  2990     next
  2991       case False hence "x < y" using `x \<le> y` by auto
  2992       from tan_monotone[OF `- (pi/2) < x` this `y < pi / 2`] show ?thesis by auto
  2993     qed
  2994     thus False using `tan y < tan x` by auto
  2995   qed
  2996 qed
  2997 
  2998 lemma tan_inverse: "1 / (tan y) = tan (pi / 2 - y)"
  2999   unfolding tan_def sin_cos_eq[of y] cos_sin_eq[of y] by auto
  3000 
  3001 lemma tan_periodic_pi[simp]: "tan (x + pi) = tan x"
  3002   by (simp add: tan_def)
  3003 
  3004 lemma tan_periodic_nat[simp]:
  3005   fixes n :: nat
  3006   shows "tan (x + real n * pi) = tan x"
  3007 proof (induct n arbitrary: x)
  3008   case 0
  3009   then show ?case by simp
  3010 next
  3011   case (Suc n)
  3012   have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi"
  3013     unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
  3014   show ?case unfolding split_pi_off using Suc by auto
  3015 qed
  3016 
  3017 lemma tan_periodic_int[simp]: fixes i :: int shows "tan (x + real i * pi) = tan x"
  3018 proof (cases "0 \<le> i")
  3019   case True
  3020   hence i_nat: "real i = real (nat i)" by auto
  3021   show ?thesis unfolding i_nat by auto
  3022 next
  3023   case False
  3024   hence i_nat: "real i = - real (nat (-i))" by auto
  3025   have "tan x = tan (x + real i * pi - real i * pi)"
  3026     by auto
  3027   also have "\<dots> = tan (x + real i * pi)"
  3028     unfolding i_nat mult_minus_left diff_minus_eq_add by (rule tan_periodic_nat)
  3029   finally show ?thesis by auto
  3030 qed
  3031 
  3032 lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
  3033   using tan_periodic_int[of _ "numeral n" ] unfolding real_numeral .
  3034 
  3035 subsection {* Inverse Trigonometric Functions *}
  3036 
  3037 definition arcsin :: "real => real"
  3038   where "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
  3039 
  3040 definition arccos :: "real => real"
  3041   where "arccos y = (THE x. 0 \<le> x & x \<le> pi & cos x = y)"
  3042 
  3043 definition arctan :: "real => real"
  3044   where "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)"
  3045 
  3046 lemma arcsin:
  3047   "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow>
  3048     -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2 & sin(arcsin y) = y"
  3049   unfolding arcsin_def by (rule theI' [OF sin_total])
  3050 
  3051 lemma arcsin_pi:
  3052   "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi & sin(arcsin y) = y"
  3053   apply (drule (1) arcsin)
  3054   apply (force intro: order_trans)
  3055   done
  3056 
  3057 lemma sin_arcsin [simp]: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> sin(arcsin y) = y"
  3058   by (blast dest: arcsin)
  3059 
  3060 lemma arcsin_bounded: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2"
  3061   by (blast dest: arcsin)
  3062 
  3063 lemma arcsin_lbound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y"
  3064   by (blast dest: arcsin)
  3065 
  3066 lemma arcsin_ubound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin y \<le> pi/2"
  3067   by (blast dest: arcsin)
  3068 
  3069 lemma arcsin_lt_bounded:
  3070      "[| -1 < y; y < 1 |] ==> -(pi/2) < arcsin y & arcsin y < pi/2"
  3071   apply (frule order_less_imp_le)
  3072   apply (frule_tac y = y in order_less_imp_le)
  3073   apply (frule arcsin_bounded)
  3074   apply (safe, simp)
  3075   apply (drule_tac y = "arcsin y" in order_le_imp_less_or_eq)
  3076   apply (drule_tac [2] y = "pi/2" in order_le_imp_less_or_eq, safe)
  3077   apply (drule_tac [!] f = sin in arg_cong, auto)
  3078   done
  3079 
  3080 lemma arcsin_sin: "[|-(pi/2) \<le> x; x \<le> pi/2 |] ==> arcsin(sin x) = x"
  3081   apply (unfold arcsin_def)
  3082   apply (rule the1_equality)
  3083   apply (rule sin_total, auto)
  3084   done
  3085 
  3086 lemma arccos:
  3087      "[| -1 \<le> y; y \<le> 1 |]
  3088       ==> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
  3089   unfolding arccos_def by (rule theI' [OF cos_total])
  3090 
  3091 lemma cos_arccos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arccos y) = y"
  3092   by (blast dest: arccos)
  3093 
  3094 lemma arccos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y & arccos y \<le> pi"
  3095   by (blast dest: arccos)
  3096 
  3097 lemma arccos_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y"
  3098   by (blast dest: arccos)
  3099 
  3100 lemma arccos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arccos y \<le> pi"
  3101   by (blast dest: arccos)
  3102 
  3103 lemma arccos_lt_bounded:
  3104      "[| -1 < y; y < 1 |]
  3105       ==> 0 < arccos y & arccos y < pi"
  3106   apply (frule order_less_imp_le)
  3107   apply (frule_tac y = y in order_less_imp_le)
  3108   apply (frule arccos_bounded, auto)
  3109   apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
  3110   apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
  3111   apply (drule_tac [!] f = cos in arg_cong, auto)
  3112   done
  3113 
  3114 lemma arccos_cos: "[|0 \<le> x; x \<le> pi |] ==> arccos(cos x) = x"
  3115   apply (simp add: arccos_def)
  3116   apply (auto intro!: the1_equality cos_total)
  3117   done
  3118 
  3119 lemma arccos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arccos(cos x) = -x"
  3120   apply (simp add: arccos_def)
  3121   apply (auto intro!: the1_equality cos_total)
  3122   done
  3123 
  3124 lemma cos_arcsin: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> cos (arcsin x) = sqrt (1 - x\<^sup>2)"
  3125   apply (subgoal_tac "x\<^sup>2 \<le> 1")
  3126   apply (rule power2_eq_imp_eq)
  3127   apply (simp add: cos_squared_eq)
  3128   apply (rule cos_ge_zero)
  3129   apply (erule (1) arcsin_lbound)
  3130   apply (erule (1) arcsin_ubound)
  3131   apply simp
  3132   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
  3133   apply (rule power_mono, simp, simp)
  3134   done
  3135 
  3136 lemma sin_arccos: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> sin (arccos x) = sqrt (1 - x\<^sup>2)"
  3137   apply (subgoal_tac "x\<^sup>2 \<le> 1")
  3138   apply (rule power2_eq_imp_eq)
  3139   apply (simp add: sin_squared_eq)
  3140   apply (rule sin_ge_zero)
  3141   apply (erule (1) arccos_lbound)
  3142   apply (erule (1) arccos_ubound)
  3143   apply simp
  3144   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
  3145   apply (rule power_mono, simp, simp)
  3146   done
  3147 
  3148 lemma arctan [simp]: "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
  3149   unfolding arctan_def by (rule theI' [OF tan_total])
  3150 
  3151 lemma tan_arctan: "tan (arctan y) = y"
  3152   by auto
  3153 
  3154 lemma arctan_bounded: "- (pi/2) < arctan y  & arctan y < pi/2"
  3155   by (auto simp only: arctan)
  3156 
  3157 lemma arctan_lbound: "- (pi/2) < arctan y"
  3158   by auto
  3159 
  3160 lemma arctan_ubound: "arctan y < pi/2"
  3161   by (auto simp only: arctan)
  3162 
  3163 lemma arctan_unique:
  3164   assumes "-(pi/2) < x"
  3165     and "x < pi/2"
  3166     and "tan x = y"
  3167   shows "arctan y = x"
  3168   using assms arctan [of y] tan_total [of y] by (fast elim: ex1E)
  3169 
  3170 lemma arctan_tan: "-(pi/2) < x \<Longrightarrow> x < pi/2 \<Longrightarrow> arctan (tan x) = x"
  3171   by (rule arctan_unique) simp_all
  3172 
  3173 lemma arctan_zero_zero [simp]: "arctan 0 = 0"
  3174   by (rule arctan_unique) simp_all
  3175 
  3176 lemma arctan_minus: "arctan (- x) = - arctan x"
  3177   apply (rule arctan_unique)
  3178   apply (simp only: neg_less_iff_less arctan_ubound)
  3179   apply (metis minus_less_iff arctan_lbound)
  3180   apply simp
  3181   done
  3182 
  3183 lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
  3184   by (intro less_imp_neq [symmetric] cos_gt_zero_pi
  3185     arctan_lbound arctan_ubound)
  3186 
  3187 lemma cos_arctan: "cos (arctan x) = 1 / sqrt (1 + x\<^sup>2)"
  3188 proof (rule power2_eq_imp_eq)
  3189   have "0 < 1 + x\<^sup>2" by (simp add: add_pos_nonneg)
  3190   show "0 \<le> 1 / sqrt (1 + x\<^sup>2)" by simp
  3191   show "0 \<le> cos (arctan x)"
  3192     by (intro less_imp_le cos_gt_zero_pi arctan_lbound arctan_ubound)
  3193   have "(cos (arctan x))\<^sup>2 * (1 + (tan (arctan x))\<^sup>2) = 1"
  3194     unfolding tan_def by (simp add: distrib_left power_divide)
  3195   thus "(cos (arctan x))\<^sup>2 = (1 / sqrt (1 + x\<^sup>2))\<^sup>2"
  3196     using `0 < 1 + x\<^sup>2` by (simp add: power_divide eq_divide_eq)
  3197 qed
  3198 
  3199 lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<^sup>2)"
  3200   using add_pos_nonneg [OF zero_less_one zero_le_power2 [of x]]
  3201   using tan_arctan [of x] unfolding tan_def cos_arctan
  3202   by (simp add: eq_divide_eq)
  3203 
  3204 lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
  3205   apply (rule power_inverse [THEN subst])
  3206   apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
  3207   apply (auto dest: field_power_not_zero
  3208           simp add: power_mult_distrib distrib_right power_divide tan_def
  3209                     mult_assoc power_inverse [symmetric])
  3210   done
  3211 
  3212 lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
  3213   by (metis tan_monotone' arctan_lbound arctan_ubound tan_arctan)
  3214 
  3215 lemma arctan_le_iff: "arctan x \<le> arctan y \<longleftrightarrow> x \<le> y"
  3216   by (simp only: not_less [symmetric] arctan_less_iff)
  3217 
  3218 lemma arctan_eq_iff: "arctan x = arctan y \<longleftrightarrow> x = y"
  3219   by (simp only: eq_iff [where 'a=real] arctan_le_iff)
  3220 
  3221 lemma zero_less_arctan_iff [simp]: "0 < arctan x \<longleftrightarrow> 0 < x"
  3222   using arctan_less_iff [of 0 x] by simp
  3223 
  3224 lemma arctan_less_zero_iff [simp]: "arctan x < 0 \<longleftrightarrow> x < 0"
  3225   using arctan_less_iff [of x 0] by simp
  3226 
  3227 lemma zero_le_arctan_iff [simp]: "0 \<le> arctan x \<longleftrightarrow> 0 \<le> x"
  3228   using arctan_le_iff [of 0 x] by simp
  3229 
  3230 lemma arctan_le_zero_iff [simp]: "arctan x \<le> 0 \<longleftrightarrow> x \<le> 0"
  3231   using arctan_le_iff [of x 0] by simp
  3232 
  3233 lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
  3234   using arctan_eq_iff [of x 0] by simp
  3235 
  3236 lemma continuous_on_arcsin': "continuous_on {-1 .. 1} arcsin"
  3237 proof -
  3238   have "continuous_on (sin ` {- pi / 2 .. pi / 2}) arcsin"
  3239     by (rule continuous_on_inv) (auto intro: continuous_intros simp: arcsin_sin)
  3240   also have "sin ` {- pi / 2 .. pi / 2} = {-1 .. 1}"
  3241   proof safe
  3242     fix x :: real
  3243     assume "x \<in> {-1..1}"
  3244     then show "x \<in> sin ` {- pi / 2..pi / 2}"
  3245       using arcsin_lbound arcsin_ubound
  3246       by (intro image_eqI[where x="arcsin x"]) auto
  3247   qed simp
  3248   finally show ?thesis .
  3249 qed
  3250 
  3251 lemma continuous_on_arcsin [continuous_intros]:
  3252   "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))"
  3253   using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arcsin']]
  3254   by (auto simp: comp_def subset_eq)
  3255 
  3256 lemma isCont_arcsin: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> isCont arcsin x"
  3257   using continuous_on_arcsin'[THEN continuous_on_subset, of "{ -1 <..< 1 }"]
  3258   by (auto simp: continuous_on_eq_continuous_at subset_eq)
  3259 
  3260 lemma continuous_on_arccos': "continuous_on {-1 .. 1} arccos"
  3261 proof -
  3262   have "continuous_on (cos ` {0 .. pi}) arccos"
  3263     by (rule continuous_on_inv) (auto intro: continuous_intros simp: arccos_cos)
  3264   also have "cos ` {0 .. pi} = {-1 .. 1}"
  3265   proof safe
  3266     fix x :: real
  3267     assume "x \<in> {-1..1}"
  3268     then show "x \<in> cos ` {0..pi}"
  3269       using arccos_lbound arccos_ubound
  3270       by (intro image_eqI[where x="arccos x"]) auto
  3271   qed simp
  3272   finally show ?thesis .
  3273 qed
  3274 
  3275 lemma continuous_on_arccos [continuous_intros]:
  3276   "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))"
  3277   using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arccos']]
  3278   by (auto simp: comp_def subset_eq)
  3279 
  3280 lemma isCont_arccos: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> isCont arccos x"
  3281   using continuous_on_arccos'[THEN continuous_on_subset, of "{ -1 <..< 1 }"]
  3282   by (auto simp: continuous_on_eq_continuous_at subset_eq)
  3283 
  3284 lemma isCont_arctan: "isCont arctan x"
  3285   apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify)
  3286   apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
  3287   apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
  3288   apply (erule (1) isCont_inverse_function2 [where f=tan])
  3289   apply (metis arctan_tan order_le_less_trans order_less_le_trans)
  3290   apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
  3291   done
  3292 
  3293 lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
  3294   by (rule isCont_tendsto_compose [OF isCont_arctan])
  3295 
  3296 lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
  3297   unfolding continuous_def by (rule tendsto_arctan)
  3298 
  3299 lemma continuous_on_arctan [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
  3300   unfolding continuous_on_def by (auto intro: tendsto_arctan)
  3301 
  3302 lemma DERIV_arcsin:
  3303   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<^sup>2))"
  3304   apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
  3305   apply (rule DERIV_cong [OF DERIV_sin])
  3306   apply (simp add: cos_arcsin)
  3307   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  3308   apply (rule power_strict_mono, simp, simp, simp)
  3309   apply assumption
  3310   apply assumption
  3311   apply simp
  3312   apply (erule (1) isCont_arcsin)
  3313   done
  3314 
  3315 lemma DERIV_arccos:
  3316   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<^sup>2))"
  3317   apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
  3318   apply (rule DERIV_cong [OF DERIV_cos])
  3319   apply (simp add: sin_arccos)
  3320   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  3321   apply (rule power_strict_mono, simp, simp, simp)
  3322   apply assumption
  3323   apply assumption
  3324   apply simp
  3325   apply (erule (1) isCont_arccos)
  3326   done
  3327 
  3328 lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)"
  3329   apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
  3330   apply (rule DERIV_cong [OF DERIV_tan])
  3331   apply (rule cos_arctan_not_zero)
  3332   apply (simp add: power_inverse tan_sec [symmetric])
  3333   apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
  3334   apply (simp add: add_pos_nonneg)
  3335   apply (simp, simp, simp, rule isCont_arctan)
  3336   done
  3337 
  3338 declare
  3339   DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
  3340   DERIV_arccos[THEN DERIV_chain2, derivative_intros]
  3341   DERIV_arctan[THEN DERIV_chain2, derivative_intros]
  3342 
  3343 lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
  3344   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])
  3345      (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
  3346            intro!: tan_monotone exI[of _ "pi/2"])
  3347 
  3348 lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
  3349   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])
  3350      (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
  3351            intro!: tan_monotone exI[of _ "pi/2"])
  3352 
  3353 lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"
  3354 proof (rule tendstoI)
  3355   fix e :: real
  3356   assume "0 < e"
  3357   def y \<equiv> "pi/2 - min (pi/2) e"
  3358   then have y: "0 \<le> y" "y < pi/2" "pi/2 \<le> e + y"
  3359     using `0 < e` by auto
  3360 
  3361   show "eventually (\<lambda>x. dist (arctan x) (pi / 2) < e) at_top"
  3362   proof (intro eventually_at_top_dense[THEN iffD2] exI allI impI)
  3363     fix x
  3364     assume "tan y < x"
  3365     then have "arctan (tan y) < arctan x"
  3366       by (simp add: arctan_less_iff)
  3367     with y have "y < arctan x"
  3368       by (subst (asm) arctan_tan) simp_all
  3369     with arctan_ubound[of x, arith] y `0 < e`
  3370     show "dist (arctan x) (pi / 2) < e"
  3371       by (simp add: dist_real_def)
  3372   qed
  3373 qed
  3374 
  3375 lemma tendsto_arctan_at_bot: "(arctan ---> - (pi/2)) at_bot"
  3376   unfolding filterlim_at_bot_mirror arctan_minus
  3377   by (intro tendsto_minus tendsto_arctan_at_top)
  3378 
  3379 
  3380 subsection {* More Theorems about Sin and Cos *}
  3381 
  3382 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
  3383 proof -
  3384   let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
  3385   have nonneg: "0 \<le> ?c"
  3386     by (simp add: cos_ge_zero)
  3387   have "0 = cos (pi / 4 + pi / 4)"
  3388     by simp
  3389   also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
  3390     by (simp only: cos_add power2_eq_square)
  3391   also have "\<dots> = 2 * ?c\<^sup>2 - 1"
  3392     by (simp add: sin_squared_eq)
  3393   finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
  3394     by (simp add: power_divide)
  3395   thus ?thesis
  3396     using nonneg by (rule power2_eq_imp_eq) simp
  3397 qed
  3398 
  3399 lemma cos_30: "cos (pi / 6) = sqrt 3 / 2"
  3400 proof -
  3401   let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
  3402   have pos_c: "0 < ?c"
  3403     by (rule cos_gt_zero, simp, simp)
  3404   have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
  3405     by simp
  3406   also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
  3407     by (simp only: cos_add sin_add)
  3408   also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
  3409     by (simp add: algebra_simps power2_eq_square)
  3410   finally have "?c\<^sup>2 = (sqrt 3 / 2)\<^sup>2"
  3411     using pos_c by (simp add: sin_squared_eq power_divide)
  3412   thus ?thesis
  3413     using pos_c [THEN order_less_imp_le]
  3414     by (rule power2_eq_imp_eq) simp
  3415 qed
  3416 
  3417 lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
  3418   by (simp add: sin_cos_eq cos_45)
  3419 
  3420 lemma sin_60: "sin (pi / 3) = sqrt 3 / 2"
  3421   by (simp add: sin_cos_eq cos_30)
  3422 
  3423 lemma cos_60: "cos (pi / 3) = 1 / 2"
  3424   apply (rule power2_eq_imp_eq)
  3425   apply (simp add: cos_squared_eq sin_60 power_divide)
  3426   apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
  3427   done
  3428 
  3429 lemma sin_30: "sin (pi / 6) = 1 / 2"
  3430   by (simp add: sin_cos_eq cos_60)
  3431 
  3432 lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
  3433   unfolding tan_def by (simp add: sin_30 cos_30)
  3434 
  3435 lemma tan_45: "tan (pi / 4) = 1"
  3436   unfolding tan_def by (simp add: sin_45 cos_45)
  3437 
  3438 lemma tan_60: "tan (pi / 3) = sqrt 3"
  3439   unfolding tan_def by (simp add: sin_60 cos_60)
  3440 
  3441 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
  3442 proof -
  3443   have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
  3444     by (auto simp add: algebra_simps sin_add)
  3445   thus ?thesis
  3446     by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
  3447                   mult_commute [of pi])
  3448 qed
  3449 
  3450 lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
  3451   by (simp add: cos_double mult_assoc power_add [symmetric] numeral_2_eq_2)
  3452 
  3453 lemma cos_3over2_pi [simp]: "cos (3 / 2 * pi) = 0"
  3454   apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
  3455   apply (subst cos_add, simp)
  3456   done
  3457 
  3458 lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
  3459   by (auto simp add: mult_assoc)
  3460 
  3461 lemma sin_3over2_pi [simp]: "sin (3 / 2 * pi) = - 1"
  3462   apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
  3463   apply (subst sin_add, simp)
  3464   done
  3465 
  3466 lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
  3467   apply (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib)
  3468   apply auto
  3469   done
  3470 
  3471 lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
  3472   by (auto intro!: derivative_eq_intros)
  3473 
  3474 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
  3475   by (auto simp add: sin_zero_iff even_mult_two_ex)
  3476 
  3477 lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0"
  3478   using sin_cos_squared_add3 [where x = x] by auto
  3479 
  3480 
  3481 subsection {* Machins formula *}
  3482 
  3483 lemma arctan_one: "arctan 1 = pi / 4"
  3484   by (rule arctan_unique, simp_all add: tan_45 m2pi_less_pi)
  3485 
  3486 lemma tan_total_pi4:
  3487   assumes "\<bar>x\<bar> < 1"
  3488   shows "\<exists>z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x"
  3489 proof
  3490   show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x"
  3491     unfolding arctan_one [symmetric] arctan_minus [symmetric]
  3492     unfolding arctan_less_iff using assms by auto
  3493 qed
  3494 
  3495 lemma arctan_add:
  3496   assumes "\<bar>x\<bar> \<le> 1" and "\<bar>y\<bar> < 1"
  3497   shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))"
  3498 proof (rule arctan_unique [symmetric])
  3499   have "- (pi / 4) \<le> arctan x" and "- (pi / 4) < arctan y"
  3500     unfolding arctan_one [symmetric] arctan_minus [symmetric]
  3501     unfolding arctan_le_iff arctan_less_iff using assms by auto
  3502   from add_le_less_mono [OF this]
  3503   show 1: "- (pi / 2) < arctan x + arctan y" by simp
  3504   have "arctan x \<le> pi / 4" and "arctan y < pi / 4"
  3505     unfolding arctan_one [symmetric]
  3506     unfolding arctan_le_iff arctan_less_iff using assms by auto
  3507   from add_le_less_mono [OF this]
  3508   show 2: "arctan x + arctan y < pi / 2" by simp
  3509   show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
  3510     using cos_gt_zero_pi [OF 1 2] by (simp add: tan_add)
  3511 qed
  3512 
  3513 theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)"
  3514 proof -
  3515   have "\<bar>1 / 5\<bar> < (1 :: real)" by auto
  3516   from arctan_add[OF less_imp_le[OF this] this]
  3517   have "2 * arctan (1 / 5) = arctan (5 / 12)" by auto
  3518   moreover
  3519   have "\<bar>5 / 12\<bar> < (1 :: real)" by auto
  3520   from arctan_add[OF less_imp_le[OF this] this]
  3521   have "2 * arctan (5 / 12) = arctan (120 / 119)" by auto
  3522   moreover
  3523   have "\<bar>1\<bar> \<le> (1::real)" and "\<bar>1 / 239\<bar> < (1::real)" by auto
  3524   from arctan_add[OF this]
  3525   have "arctan 1 + arctan (1 / 239) = arctan (120 / 119)" by auto
  3526   ultimately have "arctan 1 + arctan (1 / 239) = 4 * arctan (1 / 5)" by auto
  3527   thus ?thesis unfolding arctan_one by algebra
  3528 qed
  3529 
  3530 
  3531 subsection {* Introducing the arcus tangens power series *}
  3532 
  3533 lemma monoseq_arctan_series:
  3534   fixes x :: real
  3535   assumes "\<bar>x\<bar> \<le> 1"
  3536   shows "monoseq (\<lambda> n. 1 / real (n*2+1) * x^(n*2+1))" (is "monoseq ?a")
  3537 proof (cases "x = 0")
  3538   case True
  3539   thus ?thesis unfolding monoseq_def One_nat_def by auto
  3540 next
  3541   case False
  3542   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
  3543   show "monoseq ?a"
  3544   proof -
  3545     {
  3546       fix n
  3547       fix x :: real
  3548       assume "0 \<le> x" and "x \<le> 1"
  3549       have "1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<le>
  3550         1 / real (Suc (n * 2)) * x ^ Suc (n * 2)"
  3551       proof (rule mult_mono)
  3552         show "1 / real (Suc (Suc n * 2)) \<le> 1 / real (Suc (n * 2))"
  3553           by (rule frac_le) simp_all
  3554         show "0 \<le> 1 / real (Suc (n * 2))"
  3555           by auto
  3556         show "x ^ Suc (Suc n * 2) \<le> x ^ Suc (n * 2)"
  3557           by (rule power_decreasing) (simp_all add: `0 \<le> x` `x \<le> 1`)
  3558         show "0 \<le> x ^ Suc (Suc n * 2)"
  3559           by (rule zero_le_power) (simp add: `0 \<le> x`)
  3560       qed
  3561     } note mono = this
  3562 
  3563     show ?thesis
  3564     proof (cases "0 \<le> x")
  3565       case True from mono[OF this `x \<le> 1`, THEN allI]
  3566       show ?thesis unfolding Suc_eq_plus1[symmetric]
  3567         by (rule mono_SucI2)
  3568     next
  3569       case False
  3570       hence "0 \<le> -x" and "-x \<le> 1" using `-1 \<le> x` by auto
  3571       from mono[OF this]
  3572       have "\<And>n. 1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<ge>
  3573         1 / real (Suc (n * 2)) * x ^ Suc (n * 2)" using `0 \<le> -x` by auto
  3574       thus ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI1[OF allI])
  3575     qed
  3576   qed
  3577 qed
  3578 
  3579 lemma zeroseq_arctan_series:
  3580   fixes x :: real
  3581   assumes "\<bar>x\<bar> \<le> 1"
  3582   shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
  3583 proof (cases "x = 0")
  3584   case True
  3585   thus ?thesis
  3586     unfolding One_nat_def by (auto simp add: tendsto_const)
  3587 next
  3588   case False
  3589   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
  3590   show "?a ----> 0"
  3591   proof (cases "\<bar>x\<bar> < 1")
  3592     case True
  3593     hence "norm x < 1" by auto
  3594     from tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
  3595     have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
  3596       unfolding inverse_eq_divide Suc_eq_plus1 by simp
  3597     then show ?thesis using pos2 by (rule LIMSEQ_linear)
  3598   next
  3599     case False
  3600     hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
  3601     hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x"
  3602       unfolding One_nat_def by auto
  3603     from tendsto_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] tendsto_const[of x]]
  3604     show ?thesis unfolding n_eq Suc_eq_plus1 by auto
  3605   qed
  3606 qed
  3607 
  3608 lemma summable_arctan_series:
  3609   fixes x :: real and n :: nat
  3610   assumes "\<bar>x\<bar> \<le> 1"
  3611   shows "summable (\<lambda> k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
  3612   (is "summable (?c x)")
  3613   by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms])
  3614 
  3615 lemma less_one_imp_sqr_less_one:
  3616   fixes x :: real
  3617   assumes "\<bar>x\<bar> < 1"
  3618   shows "x\<^sup>2 < 1"
  3619 proof -
  3620   have "\<bar>x\<^sup>2\<bar> < 1"
  3621     by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff) 
  3622   thus ?thesis using zero_le_power2 by auto
  3623 qed
  3624 
  3625 lemma DERIV_arctan_series:
  3626   assumes "\<bar> x \<bar> < 1"
  3627   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))"
  3628   (is "DERIV ?arctan _ :> ?Int")
  3629 proof -
  3630   let ?f = "\<lambda>n. if even n then (-1)^(n div 2) * 1 / real (Suc n) else 0"
  3631 
  3632   have n_even: "\<And>n :: nat. even n \<Longrightarrow> 2 * (n div 2) = n"
  3633     by presburger
  3634   then have if_eq: "\<And>n x'. ?f n * real (Suc n) * x'^n =
  3635     (if even n then (-1)^(n div 2) * x'^(2 * (n div 2)) else 0)"
  3636     by auto
  3637 
  3638   {
  3639     fix x :: real
  3640     assume "\<bar>x\<bar> < 1"
  3641     hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
  3642     have "summable (\<lambda> n. -1 ^ n * (x\<^sup>2) ^n)"
  3643       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`])
  3644     hence "summable (\<lambda> n. -1 ^ n * x^(2*n))" unfolding power_mult .
  3645   } note summable_Integral = this
  3646 
  3647   {
  3648     fix f :: "nat \<Rightarrow> real"
  3649     have "\<And>x. f sums x = (\<lambda> n. if even n then f (n div 2) else 0) sums x"
  3650     proof
  3651       fix x :: real
  3652       assume "f sums x"
  3653       from sums_if[OF sums_zero this]
  3654       show "(\<lambda>n. if even n then f (n div 2) else 0) sums x"
  3655         by auto
  3656     next
  3657       fix x :: real
  3658       assume "(\<lambda> n. if even n then f (n div 2) else 0) sums x"
  3659       from LIMSEQ_linear[OF this[unfolded sums_def] pos2, unfolded sum_split_even_odd[unfolded mult_commute]]
  3660       show "f sums x" unfolding sums_def by auto
  3661     qed
  3662     hence "op sums f = op sums (\<lambda> n. if even n then f (n div 2) else 0)" ..
  3663   } note sums_even = this
  3664 
  3665   have Int_eq: "(\<Sum>n. ?f n * real (Suc n) * x^n) = ?Int"
  3666     unfolding if_eq mult_commute[of _ 2] suminf_def sums_even[of "\<lambda> n. -1 ^ n * x ^ (2 * n)", symmetric]
  3667     by auto
  3668 
  3669   {
  3670     fix x :: real
  3671     have if_eq': "\<And>n. (if even n then -1 ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
  3672       (if even n then -1 ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
  3673       using n_even by auto
  3674     have idx_eq: "\<And>n. n * 2 + 1 = Suc (2 * n)" by auto
  3675     have "(\<Sum>n. ?f n * x^(Suc n)) = ?arctan x"
  3676       unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. -1 ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
  3677       by auto
  3678   } note arctan_eq = this
  3679 
  3680   have "DERIV (\<lambda> x. \<Sum> n. ?f n * x^(Suc n)) x :> (\<Sum> n. ?f n * real (Suc n) * x^n)"
  3681   proof (rule DERIV_power_series')
  3682     show "x \<in> {- 1 <..< 1}" using `\<bar> x \<bar> < 1` by auto
  3683     {
  3684       fix x' :: real
  3685       assume x'_bounds: "x' \<in> {- 1 <..< 1}"
  3686       hence "\<bar>x'\<bar> < 1" by auto
  3687 
  3688       let ?S = "\<Sum> n. (-1)^n * x'^(2 * n)"
  3689       show "summable (\<lambda> n. ?f n * real (Suc n) * x'^n)" unfolding if_eq
  3690         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`])
  3691     }
  3692   qed auto
  3693   thus ?thesis unfolding Int_eq arctan_eq .
  3694 qed
  3695 
  3696 lemma arctan_series:
  3697   assumes "\<bar> x \<bar> \<le> 1"
  3698   shows "arctan x = (\<Sum>k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
  3699   (is "_ = suminf (\<lambda> n. ?c x n)")
  3700 proof -
  3701   let ?c' = "\<lambda>x n. (-1)^n * x^(n*2)"
  3702 
  3703   {
  3704     fix r x :: real
  3705     assume "0 < r" and "r < 1" and "\<bar> x \<bar> < r"
  3706     have "\<bar>x\<bar> < 1" using `r < 1` and `\<bar>x\<bar> < r` by auto
  3707     from DERIV_arctan_series[OF this] have "DERIV (\<lambda> x. suminf (?c x)) x :> (suminf (?c' x))" .
  3708   } note DERIV_arctan_suminf = this
  3709 
  3710   {
  3711     fix x :: real
  3712     assume "\<bar>x\<bar> \<le> 1"
  3713     note summable_Leibniz[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]]
  3714   } note arctan_series_borders = this
  3715 
  3716   {
  3717     fix x :: real
  3718     assume "\<bar>x\<bar> < 1"
  3719     have "arctan x = (\<Sum>k. ?c x k)"
  3720     proof -
  3721       obtain r where "\<bar>x\<bar> < r" and "r < 1"
  3722         using dense[OF `\<bar>x\<bar> < 1`] by blast
  3723       hence "0 < r" and "-r < x" and "x < r" by auto
  3724 
  3725       have suminf_eq_arctan_bounded: "\<And>x a b. \<lbrakk> -r < a ; b < r ; a < b ; a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow>
  3726         suminf (?c x) - arctan x = suminf (?c a) - arctan a"
  3727       proof -
  3728         fix x a b
  3729         assume "-r < a" and "b < r" and "a < b" and "a \<le> x" and "x \<le> b"
  3730         hence "\<bar>x\<bar> < r" by auto
  3731         show "suminf (?c x) - arctan x = suminf (?c a) - arctan a"
  3732         proof (rule DERIV_isconst2[of "a" "b"])
  3733           show "a < b" and "a \<le> x" and "x \<le> b"
  3734             using `a < b` `a \<le> x` `x \<le> b` by auto
  3735           have "\<forall>x. -r < x \<and> x < r \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
  3736           proof (rule allI, rule impI)
  3737             fix x
  3738             assume "-r < x \<and> x < r"
  3739             hence "\<bar>x\<bar> < r" by auto
  3740             hence "\<bar>x\<bar> < 1" using `r < 1` by auto
  3741             have "\<bar> - (x\<^sup>2) \<bar> < 1"
  3742               using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
  3743             hence "(\<lambda> n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))"
  3744               unfolding real_norm_def[symmetric] by (rule geometric_sums)
  3745             hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))"
  3746               unfolding power_mult_distrib[symmetric] power_mult nat_mult_commute[of _ 2] by auto
  3747             hence suminf_c'_eq_geom: "inverse (1 + x\<^sup>2) = suminf (?c' x)"
  3748               using sums_unique unfolding inverse_eq_divide by auto
  3749             have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))"
  3750               unfolding suminf_c'_eq_geom
  3751               by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
  3752             from DERIV_diff [OF this DERIV_arctan]
  3753             show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
  3754               by auto
  3755           qed
  3756           hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
  3757             using `-r < a` `b < r` by auto
  3758           thus "\<forall> y. a < y \<and> y < b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
  3759             using `\<bar>x\<bar> < r` by auto
  3760           show "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> isCont (\<lambda> x. suminf (?c x) - arctan x) y"
  3761             using DERIV_in_rball DERIV_isCont by auto
  3762         qed
  3763       qed
  3764 
  3765       have suminf_arctan_zero: "suminf (?c 0) - arctan 0 = 0"
  3766         unfolding Suc_eq_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero
  3767         by auto
  3768 
  3769       have "suminf (?c x) - arctan x = 0"
  3770       proof (cases "x = 0")
  3771         case True
  3772         thus ?thesis using suminf_arctan_zero by auto
  3773       next
  3774         case False
  3775         hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
  3776         have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
  3777           by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
  3778             (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  3779         moreover
  3780         have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
  3781           by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
  3782              (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  3783         ultimately
  3784         show ?thesis using suminf_arctan_zero by auto
  3785       qed
  3786       thus ?thesis by auto
  3787     qed
  3788   } note when_less_one = this
  3789 
  3790   show "arctan x = suminf (\<lambda> n. ?c x n)"
  3791   proof (cases "\<bar>x\<bar> < 1")
  3792     case True
  3793     thus ?thesis by (rule when_less_one)
  3794   next
  3795     case False
  3796     hence "\<bar>x\<bar> = 1" using `\<bar>x\<bar> \<le> 1` by auto
  3797     let ?a = "\<lambda>x n. \<bar>1 / real (n*2+1) * x^(n*2+1)\<bar>"
  3798     let ?diff = "\<lambda> x n. \<bar> arctan x - (\<Sum> i<n. ?c x i)\<bar>"
  3799     {
  3800       fix n :: nat
  3801       have "0 < (1 :: real)" by auto
  3802       moreover
  3803       {
  3804         fix x :: real
  3805         assume "0 < x" and "x < 1"
  3806         hence "\<bar>x\<bar> \<le> 1" and "\<bar>x\<bar> < 1" by auto
  3807         from `0 < x` have "0 < 1 / real (0 * 2 + (1::nat)) * x ^ (0 * 2 + 1)"
  3808           by auto
  3809         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]
  3810         have "0 < 1 / real (n*2+1) * x^(n*2+1)"
  3811           by (rule mult_pos_pos, auto simp only: zero_less_power[OF `0 < x`], auto)
  3812         hence a_pos: "?a x n = 1 / real (n*2+1) * x^(n*2+1)"
  3813           by (rule abs_of_pos)
  3814         have "?diff x n \<le> ?a x n"
  3815         proof (cases "even n")
  3816           case True
  3817           hence sgn_pos: "(-1)^n = (1::real)" by auto
  3818           from `even n` obtain m where "2 * m = n"
  3819             unfolding even_mult_two_ex by auto
  3820           from bounds[of m, unfolded this atLeastAtMost_iff]
  3821           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))"
  3822             by auto
  3823           also have "\<dots> = ?c x n" unfolding One_nat_def by auto
  3824           also have "\<dots> = ?a x n" unfolding sgn_pos a_pos by auto
  3825           finally show ?thesis .
  3826         next
  3827           case False
  3828           hence sgn_neg: "(-1)^n = (-1::real)" by auto
  3829           from `odd n` obtain m where m_def: "2 * m + 1 = n"
  3830             unfolding odd_Suc_mult_two_ex by auto
  3831           hence m_plus: "2 * (m + 1) = n + 1" by auto
  3832           from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
  3833           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))"
  3834             by auto
  3835           also have "\<dots> = - ?c x n" unfolding One_nat_def by auto
  3836           also have "\<dots> = ?a x n" unfolding sgn_neg a_pos by auto
  3837           finally show ?thesis .
  3838         qed
  3839         hence "0 \<le> ?a x n - ?diff x n" by auto
  3840       }
  3841       hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
  3842       moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
  3843         unfolding diff_conv_add_uminus divide_inverse
  3844         by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan
  3845           isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum
  3846           simp del: add_uminus_conv_diff)
  3847       ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
  3848         by (rule LIM_less_bound)
  3849       hence "?diff 1 n \<le> ?a 1 n" by auto
  3850     }
  3851     have "?a 1 ----> 0"
  3852       unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
  3853       by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
  3854     have "?diff 1 ----> 0"
  3855     proof (rule LIMSEQ_I)
  3856       fix r :: real
  3857       assume "0 < r"
  3858       obtain N :: nat where N_I: "\<And>n. N \<le> n \<Longrightarrow> ?a 1 n < r"
  3859         using LIMSEQ_D[OF `?a 1 ----> 0` `0 < r`] by auto
  3860       {
  3861         fix n
  3862         assume "N \<le> n" from `?diff 1 n \<le> ?a 1 n` N_I[OF this]
  3863         have "norm (?diff 1 n - 0) < r" by auto
  3864       }
  3865       thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
  3866     qed
  3867     from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
  3868     have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
  3869     hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
  3870 
  3871     show ?thesis
  3872     proof (cases "x = 1")
  3873       case True
  3874       then show ?thesis by (simp add: `arctan 1 = (\<Sum> i. ?c 1 i)`)
  3875     next
  3876       case False
  3877       hence "x = -1" using `\<bar>x\<bar> = 1` by auto
  3878 
  3879       have "- (pi / 2) < 0" using pi_gt_zero by auto
  3880       have "- (2 * pi) < 0" using pi_gt_zero by auto
  3881 
  3882       have c_minus_minus: "\<And>i. ?c (- 1) i = - ?c 1 i"
  3883         unfolding One_nat_def by auto
  3884 
  3885       have "arctan (- 1) = arctan (tan (-(pi / 4)))"
  3886         unfolding tan_45 tan_minus ..
  3887       also have "\<dots> = - (pi / 4)"
  3888         by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
  3889       also have "\<dots> = - (arctan (tan (pi / 4)))"
  3890         unfolding neg_equal_iff_equal by (rule arctan_tan[symmetric], auto simp add: order_less_trans[OF `- (2 * pi) < 0` pi_gt_zero])
  3891       also have "\<dots> = - (arctan 1)"
  3892         unfolding tan_45 ..
  3893       also have "\<dots> = - (\<Sum> i. ?c 1 i)"
  3894         using `arctan 1 = (\<Sum> i. ?c 1 i)` by auto
  3895       also have "\<dots> = (\<Sum> i. ?c (- 1) i)"
  3896         using suminf_minus[OF sums_summable[OF `(?c 1) sums (arctan 1)`]]
  3897         unfolding c_minus_minus by auto
  3898       finally show ?thesis using `x = -1` by auto
  3899     qed
  3900   qed
  3901 qed
  3902 
  3903 lemma arctan_half:
  3904   fixes x :: real
  3905   shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x\<^sup>2)))"
  3906 proof -
  3907   obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x"
  3908     using tan_total by blast
  3909   hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2"
  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 using `cos y \<noteq> 0` by (simp add: field_simps)
  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