equal
deleted
inserted
replaced
1407 assumes lt: "a < b" |
1407 assumes lt: "a < b" |
1408 and contf: "continuous_on {a..b} f" |
1408 and contf: "continuous_on {a..b} f" |
1409 and dif: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> f differentiable (at x)" |
1409 and dif: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> f differentiable (at x)" |
1410 shows "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l" |
1410 shows "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l" |
1411 proof - |
1411 proof - |
1412 obtain f' where derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)" |
1412 obtain f' :: "real \<Rightarrow> real \<Rightarrow> real" |
|
1413 where derf: "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (f has_derivative f' x) (at x)" |
1413 using dif unfolding differentiable_def by metis |
1414 using dif unfolding differentiable_def by metis |
1414 then obtain z where "a < z" "z < b" "f b - f a = (f' z) (b - a)" |
1415 then obtain z where "a < z" "z < b" "f b - f a = (f' z) (b - a)" |
1415 using mvt [OF lt contf] by blast |
1416 using mvt [OF lt contf] by blast |
1416 then show ?thesis |
1417 then show ?thesis |
1417 by (metis derf dif has_derivative_unique has_field_derivative_imp_has_derivative linordered_field_class.sign_simps(5) real_differentiable_def) |
1418 by (simp add: ac_simps) |
|
1419 (metis derf dif has_derivative_unique has_field_derivative_imp_has_derivative real_differentiable_def) |
1418 qed |
1420 qed |
1419 |
1421 |
1420 corollary MVT2: |
1422 corollary MVT2: |
1421 assumes "a < b" and der: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> DERIV f x :> f' x" |
1423 assumes "a < b" and der: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> DERIV f x :> f' x" |
1422 shows "\<exists>z::real. a < z \<and> z < b \<and> (f b - f a = (b - a) * f' z)" |
1424 shows "\<exists>z::real. a < z \<and> z < b \<and> (f b - f a = (b - a) * f' z)" |