# HG changeset patch
# User huffman
# Date 1394813373 25200
# Node ID 304e37faf1ac9aca2ed7b3fbc64243b117720059
# Parent  64eeda68e693fde78ab28318ec791c51c16d5eb5
generalization of differential_zero_maxmin to class real_normed_vector

diff -r 64eeda68e693 -r 304e37faf1ac src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Mar 14 12:09:51 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Mar 14 09:09:33 2014 -0700
@@ -617,110 +617,84 @@
     unfolding euclidean_representation ..
 qed
 
-text {* We do not introduce @{text jacobian}, which is defined on matrices, instead we use
-  the unfolding of it. *}
+text {* Derivatives of local minima and maxima are zero. *}
 
-lemma jacobian_works:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  shows "f differentiable net \<longleftrightarrow>
-    (f has_derivative (\<lambda>h. \<Sum>i\<in>Basis.
-      (\<Sum>j\<in>Basis. frechet_derivative f net j \<bullet> i * (h \<bullet> j)) *\<^sub>R i)) net"
-    (is "?differentiable \<longleftrightarrow> (f has_derivative (\<lambda>h. \<Sum>i\<in>Basis. ?SUM h i *\<^sub>R i)) net")
+lemma has_derivative_local_min:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> real"
+  assumes deriv: "(f has_derivative f') (at x)"
+  assumes min: "eventually (\<lambda>y. f x \<le> f y) (at x)"
+  shows "f' = (\<lambda>h. 0)"
 proof
-  assume *: ?differentiable
-  {
-    fix h i
-    have "?SUM h i = frechet_derivative f net h \<bullet> i"
-      using *
-      by (auto intro!: setsum_cong simp: linear_componentwise[of _ h i] linear_frechet_derivative)
-  }
-  with * show "(f has_derivative (\<lambda>h. \<Sum>i\<in>Basis. ?SUM h i *\<^sub>R i)) net"
-    by (simp add: frechet_derivative_works euclidean_representation)
-qed (auto intro!: differentiableI)
+  fix h :: 'a
+  interpret f': bounded_linear f'
+    using deriv by (rule FDERIV_bounded_linear)
+  show "f' h = 0"
+  proof (cases "h = 0")
+    assume "h \<noteq> 0"
+    from min obtain d where d1: "0 < d" and d2: "\<forall>y\<in>ball x d. f x \<le> f y"
+      unfolding eventually_at by (force simp: dist_commute)
+    have "FDERIV (\<lambda>r. x + r *\<^sub>R h) 0 :> (\<lambda>r. r *\<^sub>R h)"
+      by (intro FDERIV_eq_intros, auto)
+    then have "FDERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> (\<lambda>k. f' (k *\<^sub>R h))"
+      by (rule FDERIV_compose, simp add: deriv)
+    then have "DERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> f' h"
+      unfolding deriv_fderiv by (simp add: f'.scaleR)
+    moreover have "0 < d / norm h"
+      using d1 and `h \<noteq> 0` by (simp add: divide_pos_pos)
+    moreover have "\<forall>y. \<bar>0 - y\<bar> < d / norm h \<longrightarrow> f (x + 0 *\<^sub>R h) \<le> f (x + y *\<^sub>R h)"
+      using `h \<noteq> 0` by (auto simp add: d2 dist_norm pos_less_divide_eq)
+    ultimately show "f' h = 0"
+      by (rule DERIV_local_min)
+  qed (simp add: f'.zero)
+qed
 
-lemma differential_zero_maxmin_component:
+lemma has_derivative_local_max:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> real"
+  assumes "(f has_derivative f') (at x)"
+  assumes "eventually (\<lambda>y. f y \<le> f x) (at x)"
+  shows "f' = (\<lambda>h. 0)"
+  using has_derivative_local_min [of "\<lambda>x. - f x" "\<lambda>h. - f' h" "x"]
+  using assms unfolding fun_eq_iff by simp
+
+lemma differential_zero_maxmin:
+  fixes f::"'a::real_normed_vector \<Rightarrow> real"
+  assumes "x \<in> s"
+    and "open s"
+    and deriv: "(f has_derivative f') (at x)"
+    and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
+  shows "f' = (\<lambda>v. 0)"
+  using mono
+proof
+  assume "\<forall>y\<in>s. f y \<le> f x"
+  with `x \<in> s` and `open s` have "eventually (\<lambda>y. f y \<le> f x) (at x)"
+    unfolding eventually_at_topological by auto
+  with deriv show ?thesis
+    by (rule has_derivative_local_max)
+next
+  assume "\<forall>y\<in>s. f x \<le> f y"
+  with `x \<in> s` and `open s` have "eventually (\<lambda>y. f x \<le> f y) (at x)"
+    unfolding eventually_at_topological by auto
+  with deriv show ?thesis
+    by (rule has_derivative_local_min)
+qed
+
+lemma differential_zero_maxmin_component: (* TODO: delete? *)
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes k: "k \<in> Basis"
     and ball: "0 < e" "(\<forall>y \<in> ball x e. (f y)\<bullet>k \<le> (f x)\<bullet>k) \<or> (\<forall>y\<in>ball x e. (f x)\<bullet>k \<le> (f y)\<bullet>k)"
     and diff: "f differentiable (at x)"
   shows "(\<Sum>j\<in>Basis. (frechet_derivative f (at x) j \<bullet> k) *\<^sub>R j) = (0::'a)" (is "?D k = 0")
-proof (rule ccontr)
-  assume "\<not> ?thesis"
-  then obtain j where j: "?D k \<bullet> j \<noteq> 0" "j \<in> Basis"
-    unfolding euclidean_eq_iff[of _ "0::'a"] by auto
-  then have *: "\<bar>?D k \<bullet> j\<bar> / 2 > 0"
-    by auto
-  note as = diff[unfolded jacobian_works has_derivative_at_alt]
-  obtain e' where e':
-    "0 < e'"
-    "(\<And>y. norm (y - x) < e' \<Longrightarrow>
-        norm (f y - f x -
-          (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative f (at x) j \<bullet> i * ((y - x) \<bullet> j)) *\<^sub>R i))
-        \<le> \<bar>(\<Sum>j\<in>Basis. (frechet_derivative f (at x) j \<bullet> k) *\<^sub>R j) \<bullet> j\<bar> / 2 * norm (y - x))"
-    using as[THEN conjunct2] * by blast
-  obtain d where d: "0 < d" "d < e" "d < e'"
-    using real_lbound_gt_zero[OF ball(1) e'(1)] by blast
-  {
-    fix c
-    assume "abs c \<le> d"
-    then have *: "norm (x + c *\<^sub>R j - x) < e'"
-      using norm_Basis[OF j(2)] d by auto
-    let ?v = "(\<Sum>i\<in>Basis. (\<Sum>l\<in>Basis. ?D i \<bullet> l * ((c *\<^sub>R j :: 'a) \<bullet> l)) *\<^sub>R i)"
-    have if_dist: "\<And> P a b c. a * (if P then b else c) = (if P then a * b else a * c)"
-      by auto
-    have "\<bar>(f (x + c *\<^sub>R j) - f x - ?v) \<bullet> k\<bar> \<le> norm (f (x + c *\<^sub>R j) - f x - ?v)"
-      by (rule Basis_le_norm[OF k])
-    also have "\<dots> \<le> \<bar>?D k \<bullet> j\<bar> / 2 * \<bar>c\<bar>"
-      using e'(2)[OF *] and norm_Basis[OF j(2)] j
-      by simp
-    finally have "\<bar>(f (x + c *\<^sub>R j) - f x - ?v) \<bullet> k\<bar> \<le> \<bar>?D k \<bullet> j\<bar> / 2 * \<bar>c\<bar>"
-      by simp
-    then have "\<bar>f (x + c *\<^sub>R j) \<bullet> k - f x \<bullet> k - c * (?D k \<bullet> j)\<bar> \<le> \<bar>?D k \<bullet> j\<bar> / 2 * \<bar>c\<bar>"
-      using j k
-      by (simp add: inner_simps field_simps inner_Basis setsum_cases if_dist)
-  }
-  note * = this
-  have "x + d *\<^sub>R j \<in> ball x e" "x - d *\<^sub>R j \<in> ball x e"
-    unfolding mem_ball dist_norm
-    using norm_Basis[OF j(2)] d
-    by auto
-  then have **: "((f (x - d *\<^sub>R j))\<bullet>k \<le> (f x)\<bullet>k \<and> (f (x + d *\<^sub>R j))\<bullet>k \<le> (f x)\<bullet>k) \<or>
-      ((f (x - d *\<^sub>R j))\<bullet>k \<ge> (f x)\<bullet>k \<and> (f (x + d *\<^sub>R j))\<bullet>k \<ge> (f x)\<bullet>k)"
-    using ball by auto
-  have ***: "\<And>y y1 y2 d dx :: real. y1 \<le> y \<and> y2 \<le> y \<or> y \<le> y1 \<and> y \<le> y2 \<Longrightarrow>
-      d < abs dx \<Longrightarrow> abs (y1 - y - - dx) \<le> d \<Longrightarrow> abs (y2 - y - dx) \<le> d \<Longrightarrow> False"
-    by arith
-  show False
-    apply (rule ***[OF **, where dx="d * (?D k \<bullet> j)" and d="\<bar>?D k \<bullet> j\<bar> / 2 * \<bar>d\<bar>"])
-    using *[of "-d"] and *[of d] and d(1) and j
-    unfolding mult_minus_left
-    unfolding abs_mult diff_minus_eq_add scaleR_minus_left
-    unfolding algebra_simps
-    apply (auto intro: mult_pos_pos)
-    done
-qed
-
-text {* In particular if we have a mapping into @{typ "real"}. *}
-
-lemma differential_zero_maxmin:
-  fixes f::"'a::euclidean_space \<Rightarrow> real"
-  assumes "x \<in> s"
-    and "open s"
-    and deriv: "(f has_derivative f') (at x)"
-    and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
-  shows "f' = (\<lambda>v. 0)"
 proof -
-  obtain e where e: "e > 0" "ball x e \<subseteq> s"
-    using `open s`[unfolded open_contains_ball] and `x \<in> s` by auto
-  with differential_zero_maxmin_component[where 'b=real, of 1 e x f] mono deriv
-  have "(\<Sum>j\<in>Basis. frechet_derivative f (at x) j *\<^sub>R j) = (0::'a)"
-    by (auto simp: Basis_real_def differentiable_def)
-  with frechet_derivative_at[OF deriv, symmetric]
-  have "\<forall>i\<in>Basis. f' i = 0"
-    by (simp add: euclidean_eq_iff[of _ "0::'a"] inner_setsum_left_Basis)
-  with derivative_is_linear[OF deriv, THEN linear_componentwise, of _ 1]
-  show ?thesis
-    by (simp add: fun_eq_iff)
+  let ?f' = "frechet_derivative f (at x)"
+  have "x \<in> ball x e" using `0 < e` by simp
+  moreover have "open (ball x e)" by simp
+  moreover have "((\<lambda>x. f x \<bullet> k) has_derivative (\<lambda>h. ?f' h \<bullet> k)) (at x)"
+    using bounded_linear_inner_left diff[unfolded frechet_derivative_works]
+    by (rule bounded_linear.FDERIV)
+  ultimately have "(\<lambda>h. frechet_derivative f (at x) h \<bullet> k) = (\<lambda>v. 0)"
+    using ball(2) by (rule differential_zero_maxmin)
+  then show ?thesis
+    unfolding fun_eq_iff by simp
 qed
 
 lemma rolle: