# HG changeset patch # User huffman # Date 1395363333 25200 # Node ID 2a091015a89651715e10bb4b2c94e2dfe481f34e # Parent 9b32aafecec172f0eb6a662de6d396a3380b6c50 tuned proofs diff -r 9b32aafecec1 -r 2a091015a896 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Mar 24 16:33:36 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Mar 20 17:55:33 2014 -0700 @@ -707,22 +707,24 @@ assumes "a < b" and "\x\{a..b}. (f has_derivative f' x) (at x within {a..b})" shows "\x\{a<.. {a <..< b}" - show "(f has_derivative f' x) (at x)" - unfolding has_derivative_within_open[OF x open_greaterThanLessThan,symmetric] - apply (rule has_derivative_within_subset) - apply (rule assms(2)[rule_format]) - using x - apply auto - done -qed (insert assms(2), auto) +proof (rule mvt) + have "f differentiable_on {a..b}" + using assms(2) unfolding differentiable_on_def differentiable_def by fast + then show "continuous_on {a..b} f" + by (rule differentiable_imp_continuous_on) + show "\x\{a<.. {a <..< b}" + show "(f has_derivative f' x) (at x)" + unfolding at_within_open[OF x open_greaterThanLessThan,symmetric] + apply (rule has_derivative_within_subset) + apply (rule assms(2)[rule_format]) + using x + apply auto + done + qed +qed (rule assms(1)) lemma mvt_very_simple: fixes f :: "real \ real" @@ -758,18 +760,16 @@ and "\x\{a<..x\{a<.. norm (f' x (b - a))" proof - - have "\x\{a<.. (f b - f a) \ f) b - (op \ (f b - f a) \ f) a = (f b - f a) \ f' x (b - a)" + have "\x\{a<.. f b - (f b - f a) \ f a = (f b - f a) \ f' x (b - a)" apply (rule mvt) apply (rule assms(1)) - apply (rule continuous_on_inner continuous_on_intros assms(2) ballI)+ - unfolding o_def - apply (rule has_derivative_inner_right) + apply (intro continuous_on_intros assms(2)) using assms(3) - apply auto + apply (fast intro: has_derivative_inner_right) done then obtain x where x: "x \ {a<.. (f b - f a) \ f) b - (op \ (f b - f a) \ f) a = (f b - f a) \ f' x (b - a)" .. + "(f b - f a) \ f b - (f b - f a) \ f a = (f b - f a) \ f' x (b - a)" .. show ?thesis proof (cases "f a = f b") case False @@ -778,9 +778,7 @@ also have "\ = (f b - f a) \ (f b - f a)" unfolding power2_norm_eq_inner .. also have "\ = (f b - f a) \ f' x (b - a)" - using x - unfolding inner_simps - by (auto simp add: inner_diff_left) + using x(2) by (simp only: inner_diff_right) also have "\ \ norm (f b - f a) * norm (f' x (b - a))" by (rule norm_cauchy_schwarz) finally show ?thesis