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
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
`