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