author immler Tue May 05 18:45:10 2015 +0200 (2015-05-05) changeset 60178 f620c70f9e9b parent 60177 2bfcb83531c6 child 60179 d87c8c2d4938
generalized differentiable_bound; some further variations of differentiable_bound
```     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.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.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.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. *}
```