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