1253 |
1253 |
1254 lemma DERIV_inverse_function: |
1254 lemma DERIV_inverse_function: |
1255 fixes f g :: "real \<Rightarrow> real" |
1255 fixes f g :: "real \<Rightarrow> real" |
1256 assumes der: "DERIV f (g x) :> D" |
1256 assumes der: "DERIV f (g x) :> D" |
1257 assumes neq: "D \<noteq> 0" |
1257 assumes neq: "D \<noteq> 0" |
1258 assumes e: "0 < e" |
1258 assumes a: "a < x" and b: "x < b" |
1259 assumes inj: "\<forall>y. \<bar>y - x\<bar> \<le> e \<longrightarrow> f (g y) = y" |
1259 assumes inj: "\<forall>y. a < y \<and> y < b \<longrightarrow> f (g y) = y" |
1260 assumes cont: "isCont g x" |
1260 assumes cont: "isCont g x" |
1261 shows "DERIV g x :> inverse D" |
1261 shows "DERIV g x :> inverse D" |
1262 unfolding DERIV_iff2 |
1262 unfolding DERIV_iff2 |
1263 proof (rule LIM_equal2 [OF e]) |
1263 proof (rule LIM_equal2) |
|
1264 show "0 < min (x - a) (b - x)" |
|
1265 using a b by simp |
|
1266 next |
1264 fix y |
1267 fix y |
1265 assume "y \<noteq> x" and "norm (y - x) < e" |
1268 assume "norm (y - x) < min (x - a) (b - x)" |
|
1269 hence "a < y" and "y < b" |
|
1270 by (simp_all add: abs_less_iff) |
1266 thus "(g y - g x) / (y - x) = |
1271 thus "(g y - g x) / (y - x) = |
1267 inverse ((f (g y) - x) / (g y - g x))" |
1272 inverse ((f (g y) - x) / (g y - g x))" |
1268 by (simp add: inj) |
1273 by (simp add: inj) |
1269 next |
1274 next |
1270 have "(\<lambda>z. (f z - f (g x)) / (z - g x)) -- g x --> D" |
1275 have "(\<lambda>z. (f z - f (g x)) / (z - g x)) -- g x --> D" |
1271 by (rule der [unfolded DERIV_iff2]) |
1276 by (rule der [unfolded DERIV_iff2]) |
1272 hence 1: "(\<lambda>z. (f z - x) / (z - g x)) -- g x --> D" |
1277 hence 1: "(\<lambda>z. (f z - x) / (z - g x)) -- g x --> D" |
1273 using inj e by simp |
1278 using inj a b by simp |
1274 have 2: "\<exists>d>0. \<forall>y. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow> g y \<noteq> g x" |
1279 have 2: "\<exists>d>0. \<forall>y. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow> g y \<noteq> g x" |
1275 proof (safe intro!: exI) |
1280 proof (safe intro!: exI) |
1276 show "0 < e" using e . |
1281 show "0 < min (x - a) (b - x)" |
|
1282 using a b by simp |
1277 next |
1283 next |
1278 fix y |
1284 fix y |
1279 assume y: "norm (y - x) < e" |
1285 assume "norm (y - x) < min (x - a) (b - x)" |
|
1286 hence y: "a < y" "y < b" |
|
1287 by (simp_all add: abs_less_iff) |
1280 assume "g y = g x" |
1288 assume "g y = g x" |
1281 hence "f (g y) = f (g x)" by simp |
1289 hence "f (g y) = f (g x)" by simp |
1282 hence "y = x" using inj y by simp |
1290 hence "y = x" using inj y a b by simp |
1283 also assume "y \<noteq> x" |
1291 also assume "y \<noteq> x" |
1284 finally show False by simp |
1292 finally show False by simp |
1285 qed |
1293 qed |
1286 have "(\<lambda>y. (f (g y) - x) / (g y - g x)) -- x --> D" |
1294 have "(\<lambda>y. (f (g y) - x) / (g y - g x)) -- x --> D" |
1287 using cont 1 2 by (rule isCont_LIM_compose2) |
1295 using cont 1 2 by (rule isCont_LIM_compose2) |