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