# HG changeset patch
# User immler
# Date 1430844310 -7200
# Node ID f620c70f9e9b2be862e30b5f424d4faa4b04d07d
# Parent  2bfcb83531c6622f1d8481707a175610bee78bd4
generalized differentiable_bound; some further variations of differentiable_bound

diff -r 2bfcb83531c6 -r f620c70f9e9b src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Tue May 05 18:45:10 2015 +0200
+++ b/src/HOL/Library/Convex.thy	Tue May 05 18:45:10 2015 +0200
@@ -389,6 +389,16 @@
     using `convex s` by (rule convex_linear_image)
 qed
 
+lemma convex_scaled:
+  assumes "convex s"
+  shows "convex ((\<lambda>x. x *\<^sub>R c) ` s)"
+proof -
+  have "linear (\<lambda>x. x *\<^sub>R c)"
+    by (simp add: linearI scaleR_add_left)
+  then show ?thesis
+    using `convex s` by (rule convex_linear_image)
+qed
+
 lemma convex_negations:
   assumes "convex s"
   shows "convex ((\<lambda>x. - x) ` s)"
diff -r 2bfcb83531c6 -r f620c70f9e9b src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue May 05 18:45:10 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue May 05 18:45:10 2015 +0200
@@ -779,10 +779,225 @@
   qed
 qed
 
-text {* Still more general bound theorem. *}
+
+subsection {* More general bound theorems *}
+
+lemma differentiable_bound_general:
+  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
+  assumes "a < b"
+    and f_cont: "continuous_on {a .. b} f"
+    and phi_cont: "continuous_on {a .. b} \<phi>"
+    and f': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
+    and phi': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<phi> has_vector_derivative \<phi>' x) (at x)"
+    and bnd: "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> norm (f' x) \<le> \<phi>' x"
+  shows "norm (f b - f a) \<le> \<phi> b - \<phi> a"
+proof -
+  {
+    fix x assume x: "a < x" "x < b"
+    have "0 \<le> norm (f' x)" by simp
+    also have "\<dots> \<le> \<phi>' x" using x by (auto intro!: bnd)
+    finally have "0 \<le> \<phi>' x" .
+  } note phi'_nonneg = this
+  note f_tendsto = assms(2)[simplified continuous_on_def, rule_format]
+  note phi_tendsto = assms(3)[simplified continuous_on_def, rule_format]
+  {
+    fix e::real assume "e > 0"
+    def e2 \<equiv> "e / 2" with `e > 0` have "e2 > 0" by simp
+    let ?le = "\<lambda>x1. norm (f x1 - f a) \<le> \<phi> x1 - \<phi> a + e * (x1 - a) + e"
+    def A \<equiv> "{x2. a \<le> x2 \<and> x2 \<le> b \<and> (\<forall>x1\<in>{a ..< x2}. ?le x1)}"
+    have A_subset: "A \<subseteq> {a .. b}" by (auto simp: A_def)
+    {
+      fix x2
+      assume a: "a \<le> x2" "x2 \<le> b" and le: "\<forall>x1\<in>{a..<x2}. ?le x1"
+      have "?le x2" using `e > 0`
+      proof cases
+        assume "x2 \<noteq> a" with a have "a < x2" by simp
+        have "at x2 within {a <..<x2}\<noteq> bot"
+          using `a < x2`
+          by (auto simp: trivial_limit_within islimpt_in_closure)
+        moreover
+        have "((\<lambda>x1. (\<phi> x1 - \<phi> a) + e * (x1 - a) + e) ---> (\<phi> x2 - \<phi> a) + e * (x2 - a) + e) (at x2 within {a <..<x2})"
+          "((\<lambda>x1. norm (f x1 - f a)) ---> norm (f x2 - f a)) (at x2 within {a <..<x2})"
+          using a
+          by (auto intro!: tendsto_eq_intros f_tendsto phi_tendsto
+            intro: tendsto_within_subset[where S="{a .. b}"])
+        moreover
+        have "eventually (\<lambda>x. x > a) (at x2 within {a <..<x2})"
+          by (auto simp: eventually_at_filter)
+        hence "eventually ?le (at x2 within {a <..<x2})"
+          unfolding eventually_at_filter
+          by eventually_elim (insert le, auto)
+        ultimately
+        show ?thesis
+          by (rule tendsto_le)
+      qed simp
+    } note le_cont = this
+    have "a \<in> A"
+      using assms by (auto simp: A_def)
+    hence [simp]: "A \<noteq> {}" by auto
+    have A_ivl: "\<And>x1 x2. x2 \<in> A \<Longrightarrow> x1 \<in> {a ..x2} \<Longrightarrow> x1 \<in> A"
+      by (simp add: A_def)
+    have [simp]: "bdd_above A" by (auto simp: A_def)
+    def y \<equiv> "Sup A"
+    have "y \<le> b"
+      unfolding y_def
+      by (simp add: cSup_le_iff) (simp add: A_def)
+     have leI: "\<And>x x1. a \<le> x1 \<Longrightarrow> x \<in> A \<Longrightarrow> x1 < x \<Longrightarrow> ?le x1"
+       by (auto simp: A_def intro!: le_cont)
+    have y_all_le: "\<forall>x1\<in>{a..<y}. ?le x1"
+      by (auto simp: y_def less_cSup_iff leI)
+    have "a \<le> y"
+      by (metis `a \<in> A` `bdd_above A` cSup_upper y_def)
+    have "y \<in> A"
+      using y_all_le `a \<le> y` `y \<le> b`
+      by (auto simp: A_def)
+    hence "A = {a .. y}"
+      using A_subset
+      by (auto simp: subset_iff y_def cSup_upper intro: A_ivl)
+    from le_cont[OF `a \<le> y` `y \<le> b` y_all_le] have le_y: "?le y" .
+    {
+      assume "a \<noteq> y" with `a \<le> y` have "a < y" by simp
+      have "y = b"
+      proof (rule ccontr)
+        assume "y \<noteq> b"
+        hence "y < b" using `y \<le> b` by simp
+        let ?F = "at y within {y..<b}"
+        from f' phi'
+        have "(f has_vector_derivative f' y) ?F"
+          and "(\<phi> has_vector_derivative \<phi>' y) ?F"
+          using `a < y` `y < b`
+          by (auto simp add: at_within_open[of _ "{a<..<b}"] has_vector_derivative_def
+            intro!: has_derivative_subset[where s="{a<..<b}" and t="{y..<b}"])
+        hence "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \<le> e2 * \<bar>x1 - y\<bar>"
+            "\<forall>\<^sub>F x1 in ?F. norm (\<phi> x1 - \<phi> y - (x1 - y) *\<^sub>R \<phi>' y) \<le> e2 * \<bar>x1 - y\<bar>"
+          using `e2 > 0`
+          by (auto simp: has_derivative_within_alt2 has_vector_derivative_def)
+        moreover
+        have "\<forall>\<^sub>F x1 in ?F. y \<le> x1" "\<forall>\<^sub>F x1 in ?F. x1 < b"
+          by (auto simp: eventually_at_filter)
+        ultimately
+        have "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y) \<le> (\<phi> x1 - \<phi> y) + e * \<bar>x1 - y\<bar>"
+          (is "\<forall>\<^sub>F x1 in ?F. ?le' x1")
+        proof eventually_elim
+          case elim
+          from norm_triangle_ineq2[THEN order_trans, OF elim(1)]
+          have "norm (f x1 - f y) \<le> norm (f' y) * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
+            by (simp add: ac_simps)
+          also have "norm (f' y) \<le> \<phi>' y" using bnd `a < y` `y < b` by simp
+          also
+          from elim have "\<phi>' y * \<bar>x1 - y\<bar> \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar>"
+            by (simp add: ac_simps)
+          finally
+          have "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
+            by (auto simp: mult_right_mono)
+          thus ?case by (simp add: e2_def)
+        qed
+        moreover have "?le' y" by simp
+        ultimately obtain S
+        where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..<b} \<Longrightarrow> ?le' x"
+          unfolding eventually_at_topological
+          by metis
+        from `open S` obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
+          by (force simp: dist_commute open_real_def ball_def
+            dest!: bspec[OF _ `y \<in> S`])
+        def d' \<equiv> "min ((y + b)/2) (y + (d/2))"
+        have "d' \<in> A"
+          unfolding A_def
+        proof safe
+          show "a \<le> d'" using `a < y` `0 < d` `y < b` by (simp add: d'_def)
+          show "d' \<le> b" using `y < b` by (simp add: d'_def min_def)
+          fix x1
+          assume x1: "x1 \<in> {a..<d'}"
+          {
+            assume "x1 < y"
+            hence "?le x1"
+              using `x1 \<in> {a..<d'}` y_all_le by auto
+          } moreover {
+            assume "x1 \<ge> y"
+            hence x1': "x1 \<in> S" "x1 \<in> {y..<b}" using x1
+              by (auto simp: d'_def dist_real_def intro!: d)
+            have "norm (f x1 - f a) \<le> norm (f x1 - f y) + norm (f y - f a)"
+              by (rule order_trans[OF _ norm_triangle_ineq]) simp
+            also note S(3)[OF x1']
+            also note le_y
+            finally have "?le x1"
+              using `x1 \<ge> y` by (auto simp: algebra_simps)
+          } ultimately show "?le x1" by arith
+        qed
+        hence "d' \<le> y"
+          unfolding y_def
+          by (rule cSup_upper) simp
+        thus False using `d > 0` `y < b`
+          by (simp add: d'_def min_def split: split_if_asm)
+      qed
+    } moreover {
+      assume "a = y"
+      with `a < b` have "y < b" by simp
+      with `a = y` f_cont phi_cont `e2 > 0`
+      have 1: "\<forall>\<^sub>F x in at y within {y..b}. dist (f x) (f y) < e2"
+       and 2: "\<forall>\<^sub>F x in at y within {y..b}. dist (\<phi> x) (\<phi> y) < e2"
+        by (auto simp: continuous_on_def tendsto_iff)
+      have 3: "eventually (\<lambda>x. y < x) (at y within {y..b})"
+        by (auto simp: eventually_at_filter)
+      have 4: "eventually (\<lambda>x::real. x < b) (at y within {y..b})"
+        using _ `y < b`
+        by (rule order_tendstoD) (auto intro!: tendsto_eq_intros)
+      from 1 2 3 4
+      have eventually_le: "eventually (\<lambda>x. ?le x) (at y within {y .. b})"
+      proof eventually_elim
+        case (elim x1)
+        have "norm (f x1 - f a) = norm (f x1 - f y)"
+          by (simp add: `a = y`)
+        also have "norm (f x1 - f y) \<le> e2"
+          using elim `a = y` by (auto simp : dist_norm intro!:  less_imp_le)
+        also have "\<dots> \<le> e2 + (\<phi> x1 - \<phi> a + e2 + e * (x1 - a))"
+          using `0 < e` elim
+          by (intro add_increasing2[OF add_nonneg_nonneg order.refl])
+            (auto simp: `a = y` dist_norm intro!: mult_nonneg_nonneg)
+        also have "\<dots> = \<phi> x1 - \<phi> a + e * (x1 - a) + e"
+          by (simp add: e2_def)
+        finally show "?le x1" .
+      qed
+      from this[unfolded eventually_at_topological] `?le y`
+      obtain S
+      where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
+        by metis
+      from `open S` obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
+        by (force simp: dist_commute open_real_def ball_def
+          dest!: bspec[OF _ `y \<in> S`])
+      def d' \<equiv> "min b (y + (d/2))"
+      have "d' \<in> A"
+        unfolding A_def
+      proof safe
+        show "a \<le> d'" using `a = y` `0 < d` `y < b` by (simp add: d'_def)
+        show "d' \<le> b" by (simp add: d'_def)
+        fix x1
+        assume "x1 \<in> {a..<d'}"
+        hence "x1 \<in> S" "x1 \<in> {y..b}"
+          by (auto simp: `a = y` d'_def dist_real_def intro!: d )
+        thus "?le x1"
+          by (rule S)
+      qed
+      hence "d' \<le> y"
+        unfolding y_def
+        by (rule cSup_upper) simp
+      hence "y = b" using `d > 0` `y < b`
+        by (simp add: d'_def)
+    } ultimately have "y = b"
+      by auto
+    with le_y have "norm (f b - f a) \<le> \<phi> b - \<phi> a + e * (b - a + 1)"
+      by (simp add: algebra_simps)
+  } note * = this
+  {
+    fix e::real assume "e > 0"
+    hence "norm (f b - f a) \<le> \<phi> b - \<phi> a + e"
+      using *[of "e / (b - a + 1)"] `a < b` by simp
+  } thus ?thesis
+    by (rule field_le_epsilon)
+qed
 
 lemma differentiable_bound:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "convex s"
     and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)"
     and "\<forall>x\<in>s. onorm (f' x) \<le> B"
@@ -791,14 +1006,15 @@
   shows "norm (f x - f y) \<le> B * norm (x - y)"
 proof -
   let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
+  let ?\<phi> = "\<lambda>h. h * B * norm (x - y)"
   have *: "\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s"
     using assms(1)[unfolded convex_alt,rule_format,OF x y]
     unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
     by (auto simp add: algebra_simps)
-  then have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
+  have 0: "continuous_on (?p ` {0..1}) f"
+    using *
+    unfolding continuous_on_eq_continuous_within
     apply -
-    apply (rule continuous_intros)+
-    unfolding continuous_on_eq_continuous_within
     apply rule
     apply (rule differentiable_imp_continuous_within)
     unfolding differentiable_def
@@ -807,51 +1023,93 @@
     apply (rule assms(2)[rule_format])
     apply auto
     done
-  have 2: "\<forall>u\<in>{0 <..< 1}.
-    ((f \<circ> ?p) has_derivative f' (x + u *\<^sub>R (y - x)) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u)"
-  proof rule
-    case goal1
-    let ?u = "x + u *\<^sub>R (y - x)"
+  from * have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
+    by (intro continuous_intros 0)+
+  {
+    fix u::real assume u: "u \<in>{0 <..< 1}"
+    let ?u = "?p u"
+    interpret linear "(f' ?u)"
+      using u by (auto intro!: has_derivative_linear assms(2)[rule_format] *)
     have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
       apply (rule diff_chain_within)
       apply (rule derivative_intros)+
       apply (rule has_derivative_within_subset)
       apply (rule assms(2)[rule_format])
-      using goal1 *
+      using u *
       apply auto
       done
-    then show ?case
-      by (simp add: has_derivative_within_open[OF goal1 open_greaterThanLessThan])
-  qed
-  obtain u where u:
-      "u \<in> {0<..<1}"
-      "norm ((f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 1 - (f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 0)
-        \<le> norm ((f' (x + u *\<^sub>R (y - x)) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (1 - 0))"
-    using mvt_general[OF zero_less_one 1 2] ..
-  have **: "\<And>x y. x \<in> s \<Longrightarrow> norm (f' x y) \<le> B * norm y"
-  proof -
-    case goal1
-    have "norm (f' x y) \<le> onorm (f' x) * norm y"
-      by (rule onorm[OF has_derivative_bounded_linear[OF assms(2)[rule_format,OF goal1]]])
-    also have "\<dots> \<le> B * norm y"
-      apply (rule mult_right_mono)
-      using assms(3)[rule_format,OF goal1]
-      apply (auto simp add: field_simps)
-      done
-    finally show ?case
-      by simp
-  qed
+    hence "((f \<circ> ?p) has_vector_derivative f' ?u (y - x)) (at u)"
+      by (simp add: has_derivative_within_open[OF u open_greaterThanLessThan]
+        scaleR has_vector_derivative_def o_def)
+  } note 2 = this
+  {
+    have "continuous_on {0..1} ?\<phi>"
+      by (rule continuous_intros)+
+  } note 3 = this
+  {
+    fix u::real assume u: "u \<in>{0 <..< 1}"
+    have "(?\<phi> has_vector_derivative B * norm (x - y)) (at u)"
+      by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
+  } note 4 = this
+  {
+    fix u::real assume u: "u \<in>{0 <..< 1}"
+    let ?u = "?p u"
+    interpret bounded_linear "(f' ?u)"
+      using u by (auto intro!: has_derivative_bounded_linear assms(2)[rule_format] *)
+    have "norm (f' ?u (y - x)) \<le> onorm (f' ?u) * norm (y - x)"
+      by (rule onorm) fact
+    also have "onorm (f' ?u) \<le> B"
+      using u by (auto intro!: assms(3)[rule_format] *)
+    finally have "norm ((f' ?u) (y - x)) \<le> B * norm (x - y)"
+      by (simp add: mult_right_mono norm_minus_commute)
+  } note 5 = this
   have "norm (f x - f y) = norm ((f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 1 - (f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 0)"
     by (auto simp add: norm_minus_commute)
-  also have "\<dots> \<le> norm (f' (x + u *\<^sub>R (y - x)) (y - x))"
-    using u by auto
-  also have "\<dots> \<le> B * norm(y - x)"
-    apply (rule **)
-    using * and u
-    apply auto
-    done
-  finally show ?thesis
-    by (auto simp add: norm_minus_commute)
+  also
+  from differentiable_bound_general[OF zero_less_one 1, OF 3 2 4 5]
+  have "norm ((f \<circ> ?p) 1 - (f \<circ> ?p) 0) \<le> B * norm (x - y)"
+    by simp
+  finally show ?thesis .
+qed
+
+lemma
+  differentiable_bound_segment:
+  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R a \<in> G"
+  assumes f': "\<And>x. x \<in> G \<Longrightarrow> (f has_derivative f' x) (at x within G)"
+  assumes B: "\<forall>x\<in>{0..1}. onorm (f' (x0 + x *\<^sub>R a)) \<le> B"
+  shows "norm (f (x0 + a) - f x0) \<le> norm a * B"
+proof -
+  let ?G = "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}"
+  have "?G = op + x0 ` (\<lambda>x. x *\<^sub>R a) ` {0..1}" by auto
+  also have "convex \<dots>"
+    by (intro convex_translation convex_scaled convex_real_interval)
+  finally have "convex ?G" .
+  moreover have "?G \<subseteq> G" "x0 \<in> ?G" "x0 + a \<in> ?G" using assms by (auto intro: image_eqI[where x=1])
+  ultimately show ?thesis
+    using has_derivative_subset[OF f' `?G \<subseteq> G`] B
+      differentiable_bound[of "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}" f f' B "x0 + a" x0]
+    by (auto simp: ac_simps)
+qed
+
+lemma differentiable_bound_linearization:
+  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> a + t *\<^sub>R (b - a) \<in> S"
+  assumes f'[derivative_intros]: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
+  assumes B: "\<forall>x\<in>S. onorm (f' x - f' x0) \<le> B"
+  assumes "x0 \<in> S"
+  shows "norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B"
+proof -
+  def g \<equiv> "\<lambda>x. f x - f' x0 x"
+  have g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative (\<lambda>i. f' x i - f' x0 i)) (at x within S)"
+    unfolding g_def using assms
+    by (auto intro!: derivative_eq_intros
+      bounded_linear.has_derivative[OF has_derivative_bounded_linear, OF f'])
+  from B have B: "\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B"
+     using assms by (auto simp: fun_diff_def)
+  from differentiable_bound_segment[OF assms(1) g B] `x0 \<in> S`
+  show ?thesis
+    by (simp add: g_def field_simps linear_sub[OF has_derivative_linear[OF f']])
 qed
 
 text {* In particular. *}