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