relaxed class constraints for exp
authorimmler
Mon Oct 13 18:55:05 2014 +0200 (2014-10-13)
changeset 586567f14d5d9b933
parent 58655 46a19b1d3dd2
child 58667 d2a7b443ceb2
relaxed class constraints for exp
src/HOL/NSA/HTranscendental.thy
src/HOL/Power.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/NSA/HTranscendental.thy	Mon Oct 13 16:07:11 2014 +0200
     1.2 +++ b/src/HOL/NSA/HTranscendental.thy	Mon Oct 13 18:55:05 2014 +0200
     1.3 @@ -263,7 +263,8 @@
     1.4  lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
     1.5  by (auto intro: STAR_exp_Infinitesimal)
     1.6  
     1.7 -lemma STAR_exp_add: "!!x y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
     1.8 +lemma STAR_exp_add:
     1.9 +  "!!(x::'a:: {banach,real_normed_field} star) y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
    1.10  by transfer (rule exp_add)
    1.11  
    1.12  lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
    1.13 @@ -289,7 +290,8 @@
    1.14  apply (rule order_trans [of _ "1+x"], auto) 
    1.15  done
    1.16  
    1.17 -lemma starfun_exp_minus: "!!x. ( *f* exp) (-x) = inverse(( *f* exp) x)"
    1.18 +lemma starfun_exp_minus:
    1.19 +  "!!x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)"
    1.20  by transfer (rule exp_minus)
    1.21  
    1.22  (* exp (-oo) is infinitesimal *)
     2.1 --- a/src/HOL/Power.thy	Mon Oct 13 16:07:11 2014 +0200
     2.2 +++ b/src/HOL/Power.thy	Mon Oct 13 18:55:05 2014 +0200
     2.3 @@ -103,6 +103,19 @@
     2.4    ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult.assoc)
     2.5  qed
     2.6  
     2.7 +lemma power_commuting_commutes:
     2.8 +  assumes "x * y = y * x"
     2.9 +  shows "x ^ n * y = y * x ^n"
    2.10 +proof (induct n)
    2.11 +  case (Suc n)
    2.12 +  have "x ^ Suc n * y = x ^ n * y * x"
    2.13 +    by (subst power_Suc2) (simp add: assms ac_simps)
    2.14 +  also have "\<dots> = y * x ^ Suc n"
    2.15 +    unfolding Suc power_Suc2
    2.16 +    by (simp add: ac_simps)
    2.17 +  finally show ?case .
    2.18 +qed simp
    2.19 +
    2.20  end
    2.21  
    2.22  context comm_monoid_mult
     3.1 --- a/src/HOL/Probability/Borel_Space.thy	Mon Oct 13 16:07:11 2014 +0200
     3.2 +++ b/src/HOL/Probability/Borel_Space.thy	Mon Oct 13 18:55:05 2014 +0200
     3.3 @@ -880,7 +880,8 @@
     3.4    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
     3.5    unfolding log_def by auto
     3.6  
     3.7 -lemma borel_measurable_exp[measurable]: "exp \<in> borel_measurable borel"
     3.8 +lemma borel_measurable_exp[measurable]:
     3.9 +  "(exp::'a::{real_normed_field,banach}\<Rightarrow>'a) \<in> borel_measurable borel"
    3.10    by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp)
    3.11  
    3.12  lemma measurable_real_floor[measurable]:
     4.1 --- a/src/HOL/Transcendental.thy	Mon Oct 13 16:07:11 2014 +0200
     4.2 +++ b/src/HOL/Transcendental.thy	Mon Oct 13 18:55:05 2014 +0200
     4.3 @@ -931,7 +931,7 @@
     4.4  
     4.5  subsection {* Exponential Function *}
     4.6  
     4.7 -definition exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
     4.8 +definition exp :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
     4.9    where "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
    4.10  
    4.11  lemma summable_exp_generic:
    4.12 @@ -1001,22 +1001,40 @@
    4.13  
    4.14  declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
    4.15  
    4.16 -lemma isCont_exp: "isCont exp x"
    4.17 +lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
    4.18 +proof -
    4.19 +  from summable_norm[OF summable_norm_exp, of x]
    4.20 +  have "norm (exp x) \<le> (\<Sum>n. inverse (real (fact n)) * norm (x ^ n))"
    4.21 +    by (simp add: exp_def)
    4.22 +  also have "\<dots> \<le> exp (norm x)"
    4.23 +    using summable_exp_generic[of "norm x"] summable_norm_exp[of x]
    4.24 +    by (auto simp: exp_def intro!: suminf_le norm_power_ineq)
    4.25 +  finally show ?thesis .
    4.26 +qed
    4.27 +
    4.28 +lemma isCont_exp:
    4.29 +  fixes x::"'a::{real_normed_field,banach}"
    4.30 +  shows "isCont exp x"
    4.31    by (rule DERIV_exp [THEN DERIV_isCont])
    4.32  
    4.33 -lemma isCont_exp' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a"
    4.34 +lemma isCont_exp' [simp]:
    4.35 +  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
    4.36 +  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a"
    4.37    by (rule isCont_o2 [OF _ isCont_exp])
    4.38  
    4.39  lemma tendsto_exp [tendsto_intros]:
    4.40 -  "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
    4.41 +  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
    4.42 +  shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
    4.43    by (rule isCont_tendsto_compose [OF isCont_exp])
    4.44  
    4.45  lemma continuous_exp [continuous_intros]:
    4.46 -  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
    4.47 +  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
    4.48 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
    4.49    unfolding continuous_def by (rule tendsto_exp)
    4.50  
    4.51  lemma continuous_on_exp [continuous_intros]:
    4.52 -  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
    4.53 +  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
    4.54 +  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
    4.55    unfolding continuous_on_def by (auto intro: tendsto_exp)
    4.56  
    4.57  
    4.58 @@ -1034,9 +1052,10 @@
    4.59  lemma exp_zero [simp]: "exp 0 = 1"
    4.60    unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
    4.61  
    4.62 -lemma exp_series_add:
    4.63 -  fixes x y :: "'a::{real_field}"
    4.64 +lemma exp_series_add_commuting:
    4.65 +  fixes x y :: "'a::{real_normed_algebra_1, banach}"
    4.66    defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
    4.67 +  assumes comm: "x * y = y * x"
    4.68    shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n - i))"
    4.69  proof (induct n)
    4.70    case 0
    4.71 @@ -1048,6 +1067,8 @@
    4.72      unfolding S_def by (simp del: mult_Suc)
    4.73    hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)"
    4.74      by simp
    4.75 +  have S_comm: "\<And>n. S x n * y = y * S x n"
    4.76 +    by (simp add: power_commuting_commutes comm S_def)
    4.77  
    4.78    have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
    4.79      by (simp only: times_S)
    4.80 @@ -1056,9 +1077,12 @@
    4.81    also have "\<dots> = x * (\<Sum>i\<le>n. S x i * S y (n-i))
    4.82                  + y * (\<Sum>i\<le>n. S x i * S y (n-i))"
    4.83      by (rule distrib_right)
    4.84 -  also have "\<dots> = (\<Sum>i\<le>n. (x * S x i) * S y (n-i))
    4.85 +  also have "\<dots> = (\<Sum>i\<le>n. x * S x i * S y (n-i))
    4.86 +                + (\<Sum>i\<le>n. S x i * y * S y (n-i))"
    4.87 +    by (simp add: setsum_right_distrib ac_simps S_comm)
    4.88 +  also have "\<dots> = (\<Sum>i\<le>n. x * S x i * S y (n-i))
    4.89                  + (\<Sum>i\<le>n. S x i * (y * S y (n-i)))"
    4.90 -    by (simp only: setsum_right_distrib ac_simps)
    4.91 +    by (simp add: ac_simps)
    4.92    also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
    4.93                  + (\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
    4.94      by (simp add: times_S Suc_diff_le)
    4.95 @@ -1080,12 +1104,16 @@
    4.96      by (simp del: setsum_cl_ivl_Suc)
    4.97  qed
    4.98  
    4.99 -lemma exp_add: "exp (x + y) = exp x * exp y"
   4.100 +lemma exp_add_commuting: "x * y = y * x \<Longrightarrow> exp (x + y) = exp x * exp y"
   4.101    unfolding exp_def
   4.102 -  by (simp only: Cauchy_product summable_norm_exp exp_series_add)
   4.103 -
   4.104 -lemma mult_exp_exp: "exp x * exp y = exp (x + y)"
   4.105 -  by (rule exp_add [symmetric])
   4.106 +  by (simp only: Cauchy_product summable_norm_exp exp_series_add_commuting)
   4.107 +
   4.108 +lemma exp_add:
   4.109 +  fixes x y::"'a::{real_normed_field,banach}"
   4.110 +  shows "exp (x + y) = exp x * exp y"
   4.111 +  by (rule exp_add_commuting) (simp add: ac_simps)
   4.112 +
   4.113 +lemmas mult_exp_exp = exp_add [symmetric]
   4.114  
   4.115  lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
   4.116    unfolding exp_def
   4.117 @@ -1096,15 +1124,23 @@
   4.118  
   4.119  lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
   4.120  proof
   4.121 -  have "exp x * exp (- x) = 1" by (simp add: mult_exp_exp)
   4.122 +  have "exp x * exp (- x) = 1" by (simp add: exp_add_commuting[symmetric])
   4.123    also assume "exp x = 0"
   4.124    finally show "False" by simp
   4.125  qed
   4.126  
   4.127 -lemma exp_minus: "exp (- x) = inverse (exp x)"
   4.128 -  by (rule inverse_unique [symmetric], simp add: mult_exp_exp)
   4.129 -
   4.130 -lemma exp_diff: "exp (x - y) = exp x / exp y"
   4.131 +lemma exp_minus_inverse:
   4.132 +  shows "exp x * exp (- x) = 1"
   4.133 +  by (simp add: exp_add_commuting[symmetric])
   4.134 +
   4.135 +lemma exp_minus:
   4.136 +  fixes x :: "'a::{real_normed_field, banach}"
   4.137 +  shows "exp (- x) = inverse (exp x)"
   4.138 +  by (intro inverse_unique [symmetric] exp_minus_inverse)
   4.139 +
   4.140 +lemma exp_diff:
   4.141 +  fixes x :: "'a::{real_normed_field, banach}"
   4.142 +  shows "exp (x - y) = exp x / exp y"
   4.143    using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
   4.144  
   4.145