src/HOL/Transcendental.thy
 changeset 59730 b7c394c7a619 parent 59669 de7792ea4090 child 59731 7fccaeec22f0
```     1.1 --- a/src/HOL/Transcendental.thy	Tue Mar 10 16:12:35 2015 +0000
1.2 +++ b/src/HOL/Transcendental.thy	Mon Mar 16 15:30:00 2015 +0000
1.3 @@ -10,6 +10,12 @@
1.4  imports Binomial Series Deriv NthRoot
1.5  begin
1.6
1.7 +lemma of_real_fact [simp]: "of_real (fact n) = fact n"
1.8 +  by (metis of_nat_fact of_real_of_nat_eq)
1.9 +
1.10 +lemma real_fact_nat [simp]: "real (fact n :: nat) = fact n"
1.11 +  by (simp add: real_of_nat_def)
1.12 +
1.13  lemma root_test_convergence:
1.14    fixes f :: "nat \<Rightarrow> 'a::banach"
1.15    assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
1.16 @@ -54,13 +60,13 @@
1.17        (x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))"
1.18  proof (induct n)
1.19    case (Suc n)
1.20 -  have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x ^ n) - y * (y * y ^ n)"
1.21 +  have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x^n) - y * (y * y ^ n)"
1.22      by simp
1.23 -  also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x ^ n)"
1.24 +  also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)"
1.26 -  also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
1.27 +  also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
1.28      by (simp only: Suc)
1.29 -  also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
1.30 +  also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
1.31      by (simp only: mult.left_commute)
1.32    also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
1.33      by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
1.34 @@ -100,40 +106,40 @@
1.35
1.36  lemma powser_insidea:
1.37    fixes x z :: "'a::real_normed_div_algebra"
1.38 -  assumes 1: "summable (\<lambda>n. f n * x ^ n)"
1.39 +  assumes 1: "summable (\<lambda>n. f n * x^n)"
1.40      and 2: "norm z < norm x"
1.41    shows "summable (\<lambda>n. norm (f n * z ^ n))"
1.42  proof -
1.43    from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
1.44 -  from 1 have "(\<lambda>n. f n * x ^ n) ----> 0"
1.45 +  from 1 have "(\<lambda>n. f n * x^n) ----> 0"
1.46      by (rule summable_LIMSEQ_zero)
1.47 -  hence "convergent (\<lambda>n. f n * x ^ n)"
1.48 +  hence "convergent (\<lambda>n. f n * x^n)"
1.49      by (rule convergentI)
1.50 -  hence "Cauchy (\<lambda>n. f n * x ^ n)"
1.51 +  hence "Cauchy (\<lambda>n. f n * x^n)"
1.52      by (rule convergent_Cauchy)
1.53 -  hence "Bseq (\<lambda>n. f n * x ^ n)"
1.54 +  hence "Bseq (\<lambda>n. f n * x^n)"
1.55      by (rule Cauchy_Bseq)
1.56 -  then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K"
1.57 +  then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x^n) \<le> K"
1.58      by (simp add: Bseq_def, safe)
1.59    have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
1.60 -                   K * norm (z ^ n) * inverse (norm (x ^ n))"
1.61 +                   K * norm (z ^ n) * inverse (norm (x^n))"
1.62    proof (intro exI allI impI)
1.63      fix n::nat
1.64      assume "0 \<le> n"
1.65 -    have "norm (norm (f n * z ^ n)) * norm (x ^ n) =
1.66 -          norm (f n * x ^ n) * norm (z ^ n)"
1.67 +    have "norm (norm (f n * z ^ n)) * norm (x^n) =
1.68 +          norm (f n * x^n) * norm (z ^ n)"
1.69        by (simp add: norm_mult abs_mult)
1.70      also have "\<dots> \<le> K * norm (z ^ n)"
1.71        by (simp only: mult_right_mono 4 norm_ge_zero)
1.72 -    also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))"
1.73 +    also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x^n)) * norm (x^n))"
1.75 -    also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)"
1.76 +    also have "\<dots> = K * norm (z ^ n) * inverse (norm (x^n)) * norm (x^n)"
1.77        by (simp only: mult.assoc)
1.78      finally show "norm (norm (f n * z ^ n)) \<le>
1.79 -                  K * norm (z ^ n) * inverse (norm (x ^ n))"
1.80 +                  K * norm (z ^ n) * inverse (norm (x^n))"
1.81        by (simp add: mult_le_cancel_right x_neq_0)
1.82    qed
1.83 -  moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
1.84 +  moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))"
1.85    proof -
1.86      from 2 have "norm (norm (z * inverse x)) < 1"
1.87        using x_neq_0
1.88 @@ -142,7 +148,7 @@
1.89        by (rule summable_geometric)
1.90      hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
1.91        by (rule summable_mult)
1.92 -    thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
1.93 +    thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))"
1.94        using x_neq_0
1.95        by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
1.96                      power_inverse norm_power mult.assoc)
1.97 @@ -154,7 +160,7 @@
1.98  lemma powser_inside:
1.99    fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
1.100    shows
1.101 -    "summable (\<lambda>n. f n * (x ^ n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
1.102 +    "summable (\<lambda>n. f n * (x^n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
1.103        summable (\<lambda>n. f n * (z ^ n))"
1.104    by (rule powser_insidea [THEN summable_norm_cancel])
1.105
1.106 @@ -581,7 +587,7 @@
1.107    fixes x :: "'a::{real_normed_field,banach}"
1.108    assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
1.109      and 2: "norm x < norm K"
1.110 -  shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
1.111 +  shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h
1.112               - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
1.113  proof -
1.114    from dense [OF 2]
1.115 @@ -629,7 +635,7 @@
1.116      hence "norm x + norm h < r" by simp
1.117      with norm_triangle_ineq have xh: "norm (x + h) < r"
1.118        by (rule order_le_less_trans)
1.119 -    show "norm (c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))
1.120 +    show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))
1.121            \<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
1.122        apply (simp only: norm_mult mult.assoc)
1.123        apply (rule mult_left_mono [OF _ norm_ge_zero])
1.124 @@ -645,11 +651,11 @@
1.125        and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
1.126        and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
1.127        and 4: "norm x < norm K"
1.128 -  shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
1.129 +  shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. (diffs c) n * x^n)"
1.130    unfolding DERIV_def
1.131  proof (rule LIM_zero_cancel)
1.132 -  show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
1.133 -            - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
1.134 +  show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x^n)) / h
1.135 +            - suminf (\<lambda>n. diffs c n * x^n)) -- 0 --> 0"
1.136    proof (rule LIM_equal2)
1.137      show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
1.138    next
1.139 @@ -658,18 +664,18 @@
1.140      hence "norm x + norm h < norm K" by simp
1.141      hence 5: "norm (x + h) < norm K"
1.142        by (rule norm_triangle_ineq [THEN order_le_less_trans])
1.143 -    have "summable (\<lambda>n. c n * x ^ n)"
1.144 +    have "summable (\<lambda>n. c n * x^n)"
1.145        and "summable (\<lambda>n. c n * (x + h) ^ n)"
1.146 -      and "summable (\<lambda>n. diffs c n * x ^ n)"
1.147 +      and "summable (\<lambda>n. diffs c n * x^n)"
1.148        using 1 2 4 5 by (auto elim: powser_inside)
1.149 -    then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
1.150 -          (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h - of_nat n * c n * x ^ (n - Suc 0))"
1.151 +    then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x^n)) / h - (\<Sum>n. diffs c n * x^n) =
1.152 +          (\<Sum>n. (c n * (x + h) ^ n - c n * x^n) / h - of_nat n * c n * x ^ (n - Suc 0))"
1.153        by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums)
1.154 -    then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
1.155 -          (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
1.156 +    then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x^n)) / h - (\<Sum>n. diffs c n * x^n) =
1.157 +          (\<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))"
1.159    next
1.160 -    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
1.161 +    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
1.162        by (rule termdiffs_aux [OF 3 4])
1.163    qed
1.164  qed
1.165 @@ -889,7 +895,7 @@
1.166            fix n
1.167            have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)"
1.168              by (rule mult_left_mono) auto
1.169 -          show "norm (f n * x ^ n) \<le> norm (f n * real (Suc n) * x ^ n)"
1.170 +          show "norm (f n * x^n) \<le> norm (f n * real (Suc n) * x^n)"
1.171              unfolding real_norm_def abs_mult
1.172              by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right])
1.173          qed (rule powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`])
1.174 @@ -925,14 +931,14 @@
1.175  subsection {* Exponential Function *}
1.176
1.177  definition exp :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
1.178 -  where "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
1.179 +  where "exp = (\<lambda>x. \<Sum>n. x^n /\<^sub>R fact n)"
1.180
1.181  lemma summable_exp_generic:
1.182    fixes x :: "'a::{real_normed_algebra_1,banach}"
1.183 -  defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
1.184 +  defines S_def: "S \<equiv> \<lambda>n. x^n /\<^sub>R fact n"
1.185    shows "summable S"
1.186  proof -
1.187 -  have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)"
1.188 +  have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R (Suc n)"
1.189      unfolding S_def by (simp del: mult_Suc)
1.190    obtain r :: real where r0: "0 < r" and r1: "r < 1"
1.191      using dense [OF zero_less_one] by fast
1.192 @@ -959,26 +965,29 @@
1.193
1.194  lemma summable_norm_exp:
1.195    fixes x :: "'a::{real_normed_algebra_1,banach}"
1.196 -  shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
1.197 +  shows "summable (\<lambda>n. norm (x^n /\<^sub>R fact n))"
1.198  proof (rule summable_norm_comparison_test [OF exI, rule_format])
1.199 -  show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
1.200 +  show "summable (\<lambda>n. norm x^n /\<^sub>R fact n)"
1.201      by (rule summable_exp_generic)
1.202    fix n
1.203 -  show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
1.204 +  show "norm (x^n /\<^sub>R fact n) \<le> norm x^n /\<^sub>R fact n"
1.206  qed
1.207
1.208 -lemma summable_exp: "summable (\<lambda>n. inverse (real (fact n)) * x ^ n)"
1.209 -  using summable_exp_generic [where x=x] by simp
1.210 -
1.211 -lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x"
1.212 +lemma summable_exp:
1.213 +  fixes x :: "'a::{real_normed_field,banach}"
1.214 +  shows "summable (\<lambda>n. inverse (fact n) * x^n)"
1.215 +  using summable_exp_generic [where x=x]
1.216 +  by (simp add: scaleR_conv_of_real nonzero_of_real_inverse)
1.217 +
1.218 +lemma exp_converges: "(\<lambda>n. x^n /\<^sub>R fact n) sums exp x"
1.219    unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
1.220
1.221 -
1.222  lemma exp_fdiffs:
1.223 -      "diffs (\<lambda>n. inverse(real (fact n))) = (\<lambda>n. inverse(real (fact n)))"
1.224 -  by (simp add: diffs_def mult.assoc [symmetric] real_of_nat_def of_nat_mult
1.225 -        del: mult_Suc of_nat_Suc)
1.226 +  fixes XXX :: "'a::{real_normed_field,banach}"
1.227 +  shows "diffs (\<lambda>n. inverse (fact n)) = (\<lambda>n. inverse (fact n :: 'a))"
1.228 +  by (simp add: diffs_def mult_ac nonzero_inverse_mult_distrib nonzero_of_real_inverse
1.229 +           del: mult_Suc of_nat_Suc)
1.230
1.231  lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
1.233 @@ -997,7 +1006,7 @@
1.234  lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
1.235  proof -
1.236    from summable_norm[OF summable_norm_exp, of x]
1.237 -  have "norm (exp x) \<le> (\<Sum>n. inverse (real (fact n)) * norm (x ^ n))"
1.238 +  have "norm (exp x) \<le> (\<Sum>n. inverse (fact n) * norm (x^n))"
1.240    also have "\<dots> \<le> exp (norm x)"
1.241      using summable_exp_generic[of "norm x"] summable_norm_exp[of x]
1.242 @@ -1047,7 +1056,7 @@
1.243
1.245    fixes x y :: "'a::{real_normed_algebra_1, banach}"
1.246 -  defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
1.247 +  defines S_def: "S \<equiv> \<lambda>x n. x^n /\<^sub>R fact n"
1.248    assumes comm: "x * y = y * x"
1.249    shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n - i))"
1.250  proof (induct n)
1.251 @@ -1182,9 +1191,9 @@
1.252  using order_le_imp_less_or_eq [OF assms]
1.253  proof
1.254    assume "0 < x"
1.255 -  have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
1.256 +  have "1+x \<le> (\<Sum>n<2. inverse (fact n) * x^n)"
1.257      by (auto simp add: numeral_2_eq_2)
1.258 -  also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
1.259 +  also have "... \<le> (\<Sum>n. inverse (fact n) * x^n)"
1.260      apply (rule setsum_le_suminf [OF summable_exp])
1.261      using `0 < x`
1.262      apply (auto  simp add:  zero_le_mult_iff)
1.263 @@ -1297,7 +1306,7 @@
1.264  lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
1.265    by (rule ln_unique) (simp add: exp_diff)
1.266
1.267 -lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
1.268 +lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
1.269    by (rule ln_unique) (simp add: exp_real_of_nat_mult)
1.270
1.271  lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
1.272 @@ -1424,7 +1433,7 @@
1.273        fix x :: real
1.274        assume "x \<in> {- 1<..<1}"
1.275        hence "norm (-x) < 1" by auto
1.276 -      show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
1.277 +      show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)"
1.278          unfolding One_nat_def
1.279          by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
1.280      qed
1.281 @@ -1439,12 +1448,14 @@
1.282    thus ?thesis by auto
1.283  qed
1.284
1.285 -lemma exp_first_two_terms: "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
1.286 +lemma exp_first_two_terms:
1.287 +  fixes x :: "'a::{real_normed_field,banach}"
1.288 +  shows "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
1.289  proof -
1.290 -  have "exp x = suminf (\<lambda>n. inverse(fact n) * (x ^ n))"
1.291 -    by (simp add: exp_def)
1.292 +  have "exp x = suminf (\<lambda>n. inverse(fact n) * (x^n))"
1.293 +    by (simp add: exp_def scaleR_conv_of_real nonzero_of_real_inverse)
1.294    also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) +
1.295 -    (\<Sum> n::nat<2. inverse(fact n) * (x ^ n))" (is "_ = _ + ?a")
1.296 +    (\<Sum> n::nat<2. inverse(fact n) * (x^n))" (is "_ = _ + ?a")
1.297      by (rule suminf_split_initial_segment)
1.298    also have "?a = 1 + x"
1.300 @@ -1458,21 +1469,22 @@
1.301    assume b: "x <= 1"
1.302    {
1.303      fix n :: nat
1.304 -    have "2 * 2 ^ n \<le> fact (n + 2)"
1.305 +    have "(2::nat) * 2 ^ n \<le> fact (n + 2)"
1.306        by (induct n) simp_all
1.307 -    hence "real ((2::nat) * 2 ^ n) \<le> real (fact (n + 2))"
1.308 +    hence "real ((2::nat) * 2 ^ n) \<le> real_of_nat (fact (n + 2))"
1.309        by (simp only: real_of_nat_le_iff)
1.310 -    hence "2 * 2 ^ n \<le> real (fact (n + 2))"
1.311 -      by simp
1.312 -    hence "inverse (fact (n + 2)) \<le> inverse (2 * 2 ^ n)"
1.313 +    hence "((2::real) * 2 ^ n) \<le> fact (n + 2)"
1.314 +      unfolding of_nat_fact real_of_nat_def
1.315 +      by (simp add: of_nat_mult of_nat_power)
1.316 +    hence "inverse (fact (n + 2)) \<le> inverse ((2::real) * 2 ^ n)"
1.317        by (rule le_imp_inverse_le) simp
1.318 -    hence "inverse (fact (n + 2)) \<le> 1/2 * (1/2)^n"
1.319 +    hence "inverse (fact (n + 2)) \<le> 1/(2::real) * (1/2)^n"
1.321      hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
1.322        by (rule mult_mono)
1.323          (rule mult_mono, simp_all add: power_le_one a b)
1.324      hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
1.327    note aux1 = this
1.328    have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
1.329      by (intro sums_mult geometric_sums, simp)
1.330 @@ -2140,7 +2152,7 @@
1.331  lemma log_powr: "log b (x powr y) = y * log b x"
1.332    by (simp add: log_def ln_powr)
1.333
1.334 -lemma log_nat_power: "0 < x \<Longrightarrow> log b (x ^ n) = real n * log b x"
1.335 +lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
1.336    by (simp add: log_powr powr_realpow [symmetric])
1.337
1.338  lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
1.339 @@ -2342,10 +2354,10 @@
1.340  subsection {* Sine and Cosine *}
1.341
1.342  definition sin_coeff :: "nat \<Rightarrow> real" where
1.343 -  "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n))"
1.344 +  "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / (fact n))"
1.345
1.346  definition cos_coeff :: "nat \<Rightarrow> real" where
1.347 -  "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
1.348 +  "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / (fact n) else 0)"
1.349
1.350  definition sin :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
1.351    where "sin = (\<lambda>x. \<Sum>n. sin_coeff n *\<^sub>R x^n)"
1.352 @@ -2377,7 +2389,7 @@
1.353
1.354  lemma summable_norm_cos:
1.355    fixes x :: "'a::{real_normed_algebra_1,banach}"
1.356 -  shows "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x ^ n))"
1.357 +  shows "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x^n))"
1.358    unfolding cos_coeff_def
1.359    apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
1.360    apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
1.361 @@ -2398,7 +2410,7 @@
1.362    have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R  x^n)) = (\<lambda>n. sin_coeff n *\<^sub>R  (of_real x)^n)"
1.363    proof
1.364      fix n
1.365 -    show "of_real (sin_coeff n *\<^sub>R  x ^ n) = sin_coeff n *\<^sub>R of_real x ^ n"
1.366 +    show "of_real (sin_coeff n *\<^sub>R  x^n) = sin_coeff n *\<^sub>R of_real x^n"
1.368    qed
1.369    also have "... sums (sin (of_real x))"
1.370 @@ -2416,7 +2428,7 @@
1.371    have "(\<lambda>n. of_real (cos_coeff n *\<^sub>R  x^n)) = (\<lambda>n. cos_coeff n *\<^sub>R  (of_real x)^n)"
1.372    proof
1.373      fix n
1.374 -    show "of_real (cos_coeff n *\<^sub>R  x ^ n) = cos_coeff n *\<^sub>R of_real x ^ n"
1.375 +    show "of_real (cos_coeff n *\<^sub>R  x^n) = cos_coeff n *\<^sub>R of_real x^n"
1.377    qed
1.378    also have "... sums (cos (of_real x))"
1.379 @@ -2549,7 +2561,7 @@
1.380    fixes x :: "'a::{real_normed_field,banach}"
1.381    shows "(\<lambda>p. \<Sum>n\<le>p.
1.382            if even p \<and> even n
1.383 -          then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
1.384 +          then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
1.385           sums (cos x * cos y)"
1.386  proof -
1.387    { fix n p::nat
1.388 @@ -2557,12 +2569,12 @@
1.389      then have *: "even n \<Longrightarrow> even p \<Longrightarrow> (-1) ^ (n div 2) * (-1) ^ ((p - n) div 2) = (-1 :: real) ^ (p div 2)"
1.391      have "(cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
1.392 -          (if even p \<and> even n then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
1.393 +          (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)"
1.394      using `n\<le>p`
1.395        by (auto simp: * algebra_simps cos_coeff_def binomial_fact real_of_nat_def)
1.396    }
1.397    then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> even n
1.398 -                  then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
1.399 +                  then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
1.400               (\<lambda>p. \<Sum>n\<le>p. (cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
1.401      by simp
1.402    also have "... = (\<lambda>p. \<Sum>n\<le>p. (cos_coeff n *\<^sub>R x^n) * (cos_coeff (p - n) *\<^sub>R y^(p-n)))"
1.403 @@ -2578,7 +2590,7 @@
1.404    fixes x :: "'a::{real_normed_field,banach}"
1.405    shows "(\<lambda>p. \<Sum>n\<le>p.
1.406            if even p \<and> odd n
1.407 -               then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
1.408 +               then - ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
1.409           sums (sin x * sin y)"
1.410  proof -
1.411    { fix n p::nat
1.412 @@ -2596,12 +2608,12 @@
1.413      } then
1.414      have "(sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
1.415            (if even p \<and> odd n
1.416 -          then -((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
1.417 +          then -((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
1.418      using `n\<le>p`
1.419        by (auto simp:  algebra_simps sin_coeff_def binomial_fact real_of_nat_def)
1.420    }
1.421    then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> odd n
1.422 -               then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
1.423 +               then - ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
1.424               (\<lambda>p. \<Sum>n\<le>p. (sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
1.425      by simp
1.426    also have "... = (\<lambda>p. \<Sum>n\<le>p. (sin_coeff n *\<^sub>R x^n) * (sin_coeff (p - n) *\<^sub>R y^(p-n)))"
1.427 @@ -2616,31 +2628,31 @@
1.428    fixes x :: "'a::{real_normed_field,banach}"
1.429    shows
1.430    "(\<lambda>p. \<Sum>n\<le>p. if even p
1.431 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.432 +               then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.433                 else 0)
1.434          sums cos (x + y)"
1.435  proof -
1.436    { fix p::nat
1.437      have "(\<Sum>n\<le>p. if even p
1.438 -                  then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.439 +                  then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.440                    else 0) =
1.441            (if even p
1.442 -                  then \<Sum>n\<le>p. ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.443 +                  then \<Sum>n\<le>p. ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.444                    else 0)"
1.445        by simp
1.446      also have "... = (if even p
1.447 -                  then of_real ((-1) ^ (p div 2) / of_nat (fact p)) * (\<Sum>n\<le>p. (p choose n) *\<^sub>R (x^n) * y^(p-n))
1.448 +                  then of_real ((-1) ^ (p div 2) / (fact p)) * (\<Sum>n\<le>p. (p choose n) *\<^sub>R (x^n) * y^(p-n))
1.449                    else 0)"
1.450        by (auto simp: setsum_right_distrib field_simps scaleR_conv_of_real nonzero_of_real_divide)
1.451      also have "... = cos_coeff p *\<^sub>R ((x + y) ^ p)"
1.452        by (simp add: cos_coeff_def binomial_ring [of x y]  scaleR_conv_of_real real_of_nat_def atLeast0AtMost)
1.453      finally have "(\<Sum>n\<le>p. if even p
1.454 -                  then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.455 +                  then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.456                    else 0) = cos_coeff p *\<^sub>R ((x + y) ^ p)" .
1.457    }
1.458    then have "(\<lambda>p. \<Sum>n\<le>p.
1.459                 if even p
1.460 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.461 +               then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.462                 else 0)
1.463          = (\<lambda>p. cos_coeff p *\<^sub>R ((x+y)^p))"
1.464          by simp
1.465 @@ -2656,15 +2668,15 @@
1.466    { fix n p::nat
1.467      assume "n\<le>p"
1.468      then have "(if even p \<and> even n
1.469 -               then ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) -
1.470 +               then ((- 1) ^ (p div 2) * int (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) -
1.471            (if even p \<and> odd n
1.472 -               then - ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
1.473 +               then - ((- 1) ^ (p div 2) * int (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
1.474            = (if even p
1.475 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
1.476 +               then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
1.477        by simp
1.478    }
1.479    then have "(\<lambda>p. \<Sum>n\<le>p. (if even p
1.480 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
1.481 +               then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
1.482          sums (cos x * cos y - sin x * sin y)"
1.483      using sums_diff [OF cos_x_cos_y [of x y] sin_x_sin_y [of x y]]
1.484      by (simp add: setsum_subtractf [symmetric])
1.485 @@ -2701,7 +2713,6 @@
1.486  by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel]
1.487                suminf_minus sums_iff equation_minus_iff)
1.488
1.489 -
1.491    fixes x :: "'a::{real_normed_field,banach}"
1.492    shows "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
1.493 @@ -2787,7 +2798,7 @@
1.494
1.495  lemma sin_paired:
1.496    fixes x :: real
1.497 -  shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
1.498 +  shows "(\<lambda>n. (- 1) ^ n / (fact (2 * n + 1)) * x ^ (2 * n + 1)) sums  sin x"
1.499  proof -
1.500    have "(\<lambda>n. \<Sum>k = n*2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
1.501      apply (rule sums_group)
1.502 @@ -2801,7 +2812,7 @@
1.503    assumes "0 < x" and "x < 2"
1.504    shows "0 < sin x"
1.505  proof -
1.506 -  let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / real (fact (2*k+1)) * x^(2*k+1)"
1.507 +  let ?f = "\<lambda>n::nat. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / (fact (2*k+1)) * x^(2*k+1)"
1.508    have pos: "\<forall>n. 0 < ?f n"
1.509    proof
1.510      fix n :: nat
1.511 @@ -2812,9 +2823,8 @@
1.512      hence "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)"
1.513        by (intro mult_strict_right_mono zero_less_power `0 < x`)
1.514      thus "0 < ?f n"
1.515 -      by (simp del: mult_Suc,
1.516 -        simp add: less_divide_eq field_simps del: mult_Suc)
1.517 -  qed
1.518 +      by (simp add: real_of_nat_def divide_simps mult_ac del: mult_Suc)
1.519 +qed
1.520    have sums: "?f sums sin x"
1.521      by (rule sin_paired [THEN sums_group], simp)
1.522    show "0 < sin x"
1.523 @@ -2830,7 +2840,7 @@
1.524
1.525  lemma cos_paired:
1.526    fixes x :: real
1.527 -  shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
1.528 +  shows "(\<lambda>n. (- 1) ^ n / (fact (2 * n)) * x ^ (2 * n)) sums cos x"
1.529  proof -
1.530    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
1.531      apply (rule sums_group)
1.532 @@ -2860,29 +2870,28 @@
1.533  lemma cos_two_less_zero [simp]:
1.534    "cos 2 < (0::real)"
1.535  proof -
1.536 -  note fact_Suc [simp del]
1.537 -  from cos_paired
1.538 -  have "(\<lambda>n. - ((- 1) ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
1.539 -    by (rule sums_minus)
1.540 -  then have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
1.541 +  note fact.simps(2) [simp del]
1.542 +  from sums_minus [OF cos_paired]
1.543 +  have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / fact (2 * n))) sums - cos (2::real)"
1.544      by simp
1.545 -  then have **: "summable (\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
1.546 +  then have **: "summable (\<lambda>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
1.547      by (rule sums_summable)
1.548 -  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
1.549 -    by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
1.550 -  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
1.551 -    < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
1.552 +  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
1.553 +    by (simp add: fact_num_eq_if realpow_num_eq_if)
1.554 +  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n  * 2 ^ (2 * n) / (fact (2 * n))))
1.555 +    < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
1.556    proof -
1.557      { fix d
1.558 -      have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
1.559 -       < real (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
1.560 -           fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
1.561 -        by (simp only: real_of_nat_mult) (auto intro!: mult_strict_mono fact_less_mono_nat)
1.562 -      then have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
1.563 -        < real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
1.564 -        by (simp only: fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
1.565 -      then have "4 * inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))))
1.566 -        < inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
1.567 +      have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
1.568 +            < (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
1.569 +              fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
1.570 +        unfolding real_of_nat_mult
1.571 +        by (rule mult_strict_mono) (simp_all add: fact_less_mono)
1.572 +      then have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
1.573 +        <  (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
1.574 +        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)
1.575 +      then have "(4::real) * inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))
1.576 +        < inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))"
1.577          by (simp add: inverse_eq_divide less_divide_eq)
1.578      }
1.579      note *** = this
1.580 @@ -2890,9 +2899,9 @@
1.581      from ** show ?thesis by (rule sumr_pos_lt_pair)
1.582        (simp add: divide_inverse mult.assoc [symmetric] ***)
1.583    qed
1.584 -  ultimately have "0 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
1.585 +  ultimately have "0 < (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
1.586      by (rule order_less_trans)
1.587 -  moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
1.588 +  moreover from * have "- cos 2 = (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
1.589      by (rule sums_unique)
1.590    ultimately have "(0::real) < - cos 2" by simp
1.591    then show ?thesis by simp
```