Theory 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*real⇒real*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 "(∃t∈Basis→{0<..<1}. (f (a + u) - f a) = (∑i∈Basis. (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 "∀i∈Basis. 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) = (∑i∈Basis. (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: "t∈Basis → {0<..<1}" and
    mvt: "f (a + u) - f a = (∑i∈Basis. (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*real⇒real*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