src/HOL/Analysis/Derivative.thy
changeset 68241 39a311f50344
parent 68239 0764ee22a4d1
child 68527 2f4e2aab190a
equal deleted inserted replaced
68240:fa63bde6d659 68241:39a311f50344
   636 qed
   636 qed
   637 
   637 
   638 lemma mvt_simple:
   638 lemma mvt_simple:
   639   fixes f :: "real \<Rightarrow> real"
   639   fixes f :: "real \<Rightarrow> real"
   640   assumes "a < b"
   640   assumes "a < b"
   641     and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
   641     and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x within {a..b})"
   642   shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)"
   642   shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)"
   643 proof (rule mvt)
   643 proof (rule mvt)
   644   have "f differentiable_on {a..b}"
   644   have "f differentiable_on {a..b}"
   645     by (meson atLeastAtMost_iff derf differentiable_at_imp_differentiable_on differentiable_def)
   645     using derf unfolding differentiable_on_def differentiable_def by force
   646   then show "continuous_on {a..b} f"
   646   then show "continuous_on {a..b} f"
   647     by (rule differentiable_imp_continuous_on)
   647     by (rule differentiable_imp_continuous_on)
   648   show "(f has_derivative f' x) (at x)" if "a < x" "x < b" for x
   648   show "(f has_derivative f' x) (at x)" if "a < x" "x < b" for x
   649     by (metis derf not_less order.asym that)
   649     by (metis at_within_Icc_at derf leI order.asym that)
   650 qed (rule assms)
   650 qed (rule assms)
   651 
   651 
   652 lemma mvt_very_simple:
   652 lemma mvt_very_simple:
   653   fixes f :: "real \<Rightarrow> real"
   653   fixes f :: "real \<Rightarrow> real"
   654   assumes "a \<le> b"
   654   assumes "a \<le> b"
   655     and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
   655     and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x within {a..b})"
   656   shows "\<exists>x\<in>{a..b}. f b - f a = f' x (b - a)"
   656   shows "\<exists>x\<in>{a..b}. f b - f a = f' x (b - a)"
   657 proof (cases "a = b")
   657 proof (cases "a = b")
   658   interpret bounded_linear "f' b"
   658   interpret bounded_linear "f' b"
   659     using assms(2) assms(1) by auto
   659     using assms(2) assms(1) by auto
   660   case True
   660   case True
  2820   assumes connect': "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f' x = g' x"
  2820   assumes connect': "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f' x = g' x"
  2821   shows "((\<lambda>x. if x \<in> S then f x else g x) has_vector_derivative
  2821   shows "((\<lambda>x. if x \<in> S then f x else g x) has_vector_derivative
  2822     (if x \<in> S then f' x else g' x)) (at x within u)"
  2822     (if x \<in> S then f' x else g' x)) (at x within u)"
  2823   unfolding has_vector_derivative_def assms
  2823   unfolding has_vector_derivative_def assms
  2824   using x_in
  2824   using x_in
  2825   apply (intro has_derivative_If_within_closures[where
  2825   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",
  2826         ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
       
  2827         THEN has_derivative_eq_rhs])
  2826         THEN has_derivative_eq_rhs])
  2828   subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption)
  2827   subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption)
  2829   subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption)
  2828   subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption)
  2830   by (auto simp: assms)
  2829   by (auto simp: assms)
  2831 
  2830