generalized differentiable_bound; some further variations of differentiable_bound
authorimmler
Tue May 05 18:45:10 2015 +0200 (2015-05-05)
changeset 60178f620c70f9e9b
parent 60177 2bfcb83531c6
child 60179 d87c8c2d4938
generalized differentiable_bound; some further variations of differentiable_bound
src/HOL/Library/Convex.thy
src/HOL/Multivariate_Analysis/Derivative.thy
     1.1 --- a/src/HOL/Library/Convex.thy	Tue May 05 18:45:10 2015 +0200
     1.2 +++ b/src/HOL/Library/Convex.thy	Tue May 05 18:45:10 2015 +0200
     1.3 @@ -389,6 +389,16 @@
     1.4      using `convex s` by (rule convex_linear_image)
     1.5  qed
     1.6  
     1.7 +lemma convex_scaled:
     1.8 +  assumes "convex s"
     1.9 +  shows "convex ((\<lambda>x. x *\<^sub>R c) ` s)"
    1.10 +proof -
    1.11 +  have "linear (\<lambda>x. x *\<^sub>R c)"
    1.12 +    by (simp add: linearI scaleR_add_left)
    1.13 +  then show ?thesis
    1.14 +    using `convex s` by (rule convex_linear_image)
    1.15 +qed
    1.16 +
    1.17  lemma convex_negations:
    1.18    assumes "convex s"
    1.19    shows "convex ((\<lambda>x. - x) ` s)"
     2.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue May 05 18:45:10 2015 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue May 05 18:45:10 2015 +0200
     2.3 @@ -779,10 +779,225 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 -text {* Still more general bound theorem. *}
     2.8 +
     2.9 +subsection {* More general bound theorems *}
    2.10 +
    2.11 +lemma differentiable_bound_general:
    2.12 +  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
    2.13 +  assumes "a < b"
    2.14 +    and f_cont: "continuous_on {a .. b} f"
    2.15 +    and phi_cont: "continuous_on {a .. b} \<phi>"
    2.16 +    and f': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
    2.17 +    and phi': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<phi> has_vector_derivative \<phi>' x) (at x)"
    2.18 +    and bnd: "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> norm (f' x) \<le> \<phi>' x"
    2.19 +  shows "norm (f b - f a) \<le> \<phi> b - \<phi> a"
    2.20 +proof -
    2.21 +  {
    2.22 +    fix x assume x: "a < x" "x < b"
    2.23 +    have "0 \<le> norm (f' x)" by simp
    2.24 +    also have "\<dots> \<le> \<phi>' x" using x by (auto intro!: bnd)
    2.25 +    finally have "0 \<le> \<phi>' x" .
    2.26 +  } note phi'_nonneg = this
    2.27 +  note f_tendsto = assms(2)[simplified continuous_on_def, rule_format]
    2.28 +  note phi_tendsto = assms(3)[simplified continuous_on_def, rule_format]
    2.29 +  {
    2.30 +    fix e::real assume "e > 0"
    2.31 +    def e2 \<equiv> "e / 2" with `e > 0` have "e2 > 0" by simp
    2.32 +    let ?le = "\<lambda>x1. norm (f x1 - f a) \<le> \<phi> x1 - \<phi> a + e * (x1 - a) + e"
    2.33 +    def A \<equiv> "{x2. a \<le> x2 \<and> x2 \<le> b \<and> (\<forall>x1\<in>{a ..< x2}. ?le x1)}"
    2.34 +    have A_subset: "A \<subseteq> {a .. b}" by (auto simp: A_def)
    2.35 +    {
    2.36 +      fix x2
    2.37 +      assume a: "a \<le> x2" "x2 \<le> b" and le: "\<forall>x1\<in>{a..<x2}. ?le x1"
    2.38 +      have "?le x2" using `e > 0`
    2.39 +      proof cases
    2.40 +        assume "x2 \<noteq> a" with a have "a < x2" by simp
    2.41 +        have "at x2 within {a <..<x2}\<noteq> bot"
    2.42 +          using `a < x2`
    2.43 +          by (auto simp: trivial_limit_within islimpt_in_closure)
    2.44 +        moreover
    2.45 +        have "((\<lambda>x1. (\<phi> x1 - \<phi> a) + e * (x1 - a) + e) ---> (\<phi> x2 - \<phi> a) + e * (x2 - a) + e) (at x2 within {a <..<x2})"
    2.46 +          "((\<lambda>x1. norm (f x1 - f a)) ---> norm (f x2 - f a)) (at x2 within {a <..<x2})"
    2.47 +          using a
    2.48 +          by (auto intro!: tendsto_eq_intros f_tendsto phi_tendsto
    2.49 +            intro: tendsto_within_subset[where S="{a .. b}"])
    2.50 +        moreover
    2.51 +        have "eventually (\<lambda>x. x > a) (at x2 within {a <..<x2})"
    2.52 +          by (auto simp: eventually_at_filter)
    2.53 +        hence "eventually ?le (at x2 within {a <..<x2})"
    2.54 +          unfolding eventually_at_filter
    2.55 +          by eventually_elim (insert le, auto)
    2.56 +        ultimately
    2.57 +        show ?thesis
    2.58 +          by (rule tendsto_le)
    2.59 +      qed simp
    2.60 +    } note le_cont = this
    2.61 +    have "a \<in> A"
    2.62 +      using assms by (auto simp: A_def)
    2.63 +    hence [simp]: "A \<noteq> {}" by auto
    2.64 +    have A_ivl: "\<And>x1 x2. x2 \<in> A \<Longrightarrow> x1 \<in> {a ..x2} \<Longrightarrow> x1 \<in> A"
    2.65 +      by (simp add: A_def)
    2.66 +    have [simp]: "bdd_above A" by (auto simp: A_def)
    2.67 +    def y \<equiv> "Sup A"
    2.68 +    have "y \<le> b"
    2.69 +      unfolding y_def
    2.70 +      by (simp add: cSup_le_iff) (simp add: A_def)
    2.71 +     have leI: "\<And>x x1. a \<le> x1 \<Longrightarrow> x \<in> A \<Longrightarrow> x1 < x \<Longrightarrow> ?le x1"
    2.72 +       by (auto simp: A_def intro!: le_cont)
    2.73 +    have y_all_le: "\<forall>x1\<in>{a..<y}. ?le x1"
    2.74 +      by (auto simp: y_def less_cSup_iff leI)
    2.75 +    have "a \<le> y"
    2.76 +      by (metis `a \<in> A` `bdd_above A` cSup_upper y_def)
    2.77 +    have "y \<in> A"
    2.78 +      using y_all_le `a \<le> y` `y \<le> b`
    2.79 +      by (auto simp: A_def)
    2.80 +    hence "A = {a .. y}"
    2.81 +      using A_subset
    2.82 +      by (auto simp: subset_iff y_def cSup_upper intro: A_ivl)
    2.83 +    from le_cont[OF `a \<le> y` `y \<le> b` y_all_le] have le_y: "?le y" .
    2.84 +    {
    2.85 +      assume "a \<noteq> y" with `a \<le> y` have "a < y" by simp
    2.86 +      have "y = b"
    2.87 +      proof (rule ccontr)
    2.88 +        assume "y \<noteq> b"
    2.89 +        hence "y < b" using `y \<le> b` by simp
    2.90 +        let ?F = "at y within {y..<b}"
    2.91 +        from f' phi'
    2.92 +        have "(f has_vector_derivative f' y) ?F"
    2.93 +          and "(\<phi> has_vector_derivative \<phi>' y) ?F"
    2.94 +          using `a < y` `y < b`
    2.95 +          by (auto simp add: at_within_open[of _ "{a<..<b}"] has_vector_derivative_def
    2.96 +            intro!: has_derivative_subset[where s="{a<..<b}" and t="{y..<b}"])
    2.97 +        hence "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \<le> e2 * \<bar>x1 - y\<bar>"
    2.98 +            "\<forall>\<^sub>F x1 in ?F. norm (\<phi> x1 - \<phi> y - (x1 - y) *\<^sub>R \<phi>' y) \<le> e2 * \<bar>x1 - y\<bar>"
    2.99 +          using `e2 > 0`
   2.100 +          by (auto simp: has_derivative_within_alt2 has_vector_derivative_def)
   2.101 +        moreover
   2.102 +        have "\<forall>\<^sub>F x1 in ?F. y \<le> x1" "\<forall>\<^sub>F x1 in ?F. x1 < b"
   2.103 +          by (auto simp: eventually_at_filter)
   2.104 +        ultimately
   2.105 +        have "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y) \<le> (\<phi> x1 - \<phi> y) + e * \<bar>x1 - y\<bar>"
   2.106 +          (is "\<forall>\<^sub>F x1 in ?F. ?le' x1")
   2.107 +        proof eventually_elim
   2.108 +          case elim
   2.109 +          from norm_triangle_ineq2[THEN order_trans, OF elim(1)]
   2.110 +          have "norm (f x1 - f y) \<le> norm (f' y) * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
   2.111 +            by (simp add: ac_simps)
   2.112 +          also have "norm (f' y) \<le> \<phi>' y" using bnd `a < y` `y < b` by simp
   2.113 +          also
   2.114 +          from elim have "\<phi>' y * \<bar>x1 - y\<bar> \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar>"
   2.115 +            by (simp add: ac_simps)
   2.116 +          finally
   2.117 +          have "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
   2.118 +            by (auto simp: mult_right_mono)
   2.119 +          thus ?case by (simp add: e2_def)
   2.120 +        qed
   2.121 +        moreover have "?le' y" by simp
   2.122 +        ultimately obtain S
   2.123 +        where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..<b} \<Longrightarrow> ?le' x"
   2.124 +          unfolding eventually_at_topological
   2.125 +          by metis
   2.126 +        from `open S` obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
   2.127 +          by (force simp: dist_commute open_real_def ball_def
   2.128 +            dest!: bspec[OF _ `y \<in> S`])
   2.129 +        def d' \<equiv> "min ((y + b)/2) (y + (d/2))"
   2.130 +        have "d' \<in> A"
   2.131 +          unfolding A_def
   2.132 +        proof safe
   2.133 +          show "a \<le> d'" using `a < y` `0 < d` `y < b` by (simp add: d'_def)
   2.134 +          show "d' \<le> b" using `y < b` by (simp add: d'_def min_def)
   2.135 +          fix x1
   2.136 +          assume x1: "x1 \<in> {a..<d'}"
   2.137 +          {
   2.138 +            assume "x1 < y"
   2.139 +            hence "?le x1"
   2.140 +              using `x1 \<in> {a..<d'}` y_all_le by auto
   2.141 +          } moreover {
   2.142 +            assume "x1 \<ge> y"
   2.143 +            hence x1': "x1 \<in> S" "x1 \<in> {y..<b}" using x1
   2.144 +              by (auto simp: d'_def dist_real_def intro!: d)
   2.145 +            have "norm (f x1 - f a) \<le> norm (f x1 - f y) + norm (f y - f a)"
   2.146 +              by (rule order_trans[OF _ norm_triangle_ineq]) simp
   2.147 +            also note S(3)[OF x1']
   2.148 +            also note le_y
   2.149 +            finally have "?le x1"
   2.150 +              using `x1 \<ge> y` by (auto simp: algebra_simps)
   2.151 +          } ultimately show "?le x1" by arith
   2.152 +        qed
   2.153 +        hence "d' \<le> y"
   2.154 +          unfolding y_def
   2.155 +          by (rule cSup_upper) simp
   2.156 +        thus False using `d > 0` `y < b`
   2.157 +          by (simp add: d'_def min_def split: split_if_asm)
   2.158 +      qed
   2.159 +    } moreover {
   2.160 +      assume "a = y"
   2.161 +      with `a < b` have "y < b" by simp
   2.162 +      with `a = y` f_cont phi_cont `e2 > 0`
   2.163 +      have 1: "\<forall>\<^sub>F x in at y within {y..b}. dist (f x) (f y) < e2"
   2.164 +       and 2: "\<forall>\<^sub>F x in at y within {y..b}. dist (\<phi> x) (\<phi> y) < e2"
   2.165 +        by (auto simp: continuous_on_def tendsto_iff)
   2.166 +      have 3: "eventually (\<lambda>x. y < x) (at y within {y..b})"
   2.167 +        by (auto simp: eventually_at_filter)
   2.168 +      have 4: "eventually (\<lambda>x::real. x < b) (at y within {y..b})"
   2.169 +        using _ `y < b`
   2.170 +        by (rule order_tendstoD) (auto intro!: tendsto_eq_intros)
   2.171 +      from 1 2 3 4
   2.172 +      have eventually_le: "eventually (\<lambda>x. ?le x) (at y within {y .. b})"
   2.173 +      proof eventually_elim
   2.174 +        case (elim x1)
   2.175 +        have "norm (f x1 - f a) = norm (f x1 - f y)"
   2.176 +          by (simp add: `a = y`)
   2.177 +        also have "norm (f x1 - f y) \<le> e2"
   2.178 +          using elim `a = y` by (auto simp : dist_norm intro!:  less_imp_le)
   2.179 +        also have "\<dots> \<le> e2 + (\<phi> x1 - \<phi> a + e2 + e * (x1 - a))"
   2.180 +          using `0 < e` elim
   2.181 +          by (intro add_increasing2[OF add_nonneg_nonneg order.refl])
   2.182 +            (auto simp: `a = y` dist_norm intro!: mult_nonneg_nonneg)
   2.183 +        also have "\<dots> = \<phi> x1 - \<phi> a + e * (x1 - a) + e"
   2.184 +          by (simp add: e2_def)
   2.185 +        finally show "?le x1" .
   2.186 +      qed
   2.187 +      from this[unfolded eventually_at_topological] `?le y`
   2.188 +      obtain S
   2.189 +      where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
   2.190 +        by metis
   2.191 +      from `open S` obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
   2.192 +        by (force simp: dist_commute open_real_def ball_def
   2.193 +          dest!: bspec[OF _ `y \<in> S`])
   2.194 +      def d' \<equiv> "min b (y + (d/2))"
   2.195 +      have "d' \<in> A"
   2.196 +        unfolding A_def
   2.197 +      proof safe
   2.198 +        show "a \<le> d'" using `a = y` `0 < d` `y < b` by (simp add: d'_def)
   2.199 +        show "d' \<le> b" by (simp add: d'_def)
   2.200 +        fix x1
   2.201 +        assume "x1 \<in> {a..<d'}"
   2.202 +        hence "x1 \<in> S" "x1 \<in> {y..b}"
   2.203 +          by (auto simp: `a = y` d'_def dist_real_def intro!: d )
   2.204 +        thus "?le x1"
   2.205 +          by (rule S)
   2.206 +      qed
   2.207 +      hence "d' \<le> y"
   2.208 +        unfolding y_def
   2.209 +        by (rule cSup_upper) simp
   2.210 +      hence "y = b" using `d > 0` `y < b`
   2.211 +        by (simp add: d'_def)
   2.212 +    } ultimately have "y = b"
   2.213 +      by auto
   2.214 +    with le_y have "norm (f b - f a) \<le> \<phi> b - \<phi> a + e * (b - a + 1)"
   2.215 +      by (simp add: algebra_simps)
   2.216 +  } note * = this
   2.217 +  {
   2.218 +    fix e::real assume "e > 0"
   2.219 +    hence "norm (f b - f a) \<le> \<phi> b - \<phi> a + e"
   2.220 +      using *[of "e / (b - a + 1)"] `a < b` by simp
   2.221 +  } thus ?thesis
   2.222 +    by (rule field_le_epsilon)
   2.223 +qed
   2.224  
   2.225  lemma differentiable_bound:
   2.226 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
   2.227 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   2.228    assumes "convex s"
   2.229      and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)"
   2.230      and "\<forall>x\<in>s. onorm (f' x) \<le> B"
   2.231 @@ -791,14 +1006,15 @@
   2.232    shows "norm (f x - f y) \<le> B * norm (x - y)"
   2.233  proof -
   2.234    let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
   2.235 +  let ?\<phi> = "\<lambda>h. h * B * norm (x - y)"
   2.236    have *: "\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s"
   2.237      using assms(1)[unfolded convex_alt,rule_format,OF x y]
   2.238      unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
   2.239      by (auto simp add: algebra_simps)
   2.240 -  then have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
   2.241 +  have 0: "continuous_on (?p ` {0..1}) f"
   2.242 +    using *
   2.243 +    unfolding continuous_on_eq_continuous_within
   2.244      apply -
   2.245 -    apply (rule continuous_intros)+
   2.246 -    unfolding continuous_on_eq_continuous_within
   2.247      apply rule
   2.248      apply (rule differentiable_imp_continuous_within)
   2.249      unfolding differentiable_def
   2.250 @@ -807,51 +1023,93 @@
   2.251      apply (rule assms(2)[rule_format])
   2.252      apply auto
   2.253      done
   2.254 -  have 2: "\<forall>u\<in>{0 <..< 1}.
   2.255 -    ((f \<circ> ?p) has_derivative f' (x + u *\<^sub>R (y - x)) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u)"
   2.256 -  proof rule
   2.257 -    case goal1
   2.258 -    let ?u = "x + u *\<^sub>R (y - x)"
   2.259 +  from * have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
   2.260 +    by (intro continuous_intros 0)+
   2.261 +  {
   2.262 +    fix u::real assume u: "u \<in>{0 <..< 1}"
   2.263 +    let ?u = "?p u"
   2.264 +    interpret linear "(f' ?u)"
   2.265 +      using u by (auto intro!: has_derivative_linear assms(2)[rule_format] *)
   2.266      have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
   2.267        apply (rule diff_chain_within)
   2.268        apply (rule derivative_intros)+
   2.269        apply (rule has_derivative_within_subset)
   2.270        apply (rule assms(2)[rule_format])
   2.271 -      using goal1 *
   2.272 +      using u *
   2.273        apply auto
   2.274        done
   2.275 -    then show ?case
   2.276 -      by (simp add: has_derivative_within_open[OF goal1 open_greaterThanLessThan])
   2.277 -  qed
   2.278 -  obtain u where u:
   2.279 -      "u \<in> {0<..<1}"
   2.280 -      "norm ((f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 1 - (f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 0)
   2.281 -        \<le> norm ((f' (x + u *\<^sub>R (y - x)) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (1 - 0))"
   2.282 -    using mvt_general[OF zero_less_one 1 2] ..
   2.283 -  have **: "\<And>x y. x \<in> s \<Longrightarrow> norm (f' x y) \<le> B * norm y"
   2.284 -  proof -
   2.285 -    case goal1
   2.286 -    have "norm (f' x y) \<le> onorm (f' x) * norm y"
   2.287 -      by (rule onorm[OF has_derivative_bounded_linear[OF assms(2)[rule_format,OF goal1]]])
   2.288 -    also have "\<dots> \<le> B * norm y"
   2.289 -      apply (rule mult_right_mono)
   2.290 -      using assms(3)[rule_format,OF goal1]
   2.291 -      apply (auto simp add: field_simps)
   2.292 -      done
   2.293 -    finally show ?case
   2.294 -      by simp
   2.295 -  qed
   2.296 +    hence "((f \<circ> ?p) has_vector_derivative f' ?u (y - x)) (at u)"
   2.297 +      by (simp add: has_derivative_within_open[OF u open_greaterThanLessThan]
   2.298 +        scaleR has_vector_derivative_def o_def)
   2.299 +  } note 2 = this
   2.300 +  {
   2.301 +    have "continuous_on {0..1} ?\<phi>"
   2.302 +      by (rule continuous_intros)+
   2.303 +  } note 3 = this
   2.304 +  {
   2.305 +    fix u::real assume u: "u \<in>{0 <..< 1}"
   2.306 +    have "(?\<phi> has_vector_derivative B * norm (x - y)) (at u)"
   2.307 +      by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
   2.308 +  } note 4 = this
   2.309 +  {
   2.310 +    fix u::real assume u: "u \<in>{0 <..< 1}"
   2.311 +    let ?u = "?p u"
   2.312 +    interpret bounded_linear "(f' ?u)"
   2.313 +      using u by (auto intro!: has_derivative_bounded_linear assms(2)[rule_format] *)
   2.314 +    have "norm (f' ?u (y - x)) \<le> onorm (f' ?u) * norm (y - x)"
   2.315 +      by (rule onorm) fact
   2.316 +    also have "onorm (f' ?u) \<le> B"
   2.317 +      using u by (auto intro!: assms(3)[rule_format] *)
   2.318 +    finally have "norm ((f' ?u) (y - x)) \<le> B * norm (x - y)"
   2.319 +      by (simp add: mult_right_mono norm_minus_commute)
   2.320 +  } note 5 = this
   2.321    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)"
   2.322      by (auto simp add: norm_minus_commute)
   2.323 -  also have "\<dots> \<le> norm (f' (x + u *\<^sub>R (y - x)) (y - x))"
   2.324 -    using u by auto
   2.325 -  also have "\<dots> \<le> B * norm(y - x)"
   2.326 -    apply (rule **)
   2.327 -    using * and u
   2.328 -    apply auto
   2.329 -    done
   2.330 -  finally show ?thesis
   2.331 -    by (auto simp add: norm_minus_commute)
   2.332 +  also
   2.333 +  from differentiable_bound_general[OF zero_less_one 1, OF 3 2 4 5]
   2.334 +  have "norm ((f \<circ> ?p) 1 - (f \<circ> ?p) 0) \<le> B * norm (x - y)"
   2.335 +    by simp
   2.336 +  finally show ?thesis .
   2.337 +qed
   2.338 +
   2.339 +lemma
   2.340 +  differentiable_bound_segment:
   2.341 +  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   2.342 +  assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R a \<in> G"
   2.343 +  assumes f': "\<And>x. x \<in> G \<Longrightarrow> (f has_derivative f' x) (at x within G)"
   2.344 +  assumes B: "\<forall>x\<in>{0..1}. onorm (f' (x0 + x *\<^sub>R a)) \<le> B"
   2.345 +  shows "norm (f (x0 + a) - f x0) \<le> norm a * B"
   2.346 +proof -
   2.347 +  let ?G = "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}"
   2.348 +  have "?G = op + x0 ` (\<lambda>x. x *\<^sub>R a) ` {0..1}" by auto
   2.349 +  also have "convex \<dots>"
   2.350 +    by (intro convex_translation convex_scaled convex_real_interval)
   2.351 +  finally have "convex ?G" .
   2.352 +  moreover have "?G \<subseteq> G" "x0 \<in> ?G" "x0 + a \<in> ?G" using assms by (auto intro: image_eqI[where x=1])
   2.353 +  ultimately show ?thesis
   2.354 +    using has_derivative_subset[OF f' `?G \<subseteq> G`] B
   2.355 +      differentiable_bound[of "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}" f f' B "x0 + a" x0]
   2.356 +    by (auto simp: ac_simps)
   2.357 +qed
   2.358 +
   2.359 +lemma differentiable_bound_linearization:
   2.360 +  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   2.361 +  assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> a + t *\<^sub>R (b - a) \<in> S"
   2.362 +  assumes f'[derivative_intros]: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
   2.363 +  assumes B: "\<forall>x\<in>S. onorm (f' x - f' x0) \<le> B"
   2.364 +  assumes "x0 \<in> S"
   2.365 +  shows "norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B"
   2.366 +proof -
   2.367 +  def g \<equiv> "\<lambda>x. f x - f' x0 x"
   2.368 +  have g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative (\<lambda>i. f' x i - f' x0 i)) (at x within S)"
   2.369 +    unfolding g_def using assms
   2.370 +    by (auto intro!: derivative_eq_intros
   2.371 +      bounded_linear.has_derivative[OF has_derivative_bounded_linear, OF f'])
   2.372 +  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"
   2.373 +     using assms by (auto simp: fun_diff_def)
   2.374 +  from differentiable_bound_segment[OF assms(1) g B] `x0 \<in> S`
   2.375 +  show ?thesis
   2.376 +    by (simp add: g_def field_simps linear_sub[OF has_derivative_linear[OF f']])
   2.377  qed
   2.378  
   2.379  text {* In particular. *}