1036 show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by (simp) |
1036 show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by (simp) |
1037 show "DERIV f z :> ((f b - f a)/(b-a))" using derF by simp |
1037 show "DERIV f z :> ((f b - f a)/(b-a))" using derF by simp |
1038 qed |
1038 qed |
1039 qed |
1039 qed |
1040 |
1040 |
|
1041 lemma MVT2: |
|
1042 "[| a < b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |] |
|
1043 ==> \<exists>z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))" |
|
1044 apply (drule MVT) |
|
1045 apply (blast intro: DERIV_isCont) |
|
1046 apply (force dest: order_less_imp_le simp add: differentiable_def) |
|
1047 apply (blast dest: DERIV_unique order_less_imp_le) |
|
1048 done |
|
1049 |
1041 |
1050 |
1042 text{*A function is constant if its derivative is 0 over an interval.*} |
1051 text{*A function is constant if its derivative is 0 over an interval.*} |
1043 |
1052 |
1044 lemma DERIV_isconst_end: |
1053 lemma DERIV_isconst_end: |
1045 fixes f :: "real => real" |
1054 fixes f :: "real => real" |
1070 \<forall>x. a < x & x < b --> DERIV f x :> 0; |
1079 \<forall>x. a < x & x < b --> DERIV f x :> 0; |
1071 a \<le> x; x \<le> b |] |
1080 a \<le> x; x \<le> b |] |
1072 ==> f x = f a" |
1081 ==> f x = f a" |
1073 apply (blast dest: DERIV_isconst1) |
1082 apply (blast dest: DERIV_isconst1) |
1074 done |
1083 done |
|
1084 |
|
1085 lemma DERIV_isconst3: fixes a b x y :: real |
|
1086 assumes "a < b" and "x \<in> {a <..< b}" and "y \<in> {a <..< b}" |
|
1087 assumes derivable: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> DERIV f x :> 0" |
|
1088 shows "f x = f y" |
|
1089 proof (cases "x = y") |
|
1090 case False |
|
1091 let ?a = "min x y" |
|
1092 let ?b = "max x y" |
|
1093 |
|
1094 have "\<forall>z. ?a \<le> z \<and> z \<le> ?b \<longrightarrow> DERIV f z :> 0" |
|
1095 proof (rule allI, rule impI) |
|
1096 fix z :: real assume "?a \<le> z \<and> z \<le> ?b" |
|
1097 hence "a < z" and "z < b" using `x \<in> {a <..< b}` and `y \<in> {a <..< b}` by auto |
|
1098 hence "z \<in> {a<..<b}" by auto |
|
1099 thus "DERIV f z :> 0" by (rule derivable) |
|
1100 qed |
|
1101 hence isCont: "\<forall>z. ?a \<le> z \<and> z \<le> ?b \<longrightarrow> isCont f z" |
|
1102 and DERIV: "\<forall>z. ?a < z \<and> z < ?b \<longrightarrow> DERIV f z :> 0" using DERIV_isCont by auto |
|
1103 |
|
1104 have "?a < ?b" using `x \<noteq> y` by auto |
|
1105 from DERIV_isconst2[OF this isCont DERIV, of x] and DERIV_isconst2[OF this isCont DERIV, of y] |
|
1106 show ?thesis by auto |
|
1107 qed auto |
1075 |
1108 |
1076 lemma DERIV_isconst_all: |
1109 lemma DERIV_isconst_all: |
1077 fixes f :: "real => real" |
1110 fixes f :: "real => real" |
1078 shows "\<forall>x. DERIV f x :> 0 ==> f(x) = f(y)" |
1111 shows "\<forall>x. DERIV f x :> 0 ==> f(x) = f(y)" |
1079 apply (rule linorder_cases [of x y]) |
1112 apply (rule linorder_cases [of x y]) |