author paulson Sun, 20 May 2018 22:10:21 +0100 changeset 68241 39a311f50344 parent 68240 fa63bde6d659 child 68242 4acc029f69e9
correcting the statements of the MVTs
```--- a/src/HOL/Analysis/Derivative.thy	Sun May 20 20:14:30 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Sun May 20 22:10:21 2018 +0100
@@ -638,21 +638,21 @@
lemma mvt_simple:
fixes f :: "real \<Rightarrow> real"
assumes "a < b"
-    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
+    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x within {a..b})"
shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)"
proof (rule mvt)
have "f differentiable_on {a..b}"
-    by (meson atLeastAtMost_iff derf differentiable_at_imp_differentiable_on differentiable_def)
+    using derf unfolding differentiable_on_def differentiable_def by force
then show "continuous_on {a..b} f"
by (rule differentiable_imp_continuous_on)
show "(f has_derivative f' x) (at x)" if "a < x" "x < b" for x
-    by (metis derf not_less order.asym that)
+    by (metis at_within_Icc_at derf leI order.asym that)
qed (rule assms)

lemma mvt_very_simple:
fixes f :: "real \<Rightarrow> real"
assumes "a \<le> b"
-    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
+    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x within {a..b})"
shows "\<exists>x\<in>{a..b}. f b - f a = f' x (b - a)"
proof (cases "a = b")
interpret bounded_linear "f' b"
@@ -2822,8 +2822,7 @@
(if x \<in> S then f' x else g' x)) (at x within u)"
unfolding has_vector_derivative_def assms
using x_in
-  apply (intro has_derivative_If_within_closures[where
-        ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
+  apply (intro has_derivative_If_within_closures[where ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
THEN has_derivative_eq_rhs])
subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption)
subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption)```