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