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