--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Apr 11 16:27:42 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Apr 12 11:18:29 2016 +0200
@@ -2525,6 +2525,85 @@
using assms
by (auto simp: vector_derivative_works DERIV_deriv_iff_has_field_derivative)
+lemma exp_scaleR_has_vector_derivative_right:
+ "((\<lambda>t. exp (t *\<^sub>R A)) has_vector_derivative exp (t *\<^sub>R A) * A) (at t within T)"
+ unfolding has_vector_derivative_def
+proof (rule has_derivativeI)
+ let ?F = "at t within (T \<inter> {t - 1 <..< t + 1})"
+ have *: "at t within T = ?F"
+ by (rule at_within_nhd[where S="{t - 1 <..< t + 1}"]) auto
+ let ?e = "\<lambda>i x. (inverse (1 + real i) * inverse (fact i) * (x - t) ^ i) *\<^sub>R (A * A ^ i)"
+ have "\<forall>\<^sub>F n in sequentially.
+ \<forall>x\<in>T \<inter> {t - 1<..<t + 1}. norm (?e n x) \<le> norm (A ^ (n + 1) /\<^sub>R fact (n + 1))"
+ by (auto simp: divide_simps power_abs intro!: mult_left_le_one_le power_le_one eventuallyI)
+ then have "uniform_limit (T \<inter> {t - 1<..<t + 1}) (\<lambda>n x. \<Sum>i<n. ?e i x) (\<lambda>x. \<Sum>i. ?e i x) sequentially"
+ by (rule weierstrass_m_test_ev) (intro summable_ignore_initial_segment summable_norm_exp)
+ moreover
+ have "\<forall>\<^sub>F x in sequentially. x > 0"
+ by (metis eventually_gt_at_top)
+ then have
+ "\<forall>\<^sub>F n in sequentially. ((\<lambda>x. \<Sum>i<n. ?e i x) \<longlongrightarrow> A) ?F"
+ by eventually_elim
+ (auto intro!: tendsto_eq_intros
+ simp: power_0_left if_distrib cond_application_beta setsum.delta
+ cong: if_cong)
+ ultimately
+ have [tendsto_intros]: "((\<lambda>x. \<Sum>i. ?e i x) \<longlongrightarrow> A) ?F"
+ by (auto intro!: swap_uniform_limit[where f="\<lambda>n x. \<Sum>i < n. ?e i x" and F = sequentially])
+ have [tendsto_intros]: "((\<lambda>x. if x = t then 0 else 1) \<longlongrightarrow> 1) ?F"
+ by (rule Lim_eventually) (simp add: eventually_at_filter)
+ have "((\<lambda>y. ((y - t) / abs (y - t)) *\<^sub>R ((\<Sum>n. ?e n y) - A)) \<longlongrightarrow> 0) (at t within T)"
+ unfolding *
+ by (rule tendsto_norm_zero_cancel) (auto intro!: tendsto_eq_intros)
+
+ moreover
+
+ have "\<forall>\<^sub>F x in at t within T. x \<noteq> t"
+ by (simp add: eventually_at_filter)
+ then have "\<forall>\<^sub>F x in at t within T. ((x - t) / \<bar>x - t\<bar>) *\<^sub>R ((\<Sum>n. ?e n x) - A) =
+ (exp ((x - t) *\<^sub>R A) - 1 - (x - t) *\<^sub>R A) /\<^sub>R norm (x - t)"
+ proof eventually_elim
+ case (elim x)
+ have "(exp ((x - t) *\<^sub>R A) - 1 - (x - t) *\<^sub>R A) /\<^sub>R norm (x - t) =
+ ((\<Sum>n. (x - t) *\<^sub>R ?e n x) - (x - t) *\<^sub>R A) /\<^sub>R norm (x - t)"
+ unfolding exp_first_term
+ by (simp add: ac_simps)
+ also
+ have "summable (\<lambda>n. ?e n x)"
+ proof -
+ from elim have "?e n x = (((x - t) *\<^sub>R A) ^ (n + 1)) /\<^sub>R fact (n + 1) /\<^sub>R (x - t)" for n
+ by simp
+ then show ?thesis
+ by (auto simp only:
+ intro!: summable_scaleR_right summable_ignore_initial_segment summable_exp_generic)
+ qed
+ then have "(\<Sum>n. (x - t) *\<^sub>R ?e n x) = (x - t) *\<^sub>R (\<Sum>n. ?e n x)"
+ by (rule suminf_scaleR_right[symmetric])
+ also have "(\<dots> - (x - t) *\<^sub>R A) /\<^sub>R norm (x - t) = (x - t) *\<^sub>R ((\<Sum>n. ?e n x) - A) /\<^sub>R norm (x - t)"
+ by (simp add: algebra_simps)
+ finally show ?case
+ by (simp add: divide_simps)
+ qed
+
+ ultimately
+
+ have "((\<lambda>y. (exp ((y - t) *\<^sub>R A) - 1 - (y - t) *\<^sub>R A) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0) (at t within T)"
+ by (rule Lim_transform_eventually[rotated])
+ from tendsto_mult_right_zero[OF this, where c="exp (t *\<^sub>R A)"]
+ show "((\<lambda>y. (exp (y *\<^sub>R A) - exp (t *\<^sub>R A) - (y - t) *\<^sub>R (exp (t *\<^sub>R A) * A)) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0)
+ (at t within T)"
+ by (rule Lim_transform_eventually[rotated])
+ (auto simp: algebra_simps divide_simps exp_add_commuting[symmetric])
+qed (rule bounded_linear_scaleR_left)
+
+lemma exp_times_scaleR_commute: "exp (t *\<^sub>R A) * A = A * exp (t *\<^sub>R A)"
+ using exp_times_arg_commute[symmetric, of "t *\<^sub>R A"]
+ by (auto simp: algebra_simps)
+
+lemma exp_scaleR_has_vector_derivative_left: "((\<lambda>t. exp (t *\<^sub>R A)) has_vector_derivative A * exp (t *\<^sub>R A)) (at t)"
+ using exp_scaleR_has_vector_derivative_right[of A t]
+ by (simp add: exp_times_scaleR_commute)
+
subsection \<open>Relation between convexity and derivative\<close>
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Apr 11 16:27:42 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Tue Apr 12 11:18:29 2016 +0200
@@ -53,6 +53,17 @@
unfolding uniform_limit_iff eventually_at
by (fastforce dest: spec[where x = "e / 2" for e])
+lemma metric_uniform_limit_imp_uniform_limit:
+ assumes f: "uniform_limit S f a F"
+ assumes le: "eventually (\<lambda>x. \<forall>y\<in>S. dist (g x y) (b y) \<le> dist (f x y) (a y)) F"
+ shows "uniform_limit S g b F"
+proof (rule uniform_limitI)
+ fix e :: real assume "0 < e"
+ from uniform_limitD[OF f this] le
+ show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (g x y) (b y) < e"
+ by eventually_elim force
+qed
+
lemma swap_uniform_limit:
assumes f: "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) (at x within S)"
assumes g: "(g \<longlongrightarrow> l) F"
@@ -352,6 +363,9 @@
lemmas uniform_limit_uminus[uniform_limit_intros] =
bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
+lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\<lambda>x y. c) (\<lambda>x. c) f"
+ by (auto intro!: uniform_limitI)
+
lemma uniform_limit_add[uniform_limit_intros]:
fixes f g::"'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
assumes "uniform_limit X f l F"
@@ -376,6 +390,14 @@
unfolding diff_conv_add_uminus
by (rule uniform_limit_intros assms)+
+lemma uniform_limit_norm[uniform_limit_intros]:
+ assumes "uniform_limit S g l f"
+ shows "uniform_limit S (\<lambda>x y. norm (g x y)) (\<lambda>x. norm (l x)) f"
+ using assms
+ apply (rule metric_uniform_limit_imp_uniform_limit)
+ apply (rule eventuallyI)
+ by (metis dist_norm norm_triangle_ineq3 real_norm_def)
+
lemma (in bounded_bilinear) bounded_uniform_limit[uniform_limit_intros]:
assumes "uniform_limit X f l F"
assumes "uniform_limit X g m F"
@@ -450,17 +472,6 @@
bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_mult]
bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_scaleR]
-lemma metric_uniform_limit_imp_uniform_limit:
- assumes f: "uniform_limit S f a F"
- assumes le: "eventually (\<lambda>x. \<forall>y\<in>S. dist (g x y) (b y) \<le> dist (f x y) (a y)) F"
- shows "uniform_limit S g b F"
-proof (rule uniform_limitI)
- fix e :: real assume "0 < e"
- from uniform_limitD[OF f this] le
- show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (g x y) (b y) < e"
- by eventually_elim force
-qed
-
lemma uniform_limit_null_comparison:
assumes "\<forall>\<^sub>F x in F. \<forall>a\<in>S. norm (f x a) \<le> g x a"
assumes "uniform_limit S g (\<lambda>_. 0) F"
--- a/src/HOL/Transcendental.thy Mon Apr 11 16:27:42 2016 +0100
+++ b/src/HOL/Transcendental.thy Tue Apr 12 11:18:29 2016 +0200
@@ -1291,6 +1291,9 @@
unfolding exp_def
by (simp only: Cauchy_product summable_norm_exp exp_series_add_commuting)
+lemma exp_times_arg_commute: "exp A * A = A * exp A"
+ by (simp add: exp_def suminf_mult[symmetric] summable_exp_generic power_commutes suminf_mult2)
+
lemma exp_add:
fixes x y::"'a::{real_normed_field,banach}"
shows "exp (x + y) = exp x * exp y"
@@ -1710,21 +1713,29 @@
thus ?thesis by auto
qed
-lemma exp_first_two_terms:
- fixes x :: "'a::{real_normed_field,banach}"
- shows "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
+lemma exp_first_terms:
+ fixes x :: "'a::{real_normed_algebra_1,banach}"
+ shows "exp x = (\<Sum>n<k. inverse(fact n) *\<^sub>R (x ^ n)) + (\<Sum>n. inverse(fact (n+k)) *\<^sub>R (x ^ (n+k)))"
proof -
- have "exp x = suminf (\<lambda>n. inverse(fact n) * (x^n))"
- by (simp add: exp_def scaleR_conv_of_real nonzero_of_real_inverse)
- also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) +
- (\<Sum> n::nat<2. inverse(fact n) * (x^n))" (is "_ = _ + ?a")
+ have "exp x = suminf (\<lambda>n. inverse(fact n) *\<^sub>R (x^n))"
+ by (simp add: exp_def)
+ also from summable_exp_generic have "... = (\<Sum> n. inverse(fact(n+k)) *\<^sub>R (x ^ (n+k))) +
+ (\<Sum> n::nat<k. inverse(fact n) *\<^sub>R (x^n))" (is "_ = _ + ?a")
by (rule suminf_split_initial_segment)
- also have "?a = 1 + x"
- by (simp add: numeral_2_eq_2)
- finally show ?thesis
- by simp
+ finally show ?thesis by simp
qed
+lemma exp_first_term:
+ fixes x :: "'a::{real_normed_algebra_1,banach}"
+ shows "exp x = 1 + (\<Sum> n. inverse(fact (Suc n)) *\<^sub>R (x ^ (Suc n)))"
+ using exp_first_terms[of x 1] by simp
+
+lemma exp_first_two_terms:
+ fixes x :: "'a::{real_normed_algebra_1,banach}"
+ shows "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) *\<^sub>R (x ^ (n+2)))"
+ using exp_first_terms[of x 2]
+ by (simp add: eval_nat_numeral)
+
lemma exp_bound: "0 <= (x::real) \<Longrightarrow> x <= 1 \<Longrightarrow> exp x <= 1 + x + x\<^sup>2"
proof -
assume a: "0 <= x"