# HG changeset patch # User immler # Date 1413219305 -7200 # Node ID 7f14d5d9b933f458cf26d7cdf1a1a74107a532e4 # Parent 46a19b1d3dd230dae5e1193cd6e45f8c43847ca8 relaxed class constraints for exp diff -r 46a19b1d3dd2 -r 7f14d5d9b933 src/HOL/NSA/HTranscendental.thy --- a/src/HOL/NSA/HTranscendental.thy Mon Oct 13 16:07:11 2014 +0200 +++ b/src/HOL/NSA/HTranscendental.thy Mon Oct 13 18:55:05 2014 +0200 @@ -263,7 +263,8 @@ lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1" by (auto intro: STAR_exp_Infinitesimal) -lemma STAR_exp_add: "!!x y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y" +lemma STAR_exp_add: + "!!(x::'a:: {banach,real_normed_field} star) y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y" by transfer (rule exp_add) lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)" @@ -289,7 +290,8 @@ apply (rule order_trans [of _ "1+x"], auto) done -lemma starfun_exp_minus: "!!x. ( *f* exp) (-x) = inverse(( *f* exp) x)" +lemma starfun_exp_minus: + "!!x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)" by transfer (rule exp_minus) (* exp (-oo) is infinitesimal *) diff -r 46a19b1d3dd2 -r 7f14d5d9b933 src/HOL/Power.thy --- a/src/HOL/Power.thy Mon Oct 13 16:07:11 2014 +0200 +++ b/src/HOL/Power.thy Mon Oct 13 18:55:05 2014 +0200 @@ -103,6 +103,19 @@ ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult.assoc) qed +lemma power_commuting_commutes: + assumes "x * y = y * x" + shows "x ^ n * y = y * x ^n" +proof (induct n) + case (Suc n) + have "x ^ Suc n * y = x ^ n * y * x" + by (subst power_Suc2) (simp add: assms ac_simps) + also have "\ = y * x ^ Suc n" + unfolding Suc power_Suc2 + by (simp add: ac_simps) + finally show ?case . +qed simp + end context comm_monoid_mult diff -r 46a19b1d3dd2 -r 7f14d5d9b933 src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Mon Oct 13 16:07:11 2014 +0200 +++ b/src/HOL/Probability/Borel_Space.thy Mon Oct 13 18:55:05 2014 +0200 @@ -880,7 +880,8 @@ "f \ borel_measurable M \ g \ borel_measurable M \ (\x. log (g x) (f x)) \ borel_measurable M" unfolding log_def by auto -lemma borel_measurable_exp[measurable]: "exp \ borel_measurable borel" +lemma borel_measurable_exp[measurable]: + "(exp::'a::{real_normed_field,banach}\'a) \ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp) lemma measurable_real_floor[measurable]: diff -r 46a19b1d3dd2 -r 7f14d5d9b933 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Mon Oct 13 16:07:11 2014 +0200 +++ b/src/HOL/Transcendental.thy Mon Oct 13 18:55:05 2014 +0200 @@ -931,7 +931,7 @@ subsection {* Exponential Function *} -definition exp :: "'a \ 'a::{real_normed_field,banach}" +definition exp :: "'a \ 'a::{real_normed_algebra_1,banach}" where "exp = (\x. \n. x ^ n /\<^sub>R real (fact n))" lemma summable_exp_generic: @@ -1001,22 +1001,40 @@ declare DERIV_exp[THEN DERIV_chain2, derivative_intros] -lemma isCont_exp: "isCont exp x" +lemma norm_exp: "norm (exp x) \ exp (norm x)" +proof - + from summable_norm[OF summable_norm_exp, of x] + have "norm (exp x) \ (\n. inverse (real (fact n)) * norm (x ^ n))" + by (simp add: exp_def) + also have "\ \ exp (norm x)" + using summable_exp_generic[of "norm x"] summable_norm_exp[of x] + by (auto simp: exp_def intro!: suminf_le norm_power_ineq) + finally show ?thesis . +qed + +lemma isCont_exp: + fixes x::"'a::{real_normed_field,banach}" + shows "isCont exp x" by (rule DERIV_exp [THEN DERIV_isCont]) -lemma isCont_exp' [simp]: "isCont f a \ isCont (\x. exp (f x)) a" +lemma isCont_exp' [simp]: + fixes f::"_ \'a::{real_normed_field,banach}" + shows "isCont f a \ isCont (\x. exp (f x)) a" by (rule isCont_o2 [OF _ isCont_exp]) lemma tendsto_exp [tendsto_intros]: - "(f ---> a) F \ ((\x. exp (f x)) ---> exp a) F" + fixes f::"_ \'a::{real_normed_field,banach}" + shows "(f ---> a) F \ ((\x. exp (f x)) ---> exp a) F" by (rule isCont_tendsto_compose [OF isCont_exp]) lemma continuous_exp [continuous_intros]: - "continuous F f \ continuous F (\x. exp (f x))" + fixes f::"_ \'a::{real_normed_field,banach}" + shows "continuous F f \ continuous F (\x. exp (f x))" unfolding continuous_def by (rule tendsto_exp) lemma continuous_on_exp [continuous_intros]: - "continuous_on s f \ continuous_on s (\x. exp (f x))" + fixes f::"_ \'a::{real_normed_field,banach}" + shows "continuous_on s f \ continuous_on s (\x. exp (f x))" unfolding continuous_on_def by (auto intro: tendsto_exp) @@ -1034,9 +1052,10 @@ lemma exp_zero [simp]: "exp 0 = 1" unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero) -lemma exp_series_add: - fixes x y :: "'a::{real_field}" +lemma exp_series_add_commuting: + fixes x y :: "'a::{real_normed_algebra_1, banach}" defines S_def: "S \ \x n. x ^ n /\<^sub>R real (fact n)" + assumes comm: "x * y = y * x" shows "S (x + y) n = (\i\n. S x i * S y (n - i))" proof (induct n) case 0 @@ -1048,6 +1067,8 @@ unfolding S_def by (simp del: mult_Suc) hence times_S: "\x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)" by simp + have S_comm: "\n. S x n * y = y * S x n" + by (simp add: power_commuting_commutes comm S_def) have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n" by (simp only: times_S) @@ -1056,9 +1077,12 @@ also have "\ = x * (\i\n. S x i * S y (n-i)) + y * (\i\n. S x i * S y (n-i))" by (rule distrib_right) - also have "\ = (\i\n. (x * S x i) * S y (n-i)) + also have "\ = (\i\n. x * S x i * S y (n-i)) + + (\i\n. S x i * y * S y (n-i))" + by (simp add: setsum_right_distrib ac_simps S_comm) + also have "\ = (\i\n. x * S x i * S y (n-i)) + (\i\n. S x i * (y * S y (n-i)))" - by (simp only: setsum_right_distrib ac_simps) + by (simp add: ac_simps) also have "\ = (\i\n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) + (\i\n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))" by (simp add: times_S Suc_diff_le) @@ -1080,12 +1104,16 @@ by (simp del: setsum_cl_ivl_Suc) qed -lemma exp_add: "exp (x + y) = exp x * exp y" +lemma exp_add_commuting: "x * y = y * x \ exp (x + y) = exp x * exp y" unfolding exp_def - by (simp only: Cauchy_product summable_norm_exp exp_series_add) - -lemma mult_exp_exp: "exp x * exp y = exp (x + y)" - by (rule exp_add [symmetric]) + by (simp only: Cauchy_product summable_norm_exp exp_series_add_commuting) + +lemma exp_add: + fixes x y::"'a::{real_normed_field,banach}" + shows "exp (x + y) = exp x * exp y" + by (rule exp_add_commuting) (simp add: ac_simps) + +lemmas mult_exp_exp = exp_add [symmetric] lemma exp_of_real: "exp (of_real x) = of_real (exp x)" unfolding exp_def @@ -1096,15 +1124,23 @@ lemma exp_not_eq_zero [simp]: "exp x \ 0" proof - have "exp x * exp (- x) = 1" by (simp add: mult_exp_exp) + have "exp x * exp (- x) = 1" by (simp add: exp_add_commuting[symmetric]) also assume "exp x = 0" finally show "False" by simp qed -lemma exp_minus: "exp (- x) = inverse (exp x)" - by (rule inverse_unique [symmetric], simp add: mult_exp_exp) - -lemma exp_diff: "exp (x - y) = exp x / exp y" +lemma exp_minus_inverse: + shows "exp x * exp (- x) = 1" + by (simp add: exp_add_commuting[symmetric]) + +lemma exp_minus: + fixes x :: "'a::{real_normed_field, banach}" + shows "exp (- x) = inverse (exp x)" + by (intro inverse_unique [symmetric] exp_minus_inverse) + +lemma exp_diff: + fixes x :: "'a::{real_normed_field, banach}" + shows "exp (x - y) = exp x / exp y" using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)