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