Theory Ordinary_Differential_Equations.MVT_Ex

theory MVT_Ex
imports
  "HOL-Analysis.Analysis"
  "HOL-Decision_Procs.Approximation"
  "../ODE_Auxiliarities"
begin

subsection ‹(Counter)Example of Mean Value Theorem in Euclidean Space \label{sec:countermvt}›

text ‹There is no exact analogon of the mean value theorem in the multivariate case!›

lemma MVT_wrong: assumes
  "J a u (f::real*realreal*real).
      (x. FDERIV f x :> J x) 
      (t{0<..<1}. f (a + u) - f a = J (a + t *R u) u)"
  shows "False"
proof -
  have "t::real*real. FDERIV (λt. (cos (fst t), sin (fst t))) t :> (λh. (- ((fst h) * sin (fst t)), (fst h) * cos (fst t)))"
    by (auto intro!: derivative_eq_intros)
  from assms[OF this, of "(pi, pi)" "(pi, pi)"] obtain t::real where t: "0 < t" "t < 1" and
    "pi * sin (t * pi) = 2" "cos (t * pi) = 0"
    by auto
  then obtain n where tpi: "t * pi = real_of_int n * (pi / 2)" and "odd n"
    by (auto simp: cos_zero_iff_int)
  then have teq: "t = real_of_int n / 2" by auto
  then have "n = 1" using t odd n by arith
  then have "t = 1/2" using teq by simp
  have "sin (t * pi) = 1"
    by (simp add: t = 1/2 sin_eq_1)
  with pi * sin (t * pi) = 2
  have "pi = 2" by simp
  moreover have "pi > 2" using pi_approx by simp
  ultimately show False by simp
qed

lemma MVT_corrected:
  fixes f::"'a::ordered_euclidean_space'b::euclidean_space"
  assumes fderiv: "x. x  D  (f has_derivative J x) (at x within D)"
  assumes line_in: "x. 0  x; x  1  a + x *R u  D"
  shows "(tBasis{0<..<1}. (f (a + u) - f a) = (iBasis. (J (a + t i *R u) u  i) *R i))"
proof -
  {
    fix i::'b
    assume "i  Basis"
    have subset: "((λx. a + x *R u) ` {0..1})  D"
      using line_in by force
    have "x. 0  x; x  1  ((λb. f (a + b *R u)  i) has_derivative (λb. b *R J (a + x *R u) u  i)) (at x within {0..1})"
      using line_in
      by (auto intro!: derivative_eq_intros
        has_derivative_subset[OF _ subset]
        has_derivative_in_compose[where f="λx. a + x *R u"]
        fderiv line_in
        simp add: linear.scaleR[OF has_derivative_linear[OF fderiv]])
    with zero_less_one
    have "x{0<..<1}. f (a + 1 *R u)  i - f (a + 0 *R u)  i = (1 - 0) *R J (a + x *R u) u  i"
      by (rule mvt_simple)
  }
  then obtain t where "iBasis. t i  {0<..<1}  f (a + u)  i - f a  i = J (a + t i *R u) u  i"
    by atomize_elim (force intro!: bchoice)
  hence "t  Basis  {0<..<1}" "i. i  Basis  (f (a + u) - f a)  i = J (a + t i *R u) u  i"
    by (auto simp: inner_diff_left)
  moreover hence "(f (a + u) - f a) = (iBasis. (J (a + t i *R u) u  i) *R i)"
    by (intro euclidean_eqI[where 'a='b]) simp
  ultimately show ?thesis by blast
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 .. J1}"
  assumes line_in: "x. x  {0..1}  a + x *R u  D"
  shows "f (a + u) - f a  {J0..J1}"
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 .. J1}"
  proof -
    have J: "i. i  Basis  J0  J (a + t i *R u) u"
            "i. i  Basis  J (a + t i *R u) u  J1"
      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:
  shows
  "J J0 J1 a u (f::real*realreal*real).
    (x. FDERIV f x :> J x) 
    (x. J x u  {J0 .. J1}) 
    f (a + u) - f a  {J0 .. J1}"
  by (rule_tac J = J in MVT_ivl[where D=UNIV]) auto

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..J1}"
  assumes line_in: "x. x  {0..1}  b + x *R (a - b)  D"
  shows "f a  {f b + J0..f b + J1}"
proof -
  have "f (b + (a - b)) - f b  {J0 .. J1}"
    using J_ivl MVT_ivl fderiv line_in by blast
  thus ?thesis
    by (auto simp: diff_le_eq le_diff_eq ac_simps)
qed

end