src/HOL/Transcendental.thy
author haftmann
Tue Oct 21 21:10:44 2014 +0200 (2014-10-21)
changeset 58740 cb9d84d3e7f2
parent 58729 e8ecc79aee43
child 58834 773b378d9313
permissions -rw-r--r--
turn even into an abbreviation
     1 (*  Title:      HOL/Transcendental.thy
     2     Author:     Jacques D. Fleuriot, University of Cambridge, University of Edinburgh
     3     Author:     Lawrence C Paulson
     4     Author:     Jeremy Avigad
     5 *)
     6 
     7 header{*Power Series, Transcendental Functions etc.*}
     8 
     9 theory Transcendental
    10 imports Fact Series Deriv NthRoot
    11 begin
    12 
    13 lemma root_test_convergence:
    14   fixes f :: "nat \<Rightarrow> 'a::banach"
    15   assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
    16   assumes "x < 1"
    17   shows "summable f"
    18 proof -
    19   have "0 \<le> x"
    20     by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1])
    21   from `x < 1` obtain z where z: "x < z" "z < 1"
    22     by (metis dense)
    23   from f `x < z`
    24   have "eventually (\<lambda>n. root n (norm (f n)) < z) sequentially"
    25     by (rule order_tendstoD)
    26   then have "eventually (\<lambda>n. norm (f n) \<le> z^n) sequentially"
    27     using eventually_ge_at_top
    28   proof eventually_elim
    29     fix n assume less: "root n (norm (f n)) < z" and n: "1 \<le> n"
    30     from power_strict_mono[OF less, of n] n
    31     show "norm (f n) \<le> z ^ n"
    32       by simp
    33   qed
    34   then show "summable f"
    35     unfolding eventually_sequentially
    36     using z `0 \<le> x` by (auto intro!: summable_comparison_test[OF _  summable_geometric])
    37 qed
    38 
    39 subsection {* Properties of Power Series *}
    40 
    41 lemma lemma_realpow_diff:
    42   fixes y :: "'a::monoid_mult"
    43   shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
    44 proof -
    45   assume "p \<le> n"
    46   hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le)
    47   thus ?thesis by (simp add: power_commutes)
    48 qed
    49 
    50 lemma lemma_realpow_diff_sumr2:
    51   fixes y :: "'a::{comm_ring,monoid_mult}"
    52   shows
    53     "x ^ (Suc n) - y ^ (Suc n) =
    54       (x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))"
    55 proof (induct n)
    56   case (Suc n)
    57   have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x ^ n) - y * (y * y ^ n)"
    58     by simp
    59   also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x ^ n)"
    60     by (simp add: algebra_simps)
    61   also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    62     by (simp only: Suc)
    63   also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    64     by (simp only: mult.left_commute)
    65   also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
    66     by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
    67   finally show ?case .
    68 qed simp
    69 
    70 corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *}
    71   fixes x :: "'a::{comm_ring,monoid_mult}"
    72   shows   "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
    73 using lemma_realpow_diff_sumr2[of x "n - 1" y]
    74 by (cases "n = 0") (simp_all add: field_simps)
    75 
    76 lemma lemma_realpow_rev_sumr:
    77    "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
    78     (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
    79   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 add: odd_two_times_div_two_Suc)
   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 lemmas mult_exp_exp = exp_add [symmetric]
  1110 
  1111 lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
  1112   unfolding exp_def
  1113   apply (subst suminf_of_real)
  1114   apply (rule summable_exp_generic)
  1115   apply (simp add: scaleR_conv_of_real)
  1116   done
  1117 
  1118 lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
  1119 proof
  1120   have "exp x * exp (- x) = 1" by (simp add: exp_add_commuting[symmetric])
  1121   also assume "exp x = 0"
  1122   finally show "False" by simp
  1123 qed
  1124 
  1125 lemma exp_minus_inverse:
  1126   shows "exp x * exp (- x) = 1"
  1127   by (simp add: exp_add_commuting[symmetric])
  1128 
  1129 lemma exp_minus:
  1130   fixes x :: "'a::{real_normed_field, banach}"
  1131   shows "exp (- x) = inverse (exp x)"
  1132   by (intro inverse_unique [symmetric] exp_minus_inverse)
  1133 
  1134 lemma exp_diff:
  1135   fixes x :: "'a::{real_normed_field, banach}"
  1136   shows "exp (x - y) = exp x / exp y"
  1137   using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
  1138 
  1139 
  1140 subsubsection {* Properties of the Exponential Function on Reals *}
  1141 
  1142 text {* Comparisons of @{term "exp x"} with zero. *}
  1143 
  1144 text{*Proof: because every exponential can be seen as a square.*}
  1145 lemma exp_ge_zero [simp]: "0 \<le> exp (x::real)"
  1146 proof -
  1147   have "0 \<le> exp (x/2) * exp (x/2)" by simp
  1148   thus ?thesis by (simp add: exp_add [symmetric])
  1149 qed
  1150 
  1151 lemma exp_gt_zero [simp]: "0 < exp (x::real)"
  1152   by (simp add: order_less_le)
  1153 
  1154 lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0"
  1155   by (simp add: not_less)
  1156 
  1157 lemma not_exp_le_zero [simp]: "\<not> exp (x::real) \<le> 0"
  1158   by (simp add: not_le)
  1159 
  1160 lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
  1161   by simp
  1162 
  1163 lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
  1164   by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
  1165 
  1166 text {* Strict monotonicity of exponential. *}
  1167 
  1168 lemma exp_ge_add_one_self_aux: 
  1169   assumes "0 \<le> (x::real)" shows "1+x \<le> exp(x)"
  1170 using order_le_imp_less_or_eq [OF assms]
  1171 proof 
  1172   assume "0 < x"
  1173   have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
  1174     by (auto simp add: numeral_2_eq_2)
  1175   also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
  1176     apply (rule setsum_le_suminf [OF summable_exp])
  1177     using `0 < x`
  1178     apply (auto  simp add:  zero_le_mult_iff)
  1179     done
  1180   finally show "1+x \<le> exp x" 
  1181     by (simp add: exp_def)
  1182 next
  1183   assume "0 = x"
  1184   then show "1 + x \<le> exp x"
  1185     by auto
  1186 qed
  1187 
  1188 lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x"
  1189 proof -
  1190   assume x: "0 < x"
  1191   hence "1 < 1 + x" by simp
  1192   also from x have "1 + x \<le> exp x"
  1193     by (simp add: exp_ge_add_one_self_aux)
  1194   finally show ?thesis .
  1195 qed
  1196 
  1197 lemma exp_less_mono:
  1198   fixes x y :: real
  1199   assumes "x < y"
  1200   shows "exp x < exp y"
  1201 proof -
  1202   from `x < y` have "0 < y - x" by simp
  1203   hence "1 < exp (y - x)" by (rule exp_gt_one)
  1204   hence "1 < exp y / exp x" by (simp only: exp_diff)
  1205   thus "exp x < exp y" by simp
  1206 qed
  1207 
  1208 lemma exp_less_cancel: "exp (x::real) < exp y \<Longrightarrow> x < y"
  1209   unfolding linorder_not_le [symmetric]
  1210   by (auto simp add: order_le_less exp_less_mono)
  1211 
  1212 lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y"
  1213   by (auto intro: exp_less_mono exp_less_cancel)
  1214 
  1215 lemma exp_le_cancel_iff [iff]: "exp (x::real) \<le> exp y \<longleftrightarrow> x \<le> y"
  1216   by (auto simp add: linorder_not_less [symmetric])
  1217 
  1218 lemma exp_inj_iff [iff]: "exp (x::real) = exp y \<longleftrightarrow> x = y"
  1219   by (simp add: order_eq_iff)
  1220 
  1221 text {* Comparisons of @{term "exp x"} with one. *}
  1222 
  1223 lemma one_less_exp_iff [simp]: "1 < exp (x::real) \<longleftrightarrow> 0 < x"
  1224   using exp_less_cancel_iff [where x=0 and y=x] by simp
  1225 
  1226 lemma exp_less_one_iff [simp]: "exp (x::real) < 1 \<longleftrightarrow> x < 0"
  1227   using exp_less_cancel_iff [where x=x and y=0] by simp
  1228 
  1229 lemma one_le_exp_iff [simp]: "1 \<le> exp (x::real) \<longleftrightarrow> 0 \<le> x"
  1230   using exp_le_cancel_iff [where x=0 and y=x] by simp
  1231 
  1232 lemma exp_le_one_iff [simp]: "exp (x::real) \<le> 1 \<longleftrightarrow> x \<le> 0"
  1233   using exp_le_cancel_iff [where x=x and y=0] by simp
  1234 
  1235 lemma exp_eq_one_iff [simp]: "exp (x::real) = 1 \<longleftrightarrow> x = 0"
  1236   using exp_inj_iff [where x=x and y=0] by simp
  1237 
  1238 lemma lemma_exp_total: "1 \<le> y \<Longrightarrow> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y"
  1239 proof (rule IVT)
  1240   assume "1 \<le> y"
  1241   hence "0 \<le> y - 1" by simp
  1242   hence "1 + (y - 1) \<le> exp (y - 1)" by (rule exp_ge_add_one_self_aux)
  1243   thus "y \<le> exp (y - 1)" by simp
  1244 qed (simp_all add: le_diff_eq)
  1245 
  1246 lemma exp_total: "0 < (y::real) \<Longrightarrow> \<exists>x. exp x = y"
  1247 proof (rule linorder_le_cases [of 1 y])
  1248   assume "1 \<le> y"
  1249   thus "\<exists>x. exp x = y" by (fast dest: lemma_exp_total)
  1250 next
  1251   assume "0 < y" and "y \<le> 1"
  1252   hence "1 \<le> inverse y" by (simp add: one_le_inverse_iff)
  1253   then obtain x where "exp x = inverse y" by (fast dest: lemma_exp_total)
  1254   hence "exp (- x) = y" by (simp add: exp_minus)
  1255   thus "\<exists>x. exp x = y" ..
  1256 qed
  1257 
  1258 
  1259 subsection {* Natural Logarithm *}
  1260 
  1261 definition ln :: "real \<Rightarrow> real"
  1262   where "ln x = (THE u. exp u = x)"
  1263 
  1264 lemma ln_exp [simp]: "ln (exp x) = x"
  1265   by (simp add: ln_def)
  1266 
  1267 lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
  1268   by (auto dest: exp_total)
  1269 
  1270 lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
  1271   by (metis exp_gt_zero exp_ln)
  1272 
  1273 lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
  1274   by (erule subst, rule ln_exp)
  1275 
  1276 lemma ln_one [simp]: "ln 1 = 0"
  1277   by (rule ln_unique) simp
  1278 
  1279 lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
  1280   by (rule ln_unique) (simp add: exp_add)
  1281 
  1282 lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
  1283   by (rule ln_unique) (simp add: exp_minus)
  1284 
  1285 lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
  1286   by (rule ln_unique) (simp add: exp_diff)
  1287 
  1288 lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
  1289   by (rule ln_unique) (simp add: exp_real_of_nat_mult)
  1290 
  1291 lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
  1292   by (subst exp_less_cancel_iff [symmetric]) simp
  1293 
  1294 lemma ln_le_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
  1295   by (simp add: linorder_not_less [symmetric])
  1296 
  1297 lemma ln_inj_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
  1298   by (simp add: order_eq_iff)
  1299 
  1300 lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
  1301   apply (rule exp_le_cancel_iff [THEN iffD1])
  1302   apply (simp add: exp_ge_add_one_self_aux)
  1303   done
  1304 
  1305 lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
  1306   by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
  1307 
  1308 lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
  1309   using ln_le_cancel_iff [of 1 x] by simp
  1310 
  1311 lemma ln_ge_zero_imp_ge_one: "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
  1312   using ln_le_cancel_iff [of 1 x] by simp
  1313 
  1314 lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
  1315   using ln_le_cancel_iff [of 1 x] by simp
  1316 
  1317 lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
  1318   using ln_less_cancel_iff [of x 1] by simp
  1319 
  1320 lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
  1321   using ln_less_cancel_iff [of 1 x] by simp
  1322 
  1323 lemma ln_gt_zero_imp_gt_one: "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
  1324   using ln_less_cancel_iff [of 1 x] by simp
  1325 
  1326 lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
  1327   using ln_less_cancel_iff [of 1 x] by simp
  1328 
  1329 lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
  1330   using ln_inj_iff [of x 1] by simp
  1331 
  1332 lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
  1333   by simp
  1334 
  1335 lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
  1336   by (auto simp add: ln_def intro!: arg_cong[where f=The])
  1337 
  1338 lemma isCont_ln: assumes "x \<noteq> 0" shows "isCont ln x"
  1339 proof cases
  1340   assume "0 < x"
  1341   moreover then have "isCont ln (exp (ln x))"
  1342     by (intro isCont_inv_fun[where d="\<bar>x\<bar>" and f=exp]) auto
  1343   ultimately show ?thesis
  1344     by simp
  1345 next
  1346   assume "\<not> 0 < x" with `x \<noteq> 0` show "isCont ln x"
  1347     unfolding isCont_def
  1348     by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
  1349        (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
  1350                 intro!: exI[of _ "\<bar>x\<bar>"])
  1351 qed
  1352 
  1353 lemma tendsto_ln [tendsto_intros]:
  1354   "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
  1355   by (rule isCont_tendsto_compose [OF isCont_ln])
  1356 
  1357 lemma continuous_ln:
  1358   "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
  1359   unfolding continuous_def by (rule tendsto_ln)
  1360 
  1361 lemma isCont_ln' [continuous_intros]:
  1362   "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
  1363   unfolding continuous_at by (rule tendsto_ln)
  1364 
  1365 lemma continuous_within_ln [continuous_intros]:
  1366   "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
  1367   unfolding continuous_within by (rule tendsto_ln)
  1368 
  1369 lemma continuous_on_ln [continuous_intros]:
  1370   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
  1371   unfolding continuous_on_def by (auto intro: tendsto_ln)
  1372 
  1373 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
  1374   apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
  1375   apply (auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln)
  1376   done
  1377 
  1378 lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
  1379   by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
  1380 
  1381 declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
  1382 
  1383 lemma ln_series:
  1384   assumes "0 < x" and "x < 2"
  1385   shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))"
  1386   (is "ln x = suminf (?f (x - 1))")
  1387 proof -
  1388   let ?f' = "\<lambda>x n. (-1)^n * (x - 1)^n"
  1389 
  1390   have "ln x - suminf (?f (x - 1)) = ln 1 - suminf (?f (1 - 1))"
  1391   proof (rule DERIV_isconst3[where x=x])
  1392     fix x :: real
  1393     assume "x \<in> {0 <..< 2}"
  1394     hence "0 < x" and "x < 2" by auto
  1395     have "norm (1 - x) < 1"
  1396       using `0 < x` and `x < 2` by auto
  1397     have "1 / x = 1 / (1 - (1 - x))" by auto
  1398     also have "\<dots> = (\<Sum> n. (1 - x)^n)"
  1399       using geometric_sums[OF `norm (1 - x) < 1`] by (rule sums_unique)
  1400     also have "\<dots> = suminf (?f' x)"
  1401       unfolding power_mult_distrib[symmetric]
  1402       by (rule arg_cong[where f=suminf], rule arg_cong[where f="op ^"], auto)
  1403     finally have "DERIV ln x :> suminf (?f' x)"
  1404       using DERIV_ln[OF `0 < x`] unfolding divide_inverse by auto
  1405     moreover
  1406     have repos: "\<And> h x :: real. h - 1 + x = h + x - 1" by auto
  1407     have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :>
  1408       (\<Sum>n. (-1)^n * (1 / real (n + 1)) * real (Suc n) * (x - 1) ^ n)"
  1409     proof (rule DERIV_power_series')
  1410       show "x - 1 \<in> {- 1<..<1}" and "(0 :: real) < 1"
  1411         using `0 < x` `x < 2` by auto
  1412       fix x :: real
  1413       assume "x \<in> {- 1<..<1}"
  1414       hence "norm (-x) < 1" by auto
  1415       show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
  1416         unfolding One_nat_def
  1417         by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
  1418     qed
  1419     hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
  1420       unfolding One_nat_def by auto
  1421     hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)"
  1422       unfolding DERIV_def repos .
  1423     ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
  1424       by (rule DERIV_diff)
  1425     thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
  1426   qed (auto simp add: assms)
  1427   thus ?thesis by auto
  1428 qed
  1429 
  1430 lemma exp_first_two_terms: "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
  1431 proof -
  1432   have "exp x = suminf (\<lambda>n. inverse(fact n) * (x ^ n))"
  1433     by (simp add: exp_def)
  1434   also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) + 
  1435     (\<Sum> n::nat<2. inverse(fact n) * (x ^ n))" (is "_ = _ + ?a")
  1436     by (rule suminf_split_initial_segment)
  1437   also have "?a = 1 + x"
  1438     by (simp add: numeral_2_eq_2)
  1439   finally show ?thesis
  1440     by simp
  1441 qed
  1442 
  1443 lemma exp_bound: "0 <= (x::real) \<Longrightarrow> x <= 1 \<Longrightarrow> exp x <= 1 + x + x\<^sup>2"
  1444 proof -
  1445   assume a: "0 <= x"
  1446   assume b: "x <= 1"
  1447   {
  1448     fix n :: nat
  1449     have "2 * 2 ^ n \<le> fact (n + 2)"
  1450       by (induct n) simp_all
  1451     hence "real ((2::nat) * 2 ^ n) \<le> real (fact (n + 2))"
  1452       by (simp only: real_of_nat_le_iff)
  1453     hence "2 * 2 ^ n \<le> real (fact (n + 2))"
  1454       by simp
  1455     hence "inverse (fact (n + 2)) \<le> inverse (2 * 2 ^ n)"
  1456       by (rule le_imp_inverse_le) simp
  1457     hence "inverse (fact (n + 2)) \<le> 1/2 * (1/2)^n"
  1458       by (simp add: power_inverse)
  1459     hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
  1460       by (rule mult_mono)
  1461         (rule mult_mono, simp_all add: power_le_one a b)
  1462     hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
  1463       unfolding power_add by (simp add: ac_simps del: fact_Suc) }
  1464   note aux1 = this
  1465   have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
  1466     by (intro sums_mult geometric_sums, simp)
  1467   hence aux2: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2"
  1468     by simp
  1469   have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <= x\<^sup>2"
  1470   proof -
  1471     have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <=
  1472         suminf (\<lambda>n. (x\<^sup>2/2) * ((1/2)^n))"
  1473       apply (rule suminf_le)
  1474       apply (rule allI, rule aux1)
  1475       apply (rule summable_exp [THEN summable_ignore_initial_segment])
  1476       by (rule sums_summable, rule aux2)
  1477     also have "... = x\<^sup>2"
  1478       by (rule sums_unique [THEN sym], rule aux2)
  1479     finally show ?thesis .
  1480   qed
  1481   thus ?thesis unfolding exp_first_two_terms by auto
  1482 qed
  1483 
  1484 lemma ln_one_minus_pos_upper_bound: "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
  1485 proof -
  1486   assume a: "0 <= (x::real)" and b: "x < 1"
  1487   have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)"
  1488     by (simp add: algebra_simps power2_eq_square power3_eq_cube)
  1489   also have "... <= 1"
  1490     by (auto simp add: a)
  1491   finally have "(1 - x) * (1 + x + x\<^sup>2) <= 1" .
  1492   moreover have c: "0 < 1 + x + x\<^sup>2"
  1493     by (simp add: add_pos_nonneg a)
  1494   ultimately have "1 - x <= 1 / (1 + x + x\<^sup>2)"
  1495     by (elim mult_imp_le_div_pos)
  1496   also have "... <= 1 / exp x"
  1497     by (metis a abs_one b exp_bound exp_gt_zero frac_le less_eq_real_def real_sqrt_abs 
  1498               real_sqrt_pow2_iff real_sqrt_power)
  1499   also have "... = exp (-x)"
  1500     by (auto simp add: exp_minus divide_inverse)
  1501   finally have "1 - x <= exp (- x)" .
  1502   also have "1 - x = exp (ln (1 - x))"
  1503     by (metis b diff_0 exp_ln_iff less_iff_diff_less_0 minus_diff_eq)
  1504   finally have "exp (ln (1 - x)) <= exp (- x)" .
  1505   thus ?thesis by (auto simp only: exp_le_cancel_iff)
  1506 qed
  1507 
  1508 lemma exp_ge_add_one_self [simp]: "1 + (x::real) <= exp x"
  1509   apply (case_tac "0 <= x")
  1510   apply (erule exp_ge_add_one_self_aux)
  1511   apply (case_tac "x <= -1")
  1512   apply (subgoal_tac "1 + x <= 0")
  1513   apply (erule order_trans)
  1514   apply simp
  1515   apply simp
  1516   apply (subgoal_tac "1 + x = exp(ln (1 + x))")
  1517   apply (erule ssubst)
  1518   apply (subst exp_le_cancel_iff)
  1519   apply (subgoal_tac "ln (1 - (- x)) <= - (- x)")
  1520   apply simp
  1521   apply (rule ln_one_minus_pos_upper_bound)
  1522   apply auto
  1523 done
  1524 
  1525 lemma ln_one_plus_pos_lower_bound: "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> x - x\<^sup>2 <= ln (1 + x)"
  1526 proof -
  1527   assume a: "0 <= x" and b: "x <= 1"
  1528   have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)"
  1529     by (rule exp_diff)
  1530   also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)"
  1531     by (metis a b divide_right_mono exp_bound exp_ge_zero)
  1532   also have "... <= (1 + x + x\<^sup>2) / (1 + x\<^sup>2)"
  1533     by (simp add: a divide_left_mono add_pos_nonneg)
  1534   also from a have "... <= 1 + x"
  1535     by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
  1536   finally have "exp (x - x\<^sup>2) <= 1 + x" .
  1537   also have "... = exp (ln (1 + x))"
  1538   proof -
  1539     from a have "0 < 1 + x" by auto
  1540     thus ?thesis
  1541       by (auto simp only: exp_ln_iff [THEN sym])
  1542   qed
  1543   finally have "exp (x - x\<^sup>2) <= exp (ln (1 + x))" .
  1544   thus ?thesis
  1545     by (metis exp_le_cancel_iff) 
  1546 qed
  1547 
  1548 lemma ln_one_minus_pos_lower_bound:
  1549   "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
  1550 proof -
  1551   assume a: "0 <= x" and b: "x <= (1 / 2)"
  1552   from b have c: "x < 1" by auto
  1553   then have "ln (1 - x) = - ln (1 + x / (1 - x))"
  1554     apply (subst ln_inverse [symmetric])
  1555     apply (simp add: field_simps)
  1556     apply (rule arg_cong [where f=ln])
  1557     apply (simp add: field_simps)
  1558     done
  1559   also have "- (x / (1 - x)) <= ..."
  1560   proof -
  1561     have "ln (1 + x / (1 - x)) <= x / (1 - x)"
  1562       using a c by (intro ln_add_one_self_le_self) auto
  1563     thus ?thesis
  1564       by auto
  1565   qed
  1566   also have "- (x / (1 - x)) = -x / (1 - x)"
  1567     by auto
  1568   finally have d: "- x / (1 - x) <= ln (1 - x)" .
  1569   have "0 < 1 - x" using a b by simp
  1570   hence e: "-x - 2 * x\<^sup>2 <= - x / (1 - x)"
  1571     using mult_right_le_one_le[of "x*x" "2*x"] a b
  1572     by (simp add: field_simps power2_eq_square)
  1573   from e d show "- x - 2 * x\<^sup>2 <= ln (1 - x)"
  1574     by (rule order_trans)
  1575 qed
  1576 
  1577 lemma ln_add_one_self_le_self2: "-1 < x \<Longrightarrow> ln(1 + x) <= x"
  1578   apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp)
  1579   apply (subst ln_le_cancel_iff)
  1580   apply auto
  1581   done
  1582 
  1583 lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
  1584   "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
  1585 proof -
  1586   assume x: "0 <= x"
  1587   assume x1: "x <= 1"
  1588   from x have "ln (1 + x) <= x"
  1589     by (rule ln_add_one_self_le_self)
  1590   then have "ln (1 + x) - x <= 0"
  1591     by simp
  1592   then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
  1593     by (rule abs_of_nonpos)
  1594   also have "... = x - ln (1 + x)"
  1595     by simp
  1596   also have "... <= x\<^sup>2"
  1597   proof -
  1598     from x x1 have "x - x\<^sup>2 <= ln (1 + x)"
  1599       by (intro ln_one_plus_pos_lower_bound)
  1600     thus ?thesis
  1601       by simp
  1602   qed
  1603   finally show ?thesis .
  1604 qed
  1605 
  1606 lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
  1607   "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  1608 proof -
  1609   assume a: "-(1 / 2) <= x"
  1610   assume b: "x <= 0"
  1611   have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
  1612     apply (subst abs_of_nonpos)
  1613     apply simp
  1614     apply (rule ln_add_one_self_le_self2)
  1615     using a apply auto
  1616     done
  1617   also have "... <= 2 * x\<^sup>2"
  1618     apply (subgoal_tac "- (-x) - 2 * (-x)\<^sup>2 <= ln (1 - (-x))")
  1619     apply (simp add: algebra_simps)
  1620     apply (rule ln_one_minus_pos_lower_bound)
  1621     using a b apply auto
  1622     done
  1623   finally show ?thesis .
  1624 qed
  1625 
  1626 lemma abs_ln_one_plus_x_minus_x_bound:
  1627     "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  1628   apply (case_tac "0 <= x")
  1629   apply (rule order_trans)
  1630   apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
  1631   apply auto
  1632   apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos)
  1633   apply auto
  1634   done
  1635 
  1636 lemma ln_x_over_x_mono: "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
  1637 proof -
  1638   assume x: "exp 1 <= x" "x <= y"
  1639   moreover have "0 < exp (1::real)" by simp
  1640   ultimately have a: "0 < x" and b: "0 < y"
  1641     by (fast intro: less_le_trans order_trans)+
  1642   have "x * ln y - x * ln x = x * (ln y - ln x)"
  1643     by (simp add: algebra_simps)
  1644   also have "... = x * ln(y / x)"
  1645     by (simp only: ln_div a b)
  1646   also have "y / x = (x + (y - x)) / x"
  1647     by simp
  1648   also have "... = 1 + (y - x) / x"
  1649     using x a by (simp add: field_simps)
  1650   also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
  1651     using x a 
  1652     by (intro mult_left_mono ln_add_one_self_le_self) simp_all
  1653   also have "... = y - x" using a by simp
  1654   also have "... = (y - x) * ln (exp 1)" by simp
  1655   also have "... <= (y - x) * ln x"
  1656     apply (rule mult_left_mono)
  1657     apply (subst ln_le_cancel_iff)
  1658     apply fact
  1659     apply (rule a)
  1660     apply (rule x)
  1661     using x apply simp
  1662     done
  1663   also have "... = y * ln x - x * ln x"
  1664     by (rule left_diff_distrib)
  1665   finally have "x * ln y <= y * ln x"
  1666     by arith
  1667   then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps)
  1668   also have "... = y * (ln x / x)" by simp
  1669   finally show ?thesis using b by (simp add: field_simps)
  1670 qed
  1671 
  1672 lemma ln_le_minus_one: "0 < x \<Longrightarrow> ln x \<le> x - 1"
  1673   using exp_ge_add_one_self[of "ln x"] by simp
  1674 
  1675 lemma ln_eq_minus_one:
  1676   assumes "0 < x" "ln x = x - 1"
  1677   shows "x = 1"
  1678 proof -
  1679   let ?l = "\<lambda>y. ln y - y + 1"
  1680   have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
  1681     by (auto intro!: derivative_eq_intros)
  1682 
  1683   show ?thesis
  1684   proof (cases rule: linorder_cases)
  1685     assume "x < 1"
  1686     from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast
  1687     from `x < a` have "?l x < ?l a"
  1688     proof (rule DERIV_pos_imp_increasing, safe)
  1689       fix y
  1690       assume "x \<le> y" "y \<le> a"
  1691       with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y"
  1692         by (auto simp: field_simps)
  1693       with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
  1694         by auto
  1695     qed
  1696     also have "\<dots> \<le> 0"
  1697       using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps)
  1698     finally show "x = 1" using assms by auto
  1699   next
  1700     assume "1 < x"
  1701     from dense[OF this] obtain a where "1 < a" "a < x" by blast
  1702     from `a < x` have "?l x < ?l a"
  1703     proof (rule DERIV_neg_imp_decreasing, safe)
  1704       fix y
  1705       assume "a \<le> y" "y \<le> x"
  1706       with `1 < a` have "1 / y - 1 < 0" "0 < y"
  1707         by (auto simp: field_simps)
  1708       with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0"
  1709         by blast
  1710     qed
  1711     also have "\<dots> \<le> 0"
  1712       using ln_le_minus_one `1 < a` by (auto simp: field_simps)
  1713     finally show "x = 1" using assms by auto
  1714   next
  1715     assume "x = 1"
  1716     then show ?thesis by simp
  1717   qed
  1718 qed
  1719 
  1720 lemma exp_at_bot: "(exp ---> (0::real)) at_bot"
  1721   unfolding tendsto_Zfun_iff
  1722 proof (rule ZfunI, simp add: eventually_at_bot_dense)
  1723   fix r :: real assume "0 < r"
  1724   {
  1725     fix x
  1726     assume "x < ln r"
  1727     then have "exp x < exp (ln r)"
  1728       by simp
  1729     with `0 < r` have "exp x < r"
  1730       by simp
  1731   }
  1732   then show "\<exists>k. \<forall>n<k. exp n < r" by auto
  1733 qed
  1734 
  1735 lemma exp_at_top: "LIM x at_top. exp x :: real :> at_top"
  1736   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"])
  1737      (auto intro: eventually_gt_at_top)
  1738 
  1739 lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
  1740   by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  1741      (auto simp: eventually_at_filter)
  1742 
  1743 lemma ln_at_top: "LIM x at_top. ln x :> at_top"
  1744   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  1745      (auto intro: eventually_gt_at_top)
  1746 
  1747 lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
  1748 proof (induct k)
  1749   case 0
  1750   show "((\<lambda>x. x ^ 0 / exp x) ---> (0::real)) at_top"
  1751     by (simp add: inverse_eq_divide[symmetric])
  1752        (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono
  1753               at_top_le_at_infinity order_refl)
  1754 next
  1755   case (Suc k)
  1756   show ?case
  1757   proof (rule lhospital_at_top_at_top)
  1758     show "eventually (\<lambda>x. DERIV (\<lambda>x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top"
  1759       by eventually_elim (intro derivative_eq_intros, auto)
  1760     show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top"
  1761       by eventually_elim auto
  1762     show "eventually (\<lambda>x. exp x \<noteq> 0) at_top"
  1763       by auto
  1764     from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
  1765     show "((\<lambda>x. real (Suc k) * x ^ k / exp x) ---> 0) at_top"
  1766       by simp
  1767   qed (rule exp_at_top)
  1768 qed
  1769 
  1770 
  1771 definition powr :: "[real,real] => real"  (infixr "powr" 80)
  1772   -- {*exponentation with real exponent*}
  1773   where "x powr a = exp(a * ln x)"
  1774 
  1775 definition log :: "[real,real] => real"
  1776   -- {*logarithm of @{term x} to base @{term a}*}
  1777   where "log a x = ln x / ln a"
  1778 
  1779 
  1780 lemma tendsto_log [tendsto_intros]:
  1781   "\<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"
  1782   unfolding log_def by (intro tendsto_intros) auto
  1783 
  1784 lemma continuous_log:
  1785   assumes "continuous F f"
  1786     and "continuous F g"
  1787     and "0 < f (Lim F (\<lambda>x. x))"
  1788     and "f (Lim F (\<lambda>x. x)) \<noteq> 1"
  1789     and "0 < g (Lim F (\<lambda>x. x))"
  1790   shows "continuous F (\<lambda>x. log (f x) (g x))"
  1791   using assms unfolding continuous_def by (rule tendsto_log)
  1792 
  1793 lemma continuous_at_within_log[continuous_intros]:
  1794   assumes "continuous (at a within s) f"
  1795     and "continuous (at a within s) g"
  1796     and "0 < f a"
  1797     and "f a \<noteq> 1"
  1798     and "0 < g a"
  1799   shows "continuous (at a within s) (\<lambda>x. log (f x) (g x))"
  1800   using assms unfolding continuous_within by (rule tendsto_log)
  1801 
  1802 lemma isCont_log[continuous_intros, simp]:
  1803   assumes "isCont f a" "isCont g a" "0 < f a" "f a \<noteq> 1" "0 < g a"
  1804   shows "isCont (\<lambda>x. log (f x) (g x)) a"
  1805   using assms unfolding continuous_at by (rule tendsto_log)
  1806 
  1807 lemma continuous_on_log[continuous_intros]:
  1808   assumes "continuous_on s f" "continuous_on s g"
  1809     and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
  1810   shows "continuous_on s (\<lambda>x. log (f x) (g x))"
  1811   using assms unfolding continuous_on_def by (fast intro: tendsto_log)
  1812 
  1813 lemma powr_one_eq_one [simp]: "1 powr a = 1"
  1814   by (simp add: powr_def)
  1815 
  1816 lemma powr_zero_eq_one [simp]: "x powr 0 = 1"
  1817   by (simp add: powr_def)
  1818 
  1819 lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)"
  1820   by (simp add: powr_def)
  1821 declare powr_one_gt_zero_iff [THEN iffD2, simp]
  1822 
  1823 lemma powr_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
  1824   by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
  1825 
  1826 lemma powr_gt_zero [simp]: "0 < x powr a"
  1827   by (simp add: powr_def)
  1828 
  1829 lemma powr_ge_pzero [simp]: "0 <= x powr y"
  1830   by (rule order_less_imp_le, rule powr_gt_zero)
  1831 
  1832 lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
  1833   by (simp add: powr_def)
  1834 
  1835 lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
  1836   apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
  1837   apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
  1838   done
  1839 
  1840 lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
  1841   apply (simp add: powr_def)
  1842   apply (subst exp_diff [THEN sym])
  1843   apply (simp add: left_diff_distrib)
  1844   done
  1845 
  1846 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
  1847   by (simp add: powr_def exp_add [symmetric] distrib_right)
  1848 
  1849 lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
  1850   using assms by (auto simp: powr_add)
  1851 
  1852 lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
  1853   by (simp add: powr_def)
  1854 
  1855 lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
  1856   by (simp add: powr_powr mult.commute)
  1857 
  1858 lemma powr_minus: "x powr (-a) = inverse (x powr a)"
  1859   by (simp add: powr_def exp_minus [symmetric])
  1860 
  1861 lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
  1862   by (simp add: divide_inverse powr_minus)
  1863 
  1864 lemma powr_less_mono: "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
  1865   by (simp add: powr_def)
  1866 
  1867 lemma powr_less_cancel: "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
  1868   by (simp add: powr_def)
  1869 
  1870 lemma powr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
  1871   by (blast intro: powr_less_cancel powr_less_mono)
  1872 
  1873 lemma powr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
  1874   by (simp add: linorder_not_less [symmetric])
  1875 
  1876 lemma log_ln: "ln x = log (exp(1)) x"
  1877   by (simp add: log_def)
  1878 
  1879 lemma DERIV_log:
  1880   assumes "x > 0"
  1881   shows "DERIV (\<lambda>y. log b y) x :> 1 / (ln b * x)"
  1882 proof -
  1883   def lb \<equiv> "1 / ln b"
  1884   moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x"
  1885     using `x > 0` by (auto intro!: derivative_eq_intros)
  1886   ultimately show ?thesis
  1887     by (simp add: log_def)
  1888 qed
  1889 
  1890 lemmas DERIV_log[THEN DERIV_chain2, derivative_intros]
  1891 
  1892 lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
  1893   by (simp add: powr_def log_def)
  1894 
  1895 lemma log_powr_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log a (a powr y) = y"
  1896   by (simp add: log_def powr_def)
  1897 
  1898 lemma log_mult:
  1899   "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow>
  1900     log a (x * y) = log a x + log a y"
  1901   by (simp add: log_def ln_mult divide_inverse distrib_right)
  1902 
  1903 lemma log_eq_div_ln_mult_log:
  1904   "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow>
  1905     log a x = (ln b/ln a) * log b x"
  1906   by (simp add: log_def divide_inverse)
  1907 
  1908 text{*Base 10 logarithms*}
  1909 lemma log_base_10_eq1: "0 < x \<Longrightarrow> log 10 x = (ln (exp 1) / ln 10) * ln x"
  1910   by (simp add: log_def)
  1911 
  1912 lemma log_base_10_eq2: "0 < x \<Longrightarrow> log 10 x = (log 10 (exp 1)) * ln x"
  1913   by (simp add: log_def)
  1914 
  1915 lemma log_one [simp]: "log a 1 = 0"
  1916   by (simp add: log_def)
  1917 
  1918 lemma log_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> log a a = 1"
  1919   by (simp add: log_def)
  1920 
  1921 lemma log_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log a (inverse x) = - log a x"
  1922   apply (rule_tac a1 = "log a x" in add_left_cancel [THEN iffD1])
  1923   apply (simp add: log_mult [symmetric])
  1924   done
  1925 
  1926 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"
  1927   by (simp add: log_mult divide_inverse log_inverse)
  1928 
  1929 lemma log_less_cancel_iff [simp]:
  1930   "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a x < log a y \<longleftrightarrow> x < y"
  1931   apply safe
  1932   apply (rule_tac [2] powr_less_cancel)
  1933   apply (drule_tac a = "log a x" in powr_less_mono, auto)
  1934   done
  1935 
  1936 lemma log_inj:
  1937   assumes "1 < b"
  1938   shows "inj_on (log b) {0 <..}"
  1939 proof (rule inj_onI, simp)
  1940   fix x y
  1941   assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
  1942   show "x = y"
  1943   proof (cases rule: linorder_cases)
  1944     assume "x = y"
  1945     then show ?thesis by simp
  1946   next
  1947     assume "x < y" hence "log b x < log b y"
  1948       using log_less_cancel_iff[OF `1 < b`] pos by simp
  1949     then show ?thesis using * by simp
  1950   next
  1951     assume "y < x" hence "log b y < log b x"
  1952       using log_less_cancel_iff[OF `1 < b`] pos by simp
  1953     then show ?thesis using * by simp
  1954   qed
  1955 qed
  1956 
  1957 lemma log_le_cancel_iff [simp]:
  1958   "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (log a x \<le> log a y) = (x \<le> y)"
  1959   by (simp add: linorder_not_less [symmetric])
  1960 
  1961 lemma zero_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < log a x \<longleftrightarrow> 1 < x"
  1962   using log_less_cancel_iff[of a 1 x] by simp
  1963 
  1964 lemma zero_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 \<le> log a x \<longleftrightarrow> 1 \<le> x"
  1965   using log_le_cancel_iff[of a 1 x] by simp
  1966 
  1967 lemma log_less_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 0 \<longleftrightarrow> x < 1"
  1968   using log_less_cancel_iff[of a x 1] by simp
  1969 
  1970 lemma log_le_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 0 \<longleftrightarrow> x \<le> 1"
  1971   using log_le_cancel_iff[of a x 1] by simp
  1972 
  1973 lemma one_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 < log a x \<longleftrightarrow> a < x"
  1974   using log_less_cancel_iff[of a a x] by simp
  1975 
  1976 lemma one_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> log a x \<longleftrightarrow> a \<le> x"
  1977   using log_le_cancel_iff[of a a x] by simp
  1978 
  1979 lemma log_less_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 1 \<longleftrightarrow> x < a"
  1980   using log_less_cancel_iff[of a x a] by simp
  1981 
  1982 lemma log_le_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 1 \<longleftrightarrow> x \<le> a"
  1983   using log_le_cancel_iff[of a x a] by simp
  1984 
  1985 lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
  1986   apply (induct n)
  1987   apply simp
  1988   apply (subgoal_tac "real(Suc n) = real n + 1")
  1989   apply (erule ssubst)
  1990   apply (subst powr_add, simp, simp)
  1991   done
  1992 
  1993 lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
  1994   unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
  1995 
  1996 lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
  1997 by(simp add: powr_realpow_numeral)
  1998 
  1999 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
  2000   apply (case_tac "x = 0", simp, simp)
  2001   apply (rule powr_realpow [THEN sym], simp)
  2002   done
  2003 
  2004 lemma powr_int:
  2005   assumes "x > 0"
  2006   shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))"
  2007 proof (cases "i < 0")
  2008   case True
  2009   have r: "x powr i = 1 / x powr (-i)" by (simp add: powr_minus field_simps)
  2010   show ?thesis using `i < 0` `x > 0` by (simp add: r field_simps powr_realpow[symmetric])
  2011 next
  2012   case False
  2013   then show ?thesis by (simp add: assms powr_realpow[symmetric])
  2014 qed
  2015 
  2016 lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
  2017   using powr_realpow [of x 1] by simp
  2018 
  2019 lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
  2020   by (fact powr_realpow_numeral)
  2021 
  2022 lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
  2023   using powr_int [of x "- 1"] by simp
  2024 
  2025 lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
  2026   using powr_int [of x "- numeral n"] by simp
  2027 
  2028 lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
  2029   by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
  2030 
  2031 lemma ln_powr: "ln (x powr y) = y * ln x"
  2032   by (simp add: powr_def)
  2033 
  2034 lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) =  ln b / n"
  2035 by(simp add: root_powr_inverse ln_powr)
  2036 
  2037 lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
  2038   by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult.commute)
  2039 
  2040 lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) =  log b a / n"
  2041 by(simp add: log_def ln_root)
  2042 
  2043 lemma log_powr: "log b (x powr y) = y * log b x"
  2044   by (simp add: log_def ln_powr)
  2045 
  2046 lemma log_nat_power: "0 < x \<Longrightarrow> log b (x ^ n) = real n * log b x"
  2047   by (simp add: log_powr powr_realpow [symmetric])
  2048 
  2049 lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
  2050   by (simp add: log_def)
  2051 
  2052 lemma log_base_pow: "0 < a \<Longrightarrow> log (a ^ n) x = log a x / n"
  2053   by (simp add: log_def ln_realpow)
  2054 
  2055 lemma log_base_powr: "log (a powr b) x = log a x / b"
  2056   by (simp add: log_def ln_powr)
  2057 
  2058 lemma log_base_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> log (root n b) x = n * (log b x)"
  2059 by(simp add: log_def ln_root)
  2060 
  2061 lemma ln_bound: "1 <= x ==> ln x <= x"
  2062   apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
  2063   apply simp
  2064   apply (rule ln_add_one_self_le_self, simp)
  2065   done
  2066 
  2067 lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b"
  2068   apply (cases "x = 1", simp)
  2069   apply (cases "a = b", simp)
  2070   apply (rule order_less_imp_le)
  2071   apply (rule powr_less_mono, auto)
  2072   done
  2073 
  2074 lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a"
  2075   apply (subst powr_zero_eq_one [THEN sym])
  2076   apply (rule powr_mono, assumption+)
  2077   done
  2078 
  2079 lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
  2080   apply (unfold powr_def)
  2081   apply (rule exp_less_mono)
  2082   apply (rule mult_strict_left_mono)
  2083   apply (subst ln_less_cancel_iff, assumption)
  2084   apply (rule order_less_trans)
  2085   prefer 2
  2086   apply assumption+
  2087   done
  2088 
  2089 lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
  2090   apply (unfold powr_def)
  2091   apply (rule exp_less_mono)
  2092   apply (rule mult_strict_left_mono_neg)
  2093   apply (subst ln_less_cancel_iff)
  2094   apply assumption
  2095   apply (rule order_less_trans)
  2096   prefer 2
  2097   apply assumption+
  2098   done
  2099 
  2100 lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
  2101   apply (case_tac "a = 0", simp)
  2102   apply (case_tac "x = y", simp)
  2103   apply (metis less_eq_real_def powr_less_mono2)
  2104   done
  2105 
  2106 lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
  2107   unfolding powr_def exp_inj_iff by simp
  2108 
  2109 lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
  2110   by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute 
  2111             order.strict_trans2 powr_gt_zero zero_less_one)
  2112 
  2113 lemma ln_powr_bound2:
  2114   assumes "1 < x" and "0 < a"
  2115   shows "(ln x) powr a <= (a powr a) * x"
  2116 proof -
  2117   from assms have "ln x <= (x powr (1 / a)) / (1 / a)"
  2118     by (metis less_eq_real_def ln_powr_bound zero_less_divide_1_iff)
  2119   also have "... = a * (x powr (1 / a))"
  2120     by simp
  2121   finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
  2122     by (metis assms less_imp_le ln_gt_zero powr_mono2)
  2123   also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
  2124     by (metis assms(2) powr_mult powr_gt_zero)
  2125   also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
  2126     by (rule powr_powr)
  2127   also have "... = x" using assms
  2128     by auto
  2129   finally show ?thesis .
  2130 qed
  2131 
  2132 lemma tendsto_powr [tendsto_intros]:
  2133   "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
  2134   unfolding powr_def by (intro tendsto_intros)
  2135 
  2136 lemma continuous_powr:
  2137   assumes "continuous F f"
  2138     and "continuous F g"
  2139     and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
  2140   shows "continuous F (\<lambda>x. (f x) powr (g x))"
  2141   using assms unfolding continuous_def by (rule tendsto_powr)
  2142 
  2143 lemma continuous_at_within_powr[continuous_intros]:
  2144   assumes "continuous (at a within s) f"
  2145     and "continuous (at a within s) g"
  2146     and "f a \<noteq> 0"
  2147   shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
  2148   using assms unfolding continuous_within by (rule tendsto_powr)
  2149 
  2150 lemma isCont_powr[continuous_intros, simp]:
  2151   assumes "isCont f a" "isCont g a" "f a \<noteq> 0"
  2152   shows "isCont (\<lambda>x. (f x) powr g x) a"
  2153   using assms unfolding continuous_at by (rule tendsto_powr)
  2154 
  2155 lemma continuous_on_powr[continuous_intros]:
  2156   assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0"
  2157   shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
  2158   using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
  2159 
  2160 (* FIXME: generalize by replacing d by with g x and g ---> d? *)
  2161 lemma tendsto_zero_powrI:
  2162   assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
  2163     and "0 < d"
  2164   shows "((\<lambda>x. f x powr d) ---> 0) F"
  2165 proof (rule tendstoI)
  2166   fix e :: real assume "0 < e"
  2167   def Z \<equiv> "e powr (1 / d)"
  2168   with `0 < e` have "0 < Z" by simp
  2169   with assms have "eventually (\<lambda>x. 0 < f x \<and> dist (f x) 0 < Z) F"
  2170     by (intro eventually_conj tendstoD)
  2171   moreover
  2172   from assms have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> x powr d < Z powr d"
  2173     by (intro powr_less_mono2) (auto simp: dist_real_def)
  2174   with assms `0 < e` have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> dist (x powr d) 0 < e"
  2175     unfolding dist_real_def Z_def by (auto simp: powr_powr)
  2176   ultimately
  2177   show "eventually (\<lambda>x. dist (f x powr d) 0 < e) F" by (rule eventually_elim1)
  2178 qed
  2179 
  2180 lemma tendsto_neg_powr:
  2181   assumes "s < 0"
  2182     and "LIM x F. f x :> at_top"
  2183   shows "((\<lambda>x. f x powr s) ---> 0) F"
  2184 proof (rule tendstoI)
  2185   fix e :: real assume "0 < e"
  2186   def Z \<equiv> "e powr (1 / s)"
  2187   from assms have "eventually (\<lambda>x. Z < f x) F"
  2188     by (simp add: filterlim_at_top_dense)
  2189   moreover
  2190   from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
  2191     by (auto simp: Z_def intro!: powr_less_mono2_neg)
  2192   with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
  2193     by (simp add: powr_powr Z_def dist_real_def)
  2194   ultimately
  2195   show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
  2196 qed
  2197 
  2198 (* it is funny that this isn't in the library! It could go in Transcendental *)
  2199 lemma tendsto_exp_limit_at_right:
  2200   fixes x :: real
  2201   shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)"
  2202 proof cases
  2203   assume "x \<noteq> 0"
  2204 
  2205   have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
  2206     by (auto intro!: derivative_eq_intros)
  2207   then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
  2208     by (auto simp add: has_field_derivative_def field_has_derivative_at) 
  2209   then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)"
  2210     by (rule tendsto_intros)
  2211   then show ?thesis
  2212   proof (rule filterlim_mono_eventually)
  2213     show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
  2214       unfolding eventually_at_right[OF zero_less_one]
  2215       using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
  2216   qed (simp_all add: at_eq_sup_left_right)
  2217 qed simp
  2218 
  2219 lemma tendsto_exp_limit_at_top:
  2220   fixes x :: real
  2221   shows "((\<lambda>y. (1 + x / y) powr y) ---> exp x) at_top"
  2222   apply (subst filterlim_at_top_to_right)
  2223   apply (simp add: inverse_eq_divide)
  2224   apply (rule tendsto_exp_limit_at_right)
  2225   done
  2226 
  2227 lemma tendsto_exp_limit_sequentially:
  2228   fixes x :: real
  2229   shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x"
  2230 proof (rule filterlim_mono_eventually)
  2231   from reals_Archimedean2 [of "abs x"] obtain n :: nat where *: "real n > abs x" ..
  2232   hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
  2233     apply (intro eventually_sequentiallyI [of n])
  2234     apply (case_tac "x \<ge> 0")
  2235     apply (rule add_pos_nonneg, auto intro: divide_nonneg_nonneg)
  2236     apply (subgoal_tac "x / real xa > -1")
  2237     apply (auto simp add: field_simps)
  2238     done
  2239   then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
  2240     by (rule eventually_elim1) (erule powr_realpow)
  2241   show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x"
  2242     by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially])
  2243 qed auto
  2244 
  2245 subsection {* Sine and Cosine *}
  2246 
  2247 definition sin_coeff :: "nat \<Rightarrow> real" where
  2248   "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n))"
  2249 
  2250 definition cos_coeff :: "nat \<Rightarrow> real" where
  2251   "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
  2252 
  2253 definition sin :: "real \<Rightarrow> real"
  2254   where "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
  2255 
  2256 definition cos :: "real \<Rightarrow> real"
  2257   where "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
  2258 
  2259 lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
  2260   unfolding sin_coeff_def by simp
  2261 
  2262 lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
  2263   unfolding cos_coeff_def by simp
  2264 
  2265 lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
  2266   unfolding cos_coeff_def sin_coeff_def
  2267   by (simp del: mult_Suc)
  2268 
  2269 lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
  2270   unfolding cos_coeff_def sin_coeff_def
  2271   by (simp del: mult_Suc) (auto elim: oddE)
  2272 
  2273 lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
  2274   unfolding sin_coeff_def
  2275   apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
  2276   apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  2277   done
  2278 
  2279 lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
  2280   unfolding cos_coeff_def
  2281   apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
  2282   apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  2283   done
  2284 
  2285 lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
  2286   unfolding sin_def by (rule summable_sin [THEN summable_sums])
  2287 
  2288 lemma cos_converges: "(\<lambda>n. cos_coeff n * x ^ n) sums cos(x)"
  2289   unfolding cos_def by (rule summable_cos [THEN summable_sums])
  2290 
  2291 lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff"
  2292   by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
  2293 
  2294 lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
  2295   by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
  2296 
  2297 text{*Now at last we can get the derivatives of exp, sin and cos*}
  2298 
  2299 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
  2300   unfolding sin_def cos_def
  2301   apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
  2302   apply (simp_all add: diffs_sin_coeff diffs_cos_coeff
  2303     summable_minus summable_sin summable_cos)
  2304   done
  2305 
  2306 declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
  2307 
  2308 lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
  2309   unfolding cos_def sin_def
  2310   apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
  2311   apply (simp_all add: diffs_sin_coeff diffs_cos_coeff diffs_minus
  2312     summable_minus summable_sin summable_cos suminf_minus)
  2313   done
  2314 
  2315 declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
  2316 
  2317 lemma isCont_sin: "isCont sin x"
  2318   by (rule DERIV_sin [THEN DERIV_isCont])
  2319 
  2320 lemma isCont_cos: "isCont cos x"
  2321   by (rule DERIV_cos [THEN DERIV_isCont])
  2322 
  2323 lemma isCont_sin' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
  2324   by (rule isCont_o2 [OF _ isCont_sin])
  2325 
  2326 lemma isCont_cos' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
  2327   by (rule isCont_o2 [OF _ isCont_cos])
  2328 
  2329 lemma tendsto_sin [tendsto_intros]:
  2330   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) ---> sin a) F"
  2331   by (rule isCont_tendsto_compose [OF isCont_sin])
  2332 
  2333 lemma tendsto_cos [tendsto_intros]:
  2334   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
  2335   by (rule isCont_tendsto_compose [OF isCont_cos])
  2336 
  2337 lemma continuous_sin [continuous_intros]:
  2338   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
  2339   unfolding continuous_def by (rule tendsto_sin)
  2340 
  2341 lemma continuous_on_sin [continuous_intros]:
  2342   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
  2343   unfolding continuous_on_def by (auto intro: tendsto_sin)
  2344 
  2345 lemma continuous_cos [continuous_intros]:
  2346   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
  2347   unfolding continuous_def by (rule tendsto_cos)
  2348 
  2349 lemma continuous_on_cos [continuous_intros]:
  2350   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
  2351   unfolding continuous_on_def by (auto intro: tendsto_cos)
  2352 
  2353 subsection {* Properties of Sine and Cosine *}
  2354 
  2355 lemma sin_zero [simp]: "sin 0 = 0"
  2356   unfolding sin_def sin_coeff_def by (simp add: powser_zero)
  2357 
  2358 lemma cos_zero [simp]: "cos 0 = 1"
  2359   unfolding cos_def cos_coeff_def by (simp add: powser_zero)
  2360 
  2361 lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
  2362 proof -
  2363   have "\<forall>x. DERIV (\<lambda>x. (sin x)\<^sup>2 + (cos x)\<^sup>2) x :> 0"
  2364     by (auto intro!: derivative_eq_intros)
  2365   hence "(sin x)\<^sup>2 + (cos x)\<^sup>2 = (sin 0)\<^sup>2 + (cos 0)\<^sup>2"
  2366     by (rule DERIV_isconst_all)
  2367   thus "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" by simp
  2368 qed
  2369 
  2370 lemma sin_cos_squared_add2 [simp]: "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
  2371   by (subst add.commute, rule sin_cos_squared_add)
  2372 
  2373 lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
  2374   using sin_cos_squared_add2 [unfolded power2_eq_square] .
  2375 
  2376 lemma sin_squared_eq: "(sin x)\<^sup>2 = 1 - (cos x)\<^sup>2"
  2377   unfolding eq_diff_eq by (rule sin_cos_squared_add)
  2378 
  2379 lemma cos_squared_eq: "(cos x)\<^sup>2 = 1 - (sin x)\<^sup>2"
  2380   unfolding eq_diff_eq by (rule sin_cos_squared_add2)
  2381 
  2382 lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
  2383   by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
  2384 
  2385 lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
  2386   using abs_sin_le_one [of x] unfolding abs_le_iff by simp
  2387 
  2388 lemma sin_le_one [simp]: "sin x \<le> 1"
  2389   using abs_sin_le_one [of x] unfolding abs_le_iff by simp
  2390 
  2391 lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
  2392   by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
  2393 
  2394 lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
  2395   using abs_cos_le_one [of x] unfolding abs_le_iff by simp
  2396 
  2397 lemma cos_le_one [simp]: "cos x \<le> 1"
  2398   using abs_cos_le_one [of x] unfolding abs_le_iff by simp
  2399 
  2400 lemma DERIV_fun_pow: "DERIV g x :> m ==>
  2401       DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
  2402   by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  2403 
  2404 lemma DERIV_fun_exp:
  2405      "DERIV g x :> m ==> DERIV (\<lambda>x. exp(g x)) x :> exp(g x) * m"
  2406   by (auto intro!: derivative_intros)
  2407 
  2408 lemma DERIV_fun_sin:
  2409      "DERIV g x :> m ==> DERIV (\<lambda>x. sin(g x)) x :> cos(g x) * m"
  2410   by (auto intro!: derivative_intros)
  2411 
  2412 lemma DERIV_fun_cos:
  2413      "DERIV g x :> m ==> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
  2414   by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  2415 
  2416 lemma sin_cos_add_lemma:
  2417   "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 +
  2418     (cos (x + y) - (cos x * cos y - sin x * sin y))\<^sup>2 = 0"
  2419   (is "?f x = 0")
  2420 proof -
  2421   have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
  2422     by (auto intro!: derivative_eq_intros simp add: algebra_simps)
  2423   hence "?f x = ?f 0"
  2424     by (rule DERIV_isconst_all)
  2425   thus ?thesis by simp
  2426 qed
  2427 
  2428 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
  2429   using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
  2430 
  2431 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
  2432   using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
  2433 
  2434 lemma sin_cos_minus_lemma:
  2435   "(sin(-x) + sin(x))\<^sup>2 + (cos(-x) - cos(x))\<^sup>2 = 0" (is "?f x = 0")
  2436 proof -
  2437   have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
  2438     by (auto intro!: derivative_eq_intros simp add: algebra_simps)
  2439   hence "?f x = ?f 0"
  2440     by (rule DERIV_isconst_all)
  2441   thus ?thesis by simp
  2442 qed
  2443 
  2444 lemma sin_minus [simp]: "sin (-x) = -sin(x)"
  2445   using sin_cos_minus_lemma [where x=x] by simp
  2446 
  2447 lemma cos_minus [simp]: "cos (-x) = cos(x)"
  2448   using sin_cos_minus_lemma [where x=x] by simp
  2449 
  2450 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
  2451   using sin_add [of x "- y"] by simp
  2452 
  2453 lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
  2454   by (simp add: sin_diff mult.commute)
  2455 
  2456 lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
  2457   using cos_add [of x "- y"] by simp
  2458 
  2459 lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
  2460   by (simp add: cos_diff mult.commute)
  2461 
  2462 lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
  2463   using sin_add [where x=x and y=x] by simp
  2464 
  2465 lemma cos_double: "cos(2* x) = ((cos x)\<^sup>2) - ((sin x)\<^sup>2)"
  2466   using cos_add [where x=x and y=x]
  2467   by (simp add: power2_eq_square)
  2468 
  2469 lemma sin_x_le_x: assumes x: "x \<ge> 0" shows "sin x \<le> x"
  2470 proof -
  2471   let ?f = "\<lambda>x. x - sin x"
  2472   from x have "?f x \<ge> ?f 0"
  2473     apply (rule DERIV_nonneg_imp_nondecreasing)
  2474     apply (intro allI impI exI[of _ "1 - cos x" for x])
  2475     apply (auto intro!: derivative_eq_intros simp: field_simps)
  2476     done
  2477   thus "sin x \<le> x" by simp
  2478 qed
  2479 
  2480 lemma sin_x_ge_neg_x: assumes x: "x \<ge> 0" shows "sin x \<ge> - x"
  2481 proof -
  2482   let ?f = "\<lambda>x. x + sin x"
  2483   from x have "?f x \<ge> ?f 0"
  2484     apply (rule DERIV_nonneg_imp_nondecreasing)
  2485     apply (intro allI impI exI[of _ "1 + cos x" for x])
  2486     apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
  2487     done
  2488   thus "sin x \<ge> -x" by simp
  2489 qed
  2490 
  2491 lemma abs_sin_x_le_abs_x: "\<bar>sin x\<bar> \<le> \<bar>x\<bar>"
  2492   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"]
  2493   by (auto simp: abs_real_def)
  2494 
  2495 subsection {* The Constant Pi *}
  2496 
  2497 definition pi :: real
  2498   where "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
  2499 
  2500 text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
  2501    hence define pi.*}
  2502 
  2503 lemma sin_paired:
  2504   "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
  2505 proof -
  2506   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
  2507     by (rule sin_converges [THEN sums_group], simp)
  2508   thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: ac_simps)
  2509 qed
  2510 
  2511 lemma sin_gt_zero:
  2512   assumes "0 < x" and "x < 2"
  2513   shows "0 < sin x"
  2514 proof -
  2515   let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / real (fact (2*k+1)) * x^(2*k+1)"
  2516   have pos: "\<forall>n. 0 < ?f n"
  2517   proof
  2518     fix n :: nat
  2519     let ?k2 = "real (Suc (Suc (4 * n)))"
  2520     let ?k3 = "real (Suc (Suc (Suc (4 * n))))"
  2521     have "x * x < ?k2 * ?k3"
  2522       using assms by (intro mult_strict_mono', simp_all)
  2523     hence "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)"
  2524       by (intro mult_strict_right_mono zero_less_power `0 < x`)
  2525     thus "0 < ?f n"
  2526       by (simp del: mult_Suc,
  2527         simp add: less_divide_eq field_simps del: mult_Suc)
  2528   qed
  2529   have sums: "?f sums sin x"
  2530     by (rule sin_paired [THEN sums_group], simp)
  2531   show "0 < sin x"
  2532     unfolding sums_unique [OF sums]
  2533     using sums_summable [OF sums] pos
  2534     by (rule suminf_pos)
  2535 qed
  2536 
  2537 lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
  2538   using sin_gt_zero [where x = x] by (auto simp add: cos_squared_eq cos_double)
  2539 
  2540 lemma cos_paired: "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
  2541 proof -
  2542   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
  2543     by (rule cos_converges [THEN sums_group], simp)
  2544   thus ?thesis unfolding cos_coeff_def by (simp add: ac_simps)
  2545 qed
  2546 
  2547 lemmas realpow_num_eq_if = power_eq_if
  2548 
  2549 lemma sumr_pos_lt_pair:
  2550   fixes f :: "nat \<Rightarrow> real"
  2551   shows "\<lbrakk>summable f;
  2552         \<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
  2553       \<Longrightarrow> setsum f {..<k} < suminf f"
  2554 unfolding One_nat_def
  2555 apply (subst suminf_split_initial_segment [where k="k"])
  2556 apply assumption
  2557 apply simp
  2558 apply (drule_tac k="k" in summable_ignore_initial_segment)
  2559 apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
  2560 apply simp
  2561 apply (frule sums_unique)
  2562 apply (drule sums_summable)
  2563 apply simp
  2564 apply (erule suminf_pos)
  2565 apply (simp add: ac_simps)
  2566 done
  2567 
  2568 lemma cos_two_less_zero [simp]:
  2569   "cos 2 < 0"
  2570 proof -
  2571   note fact_Suc [simp del]
  2572   from cos_paired
  2573   have "(\<lambda>n. - ((- 1) ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
  2574     by (rule sums_minus)
  2575   then have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
  2576     by simp
  2577   then have **: "summable (\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2578     by (rule sums_summable)
  2579   have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2580     by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
  2581   moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
  2582     < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2583   proof -
  2584     { fix d
  2585       have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  2586        < real (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
  2587            fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  2588         by (simp only: real_of_nat_mult) (auto intro!: mult_strict_mono fact_less_mono_nat)
  2589       then have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  2590         < real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
  2591         by (simp only: fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
  2592       then have "4 * inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))))
  2593         < inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  2594         by (simp add: inverse_eq_divide less_divide_eq)
  2595     }
  2596     note *** = this
  2597     have [simp]: "\<And>x y::real. 0 < x - y \<longleftrightarrow> y < x" by arith
  2598     from ** show ?thesis by (rule sumr_pos_lt_pair)
  2599       (simp add: divide_inverse mult.assoc [symmetric] ***)
  2600   qed
  2601   ultimately have "0 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2602     by (rule order_less_trans)
  2603   moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  2604     by (rule sums_unique)
  2605   ultimately have "0 < - cos 2" by simp
  2606   then show ?thesis by simp
  2607 qed
  2608 
  2609 lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
  2610 lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]
  2611 
  2612 lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 \<and> cos x = 0"
  2613 proof (rule ex_ex1I)
  2614   show "\<exists>x. 0 \<le> x & x \<le> 2 & cos x = 0"
  2615     by (rule IVT2, simp_all)
  2616 next
  2617   fix x y
  2618   assume x: "0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
  2619   assume y: "0 \<le> y \<and> y \<le> 2 \<and> cos y = 0"
  2620   have [simp]: "\<forall>x. cos differentiable (at x)"
  2621     unfolding real_differentiable_def by (auto intro: DERIV_cos)
  2622   from x y show "x = y"
  2623     apply (cut_tac less_linear [of x y], auto)
  2624     apply (drule_tac f = cos in Rolle)
  2625     apply (drule_tac [5] f = cos in Rolle)
  2626     apply (auto dest!: DERIV_cos [THEN DERIV_unique])
  2627     apply (metis order_less_le_trans less_le sin_gt_zero)
  2628     apply (metis order_less_le_trans less_le sin_gt_zero)
  2629     done
  2630 qed
  2631 
  2632 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
  2633   by (simp add: pi_def)
  2634 
  2635 lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
  2636   by (simp add: pi_half cos_is_zero [THEN theI'])
  2637 
  2638 lemma pi_half_gt_zero [simp]: "0 < pi / 2"
  2639   apply (rule order_le_neq_trans)
  2640   apply (simp add: pi_half cos_is_zero [THEN theI'])
  2641   apply (metis cos_pi_half cos_zero zero_neq_one)
  2642   done
  2643 
  2644 lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
  2645 lemmas pi_half_ge_zero [simp] = pi_half_gt_zero [THEN order_less_imp_le]
  2646 
  2647 lemma pi_half_less_two [simp]: "pi / 2 < 2"
  2648   apply (rule order_le_neq_trans)
  2649   apply (simp add: pi_half cos_is_zero [THEN theI'])
  2650   apply (metis cos_pi_half cos_two_neq_zero)
  2651   done
  2652 
  2653 lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
  2654 lemmas pi_half_le_two [simp] =  pi_half_less_two [THEN order_less_imp_le]
  2655 
  2656 lemma pi_gt_zero [simp]: "0 < pi"
  2657   using pi_half_gt_zero by simp
  2658 
  2659 lemma pi_ge_zero [simp]: "0 \<le> pi"
  2660   by (rule pi_gt_zero [THEN order_less_imp_le])
  2661 
  2662 lemma pi_neq_zero [simp]: "pi \<noteq> 0"
  2663   by (rule pi_gt_zero [THEN less_imp_neq, symmetric])
  2664 
  2665 lemma pi_not_less_zero [simp]: "\<not> pi < 0"
  2666   by (simp add: linorder_not_less)
  2667 
  2668 lemma minus_pi_half_less_zero: "-(pi/2) < 0"
  2669   by simp
  2670 
  2671 lemma m2pi_less_pi: "- (2 * pi) < pi"
  2672   by simp
  2673 
  2674 lemma sin_pi_half [simp]: "sin(pi/2) = 1"
  2675   using sin_cos_squared_add2 [where x = "pi/2"]
  2676   using sin_gt_zero [OF pi_half_gt_zero pi_half_less_two]
  2677   by (simp add: power2_eq_1_iff)
  2678 
  2679 lemma cos_pi [simp]: "cos pi = -1"
  2680   using cos_add [where x = "pi/2" and y = "pi/2"] by simp
  2681 
  2682 lemma sin_pi [simp]: "sin pi = 0"
  2683   using sin_add [where x = "pi/2" and y = "pi/2"] by simp
  2684 
  2685 lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
  2686   by (simp add: cos_diff)
  2687 
  2688 lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
  2689   by (simp add: cos_add)
  2690 
  2691 lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
  2692   by (simp add: sin_diff)
  2693 
  2694 lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
  2695   by (simp add: sin_add)
  2696 
  2697 lemma sin_periodic_pi2 [simp]: "sin (pi + x) = - sin x"
  2698   by (simp add: sin_add)
  2699 
  2700 lemma cos_periodic_pi [simp]: "cos (x + pi) = - cos x"
  2701   by (simp add: cos_add)
  2702 
  2703 lemma sin_periodic [simp]: "sin (x + 2*pi) = sin x"
  2704   by (simp add: sin_add cos_double)
  2705 
  2706 lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
  2707   by (simp add: cos_add cos_double)
  2708 
  2709 lemma cos_npi [simp]: "cos (real n * pi) = (- 1) ^ n"
  2710   by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
  2711 
  2712 lemma cos_npi2 [simp]: "cos (pi * real n) = (- 1) ^ n"
  2713   by (metis cos_npi mult.commute)
  2714 
  2715 lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
  2716   by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
  2717 
  2718 lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
  2719   by (simp add: mult.commute [of pi])
  2720 
  2721 lemma cos_two_pi [simp]: "cos (2 * pi) = 1"
  2722   by (simp add: cos_double)
  2723 
  2724 lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
  2725   by simp
  2726 
  2727 lemma sin_gt_zero2: "[| 0 < x; x < pi/2 |] ==> 0 < sin x"
  2728   by (metis sin_gt_zero order_less_trans pi_half_less_two)
  2729 
  2730 lemma sin_less_zero:
  2731   assumes "- pi/2 < x" and "x < 0"
  2732   shows "sin x < 0"
  2733 proof -
  2734   have "0 < sin (- x)" using assms by (simp only: sin_gt_zero2)
  2735   thus ?thesis by simp
  2736 qed
  2737 
  2738 lemma pi_less_4: "pi < 4"
  2739   using pi_half_less_two by auto
  2740 
  2741 lemma cos_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < cos x"
  2742   apply (cut_tac pi_less_4)
  2743   apply (cut_tac f = cos and a = 0 and b = x and y = 0 in IVT2_objl, safe, simp_all)
  2744   apply (cut_tac cos_is_zero, safe)
  2745   apply (rename_tac y z)
  2746   apply (drule_tac x = y in spec)
  2747   apply (drule_tac x = "pi/2" in spec, simp)
  2748   done
  2749 
  2750 lemma cos_gt_zero_pi: "[| -(pi/2) < x; x < pi/2 |] ==> 0 < cos x"
  2751   apply (rule_tac x = x and y = 0 in linorder_cases)
  2752   apply (metis cos_gt_zero cos_minus minus_less_iff neg_0_less_iff_less)
  2753   apply (auto intro: cos_gt_zero)
  2754   done
  2755 
  2756 lemma cos_ge_zero: "[| -(pi/2) \<le> x; x \<le> pi/2 |] ==> 0 \<le> cos x"
  2757   apply (auto simp add: order_le_less cos_gt_zero_pi)
  2758   apply (subgoal_tac "x = pi/2", auto)
  2759   done
  2760 
  2761 lemma sin_gt_zero_pi: "[| 0 < x; x < pi  |] ==> 0 < sin x"
  2762   by (simp add: sin_cos_eq cos_gt_zero_pi)
  2763 
  2764 lemma pi_ge_two: "2 \<le> pi"
  2765 proof (rule ccontr)
  2766   assume "\<not> 2 \<le> pi" hence "pi < 2" by auto
  2767   have "\<exists>y > pi. y < 2 \<and> y < 2 * pi"
  2768   proof (cases "2 < 2 * pi")
  2769     case True with dense[OF `pi < 2`] show ?thesis by auto
  2770   next
  2771     case False have "pi < 2 * pi" by auto
  2772     from dense[OF this] and False show ?thesis by auto
  2773   qed
  2774   then obtain y where "pi < y" and "y < 2" and "y < 2 * pi" by blast
  2775   hence "0 < sin y" using sin_gt_zero by auto
  2776   moreover
  2777   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
  2778   ultimately show False by auto
  2779 qed
  2780 
  2781 lemma sin_ge_zero: "[| 0 \<le> x; x \<le> pi |] ==> 0 \<le> sin x"
  2782   by (auto simp add: order_le_less sin_gt_zero_pi)
  2783 
  2784 text {* FIXME: This proof is almost identical to lemma @{text cos_is_zero}.
  2785   It should be possible to factor out some of the common parts. *}
  2786 
  2787 lemma cos_total: "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)"
  2788 proof (rule ex_ex1I)
  2789   assume y: "-1 \<le> y" "y \<le> 1"
  2790   show "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y"
  2791     by (rule IVT2, simp_all add: y)
  2792 next
  2793   fix a b
  2794   assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
  2795   assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
  2796   have [simp]: "\<forall>x. cos differentiable (at x)"
  2797     unfolding real_differentiable_def by (auto intro: DERIV_cos)
  2798   from a b show "a = b"
  2799     apply (cut_tac less_linear [of a b], auto)
  2800     apply (drule_tac f = cos in Rolle)
  2801     apply (drule_tac [5] f = cos in Rolle)
  2802     apply (auto dest!: DERIV_cos [THEN DERIV_unique])
  2803     apply (metis order_less_le_trans less_le sin_gt_zero_pi)
  2804     apply (metis order_less_le_trans less_le sin_gt_zero_pi)
  2805     done
  2806 qed
  2807 
  2808 lemma sin_total:
  2809      "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"
  2810 apply (rule ccontr)
  2811 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))")
  2812 apply (erule contrapos_np)
  2813 apply simp
  2814 apply (cut_tac y="-y" in cos_total, simp) apply simp
  2815 apply (erule ex1E)
  2816 apply (rule_tac a = "x - (pi/2)" in ex1I)
  2817 apply (simp (no_asm) add: add.assoc)
  2818 apply (rotate_tac 3)
  2819 apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all add: cos_add)
  2820 done
  2821 
  2822 lemma reals_Archimedean4:
  2823      "[| 0 < y; 0 \<le> x |] ==> \<exists>n. real n * y \<le> x & x < real (Suc n) * y"
  2824 apply (auto dest!: reals_Archimedean3)
  2825 apply (drule_tac x = x in spec, clarify)
  2826 apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y")
  2827  prefer 2 apply (erule LeastI)
  2828 apply (case_tac "LEAST m::nat. x < real m * y", simp)
  2829 apply (rename_tac m)
  2830 apply (subgoal_tac "~ x < real m * y")
  2831  prefer 2 apply (rule not_less_Least, simp, force)
  2832 done
  2833 
  2834 (* Pre Isabelle99-2 proof was simpler- numerals arithmetic
  2835    now causes some unwanted re-arrangements of literals!   *)
  2836 lemma cos_zero_lemma:
  2837      "[| 0 \<le> x; cos x = 0 |] ==>
  2838       \<exists>n::nat. ~even n & x = real n * (pi/2)"
  2839 apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
  2840 apply (subgoal_tac "0 \<le> x - real n * pi &
  2841                     (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
  2842 apply (auto simp add: algebra_simps real_of_nat_Suc)
  2843  prefer 2 apply (simp add: cos_diff)
  2844 apply (simp add: cos_diff)
  2845 apply (subgoal_tac "EX! x. 0 \<le> x & x \<le> pi & cos x = 0")
  2846 apply (rule_tac [2] cos_total, safe)
  2847 apply (drule_tac x = "x - real n * pi" in spec)
  2848 apply (drule_tac x = "pi/2" in spec)
  2849 apply (simp add: cos_diff)
  2850 apply (rule_tac x = "Suc (2 * n)" in exI)
  2851 apply (simp add: real_of_nat_Suc algebra_simps, auto)
  2852 done
  2853 
  2854 lemma sin_zero_lemma:
  2855      "[| 0 \<le> x; sin x = 0 |] ==>
  2856       \<exists>n::nat. even n & x = real n * (pi/2)"
  2857 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  2858  apply (clarify, rule_tac x = "n - 1" in exI)
  2859  apply (auto elim!: oddE simp add: real_of_nat_Suc field_simps)[1]
  2860  apply (rule cos_zero_lemma)
  2861  apply (auto simp add: cos_add)
  2862 done
  2863 
  2864 lemma cos_zero_iff:
  2865      "(cos x = 0) =
  2866       ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |
  2867        (\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
  2868 proof -
  2869   { fix n :: nat
  2870     assume "odd n"
  2871     then obtain m where "n = 2 * m + 1" ..
  2872     then have "cos (real n * pi / 2) = 0"
  2873       by (simp add: field_simps real_of_nat_Suc) (simp add: cos_add add_divide_distrib)
  2874   } note * = this
  2875   show ?thesis
  2876   apply (rule iffI)
  2877   apply (cut_tac linorder_linear [of 0 x], safe)
  2878   apply (drule cos_zero_lemma, assumption+)
  2879   apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
  2880   apply (auto dest: *)
  2881   done
  2882 qed
  2883 
  2884 (* ditto: but to a lesser extent *)
  2885 lemma sin_zero_iff:
  2886      "(sin x = 0) =
  2887       ((\<exists>n::nat. even n & (x = real n * (pi/2))) |
  2888        (\<exists>n::nat. even n & (x = -(real n * (pi/2)))))"
  2889 apply (rule iffI)
  2890 apply (cut_tac linorder_linear [of 0 x], safe)
  2891 apply (drule sin_zero_lemma, assumption+)
  2892 apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
  2893 apply (force simp add: minus_equation_iff [of x])
  2894 apply (auto elim: evenE)
  2895 done
  2896 
  2897 lemma cos_monotone_0_pi:
  2898   assumes "0 \<le> y" and "y < x" and "x \<le> pi"
  2899   shows "cos x < cos y"
  2900 proof -
  2901   have "- (x - y) < 0" using assms by auto
  2902 
  2903   from MVT2[OF `y < x` DERIV_cos[THEN impI, THEN allI]]
  2904   obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z"
  2905     by auto
  2906   hence "0 < z" and "z < pi" using assms by auto
  2907   hence "0 < sin z" using sin_gt_zero_pi by auto
  2908   hence "cos x - cos y < 0"
  2909     unfolding cos_diff minus_mult_commute[symmetric]
  2910     using `- (x - y) < 0` by (rule mult_pos_neg2)
  2911   thus ?thesis by auto
  2912 qed
  2913 
  2914 lemma cos_monotone_0_pi':
  2915   assumes "0 \<le> y" and "y \<le> x" and "x \<le> pi"
  2916   shows "cos x \<le> cos y"
  2917 proof (cases "y < x")
  2918   case True
  2919   show ?thesis
  2920     using cos_monotone_0_pi[OF `0 \<le> y` True `x \<le> pi`] by auto
  2921 next
  2922   case False
  2923   hence "y = x" using `y \<le> x` by auto
  2924   thus ?thesis by auto
  2925 qed
  2926 
  2927 lemma cos_monotone_minus_pi_0:
  2928   assumes "-pi \<le> y" and "y < x" and "x \<le> 0"
  2929   shows "cos y < cos x"
  2930 proof -
  2931   have "0 \<le> -x" and "-x < -y" and "-y \<le> pi"
  2932     using assms by auto
  2933   from cos_monotone_0_pi[OF this] show ?thesis
  2934     unfolding cos_minus .
  2935 qed
  2936 
  2937 lemma cos_monotone_minus_pi_0':
  2938   assumes "-pi \<le> y" and "y \<le> x" and "x \<le> 0"
  2939   shows "cos y \<le> cos x"
  2940 proof (cases "y < x")
  2941   case True
  2942   show ?thesis using cos_monotone_minus_pi_0[OF `-pi \<le> y` True `x \<le> 0`]
  2943     by auto
  2944 next
  2945   case False
  2946   hence "y = x" using `y \<le> x` by auto
  2947   thus ?thesis by auto
  2948 qed
  2949 
  2950 lemma sin_monotone_2pi':
  2951   assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2"
  2952   shows "sin y \<le> sin x"
  2953 proof -
  2954   have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
  2955     using pi_ge_two and assms by auto
  2956   from cos_monotone_0_pi'[OF this] show ?thesis
  2957     unfolding minus_sin_cos_eq[symmetric] by auto
  2958 qed
  2959 
  2960 
  2961 subsection {* Tangent *}
  2962 
  2963 definition tan :: "real \<Rightarrow> real"
  2964   where "tan = (\<lambda>x. sin x / cos x)"
  2965 
  2966 lemma tan_zero [simp]: "tan 0 = 0"
  2967   by (simp add: tan_def)
  2968 
  2969 lemma tan_pi [simp]: "tan pi = 0"
  2970   by (simp add: tan_def)
  2971 
  2972 lemma tan_npi [simp]: "tan (real (n::nat) * pi) = 0"
  2973   by (simp add: tan_def)
  2974 
  2975 lemma tan_minus [simp]: "tan (-x) = - tan x"
  2976   by (simp add: tan_def)
  2977 
  2978 lemma tan_periodic [simp]: "tan (x + 2*pi) = tan x"
  2979   by (simp add: tan_def)
  2980 
  2981 lemma lemma_tan_add1:
  2982   "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> 1 - tan x * tan y = cos (x + y)/(cos x * cos y)"
  2983   by (simp add: tan_def cos_add field_simps)
  2984 
  2985 lemma add_tan_eq:
  2986   "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> tan x + tan y = sin(x + y)/(cos x * cos y)"
  2987   by (simp add: tan_def sin_add field_simps)
  2988 
  2989 lemma tan_add:
  2990      "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]
  2991       ==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
  2992   by (simp add: add_tan_eq lemma_tan_add1, simp add: tan_def)
  2993 
  2994 lemma tan_double:
  2995      "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]
  2996       ==> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)"
  2997   using tan_add [of x x] by (simp add: power2_eq_square)
  2998 
  2999 lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
  3000   by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
  3001 
  3002 lemma tan_less_zero:
  3003   assumes lb: "- pi/2 < x" and "x < 0"
  3004   shows "tan x < 0"
  3005 proof -
  3006   have "0 < tan (- x)" using assms by (simp only: tan_gt_zero)
  3007   thus ?thesis by simp
  3008 qed
  3009 
  3010 lemma tan_half: "tan x = sin (2 * x) / (cos (2 * x) + 1)"
  3011   unfolding tan_def sin_double cos_double sin_squared_eq
  3012   by (simp add: power2_eq_square)
  3013 
  3014 lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
  3015   unfolding tan_def
  3016   by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
  3017 
  3018 lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
  3019   by (rule DERIV_tan [THEN DERIV_isCont])
  3020 
  3021 lemma isCont_tan' [simp]:
  3022   "\<lbrakk>isCont f a; cos (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. tan (f x)) a"
  3023   by (rule isCont_o2 [OF _ isCont_tan])
  3024 
  3025 lemma tendsto_tan [tendsto_intros]:
  3026   "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
  3027   by (rule isCont_tendsto_compose [OF isCont_tan])
  3028 
  3029 lemma continuous_tan:
  3030   "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
  3031   unfolding continuous_def by (rule tendsto_tan)
  3032 
  3033 lemma isCont_tan'' [continuous_intros]:
  3034   "continuous (at x) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. tan (f x))"
  3035   unfolding continuous_at by (rule tendsto_tan)
  3036 
  3037 lemma continuous_within_tan [continuous_intros]:
  3038   "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
  3039   unfolding continuous_within by (rule tendsto_tan)
  3040 
  3041 lemma continuous_on_tan [continuous_intros]:
  3042   "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
  3043   unfolding continuous_on_def by (auto intro: tendsto_tan)
  3044 
  3045 lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) -- pi/2 --> 0"
  3046   by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
  3047 
  3048 lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
  3049   apply (cut_tac LIM_cos_div_sin)
  3050   apply (simp only: LIM_eq)
  3051   apply (drule_tac x = "inverse y" in spec, safe, force)
  3052   apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
  3053   apply (rule_tac x = "(pi/2) - e" in exI)
  3054   apply (simp (no_asm_simp))
  3055   apply (drule_tac x = "(pi/2) - e" in spec)
  3056   apply (auto simp add: tan_def sin_diff cos_diff)
  3057   apply (rule inverse_less_iff_less [THEN iffD1])
  3058   apply (auto simp add: divide_inverse)
  3059   apply (rule mult_pos_pos)
  3060   apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
  3061   apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult.commute)
  3062   done
  3063 
  3064 lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
  3065   apply (frule order_le_imp_less_or_eq, safe)
  3066    prefer 2 apply force
  3067   apply (drule lemma_tan_total, safe)
  3068   apply (cut_tac f = tan and a = 0 and b = x and y = y in IVT_objl)
  3069   apply (auto intro!: DERIV_tan [THEN DERIV_isCont])
  3070   apply (drule_tac y = xa in order_le_imp_less_or_eq)
  3071   apply (auto dest: cos_gt_zero)
  3072   done
  3073 
  3074 lemma lemma_tan_total1: "\<exists>x. -(pi/2) < x & x < (pi/2) & tan x = y"
  3075   apply (cut_tac linorder_linear [of 0 y], safe)
  3076   apply (drule tan_total_pos)
  3077   apply (cut_tac [2] y="-y" in tan_total_pos, safe)
  3078   apply (rule_tac [3] x = "-x" in exI)
  3079   apply (auto del: exI intro!: exI)
  3080   done
  3081 
  3082 lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
  3083   apply (cut_tac y = y in lemma_tan_total1, auto)
  3084   apply hypsubst_thin
  3085   apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
  3086   apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
  3087   apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
  3088   apply (rule_tac [4] Rolle)
  3089   apply (rule_tac [2] Rolle)
  3090   apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
  3091               simp add: real_differentiable_def)
  3092   txt{*Now, simulate TRYALL*}
  3093   apply (rule_tac [!] DERIV_tan asm_rl)
  3094   apply (auto dest!: DERIV_unique [OF _ DERIV_tan]
  3095               simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym])
  3096   done
  3097 
  3098 lemma tan_monotone:
  3099   assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2"
  3100   shows "tan y < tan x"
  3101 proof -
  3102   have "\<forall>x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)"
  3103   proof (rule allI, rule impI)
  3104     fix x' :: real
  3105     assume "y \<le> x' \<and> x' \<le> x"
  3106     hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto
  3107     from cos_gt_zero_pi[OF this]
  3108     have "cos x' \<noteq> 0" by auto
  3109     thus "DERIV tan x' :> inverse ((cos x')\<^sup>2)" by (rule DERIV_tan)
  3110   qed
  3111   from MVT2[OF `y < x` this]
  3112   obtain z where "y < z" and "z < x"
  3113     and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto
  3114   hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto
  3115   hence "0 < cos z" using cos_gt_zero_pi by auto
  3116   hence inv_pos: "0 < inverse ((cos z)\<^sup>2)" by auto
  3117   have "0 < x - y" using `y < x` by auto
  3118   with inv_pos have "0 < tan x - tan y" unfolding tan_diff by auto
  3119   thus ?thesis by auto
  3120 qed
  3121 
  3122 lemma tan_monotone':
  3123   assumes "- (pi / 2) < y"
  3124     and "y < pi / 2"
  3125     and "- (pi / 2) < x"
  3126     and "x < pi / 2"
  3127   shows "(y < x) = (tan y < tan x)"
  3128 proof
  3129   assume "y < x"
  3130   thus "tan y < tan x"
  3131     using tan_monotone and `- (pi / 2) < y` and `x < pi / 2` by auto
  3132 next
  3133   assume "tan y < tan x"
  3134   show "y < x"
  3135   proof (rule ccontr)
  3136     assume "\<not> y < x" hence "x \<le> y" by auto
  3137     hence "tan x \<le> tan y"
  3138     proof (cases "x = y")
  3139       case True thus ?thesis by auto
  3140     next
  3141       case False hence "x < y" using `x \<le> y` by auto
  3142       from tan_monotone[OF `- (pi/2) < x` this `y < pi / 2`] show ?thesis by auto
  3143     qed
  3144     thus False using `tan y < tan x` by auto
  3145   qed
  3146 qed
  3147 
  3148 lemma tan_inverse: "1 / (tan y) = tan (pi / 2 - y)"
  3149   unfolding tan_def sin_cos_eq[of y] cos_sin_eq[of y] by auto
  3150 
  3151 lemma tan_periodic_pi[simp]: "tan (x + pi) = tan x"
  3152   by (simp add: tan_def)
  3153 
  3154 lemma tan_periodic_nat[simp]:
  3155   fixes n :: nat
  3156   shows "tan (x + real n * pi) = tan x"
  3157 proof (induct n arbitrary: x)
  3158   case 0
  3159   then show ?case by simp
  3160 next
  3161   case (Suc n)
  3162   have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi"
  3163     unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
  3164   show ?case unfolding split_pi_off using Suc by auto
  3165 qed
  3166 
  3167 lemma tan_periodic_int[simp]: fixes i :: int shows "tan (x + real i * pi) = tan x"
  3168 proof (cases "0 \<le> i")
  3169   case True
  3170   hence i_nat: "real i = real (nat i)" by auto
  3171   show ?thesis unfolding i_nat by auto
  3172 next
  3173   case False
  3174   hence i_nat: "real i = - real (nat (-i))" by auto
  3175   have "tan x = tan (x + real i * pi - real i * pi)"
  3176     by auto
  3177   also have "\<dots> = tan (x + real i * pi)"
  3178     unfolding i_nat mult_minus_left diff_minus_eq_add by (rule tan_periodic_nat)
  3179   finally show ?thesis by auto
  3180 qed
  3181 
  3182 lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
  3183   using tan_periodic_int[of _ "numeral n" ] unfolding real_numeral .
  3184 
  3185 subsection {* Inverse Trigonometric Functions *}
  3186 
  3187 definition arcsin :: "real => real"
  3188   where "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
  3189 
  3190 definition arccos :: "real => real"
  3191   where "arccos y = (THE x. 0 \<le> x & x \<le> pi & cos x = y)"
  3192 
  3193 definition arctan :: "real => real"
  3194   where "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)"
  3195 
  3196 lemma arcsin:
  3197   "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow>
  3198     -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2 & sin(arcsin y) = y"
  3199   unfolding arcsin_def by (rule theI' [OF sin_total])
  3200 
  3201 lemma arcsin_pi:
  3202   "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi & sin(arcsin y) = y"
  3203   apply (drule (1) arcsin)
  3204   apply (force intro: order_trans)
  3205   done
  3206 
  3207 lemma sin_arcsin [simp]: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> sin(arcsin y) = y"
  3208   by (blast dest: arcsin)
  3209 
  3210 lemma arcsin_bounded: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2"
  3211   by (blast dest: arcsin)
  3212 
  3213 lemma arcsin_lbound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> -(pi/2) \<le> arcsin y"
  3214   by (blast dest: arcsin)
  3215 
  3216 lemma arcsin_ubound: "-1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin y \<le> pi/2"
  3217   by (blast dest: arcsin)
  3218 
  3219 lemma arcsin_lt_bounded:
  3220      "[| -1 < y; y < 1 |] ==> -(pi/2) < arcsin y & arcsin y < pi/2"
  3221   apply (frule order_less_imp_le)
  3222   apply (frule_tac y = y in order_less_imp_le)
  3223   apply (frule arcsin_bounded)
  3224   apply (safe, simp)
  3225   apply (drule_tac y = "arcsin y" in order_le_imp_less_or_eq)
  3226   apply (drule_tac [2] y = "pi/2" in order_le_imp_less_or_eq, safe)
  3227   apply (drule_tac [!] f = sin in arg_cong, auto)
  3228   done
  3229 
  3230 lemma arcsin_sin: "[|-(pi/2) \<le> x; x \<le> pi/2 |] ==> arcsin(sin x) = x"
  3231   apply (unfold arcsin_def)
  3232   apply (rule the1_equality)
  3233   apply (rule sin_total, auto)
  3234   done
  3235 
  3236 lemma arccos:
  3237      "[| -1 \<le> y; y \<le> 1 |]
  3238       ==> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
  3239   unfolding arccos_def by (rule theI' [OF cos_total])
  3240 
  3241 lemma cos_arccos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arccos y) = y"
  3242   by (blast dest: arccos)
  3243 
  3244 lemma arccos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y & arccos y \<le> pi"
  3245   by (blast dest: arccos)
  3246 
  3247 lemma arccos_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y"
  3248   by (blast dest: arccos)
  3249 
  3250 lemma arccos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arccos y \<le> pi"
  3251   by (blast dest: arccos)
  3252 
  3253 lemma arccos_lt_bounded:
  3254      "[| -1 < y; y < 1 |]
  3255       ==> 0 < arccos y & arccos y < pi"
  3256   apply (frule order_less_imp_le)
  3257   apply (frule_tac y = y in order_less_imp_le)
  3258   apply (frule arccos_bounded, auto)
  3259   apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
  3260   apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
  3261   apply (drule_tac [!] f = cos in arg_cong, auto)
  3262   done
  3263 
  3264 lemma arccos_cos: "[|0 \<le> x; x \<le> pi |] ==> arccos(cos x) = x"
  3265   apply (simp add: arccos_def)
  3266   apply (auto intro!: the1_equality cos_total)
  3267   done
  3268 
  3269 lemma arccos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arccos(cos x) = -x"
  3270   apply (simp add: arccos_def)
  3271   apply (auto intro!: the1_equality cos_total)
  3272   done
  3273 
  3274 lemma cos_arcsin: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> cos (arcsin x) = sqrt (1 - x\<^sup>2)"
  3275   apply (subgoal_tac "x\<^sup>2 \<le> 1")
  3276   apply (rule power2_eq_imp_eq)
  3277   apply (simp add: cos_squared_eq)
  3278   apply (rule cos_ge_zero)
  3279   apply (erule (1) arcsin_lbound)
  3280   apply (erule (1) arcsin_ubound)
  3281   apply simp
  3282   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
  3283   apply (rule power_mono, simp, simp)
  3284   done
  3285 
  3286 lemma sin_arccos: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> sin (arccos x) = sqrt (1 - x\<^sup>2)"
  3287   apply (subgoal_tac "x\<^sup>2 \<le> 1")
  3288   apply (rule power2_eq_imp_eq)
  3289   apply (simp add: sin_squared_eq)
  3290   apply (rule sin_ge_zero)
  3291   apply (erule (1) arccos_lbound)
  3292   apply (erule (1) arccos_ubound)
  3293   apply simp
  3294   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
  3295   apply (rule power_mono, simp, simp)
  3296   done
  3297 
  3298 lemma arctan [simp]: "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
  3299   unfolding arctan_def by (rule theI' [OF tan_total])
  3300 
  3301 lemma tan_arctan: "tan (arctan y) = y"
  3302   by auto
  3303 
  3304 lemma arctan_bounded: "- (pi/2) < arctan y  & arctan y < pi/2"
  3305   by (auto simp only: arctan)
  3306 
  3307 lemma arctan_lbound: "- (pi/2) < arctan y"
  3308   by auto
  3309 
  3310 lemma arctan_ubound: "arctan y < pi/2"
  3311   by (auto simp only: arctan)
  3312 
  3313 lemma arctan_unique:
  3314   assumes "-(pi/2) < x"
  3315     and "x < pi/2"
  3316     and "tan x = y"
  3317   shows "arctan y = x"
  3318   using assms arctan [of y] tan_total [of y] by (fast elim: ex1E)
  3319 
  3320 lemma arctan_tan: "-(pi/2) < x \<Longrightarrow> x < pi/2 \<Longrightarrow> arctan (tan x) = x"
  3321   by (rule arctan_unique) simp_all
  3322 
  3323 lemma arctan_zero_zero [simp]: "arctan 0 = 0"
  3324   by (rule arctan_unique) simp_all
  3325 
  3326 lemma arctan_minus: "arctan (- x) = - arctan x"
  3327   apply (rule arctan_unique)
  3328   apply (simp only: neg_less_iff_less arctan_ubound)
  3329   apply (metis minus_less_iff arctan_lbound)
  3330   apply simp
  3331   done
  3332 
  3333 lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
  3334   by (intro less_imp_neq [symmetric] cos_gt_zero_pi
  3335     arctan_lbound arctan_ubound)
  3336 
  3337 lemma cos_arctan: "cos (arctan x) = 1 / sqrt (1 + x\<^sup>2)"
  3338 proof (rule power2_eq_imp_eq)
  3339   have "0 < 1 + x\<^sup>2" by (simp add: add_pos_nonneg)
  3340   show "0 \<le> 1 / sqrt (1 + x\<^sup>2)" by simp
  3341   show "0 \<le> cos (arctan x)"
  3342     by (intro less_imp_le cos_gt_zero_pi arctan_lbound arctan_ubound)
  3343   have "(cos (arctan x))\<^sup>2 * (1 + (tan (arctan x))\<^sup>2) = 1"
  3344     unfolding tan_def by (simp add: distrib_left power_divide)
  3345   thus "(cos (arctan x))\<^sup>2 = (1 / sqrt (1 + x\<^sup>2))\<^sup>2"
  3346     using `0 < 1 + x\<^sup>2` by (simp add: power_divide eq_divide_eq)
  3347 qed
  3348 
  3349 lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<^sup>2)"
  3350   using add_pos_nonneg [OF zero_less_one zero_le_power2 [of x]]
  3351   using tan_arctan [of x] unfolding tan_def cos_arctan
  3352   by (simp add: eq_divide_eq)
  3353 
  3354 lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
  3355   apply (rule power_inverse [THEN subst])
  3356   apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
  3357   apply (auto dest: field_power_not_zero
  3358           simp add: power_mult_distrib distrib_right power_divide tan_def
  3359                     mult.assoc power_inverse [symmetric])
  3360   done
  3361 
  3362 lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
  3363   by (metis tan_monotone' arctan_lbound arctan_ubound tan_arctan)
  3364 
  3365 lemma arctan_le_iff: "arctan x \<le> arctan y \<longleftrightarrow> x \<le> y"
  3366   by (simp only: not_less [symmetric] arctan_less_iff)
  3367 
  3368 lemma arctan_eq_iff: "arctan x = arctan y \<longleftrightarrow> x = y"
  3369   by (simp only: eq_iff [where 'a=real] arctan_le_iff)
  3370 
  3371 lemma zero_less_arctan_iff [simp]: "0 < arctan x \<longleftrightarrow> 0 < x"
  3372   using arctan_less_iff [of 0 x] by simp
  3373 
  3374 lemma arctan_less_zero_iff [simp]: "arctan x < 0 \<longleftrightarrow> x < 0"
  3375   using arctan_less_iff [of x 0] by simp
  3376 
  3377 lemma zero_le_arctan_iff [simp]: "0 \<le> arctan x \<longleftrightarrow> 0 \<le> x"
  3378   using arctan_le_iff [of 0 x] by simp
  3379 
  3380 lemma arctan_le_zero_iff [simp]: "arctan x \<le> 0 \<longleftrightarrow> x \<le> 0"
  3381   using arctan_le_iff [of x 0] by simp
  3382 
  3383 lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
  3384   using arctan_eq_iff [of x 0] by simp
  3385 
  3386 lemma continuous_on_arcsin': "continuous_on {-1 .. 1} arcsin"
  3387 proof -
  3388   have "continuous_on (sin ` {- pi / 2 .. pi / 2}) arcsin"
  3389     by (rule continuous_on_inv) (auto intro: continuous_intros simp: arcsin_sin)
  3390   also have "sin ` {- pi / 2 .. pi / 2} = {-1 .. 1}"
  3391   proof safe
  3392     fix x :: real
  3393     assume "x \<in> {-1..1}"
  3394     then show "x \<in> sin ` {- pi / 2..pi / 2}"
  3395       using arcsin_lbound arcsin_ubound
  3396       by (intro image_eqI[where x="arcsin x"]) auto
  3397   qed simp
  3398   finally show ?thesis .
  3399 qed
  3400 
  3401 lemma continuous_on_arcsin [continuous_intros]:
  3402   "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))"
  3403   using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arcsin']]
  3404   by (auto simp: comp_def subset_eq)
  3405 
  3406 lemma isCont_arcsin: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> isCont arcsin x"
  3407   using continuous_on_arcsin'[THEN continuous_on_subset, of "{ -1 <..< 1 }"]
  3408   by (auto simp: continuous_on_eq_continuous_at subset_eq)
  3409 
  3410 lemma continuous_on_arccos': "continuous_on {-1 .. 1} arccos"
  3411 proof -
  3412   have "continuous_on (cos ` {0 .. pi}) arccos"
  3413     by (rule continuous_on_inv) (auto intro: continuous_intros simp: arccos_cos)
  3414   also have "cos ` {0 .. pi} = {-1 .. 1}"
  3415   proof safe
  3416     fix x :: real
  3417     assume "x \<in> {-1..1}"
  3418     then show "x \<in> cos ` {0..pi}"
  3419       using arccos_lbound arccos_ubound
  3420       by (intro image_eqI[where x="arccos x"]) auto
  3421   qed simp
  3422   finally show ?thesis .
  3423 qed
  3424 
  3425 lemma continuous_on_arccos [continuous_intros]:
  3426   "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))"
  3427   using continuous_on_compose[of s f, OF _ continuous_on_subset[OF  continuous_on_arccos']]
  3428   by (auto simp: comp_def subset_eq)
  3429 
  3430 lemma isCont_arccos: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> isCont arccos x"
  3431   using continuous_on_arccos'[THEN continuous_on_subset, of "{ -1 <..< 1 }"]
  3432   by (auto simp: continuous_on_eq_continuous_at subset_eq)
  3433 
  3434 lemma isCont_arctan: "isCont arctan x"
  3435   apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify)
  3436   apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
  3437   apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
  3438   apply (erule (1) isCont_inverse_function2 [where f=tan])
  3439   apply (metis arctan_tan order_le_less_trans order_less_le_trans)
  3440   apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
  3441   done
  3442 
  3443 lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
  3444   by (rule isCont_tendsto_compose [OF isCont_arctan])
  3445 
  3446 lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
  3447   unfolding continuous_def by (rule tendsto_arctan)
  3448 
  3449 lemma continuous_on_arctan [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
  3450   unfolding continuous_on_def by (auto intro: tendsto_arctan)
  3451 
  3452 lemma DERIV_arcsin:
  3453   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<^sup>2))"
  3454   apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
  3455   apply (rule DERIV_cong [OF DERIV_sin])
  3456   apply (simp add: cos_arcsin)
  3457   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  3458   apply (rule power_strict_mono, simp, simp, simp)
  3459   apply assumption
  3460   apply assumption
  3461   apply simp
  3462   apply (erule (1) isCont_arcsin)
  3463   done
  3464 
  3465 lemma DERIV_arccos:
  3466   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<^sup>2))"
  3467   apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
  3468   apply (rule DERIV_cong [OF DERIV_cos])
  3469   apply (simp add: sin_arccos)
  3470   apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  3471   apply (rule power_strict_mono, simp, simp, simp)
  3472   apply assumption
  3473   apply assumption
  3474   apply simp
  3475   apply (erule (1) isCont_arccos)
  3476   done
  3477 
  3478 lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)"
  3479   apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
  3480   apply (rule DERIV_cong [OF DERIV_tan])
  3481   apply (rule cos_arctan_not_zero)
  3482   apply (simp add: power_inverse tan_sec [symmetric])
  3483   apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
  3484   apply (simp add: add_pos_nonneg)
  3485   apply (simp, simp, simp, rule isCont_arctan)
  3486   done
  3487 
  3488 declare
  3489   DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
  3490   DERIV_arccos[THEN DERIV_chain2, derivative_intros]
  3491   DERIV_arctan[THEN DERIV_chain2, derivative_intros]
  3492 
  3493 lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
  3494   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])
  3495      (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
  3496            intro!: tan_monotone exI[of _ "pi/2"])
  3497 
  3498 lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
  3499   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])
  3500      (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
  3501            intro!: tan_monotone exI[of _ "pi/2"])
  3502 
  3503 lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"
  3504 proof (rule tendstoI)
  3505   fix e :: real
  3506   assume "0 < e"
  3507   def y \<equiv> "pi/2 - min (pi/2) e"
  3508   then have y: "0 \<le> y" "y < pi/2" "pi/2 \<le> e + y"
  3509     using `0 < e` by auto
  3510 
  3511   show "eventually (\<lambda>x. dist (arctan x) (pi / 2) < e) at_top"
  3512   proof (intro eventually_at_top_dense[THEN iffD2] exI allI impI)
  3513     fix x
  3514     assume "tan y < x"
  3515     then have "arctan (tan y) < arctan x"
  3516       by (simp add: arctan_less_iff)
  3517     with y have "y < arctan x"
  3518       by (subst (asm) arctan_tan) simp_all
  3519     with arctan_ubound[of x, arith] y `0 < e`
  3520     show "dist (arctan x) (pi / 2) < e"
  3521       by (simp add: dist_real_def)
  3522   qed
  3523 qed
  3524 
  3525 lemma tendsto_arctan_at_bot: "(arctan ---> - (pi/2)) at_bot"
  3526   unfolding filterlim_at_bot_mirror arctan_minus
  3527   by (intro tendsto_minus tendsto_arctan_at_top)
  3528 
  3529 
  3530 subsection {* More Theorems about Sin and Cos *}
  3531 
  3532 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
  3533 proof -
  3534   let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
  3535   have nonneg: "0 \<le> ?c"
  3536     by (simp add: cos_ge_zero)
  3537   have "0 = cos (pi / 4 + pi / 4)"
  3538     by simp
  3539   also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
  3540     by (simp only: cos_add power2_eq_square)
  3541   also have "\<dots> = 2 * ?c\<^sup>2 - 1"
  3542     by (simp add: sin_squared_eq)
  3543   finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
  3544     by (simp add: power_divide)
  3545   thus ?thesis
  3546     using nonneg by (rule power2_eq_imp_eq) simp
  3547 qed
  3548 
  3549 lemma cos_30: "cos (pi / 6) = sqrt 3 / 2"
  3550 proof -
  3551   let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
  3552   have pos_c: "0 < ?c"
  3553     by (rule cos_gt_zero, simp, simp)
  3554   have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
  3555     by simp
  3556   also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
  3557     by (simp only: cos_add sin_add)
  3558   also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
  3559     by (simp add: algebra_simps power2_eq_square)
  3560   finally have "?c\<^sup>2 = (sqrt 3 / 2)\<^sup>2"
  3561     using pos_c by (simp add: sin_squared_eq power_divide)
  3562   thus ?thesis
  3563     using pos_c [THEN order_less_imp_le]
  3564     by (rule power2_eq_imp_eq) simp
  3565 qed
  3566 
  3567 lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
  3568   by (simp add: sin_cos_eq cos_45)
  3569 
  3570 lemma sin_60: "sin (pi / 3) = sqrt 3 / 2"
  3571   by (simp add: sin_cos_eq cos_30)
  3572 
  3573 lemma cos_60: "cos (pi / 3) = 1 / 2"
  3574   apply (rule power2_eq_imp_eq)
  3575   apply (simp add: cos_squared_eq sin_60 power_divide)
  3576   apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
  3577   done
  3578 
  3579 lemma sin_30: "sin (pi / 6) = 1 / 2"
  3580   by (simp add: sin_cos_eq cos_60)
  3581 
  3582 lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
  3583   unfolding tan_def by (simp add: sin_30 cos_30)
  3584 
  3585 lemma tan_45: "tan (pi / 4) = 1"
  3586   unfolding tan_def by (simp add: sin_45 cos_45)
  3587 
  3588 lemma tan_60: "tan (pi / 3) = sqrt 3"
  3589   unfolding tan_def by (simp add: sin_60 cos_60)
  3590 
  3591 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
  3592 proof -
  3593   have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
  3594     by (auto simp add: algebra_simps sin_add)
  3595   thus ?thesis
  3596     by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
  3597                   mult.commute [of pi])
  3598 qed
  3599 
  3600 lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
  3601   by (cases "even n") (simp_all add: cos_double mult.assoc)
  3602 
  3603 lemma cos_3over2_pi [simp]: "cos (3 / 2 * pi) = 0"
  3604   apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
  3605   apply (subst cos_add, simp)
  3606   done
  3607 
  3608 lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
  3609   by (auto simp add: mult.assoc)
  3610 
  3611 lemma sin_3over2_pi [simp]: "sin (3 / 2 * pi) = - 1"
  3612   apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
  3613   apply (subst sin_add, simp)
  3614   done
  3615 
  3616 lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
  3617   apply (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib)
  3618   apply auto
  3619   done
  3620 
  3621 lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
  3622   by (auto intro!: derivative_eq_intros)
  3623 
  3624 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
  3625   by (auto simp add: sin_zero_iff elim: evenE)
  3626 
  3627 lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0"
  3628   using sin_cos_squared_add3 [where x = x] by auto
  3629 
  3630 
  3631 subsection {* Machins formula *}
  3632 
  3633 lemma arctan_one: "arctan 1 = pi / 4"
  3634   by (rule arctan_unique, simp_all add: tan_45 m2pi_less_pi)
  3635 
  3636 lemma tan_total_pi4:
  3637   assumes "\<bar>x\<bar> < 1"
  3638   shows "\<exists>z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x"
  3639 proof
  3640   show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x"
  3641     unfolding arctan_one [symmetric] arctan_minus [symmetric]
  3642     unfolding arctan_less_iff using assms by auto
  3643 qed
  3644 
  3645 lemma arctan_add:
  3646   assumes "\<bar>x\<bar> \<le> 1" and "\<bar>y\<bar> < 1"
  3647   shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))"
  3648 proof (rule arctan_unique [symmetric])
  3649   have "- (pi / 4) \<le> arctan x" and "- (pi / 4) < arctan y"
  3650     unfolding arctan_one [symmetric] arctan_minus [symmetric]
  3651     unfolding arctan_le_iff arctan_less_iff using assms by auto
  3652   from add_le_less_mono [OF this]
  3653   show 1: "- (pi / 2) < arctan x + arctan y" by simp
  3654   have "arctan x \<le> pi / 4" and "arctan y < pi / 4"
  3655     unfolding arctan_one [symmetric]
  3656     unfolding arctan_le_iff arctan_less_iff using assms by auto
  3657   from add_le_less_mono [OF this]
  3658   show 2: "arctan x + arctan y < pi / 2" by simp
  3659   show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
  3660     using cos_gt_zero_pi [OF 1 2] by (simp add: tan_add)
  3661 qed
  3662 
  3663 theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)"
  3664 proof -
  3665   have "\<bar>1 / 5\<bar> < (1 :: real)" by auto
  3666   from arctan_add[OF less_imp_le[OF this] this]
  3667   have "2 * arctan (1 / 5) = arctan (5 / 12)" by auto
  3668   moreover
  3669   have "\<bar>5 / 12\<bar> < (1 :: real)" by auto
  3670   from arctan_add[OF less_imp_le[OF this] this]
  3671   have "2 * arctan (5 / 12) = arctan (120 / 119)" by auto
  3672   moreover
  3673   have "\<bar>1\<bar> \<le> (1::real)" and "\<bar>1 / 239\<bar> < (1::real)" by auto
  3674   from arctan_add[OF this]
  3675   have "arctan 1 + arctan (1 / 239) = arctan (120 / 119)" by auto
  3676   ultimately have "arctan 1 + arctan (1 / 239) = 4 * arctan (1 / 5)" by auto
  3677   thus ?thesis unfolding arctan_one by algebra
  3678 qed
  3679 
  3680 
  3681 subsection {* Introducing the arcus tangens power series *}
  3682 
  3683 lemma monoseq_arctan_series:
  3684   fixes x :: real
  3685   assumes "\<bar>x\<bar> \<le> 1"
  3686   shows "monoseq (\<lambda> n. 1 / real (n*2+1) * x^(n*2+1))" (is "monoseq ?a")
  3687 proof (cases "x = 0")
  3688   case True
  3689   thus ?thesis unfolding monoseq_def One_nat_def by auto
  3690 next
  3691   case False
  3692   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
  3693   show "monoseq ?a"
  3694   proof -
  3695     {
  3696       fix n
  3697       fix x :: real
  3698       assume "0 \<le> x" and "x \<le> 1"
  3699       have "1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<le>
  3700         1 / real (Suc (n * 2)) * x ^ Suc (n * 2)"
  3701       proof (rule mult_mono)
  3702         show "1 / real (Suc (Suc n * 2)) \<le> 1 / real (Suc (n * 2))"
  3703           by (rule frac_le) simp_all
  3704         show "0 \<le> 1 / real (Suc (n * 2))"
  3705           by auto
  3706         show "x ^ Suc (Suc n * 2) \<le> x ^ Suc (n * 2)"
  3707           by (rule power_decreasing) (simp_all add: `0 \<le> x` `x \<le> 1`)
  3708         show "0 \<le> x ^ Suc (Suc n * 2)"
  3709           by (rule zero_le_power) (simp add: `0 \<le> x`)
  3710       qed
  3711     } note mono = this
  3712 
  3713     show ?thesis
  3714     proof (cases "0 \<le> x")
  3715       case True from mono[OF this `x \<le> 1`, THEN allI]
  3716       show ?thesis unfolding Suc_eq_plus1[symmetric]
  3717         by (rule mono_SucI2)
  3718     next
  3719       case False
  3720       hence "0 \<le> -x" and "-x \<le> 1" using `-1 \<le> x` by auto
  3721       from mono[OF this]
  3722       have "\<And>n. 1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<ge>
  3723         1 / real (Suc (n * 2)) * x ^ Suc (n * 2)" using `0 \<le> -x` by auto
  3724       thus ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI1[OF allI])
  3725     qed
  3726   qed
  3727 qed
  3728 
  3729 lemma zeroseq_arctan_series:
  3730   fixes x :: real
  3731   assumes "\<bar>x\<bar> \<le> 1"
  3732   shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
  3733 proof (cases "x = 0")
  3734   case True
  3735   thus ?thesis
  3736     unfolding One_nat_def by auto
  3737 next
  3738   case False
  3739   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
  3740   show "?a ----> 0"
  3741   proof (cases "\<bar>x\<bar> < 1")
  3742     case True
  3743     hence "norm x < 1" by auto
  3744     from tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
  3745     have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
  3746       unfolding inverse_eq_divide Suc_eq_plus1 by simp
  3747     then show ?thesis using pos2 by (rule LIMSEQ_linear)
  3748   next
  3749     case False
  3750     hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
  3751     hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x"
  3752       unfolding One_nat_def by auto
  3753     from tendsto_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] tendsto_const[of x]]
  3754     show ?thesis unfolding n_eq Suc_eq_plus1 by auto
  3755   qed
  3756 qed
  3757 
  3758 lemma summable_arctan_series:
  3759   fixes x :: real and n :: nat
  3760   assumes "\<bar>x\<bar> \<le> 1"
  3761   shows "summable (\<lambda> k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
  3762   (is "summable (?c x)")
  3763   by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms])
  3764 
  3765 lemma less_one_imp_sqr_less_one:
  3766   fixes x :: real
  3767   assumes "\<bar>x\<bar> < 1"
  3768   shows "x\<^sup>2 < 1"
  3769 proof -
  3770   have "\<bar>x\<^sup>2\<bar> < 1"
  3771     by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff) 
  3772   thus ?thesis using zero_le_power2 by auto
  3773 qed
  3774 
  3775 lemma DERIV_arctan_series:
  3776   assumes "\<bar> x \<bar> < 1"
  3777   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))"
  3778   (is "DERIV ?arctan _ :> ?Int")
  3779 proof -
  3780   let ?f = "\<lambda>n. if even n then (-1)^(n div 2) * 1 / real (Suc n) else 0"
  3781 
  3782   have n_even: "\<And>n :: nat. even n \<Longrightarrow> 2 * (n div 2) = n"
  3783     by presburger
  3784   then have if_eq: "\<And>n x'. ?f n * real (Suc n) * x'^n =
  3785     (if even n then (-1)^(n div 2) * x'^(2 * (n div 2)) else 0)"
  3786     by auto
  3787 
  3788   {
  3789     fix x :: real
  3790     assume "\<bar>x\<bar> < 1"
  3791     hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
  3792     have "summable (\<lambda> n. (- 1) ^ n * (x\<^sup>2) ^n)"
  3793       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`])
  3794     hence "summable (\<lambda> n. (- 1) ^ n * x^(2*n))" unfolding power_mult .
  3795   } note summable_Integral = this
  3796 
  3797   {
  3798     fix f :: "nat \<Rightarrow> real"
  3799     have "\<And>x. f sums x = (\<lambda> n. if even n then f (n div 2) else 0) sums x"
  3800     proof
  3801       fix x :: real
  3802       assume "f sums x"
  3803       from sums_if[OF sums_zero this]
  3804       show "(\<lambda>n. if even n then f (n div 2) else 0) sums x"
  3805         by auto
  3806     next
  3807       fix x :: real
  3808       assume "(\<lambda> n. if even n then f (n div 2) else 0) sums x"
  3809       from LIMSEQ_linear[OF this[unfolded sums_def] pos2, unfolded sum_split_even_odd[unfolded mult.commute]]
  3810       show "f sums x" unfolding sums_def by auto
  3811     qed
  3812     hence "op sums f = op sums (\<lambda> n. if even n then f (n div 2) else 0)" ..
  3813   } note sums_even = this
  3814 
  3815   have Int_eq: "(\<Sum>n. ?f n * real (Suc n) * x^n) = ?Int"
  3816     unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * x ^ (2 * n)", symmetric]
  3817     by auto
  3818 
  3819   {
  3820     fix x :: real
  3821     have if_eq': "\<And>n. (if even n then (- 1) ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
  3822       (if even n then (- 1) ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
  3823       using n_even by auto
  3824     have idx_eq: "\<And>n. n * 2 + 1 = Suc (2 * n)" by auto
  3825     have "(\<Sum>n. ?f n * x^(Suc n)) = ?arctan x"
  3826       unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
  3827       by auto
  3828   } note arctan_eq = this
  3829 
  3830   have "DERIV (\<lambda> x. \<Sum> n. ?f n * x^(Suc n)) x :> (\<Sum> n. ?f n * real (Suc n) * x^n)"
  3831   proof (rule DERIV_power_series')
  3832     show "x \<in> {- 1 <..< 1}" using `\<bar> x \<bar> < 1` by auto
  3833     {
  3834       fix x' :: real
  3835       assume x'_bounds: "x' \<in> {- 1 <..< 1}"
  3836       then have "\<bar>x'\<bar> < 1" by auto
  3837       then
  3838         have *: "summable (\<lambda>n. (- 1) ^ n * x' ^ (2 * n))"
  3839         by (rule summable_Integral)
  3840       let ?S = "\<Sum> n. (-1)^n * x'^(2 * n)"
  3841       show "summable (\<lambda> n. ?f n * real (Suc n) * x'^n)" unfolding if_eq
  3842         apply (rule sums_summable [where l="0 + ?S"])
  3843         apply (rule sums_if)
  3844         apply (rule sums_zero)
  3845         apply (rule summable_sums)
  3846         apply (rule *)
  3847         done
  3848     }
  3849   qed auto
  3850   thus ?thesis unfolding Int_eq arctan_eq .
  3851 qed
  3852 
  3853 lemma arctan_series:
  3854   assumes "\<bar> x \<bar> \<le> 1"
  3855   shows "arctan x = (\<Sum>k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))"
  3856   (is "_ = suminf (\<lambda> n. ?c x n)")
  3857 proof -
  3858   let ?c' = "\<lambda>x n. (-1)^n * x^(n*2)"
  3859 
  3860   {
  3861     fix r x :: real
  3862     assume "0 < r" and "r < 1" and "\<bar> x \<bar> < r"
  3863     have "\<bar>x\<bar> < 1" using `r < 1` and `\<bar>x\<bar> < r` by auto
  3864     from DERIV_arctan_series[OF this] have "DERIV (\<lambda> x. suminf (?c x)) x :> (suminf (?c' x))" .
  3865   } note DERIV_arctan_suminf = this
  3866 
  3867   {
  3868     fix x :: real
  3869     assume "\<bar>x\<bar> \<le> 1"
  3870     note summable_Leibniz[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]]
  3871   } note arctan_series_borders = this
  3872 
  3873   {
  3874     fix x :: real
  3875     assume "\<bar>x\<bar> < 1"
  3876     have "arctan x = (\<Sum>k. ?c x k)"
  3877     proof -
  3878       obtain r where "\<bar>x\<bar> < r" and "r < 1"
  3879         using dense[OF `\<bar>x\<bar> < 1`] by blast
  3880       hence "0 < r" and "-r < x" and "x < r" by auto
  3881 
  3882       have suminf_eq_arctan_bounded: "\<And>x a b. \<lbrakk> -r < a ; b < r ; a < b ; a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow>
  3883         suminf (?c x) - arctan x = suminf (?c a) - arctan a"
  3884       proof -
  3885         fix x a b
  3886         assume "-r < a" and "b < r" and "a < b" and "a \<le> x" and "x \<le> b"
  3887         hence "\<bar>x\<bar> < r" by auto
  3888         show "suminf (?c x) - arctan x = suminf (?c a) - arctan a"
  3889         proof (rule DERIV_isconst2[of "a" "b"])
  3890           show "a < b" and "a \<le> x" and "x \<le> b"
  3891             using `a < b` `a \<le> x` `x \<le> b` by auto
  3892           have "\<forall>x. -r < x \<and> x < r \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
  3893           proof (rule allI, rule impI)
  3894             fix x
  3895             assume "-r < x \<and> x < r"
  3896             hence "\<bar>x\<bar> < r" by auto
  3897             hence "\<bar>x\<bar> < 1" using `r < 1` by auto
  3898             have "\<bar> - (x\<^sup>2) \<bar> < 1"
  3899               using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
  3900             hence "(\<lambda> n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))"
  3901               unfolding real_norm_def[symmetric] by (rule geometric_sums)
  3902             hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))"
  3903               unfolding power_mult_distrib[symmetric] power_mult mult.commute[of _ 2] by auto
  3904             hence suminf_c'_eq_geom: "inverse (1 + x\<^sup>2) = suminf (?c' x)"
  3905               using sums_unique unfolding inverse_eq_divide by auto
  3906             have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))"
  3907               unfolding suminf_c'_eq_geom
  3908               by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
  3909             from DERIV_diff [OF this DERIV_arctan]
  3910             show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
  3911               by auto
  3912           qed
  3913           hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
  3914             using `-r < a` `b < r` by auto
  3915           thus "\<forall> y. a < y \<and> y < b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
  3916             using `\<bar>x\<bar> < r` by auto
  3917           show "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> isCont (\<lambda> x. suminf (?c x) - arctan x) y"
  3918             using DERIV_in_rball DERIV_isCont by auto
  3919         qed
  3920       qed
  3921 
  3922       have suminf_arctan_zero: "suminf (?c 0) - arctan 0 = 0"
  3923         unfolding Suc_eq_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero
  3924         by auto
  3925 
  3926       have "suminf (?c x) - arctan x = 0"
  3927       proof (cases "x = 0")
  3928         case True
  3929         thus ?thesis using suminf_arctan_zero by auto
  3930       next
  3931         case False
  3932         hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
  3933         have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
  3934           by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
  3935             (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  3936         moreover
  3937         have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
  3938           by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
  3939              (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  3940         ultimately
  3941         show ?thesis using suminf_arctan_zero by auto
  3942       qed
  3943       thus ?thesis by auto
  3944     qed
  3945   } note when_less_one = this
  3946 
  3947   show "arctan x = suminf (\<lambda> n. ?c x n)"
  3948   proof (cases "\<bar>x\<bar> < 1")
  3949     case True
  3950     thus ?thesis by (rule when_less_one)
  3951   next
  3952     case False
  3953     hence "\<bar>x\<bar> = 1" using `\<bar>x\<bar> \<le> 1` by auto
  3954     let ?a = "\<lambda>x n. \<bar>1 / real (n*2+1) * x^(n*2+1)\<bar>"
  3955     let ?diff = "\<lambda> x n. \<bar> arctan x - (\<Sum> i<n. ?c x i)\<bar>"
  3956     {
  3957       fix n :: nat
  3958       have "0 < (1 :: real)" by auto
  3959       moreover
  3960       {
  3961         fix x :: real
  3962         assume "0 < x" and "x < 1"
  3963         hence "\<bar>x\<bar> \<le> 1" and "\<bar>x\<bar> < 1" by auto
  3964         from `0 < x` have "0 < 1 / real (0 * 2 + (1::nat)) * x ^ (0 * 2 + 1)"
  3965           by auto
  3966         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]
  3967         have "0 < 1 / real (n*2+1) * x^(n*2+1)"
  3968           by (rule mult_pos_pos, auto simp only: zero_less_power[OF `0 < x`], auto)
  3969         hence a_pos: "?a x n = 1 / real (n*2+1) * x^(n*2+1)"
  3970           by (rule abs_of_pos)
  3971         have "?diff x n \<le> ?a x n"
  3972         proof (cases "even n")
  3973           case True
  3974           hence sgn_pos: "(-1)^n = (1::real)" by auto
  3975           from `even n` obtain m where "n = 2 * m" ..
  3976           then have "2 * m = n" ..
  3977           from bounds[of m, unfolded this atLeastAtMost_iff]
  3978           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))"
  3979             by auto
  3980           also have "\<dots> = ?c x n" unfolding One_nat_def by auto
  3981           also have "\<dots> = ?a x n" unfolding sgn_pos a_pos by auto
  3982           finally show ?thesis .
  3983         next
  3984           case False
  3985           hence sgn_neg: "(-1)^n = (-1::real)" by auto
  3986           from `odd n` obtain m where "n = 2 * m + 1" ..
  3987           then have m_def: "2 * m + 1 = n" ..
  3988           hence m_plus: "2 * (m + 1) = n + 1" by auto
  3989           from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
  3990           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))"
  3991             by auto
  3992           also have "\<dots> = - ?c x n" unfolding One_nat_def by auto
  3993           also have "\<dots> = ?a x n" unfolding sgn_neg a_pos by auto
  3994           finally show ?thesis .
  3995         qed
  3996         hence "0 \<le> ?a x n - ?diff x n" by auto
  3997       }
  3998       hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
  3999       moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
  4000         unfolding diff_conv_add_uminus divide_inverse
  4001         by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan
  4002           isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum
  4003           simp del: add_uminus_conv_diff)
  4004       ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
  4005         by (rule LIM_less_bound)
  4006       hence "?diff 1 n \<le> ?a 1 n" by auto
  4007     }
  4008     have "?a 1 ----> 0"
  4009       unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
  4010       by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
  4011     have "?diff 1 ----> 0"
  4012     proof (rule LIMSEQ_I)
  4013       fix r :: real
  4014       assume "0 < r"
  4015       obtain N :: nat where N_I: "\<And>n. N \<le> n \<Longrightarrow> ?a 1 n < r"
  4016         using LIMSEQ_D[OF `?a 1 ----> 0` `0 < r`] by auto
  4017       {
  4018         fix n
  4019         assume "N \<le> n" from `?diff 1 n \<le> ?a 1 n` N_I[OF this]
  4020         have "norm (?diff 1 n - 0) < r" by auto
  4021       }
  4022       thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
  4023     qed
  4024     from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
  4025     have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
  4026     hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
  4027 
  4028     show ?thesis
  4029     proof (cases "x = 1")
  4030       case True
  4031       then show ?thesis by (simp add: `arctan 1 = (\<Sum> i. ?c 1 i)`)
  4032     next
  4033       case False
  4034       hence "x = -1" using `\<bar>x\<bar> = 1` by auto
  4035 
  4036       have "- (pi / 2) < 0" using pi_gt_zero by auto
  4037       have "- (2 * pi) < 0" using pi_gt_zero by auto
  4038 
  4039       have c_minus_minus: "\<And>i. ?c (- 1) i = - ?c 1 i"
  4040         unfolding One_nat_def by auto
  4041 
  4042       have "arctan (- 1) = arctan (tan (-(pi / 4)))"
  4043         unfolding tan_45 tan_minus ..
  4044       also have "\<dots> = - (pi / 4)"
  4045         by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
  4046       also have "\<dots> = - (arctan (tan (pi / 4)))"
  4047         unfolding neg_equal_iff_equal by (rule arctan_tan[symmetric], auto simp add: order_less_trans[OF `- (2 * pi) < 0` pi_gt_zero])
  4048       also have "\<dots> = - (arctan 1)"
  4049         unfolding tan_45 ..
  4050       also have "\<dots> = - (\<Sum> i. ?c 1 i)"
  4051         using `arctan 1 = (\<Sum> i. ?c 1 i)` by auto
  4052       also have "\<dots> = (\<Sum> i. ?c (- 1) i)"
  4053         using suminf_minus[OF sums_summable[OF `(?c 1) sums (arctan 1)`]]
  4054         unfolding c_minus_minus by auto
  4055       finally show ?thesis using `x = -1` by auto
  4056     qed
  4057   qed
  4058 qed
  4059 
  4060 lemma arctan_half:
  4061   fixes x :: real
  4062   shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x\<^sup>2)))"
  4063 proof -
  4064   obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x"
  4065     using tan_total by blast
  4066   hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2"
  4067     by auto
  4068 
  4069   have "0 < cos y" using cos_gt_zero_pi[OF low high] .
  4070   hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y"
  4071     by auto
  4072 
  4073   have "1 + (tan y)\<^sup>2 = 1 + (sin y)\<^sup>2 / (cos y)\<^sup>2"
  4074     unfolding tan_def power_divide ..
  4075   also have "\<dots> = (cos y)\<^sup>2 / (cos y)\<^sup>2 + (sin y)\<^sup>2 / (cos y)\<^sup>2"
  4076     using `cos y \<noteq> 0` by auto
  4077   also have "\<dots> = 1 / (cos y)\<^sup>2"
  4078     unfolding add_divide_distrib[symmetric] sin_cos_squared_add2 ..
  4079   finally have "1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2" .
  4080 
  4081   have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)"
  4082     unfolding tan_def using `cos y \<noteq> 0` by (simp add: field_simps)
  4083   also have "\<dots> = tan y / (1 + 1 / cos y)"
  4084     using `cos y \<noteq> 0` unfolding add_divide_distrib by auto
  4085   also have "\<dots> = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))"
  4086     unfolding cos_sqrt ..
  4087   also have "\<dots> = tan y / (1 + sqrt (1 / (cos y)\<^sup>2))"
  4088     unfolding real_sqrt_divide by auto
  4089   finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)\<^sup>2))"
  4090     unfolding `1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2` .
  4091 
  4092   have "arctan x = y"
  4093     using arctan_tan low high y_eq by auto
  4094   also have "\<dots> = 2 * (arctan (tan (y/2)))"
  4095     using arctan_tan[OF low2 high2] by auto
  4096   also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))"
  4097     unfolding tan_half by auto
  4098   finally show ?thesis
  4099     unfolding eq `tan y = x` .
  4100 qed
  4101 
  4102 lemma arctan_monotone: "x < y \<Longrightarrow> arctan x < arctan y"
  4103   by (simp only: arctan_less_iff)
  4104 
  4105 lemma arctan_monotone': "x \<le> y \<Longrightarrow> arctan x \<le> arctan y"
  4106   by (simp only: arctan_le_iff)
  4107 
  4108 lemma arctan_inverse:
  4109   assumes "x \<noteq> 0"
  4110   shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
  4111 proof (rule arctan_unique)
  4112   show "- (pi / 2) < sgn x * pi / 2 - arctan x"
  4113     using arctan_bounded [of x] assms
  4114     unfolding sgn_real_def
  4115     apply (auto simp add: algebra_simps)
  4116     apply (drule zero_less_arctan_iff [THEN iffD2])
  4117     apply arith
  4118     done
  4119   show "sgn x * pi / 2 - arctan x < pi / 2"
  4120     using arctan_bounded [of "- x"] assms
  4121     unfolding sgn_real_def arctan_minus
  4122     by (auto simp add: algebra_simps)
  4123   show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
  4124     unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
  4125     unfolding sgn_real_def
  4126     by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
  4127 qed
  4128 
  4129 theorem pi_series: "pi / 4 = (\<Sum> k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM")
  4130 proof -
  4131   have "pi / 4 = arctan 1" using arctan_one by auto
  4132   also have "\<dots> = ?SUM" using arctan_series[of 1] by auto
  4133   finally show ?thesis by auto
  4134 qed
  4135 
  4136 
  4137 subsection {* Existence of Polar Coordinates *}
  4138 
  4139 lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<^sup>2 + y\<^sup>2)\<bar> \<le> 1"
  4140   apply (rule power2_le_imp_le [OF _ zero_le_one])
  4141   apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
  4142   done
  4143 
  4144 lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
  4145   by (simp add: abs_le_iff)
  4146 
  4147 lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arccos y) = sqrt (1 - y\<^sup>2)"
  4148   by (simp add: sin_arccos abs_le_iff)
  4149 
  4150 lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]
  4151 
  4152 lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
  4153 
  4154 lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a"
  4155 proof -
  4156   have polar_ex1: "\<And>y. 0 < y \<Longrightarrow> \<exists>r a. x = r * cos a & y = r * sin a"
  4157     apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)
  4158     apply (rule_tac x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))" in exI)
  4159     apply (simp add: cos_arccos_lemma1 sin_arccos_lemma1 power_divide
  4160                      real_sqrt_mult [symmetric] right_diff_distrib)
  4161     done
  4162   show ?thesis
  4163   proof (cases "0::real" y rule: linorder_cases)
  4164     case less 
  4165       then show ?thesis by (rule polar_ex1)
  4166   next
  4167     case equal
  4168       then show ?thesis
  4169         by (force simp add: intro!: cos_zero sin_zero)
  4170   next
  4171     case greater
  4172       then show ?thesis 
  4173      using polar_ex1 [where y="-y"]
  4174     by auto (metis cos_minus minus_minus minus_mult_right sin_minus)
  4175   qed
  4176 qed
  4177 
  4178 end