# HG changeset patch
# User immler
# Date 1460452709 -7200
# Node ID f36a54da47a4d544ac3ed7e449e9c3f599186500
# Parent  7700f467892b738938f6587694371653109b29d8
added derivative of scaling in exponential function

diff -r 7700f467892b -r f36a54da47a4 src/HOL/Multivariate_Analysis/Derivative.thy
--- 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>
 
diff -r 7700f467892b -r f36a54da47a4 src/HOL/Multivariate_Analysis/Uniform_Limit.thy
--- 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"
diff -r 7700f467892b -r f36a54da47a4 src/HOL/Transcendental.thy
--- 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"