src/HOL/Analysis/Derivative.thy
 changeset 68241 39a311f50344 parent 68239 0764ee22a4d1 child 68527 2f4e2aab190a
equal 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 `