Theory Lib

theory Lib
imports
  Ordinary_Differential_Equations.ODE_Analysis
begin
section ‹Generic Mathematical Lemmas›
text‹General lemmas that don't have anything to do with dL specifically and could be fit for 
  general-purpose libraries, mostly dealing with derivatives, ODEs and vectors.›

lemma vec_extensionality:"(i. v$i = w$i)  (v = w)"
  by (simp add: vec_eq_iff)

lemma norm_axis: "norm (axis i x) = norm x"
  unfolding axis_def norm_vec_def
  unfolding L2_set_def
  by(clarsimp simp add: if_distrib[where f=norm] if_distrib[where f="λx. x2"] sum.If_cases)

lemma bounded_linear_axis: "bounded_linear (axis i)"
proof
  show "axis i (x + y) = axis i x + axis i y" "axis i (r *R x) = r *R axis i x" for x y :: "'a" and r
    by (auto simp: vec_eq_iff axis_def)
  show "K. x::'a. norm (axis i x)  norm x * K"
    by (auto simp add: norm_axis intro!: exI[of _ 1])
qed

lemma bounded_linear_vec:
  fixes f::"('a::finite)  'b::real_normed_vector  'c::real_normed_vector"
  assumes bounds:"i. bounded_linear (f i)"
  shows "bounded_linear (λx. χ i. f i x)"
proof unfold_locales
  fix r x y
  interpret bounded_linear "f i" for i by fact
  show "(χ i. f i (x + y)) = (χ i. f i x) + (χ i. f i y)"
    by (vector add)
  show "(χ i. f i (r *R x)) = r *R (χ i. f i x)"
    by (vector scaleR)
  obtain K where "norm (f i x)  norm x * K i" for x i
    using bounded by metis
  then have "norm (χ i. f i x)  norm x * (iUNIV. K i)" (is "?lhs  ?rhs") for x
    unfolding sum_distrib_left
    unfolding norm_vec_def
    by (auto intro!: L2_set_le_sum_abs[THEN order_trans] sum_mono simp: abs_mult)
  then show "K. x. norm (χ i. f i x)  norm x * K"
    by blast
qed

lift_definition blinfun_vec::"('a::finite  'b::real_normed_vector L real)  'b L (real ^ 'a)" is "(λ(f::('a  'b  real)) (x::'b). χ (i::'a). f i x)"
  by(rule bounded_linear_vec, simp)  

lemmas blinfun_vec_simps[simp] = blinfun_vec.rep_eq

lemma continuous_blinfun_vec:"(i. continuous_on UNIV (blinfun_apply (g i)))  continuous_on UNIV (blinfun_vec g)"
  by (simp add: continuous_on_vec_lambda)  

lemma blinfun_elim:"g. (blinfun_apply (blinfun_vec g)) = (λx. χ i. g i x)"
  using blinfun_vec.rep_eq by auto

lemma sup_plus:
  fixes f g::"('b::metric_space)  real"
  assumes nonempty:"R  {}"
  assumes bddf:"bdd_above (f ` R)"
  assumes bddg:"bdd_above (g ` R)"
  shows "(SUP xR. f x  + g x)  (SUP xR. f x) + (SUP xR. g x)"
proof -
  have bddfg:"bdd_above((λx. f x + g x ) ` R)" 
    using bddf bddg apply (auto simp add: bdd_above_def)
    using add_mono_thms_linordered_semiring(1) by blast
  have eq:"(SUP xR. f x + g x)  (SUP xR. f x) + (SUP xR. g x)
     (xR. (f x + g x)  (SUP xR. f x) + (SUP xR. g x))"
    apply(rule cSUP_le_iff)
     subgoal by (rule nonempty)
    subgoal by (rule bddfg)
    done
  have fs:"x. x  R  f x  (SUP xR. f x)"
    using bddf 
    by (simp add: cSUP_upper)
  have gs:"x. x  R  g x  (SUP xR. g x)"
    using bddg
    by (simp add: cSUP_upper)
  have "(xR. (f x + g x)  (SUP xR. f x) + (SUP xR. g x))"
    apply auto                    
    subgoal for x using fs[of x] gs[of x] by auto
    done
  then show ?thesis by (auto simp add: eq)
qed
     
lemma continuous_blinfun_vec':
  fixes f::"'a::{finite,linorder}  'b::{metric_space, real_normed_vector,abs}  'b L real"
  fixes S::"'b set"
  assumes conts:"i. continuous_on UNIV (f i)"
  shows "continuous_on UNIV (λx. blinfun_vec (λ i. f i x))"
proof (auto simp add:  LIM_def continuous_on_def)
  fix x1 and ε::real
  assume ε:"0 < ε"
  let ?n = "card (UNIV::'a set)"
  have conts':" i x1 ε. 0 < ε  δ>0. x2. x2  x1  dist x2 x1 < δ  dist (f i  x2) (f i x1) < ε"  
    using conts by(auto simp add: LIM_def continuous_on_def)
  have conts'':"i. δ>0. x2. x2  x1  dist x2 x1 < δ  dist (f i  x2) (f i x1) < (ε/?n)"
    subgoal for i using conts'[of "ε / ?n"  x1 i] ε by auto done
  let ?f = "(λx. blinfun_vec (λ i. f i x))"
  let ?Pδ = "(λ i δ. (δ>0  (x2. x2  x1  dist x2 x1 < δ  dist (f i  x2) (f i x1) < (ε/?n))))"
  let ?δi = "(λi. SOME δ. ?Pδ i δ)"
  have Ps:"i. δ. ?Pδ i δ" using conts'' by auto
  have Pδi:"i. ?Pδ i (?δi i)"
    subgoal for i using someI[of "?Pδ i" ] Ps[of i] by auto done
  have finU:"finite (UNIV::'a set)" by auto
  let  = "linorder_class.Min  (?δi ` UNIV)"
  have δ0s:"i. ?δi i > 0" using Pδi by blast
  then have δ0s':"i. 0 < ?δi i" by auto
  have bounds:"bdd_below (?δi ` UNIV)" 
    unfolding bdd_below_def 
    using δ0s less_eq_real_def by blast
  have δs:"i.   ?δi i"
    using bounds cINF_lower[of ?δi] by auto
  have finite:"finite ((?δi ` UNIV))" by auto
  have nonempty:"((?δi ` UNIV))  {}" by auto
  have δ:" > 0 " using Min_gr_iff[OF finite nonempty] δ0s' 
    by blast
  have conts''':"i x2. x2  x1  dist x2 x1 < ?δi i  dist (f i  x2) (f i x1) < (ε/?n)"
    subgoal for i x2 
      using conts''[of i] apply auto
      subgoal for δ
        apply(erule allE[where x=x2])
        using Pδi  δs[of i] apply (auto simp add: δs[of i])
        done
      done
    done
  have "x2. x2  x1  dist x2 x1 <   dist (blinfun_vec (λi. f i x2)) (blinfun_vec (λi. f i x1)) < ε"
  proof (auto)
    fix x2
    assume ne:"x2  x1"
    assume dist:"i. dist x2 x1 < ?δi i"
    have dists:"i. dist x2 x1 < ?δi i"
      subgoal for i using dist δs[of i] by auto done
    have euclid:"y. norm(?f x1 y - ?f x2 y) = (L2_set (λi. norm(f i x1 y - f i x2 y)) UNIV)"
      by (simp add: norm_vec_def)
    have finite:"finite (UNIV::'a set)" by auto
    have nonempty: "(UNIV::'a set)  {}" by auto
    have nonemptyB: "(UNIV::'b set)  {}" by auto
    have nonemptyR: "(UNIV::real set)  {}" by auto
    have SUP_leq:"f::('b  real).  g::('b  real).  S::'b set. S  {}  bdd_above (g ` S)  (x. x  (S::'b set)  ((f x)::real)  ((g x)::real))  (SUP xS. f x)  (SUP xS. g x)"
      by(rule cSup_mono, auto)
    have SUP_sum_comm':"R S f . finite (S::'a set)  (R::'d::metric_space set)  {} 
      (i x. ((f i x)::real)  0) 
      (i. bdd_above (f i ` R)) 
      (SUP xR . (i  S. f i x))  (i  S. (SUP xR. f i x))"
    proof -
      fix  R::"'d set" and S ::"('a)set"  and f  ::"'a  'd  real"
      assume non:"R  {} "
      assume fin:"finite S"
      assume every:"(i x. 0  f i x)"
      assume bddF:"i. bdd_above (f i ` R)"
      then have bddF':"i. M. x R. f i x  M "
        unfolding bdd_above_def by auto
      let ?boundP = "(λi M. x R. f i x  M)"
      let ?bound = "(λi::'a. SOME M. x R. f i x  M)"
      have "i. M. ?boundP i M" using bddF' by auto
      then have each_bound:"i. ?boundP i (?bound i)" 
        subgoal for i using someI[of "?boundP i"] by blast done
      let ?bigBound = "(λF. iF. (?bound i))"
      have bddG:"i::'a. F. bdd_above ((λx. iF. f i x) ` R)" 
        subgoal for i F
          using bddF[of i] unfolding bdd_above_def apply auto
          apply(rule exI[where x="?bigBound F"])
          subgoal for M
            apply auto
            subgoal for x
              using each_bound by (simp add: sum_mono)
            done
          done
        done
      show "?thesis R S f" using fin assms
      proof (induct)
        case empty
        have "((SUP xR. i{}. f i x)::real)  (i{}. SUP aR. f i a)"   by (simp add: non)
        then show ?case by auto
      next
        case (insert x F)
        have "((SUP xaR. iinsert x F. f i xa)::real)  (SUP xaR. f x xa +  (iF. f i xa))"
          using insert.hyps(2) by auto
        moreover have "...   (SUP xa R. f x xa) + (SUP xaR. (iF. f i xa))"
          by(rule sup_plus, rule non, rule bddF, rule bddG)
        moreover have "...  (SUP xa R. f x xa) + (iF. SUP aR. f i a)"
          using add_le_cancel_left conts insert.hyps(3) by blast
        moreover have "...  (i(insert x F). SUP aR. f i a)"
          by (simp add: insert.hyps(2))
        ultimately have "((SUP xaR. iinsert x F. f i xa)::real)  (i(insert x F). SUP aR. f i a)"
          by linarith
        then show ?case by auto
      qed
    qed
    have SUP_sum_comm:"R S y1 y2 . finite (S::'a set)  (R::'b set)  {}  (SUP xR . (i  S. norm(f i y1 x - f i y2 x)/norm(x)))  (i  S. (SUP xR. norm(f i y1 x - f i y2 x)/norm(x)))"
      apply(rule SUP_sum_comm')
         apply(auto)[3]
      proof (unfold bdd_above_def)
        fix R S y1 y2 i
          { fix rr :: "real  real"
            obtain bb :: "real  ('b  real)  'b set  'b" where
              ff1: "r f B. r  f ` B  f (bb r f B) = r"
              unfolding image_iff by moura
            { assume "r. ¬ rr r  norm (f i y1 - f i y2)"
              then have "r. norm (blinfun_apply (f i y1) (bb (rr r) (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) R) - blinfun_apply (f i y2) (bb (rr r) (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) R)) / norm (bb (rr r) (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) R)  rr r"
                by (metis (no_types) le_norm_blinfun minus_blinfun.rep_eq)
              then have "r. rr r  r  rr r  (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) ` R"
                using ff1 by meson }
              then have "r. rr r  r  rr r  (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) ` R"
                by blast }
        then show "r. ra(λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) ` R. ra  r"
          by meson
      qed
    have SUM_leq:"S::('a) set.  f g ::('a  real). S  {}  finite S  (x. x  S  f x < g x)  (xS. f x) < (xS. g x)"
      by(rule sum_strict_mono, auto)
    have L2:"f S. L2_set (λx. norm(f x)) S  (x  S. norm(f x))"
      using L2_set_le_sum norm_ge_zero by metis
    have L2':"y. (L2_set (λi. norm(f i x1 y - f i x2 y)) UNIV)/norm(y)  (iUNIV. norm(f i x1 y - f i x2 y))/norm(y)"
      subgoal for y
        using L2[of "(λ x. f x x1 y - f x x2 y)" UNIV]
        by (auto simp add: divide_right_mono)
      done
    have "i. (SUP yUNIV.  norm((f i x1 - f i x2) y)/norm(y)) = norm(f i x1 - f i x2)"
      by (simp add: onorm_def norm_blinfun.rep_eq)
    then have each_norm:"i. (SUP yUNIV.  norm(f i x1 y - f i x2 y)/norm(y)) = norm(f i x1 - f i x2)"
      by (metis (no_types, lifting) SUP_cong blinfun.diff_left)
    have bounded_linear:"i. bounded_linear (λy. f i x1 y - f i x2 y)" 
      by (simp add: blinfun.bounded_linear_right bounded_linear_sub)
    have each_bound:"i. bdd_above ((λy. norm(f i x1 y - f i x2 y)/norm(y)) ` UNIV)"
      using bounded_linear unfolding bdd_above_def
    proof -
      fix i :: 'a
      { fix rr :: "real  real"
        have "a r. norm (blinfun_apply (f a x1) r - blinfun_apply (f a x2) r) / norm r  norm (f a x1 - f a x2)"
          by (metis le_norm_blinfun minus_blinfun.rep_eq)
        then have "r R. r  (λr. norm (blinfun_apply (f i x1) r - blinfun_apply (f i x2) r) / norm r) ` R  r  norm (f i x1 - f i x2)"
          by blast
        then have "r. rr r  r  rr r  range (λr. norm (blinfun_apply (f i x1) r - blinfun_apply (f i x2) r) / norm r)"
          by blast }
      then show "r. rarange (λr. norm (blinfun_apply (f i x1) r - blinfun_apply (f i x2) r) / norm r). ra  r"
        by meson
    qed
    have bdd_above:"(bdd_above ((λy. (iUNIV. norm(f i x1 y - f i x2 y)/norm(y))) ` UNIV))"
      using each_bound unfolding bdd_above_def apply auto
    proof -
      assume each:"(i. M. x. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x  M)"
      let ?boundP = "(λi M. x. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x  M)"
      let ?bound = "(λi. SOME x. ?boundP i x)"
      have bounds:"i. ?boundP i (?bound i)"
        subgoal for i using each someI[of "?boundP i"] by blast done
      let ?bigBound = "i(UNIV::'a set). ?bound i"
      show "M. x. (iUNIV. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x)  M"
        apply(rule exI[where x= ?bigBound])
        by(auto simp add: bounds sum_mono) 
    qed
    have bdd_above:"(bdd_above ((λy. (iUNIV. norm(f i x1 y - f i x2 y))/norm(y)) ` UNIV))"
      using bdd_above unfolding bdd_above_def apply auto
    proof -
      fix M :: real
      assume a1: "x. (iUNIV. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x)  M"
      { fix bb :: "real  'b"
        have "b. (aUNIV. ¦blinfun_apply (f a x1) b - blinfun_apply (f a x2) b¦) / norm b  M"
          using a1 by (simp add: sum_divide_distrib)
        then have "r. (aUNIV. ¦blinfun_apply (f a x1) (bb r) - blinfun_apply (f a x2) (bb r)¦) / norm (bb r)  r"
          by blast }
      then show "r. b. (aUNIV. ¦blinfun_apply (f a x1) b - blinfun_apply (f a x2) b¦) / norm b  r"
        by meson
    qed 
    have "dist (?f x2) (?f x1) = norm((?f x2) - (?f x1))"
      by (simp add: dist_blinfun_def)
    moreover have "... = (SUP yUNIV. norm(?f x1 y - ?f x2 y)/norm(y))"
      by (metis (no_types, lifting) SUP_cong blinfun.diff_left norm_blinfun.rep_eq norm_minus_commute onorm_def)
    moreover have "... = (SUP yUNIV. (L2_set (λi. norm(f i x1 y - f i x2 y)) UNIV)/norm(y))"
      using  euclid by auto
    moreover have "...  (SUP yUNIV. (iUNIV. norm(f i x1 y - f i x2 y))/norm(y))"
      using L2' SUP_cong SUP_leq bdd_above by auto
    moreover have "... = (SUP yUNIV. (iUNIV. norm(f i x1 y - f i x2 y)/norm(y)))"
      by (simp add: sum_divide_distrib)
    moreover have "...  (iUNIV. (SUP yUNIV.  norm(f i x1 y - f i x2 y)/norm(y)))"
      by(rule SUP_sum_comm[OF finite  nonemptyB, of x1 x2]) 
    moreover have "... = (iUNIV. norm(f i x1 - f i x2))"
      using each_norm by simp
    moreover have "... = (iUNIV. dist(f i x1) (f i x2))"
      by (simp add: dist_blinfun_def)
    moreover have "... < (i(UNIV::'a set). ε / ?n)"
      using conts'''[OF ne dists] using SUM_leq[OF nonempty, of "(λi.  dist (f i x1) (f i x2))" "(λi.  ε / ?n)"]
      by (simp add: dist_commute)
    moreover have "... = ε"
      by(auto)
    ultimately show "dist (?f x2) (?f x1) < ε"
      by linarith
  qed
  then show "s>0. x2. x2  x1  dist x2 x1 < s  dist (blinfun_vec (λi. f i x2)) (blinfun_vec (λi. f i x1)) < ε"
    using δ by blast
qed

lemma has_derivative_vec[derivative_intros]:
  assumes "i. ((λx. f i x) has_derivative (λh. f' i h)) F"
  shows "((λx. χ i. f i x) has_derivative (λh. χ i. f' i h)) F"
proof -
  have *: "(χ i. f i x) = (iUNIV. axis i (f i x))" "(χ i. f' i x) = (iUNIV. axis i (f' i x))" for x
    by (simp_all add: axis_def sum.If_cases vec_eq_iff)
  show ?thesis
    unfolding *
    by (intro has_derivative_sum bounded_linear.has_derivative[OF bounded_linear_axis] assms)
qed

lemma has_derivative_proj:
  fixes j::"('a::finite)" 
  fixes f::"'a  real  real"
  assumes assm:"((λx. χ i. f i x) has_derivative (λh. χ i. f' i h)) F"
  shows "((λx. f j x) has_derivative (λh. f' j h)) F"
proof -
  have bounded_proj:"bounded_linear (λ x::(real^'a). x $ j)"
    by (simp add: bounded_linear_vec_nth)
  show "?thesis"
    using bounded_linear.has_derivative[OF bounded_proj, of "(λx. χ i. f i x)" "(λh. χ i. f' i h)", OF assm]
    by auto
qed

lemma has_derivative_proj':
  fixes i::"'a::finite"
  shows "x. ((λ x. x $ i) has_derivative (λx::(real^'a). x $ i)) (at x)"
proof -
  have bounded_proj:"bounded_linear (λ x::(real^'a). x $ i)"
    by (simp add: bounded_linear_vec_nth)
  show "?thesis"
    using bounded_proj unfolding has_derivative_def by auto
qed

lemma constant_when_zero:
  fixes v::"real  (real, 'i::finite) vec"
  assumes x0: "(v t0) $ i = x0"
  assumes sol: "(v solves_ode f) T S"
  assumes f0: "s x. s  T  f s x $ i = 0"
  assumes t0:"t0  T"
  assumes t:"t  T"
  assumes convex:"convex T"
  shows "v t $ i = x0"
proof -
  from solves_odeD[OF sol]
  have deriv: "(v has_vderiv_on (λt. f t (v t))) T" by simp
  then have "((λt. v t $ i) has_vderiv_on (λt. 0)) T"
    using f0
    by (auto simp: has_vderiv_on_def has_vector_derivative_def cart_eq_inner_axis
      intro!: derivative_eq_intros)
  from has_vderiv_on_zero_constant[OF convex this]
  obtain c where c:"x. x  T  v x $ i = c" by blast
  with x0 have "c = x0" "v t $ i = c"
    using t t0 c x0 by blast+
  then show ?thesis by simp
qed

lemma
  solves_ode_subset:
  assumes x: "(x solves_ode f) T X"
  assumes s: "S  T"
  shows "(x solves_ode f) S X"
  apply(rule solves_odeI)
   using has_vderiv_on_subset s solves_ode_vderivD x apply force
  using assms by (auto intro!: solves_odeI dest!: solves_ode_domainD)

lemma
  solves_ode_supset_range:
  assumes x: "(x solves_ode f) T X"
  assumes y: "X  Y"
  shows "(x solves_ode f) T Y"
  apply(rule solves_odeI)
   using has_vderiv_on_subset y solves_ode_vderivD x apply force
  using assms by (auto intro!: solves_odeI dest!: solves_ode_domainD)

lemma
  usolves_ode_subset:
  assumes x: "(x usolves_ode f from t0) T X"
  assumes s: "S  T"
  assumes t0: "t0  S"
  assumes S: "is_interval S"
  shows "(x usolves_ode f from t0) S X"
proof (rule usolves_odeI)
  note usolves_odeD[OF x]
  show "(x solves_ode f) S X" by (rule solves_ode_subset; fact)
  show "t0  S" "is_interval S" by(fact+)
  fix z t
  assume s: "{t0 -- t}  S" and z: "(z solves_ode f) {t0 -- t} X" and z0: "z t0 = x t0"
  then have "t0  {t0 -- t}" "is_interval {t0 -- t}"
    by auto
  moreover note s
  moreover have "(z solves_ode f) {t0--t} X"
    using solves_odeD[OF z] S  T
    by (intro solves_ode_subset_range[OF z]) force
  moreover note z0
  moreover have "t  {t0 -- t}" by simp
  ultimately show "z t = x t"
    by (meson z ta T'. t0  T'; is_interval T'; T'  T; (z solves_ode f) T' X; z t0 = x t0; ta  T'  z ta = x ta assms(2) dual_order.trans)
qed

― ‹Example of using lemmas above to show a lemma that could be useful for dL: The constant ODE›
― ‹0 does not change the state.›
lemma example:
  fixes x t::real and i::"('sz::finite)"
  assumes "t > 0"
  shows "x = (ll_on_open.flow UNIV (λt. λx. χ (i::('sz::finite)). 0) UNIV 0 (χ i. x) t) $ i"
proof -
  let ?T = UNIV
  let ?f = "(λt. λx. χ i::('sz::finite). 0)"
  let ?X = UNIV
  let ?t0.0 = 0
  let ?x0.0 = "χ i::('sz::finite). x"
  interpret ll: ll_on_open "UNIV" "(λt x. χ i::('sz::finite). 0)" UNIV
    using gt_ex
    by unfold_locales
      (auto simp: interval_def continuous_on_def local_lipschitz_def intro!: lipschitz_intros)
  have foo1:"?t0.0  ?T" by auto
  have foo2:"?x0.0  ?X" by auto
  let ?v = "ll.flow  ?t0.0 ?x0.0"
  from ll.flow_solves_ode[OF foo1 foo2]
  have solves:"(ll.flow  ?t0.0 ?x0.0 solves_ode ?f) (ll.existence_ivl  ?t0.0 ?x0.0) ?X"  by (auto)
  then have solves:"(?v solves_ode ?f) (ll.existence_ivl  ?t0.0 ?x0.0) ?X" by auto
  have thex0: "(?v ?t0.0) $ (i::('sz::finite)) = x" by auto
  have sol_help: "(?v solves_ode ?f) (ll.existence_ivl  ?t0.0 ?x0.0) ?X" using solves by auto
  have ivl:"ll.existence_ivl ?t0.0 ?x0.0 = UNIV"
    by (rule ll.existence_ivl_eq_domain)
       (auto intro!: exI[where x=0] simp: vec_eq_iff)
  have sol: "(?v solves_ode ?f) UNIV ?X" using solves ivl by auto
  have thef0: "t x. ?f t x $ i = 0" by auto
  from constant_when_zero [OF thex0 sol thef0]
  have "?v t $ i = x"
    by auto
  thus ?thesis by auto
 qed
 
lemma MVT_ivl:
  fixes f::"'a::ordered_euclidean_space'b::ordered_euclidean_space"
  assumes fderiv: "x. x  D  (f has_derivative J x) (at x within D)"
  assumes J_ivl: "x. x  D  J x u  J0"
  assumes line_in: "x. x  {0..1}  a + x *R u  D"
  shows "f (a + u) - f a  J0"
proof -
  from MVT_corrected[OF fderiv line_in] obtain t where
    t: "tBasis  {0<..<1}" and
    mvt: "f (a + u) - f a = (iBasis. (J (a + t i *R u) u  i) *R i)"
    by auto
  note mvt
  also have "  J0"
  proof -
    have J: "i. i  Basis  J0  J (a + t i *R u) u"
      using J_ivl t line_in by (auto simp: Pi_iff)
    show ?thesis
      using J
      unfolding atLeastAtMost_iff eucl_le[where 'a='b]
      by auto
  qed
  finally show ?thesis .
qed

lemma MVT_ivl':
  fixes f::"'a::ordered_euclidean_space'b::ordered_euclidean_space"
  assumes fderiv: "(x. x  D  (f has_derivative J x) (at x within D))"
  assumes J_ivl: "x. x  D  J x (a - b)  J0"
  assumes line_in: "x. x  {0..1}  b + x *R (a - b)  D"
  shows "f a  f b + J0"
proof -
  have "f (b + (a - b)) - f b  J0"
    apply (rule MVT_ivl[OF fderiv ])
      apply assumption
     apply (rule J_ivl) apply assumption
    using line_in
    apply (auto simp: diff_le_eq le_diff_eq ac_simps)
    done
  thus ?thesis
    by (auto simp: diff_le_eq le_diff_eq ac_simps)
qed
end