src/HOL/Deriv.thy
 author hoelzl Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) changeset 51481 ef949192e5d6 parent 51480 3793c3a11378 child 51526 155263089e7b permissions -rw-r--r--
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
 huffman@21164 ` 1` ```(* Title : Deriv.thy ``` huffman@21164 ` 2` ``` Author : Jacques D. Fleuriot ``` huffman@21164 ` 3` ``` Copyright : 1998 University of Cambridge ``` huffman@21164 ` 4` ``` Conversion to Isar and new proofs by Lawrence C Paulson, 2004 ``` huffman@21164 ` 5` ``` GMVT by Benjamin Porter, 2005 ``` huffman@21164 ` 6` ```*) ``` huffman@21164 ` 7` huffman@21164 ` 8` ```header{* Differentiation *} ``` huffman@21164 ` 9` huffman@21164 ` 10` ```theory Deriv ``` huffman@29987 ` 11` ```imports Lim ``` huffman@21164 ` 12` ```begin ``` huffman@21164 ` 13` huffman@22984 ` 14` ```text{*Standard Definitions*} ``` huffman@21164 ` 15` huffman@21164 ` 16` ```definition ``` huffman@21784 ` 17` ``` deriv :: "['a::real_normed_field \ 'a, 'a, 'a] \ bool" ``` huffman@21164 ` 18` ``` --{*Differentiation: D is derivative of function f at x*} ``` wenzelm@21404 ` 19` ``` ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where ``` huffman@21784 ` 20` ``` "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)" ``` huffman@21164 ` 21` huffman@21164 ` 22` ```subsection {* Derivatives *} ``` huffman@21164 ` 23` huffman@21784 ` 24` ```lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)" ``` huffman@21164 ` 25` ```by (simp add: deriv_def) ``` huffman@21164 ` 26` huffman@21784 ` 27` ```lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --> D" ``` huffman@21164 ` 28` ```by (simp add: deriv_def) ``` huffman@21164 ` 29` huffman@21164 ` 30` ```lemma DERIV_const [simp]: "DERIV (\x. k) x :> 0" ``` huffman@44568 ` 31` ``` by (simp add: deriv_def tendsto_const) ``` huffman@21164 ` 32` huffman@23069 ` 33` ```lemma DERIV_ident [simp]: "DERIV (\x. x) x :> 1" ``` huffman@44568 ` 34` ``` by (simp add: deriv_def tendsto_const cong: LIM_cong) ``` huffman@21164 ` 35` huffman@21164 ` 36` ```lemma DERIV_add: ``` huffman@21164 ` 37` ``` "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\x. f x + g x) x :> D + E" ``` huffman@44568 ` 38` ``` by (simp only: deriv_def add_diff_add add_divide_distrib tendsto_add) ``` huffman@21164 ` 39` huffman@21164 ` 40` ```lemma DERIV_minus: ``` huffman@21164 ` 41` ``` "DERIV f x :> D \ DERIV (\x. - f x) x :> - D" ``` huffman@44568 ` 42` ``` by (simp only: deriv_def minus_diff_minus divide_minus_left tendsto_minus) ``` huffman@21164 ` 43` huffman@21164 ` 44` ```lemma DERIV_diff: ``` huffman@21164 ` 45` ``` "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\x. f x - g x) x :> D - E" ``` haftmann@37887 ` 46` ```by (simp only: diff_minus DERIV_add DERIV_minus) ``` huffman@21164 ` 47` huffman@21164 ` 48` ```lemma DERIV_add_minus: ``` huffman@21164 ` 49` ``` "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\x. f x + - g x) x :> D + - E" ``` huffman@21164 ` 50` ```by (simp only: DERIV_add DERIV_minus) ``` huffman@21164 ` 51` huffman@21164 ` 52` ```lemma DERIV_isCont: "DERIV f x :> D \ isCont f x" ``` huffman@21164 ` 53` ```proof (unfold isCont_iff) ``` huffman@21164 ` 54` ``` assume "DERIV f x :> D" ``` huffman@21784 ` 55` ``` hence "(\h. (f(x+h) - f(x)) / h) -- 0 --> D" ``` huffman@21164 ` 56` ``` by (rule DERIV_D) ``` huffman@21784 ` 57` ``` hence "(\h. (f(x+h) - f(x)) / h * h) -- 0 --> D * 0" ``` huffman@44568 ` 58` ``` by (intro tendsto_mult tendsto_ident_at) ``` huffman@21784 ` 59` ``` hence "(\h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0" ``` huffman@21784 ` 60` ``` by simp ``` huffman@21784 ` 61` ``` hence "(\h. f(x+h) - f(x)) -- 0 --> 0" ``` nipkow@23398 ` 62` ``` by (simp cong: LIM_cong) ``` huffman@21164 ` 63` ``` thus "(\h. f(x+h)) -- 0 --> f(x)" ``` huffman@31338 ` 64` ``` by (simp add: LIM_def dist_norm) ``` huffman@21164 ` 65` ```qed ``` huffman@21164 ` 66` huffman@21164 ` 67` ```lemma DERIV_mult_lemma: ``` huffman@21784 ` 68` ``` fixes a b c d :: "'a::real_field" ``` huffman@21784 ` 69` ``` shows "(a * b - c * d) / h = a * ((b - d) / h) + ((a - c) / h) * d" ``` hoelzl@50331 ` 70` ``` by (simp add: field_simps diff_divide_distrib) ``` huffman@21164 ` 71` huffman@21164 ` 72` ```lemma DERIV_mult': ``` huffman@21164 ` 73` ``` assumes f: "DERIV f x :> D" ``` huffman@21164 ` 74` ``` assumes g: "DERIV g x :> E" ``` huffman@21164 ` 75` ``` shows "DERIV (\x. f x * g x) x :> f x * E + D * g x" ``` huffman@21164 ` 76` ```proof (unfold deriv_def) ``` huffman@21164 ` 77` ``` from f have "isCont f x" ``` huffman@21164 ` 78` ``` by (rule DERIV_isCont) ``` huffman@21164 ` 79` ``` hence "(\h. f(x+h)) -- 0 --> f x" ``` huffman@21164 ` 80` ``` by (simp only: isCont_iff) ``` huffman@21784 ` 81` ``` hence "(\h. f(x+h) * ((g(x+h) - g x) / h) + ``` huffman@21784 ` 82` ``` ((f(x+h) - f x) / h) * g x) ``` huffman@21164 ` 83` ``` -- 0 --> f x * E + D * g x" ``` huffman@44568 ` 84` ``` by (intro tendsto_intros DERIV_D f g) ``` huffman@21784 ` 85` ``` thus "(\h. (f(x+h) * g(x+h) - f x * g x) / h) ``` huffman@21164 ` 86` ``` -- 0 --> f x * E + D * g x" ``` huffman@21164 ` 87` ``` by (simp only: DERIV_mult_lemma) ``` huffman@21164 ` 88` ```qed ``` huffman@21164 ` 89` huffman@21164 ` 90` ```lemma DERIV_mult: ``` hoelzl@50331 ` 91` ``` "DERIV f x :> Da \ DERIV g x :> Db \ DERIV (\x. f x * g x) x :> Da * g x + Db * f x" ``` hoelzl@50331 ` 92` ``` by (drule (1) DERIV_mult', simp only: mult_commute add_commute) ``` huffman@21164 ` 93` huffman@21164 ` 94` ```lemma DERIV_unique: ``` hoelzl@50331 ` 95` ``` "DERIV f x :> D \ DERIV f x :> E \ D = E" ``` hoelzl@50331 ` 96` ``` unfolding deriv_def by (rule LIM_unique) ``` huffman@21164 ` 97` huffman@21164 ` 98` ```text{*Differentiation of finite sum*} ``` huffman@21164 ` 99` hoelzl@31880 ` 100` ```lemma DERIV_setsum: ``` hoelzl@31880 ` 101` ``` assumes "finite S" ``` hoelzl@31880 ` 102` ``` and "\ n. n \ S \ DERIV (%x. f x n) x :> (f' x n)" ``` hoelzl@31880 ` 103` ``` shows "DERIV (%x. setsum (f x) S) x :> setsum (f' x) S" ``` hoelzl@31880 ` 104` ``` using assms by induct (auto intro!: DERIV_add) ``` hoelzl@31880 ` 105` huffman@21164 ` 106` ```lemma DERIV_sumr [rule_format (no_asm)]: ``` huffman@21164 ` 107` ``` "(\r. m \ r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) ``` huffman@21164 ` 108` ``` --> DERIV (%x. \n=m.. (\r=m.. 'a" shows ``` huffman@21784 ` 115` ``` "((%h. (f(a + h) - f(a)) / h) -- 0 --> D) = ``` huffman@21164 ` 116` ``` ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)" ``` huffman@21164 ` 117` ```apply (rule iffI) ``` huffman@21164 ` 118` ```apply (drule_tac k="- a" in LIM_offset) ``` huffman@21164 ` 119` ```apply (simp add: diff_minus) ``` huffman@21164 ` 120` ```apply (drule_tac k="a" in LIM_offset) ``` huffman@21164 ` 121` ```apply (simp add: add_commute) ``` huffman@21164 ` 122` ```done ``` huffman@21164 ` 123` huffman@21784 ` 124` ```lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --> D)" ``` huffman@21784 ` 125` ```by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff) ``` huffman@21164 ` 126` huffman@21164 ` 127` ```lemma DERIV_inverse_lemma: ``` huffman@21784 ` 128` ``` "\a \ 0; b \ (0::'a::real_normed_field)\ ``` huffman@21784 ` 129` ``` \ (inverse a - inverse b) / h ``` huffman@21784 ` 130` ``` = - (inverse a * ((a - b) / h) * inverse b)" ``` huffman@21164 ` 131` ```by (simp add: inverse_diff_inverse) ``` huffman@21164 ` 132` huffman@21164 ` 133` ```lemma DERIV_inverse': ``` huffman@21164 ` 134` ``` assumes der: "DERIV f x :> D" ``` huffman@21164 ` 135` ``` assumes neq: "f x \ 0" ``` huffman@21164 ` 136` ``` shows "DERIV (\x. inverse (f x)) x :> - (inverse (f x) * D * inverse (f x))" ``` huffman@21164 ` 137` ``` (is "DERIV _ _ :> ?E") ``` huffman@21164 ` 138` ```proof (unfold DERIV_iff2) ``` huffman@21164 ` 139` ``` from der have lim_f: "f -- x --> f x" ``` huffman@21164 ` 140` ``` by (rule DERIV_isCont [unfolded isCont_def]) ``` huffman@21164 ` 141` huffman@21164 ` 142` ``` from neq have "0 < norm (f x)" by simp ``` huffman@21164 ` 143` ``` with LIM_D [OF lim_f] obtain s ``` huffman@21164 ` 144` ``` where s: "0 < s" ``` huffman@21164 ` 145` ``` and less_fx: "\z. \z \ x; norm (z - x) < s\ ``` huffman@21164 ` 146` ``` \ norm (f z - f x) < norm (f x)" ``` huffman@21164 ` 147` ``` by fast ``` huffman@21164 ` 148` huffman@21784 ` 149` ``` show "(\z. (inverse (f z) - inverse (f x)) / (z - x)) -- x --> ?E" ``` huffman@21164 ` 150` ``` proof (rule LIM_equal2 [OF s]) ``` huffman@21784 ` 151` ``` fix z ``` huffman@21164 ` 152` ``` assume "z \ x" "norm (z - x) < s" ``` huffman@21164 ` 153` ``` hence "norm (f z - f x) < norm (f x)" by (rule less_fx) ``` huffman@21164 ` 154` ``` hence "f z \ 0" by auto ``` huffman@21784 ` 155` ``` thus "(inverse (f z) - inverse (f x)) / (z - x) = ``` huffman@21784 ` 156` ``` - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x))" ``` huffman@21164 ` 157` ``` using neq by (rule DERIV_inverse_lemma) ``` huffman@21164 ` 158` ``` next ``` huffman@21784 ` 159` ``` from der have "(\z. (f z - f x) / (z - x)) -- x --> D" ``` huffman@21164 ` 160` ``` by (unfold DERIV_iff2) ``` huffman@21784 ` 161` ``` thus "(\z. - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x))) ``` huffman@21164 ` 162` ``` -- x --> ?E" ``` huffman@44568 ` 163` ``` by (intro tendsto_intros lim_f neq) ``` huffman@21164 ` 164` ``` qed ``` huffman@21164 ` 165` ```qed ``` huffman@21164 ` 166` huffman@21164 ` 167` ```lemma DERIV_divide: ``` huffman@21784 ` 168` ``` "\DERIV f x :> D; DERIV g x :> E; g x \ 0\ ``` huffman@21784 ` 169` ``` \ DERIV (\x. f x / g x) x :> (D * g x - f x * E) / (g x * g x)" ``` huffman@21164 ` 170` ```apply (subgoal_tac "f x * - (inverse (g x) * E * inverse (g x)) + ``` huffman@21164 ` 171` ``` D * inverse (g x) = (D * g x - f x * E) / (g x * g x)") ``` huffman@21164 ` 172` ```apply (erule subst) ``` huffman@21164 ` 173` ```apply (unfold divide_inverse) ``` huffman@21164 ` 174` ```apply (erule DERIV_mult') ``` huffman@21164 ` 175` ```apply (erule (1) DERIV_inverse') ``` nipkow@23477 ` 176` ```apply (simp add: ring_distribs nonzero_inverse_mult_distrib) ``` huffman@21164 ` 177` ```done ``` huffman@21164 ` 178` huffman@21164 ` 179` ```lemma DERIV_power_Suc: ``` haftmann@31017 ` 180` ``` fixes f :: "'a \ 'a::{real_normed_field}" ``` huffman@21164 ` 181` ``` assumes f: "DERIV f x :> D" ``` huffman@23431 ` 182` ``` shows "DERIV (\x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)" ``` huffman@21164 ` 183` ```proof (induct n) ``` huffman@21164 ` 184` ```case 0 ``` huffman@30273 ` 185` ``` show ?case by (simp add: f) ``` huffman@21164 ` 186` ```case (Suc k) ``` huffman@21164 ` 187` ``` from DERIV_mult' [OF f Suc] show ?case ``` nipkow@23477 ` 188` ``` apply (simp only: of_nat_Suc ring_distribs mult_1_left) ``` nipkow@29667 ` 189` ``` apply (simp only: power_Suc algebra_simps) ``` huffman@21164 ` 190` ``` done ``` huffman@21164 ` 191` ```qed ``` huffman@21164 ` 192` huffman@21164 ` 193` ```lemma DERIV_power: ``` haftmann@31017 ` 194` ``` fixes f :: "'a \ 'a::{real_normed_field}" ``` huffman@21164 ` 195` ``` assumes f: "DERIV f x :> D" ``` huffman@21784 ` 196` ``` shows "DERIV (\x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))" ``` huffman@30273 ` 197` ```by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc) ``` huffman@21164 ` 198` huffman@29975 ` 199` ```text {* Caratheodory formulation of derivative at a point *} ``` huffman@21164 ` 200` huffman@21164 ` 201` ```lemma CARAT_DERIV: ``` huffman@21164 ` 202` ``` "(DERIV f x :> l) = ``` huffman@21784 ` 203` ``` (\g. (\z. f z - f x = g z * (z-x)) & isCont g x & g x = l)" ``` huffman@21164 ` 204` ``` (is "?lhs = ?rhs") ``` huffman@21164 ` 205` ```proof ``` huffman@21164 ` 206` ``` assume der: "DERIV f x :> l" ``` huffman@21784 ` 207` ``` show "\g. (\z. f z - f x = g z * (z-x)) \ isCont g x \ g x = l" ``` huffman@21164 ` 208` ``` proof (intro exI conjI) ``` huffman@21784 ` 209` ``` let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))" ``` nipkow@23413 ` 210` ``` show "\z. f z - f x = ?g z * (z-x)" by simp ``` huffman@21164 ` 211` ``` show "isCont ?g x" using der ``` huffman@21164 ` 212` ``` by (simp add: isCont_iff DERIV_iff diff_minus ``` huffman@21164 ` 213` ``` cong: LIM_equal [rule_format]) ``` huffman@21164 ` 214` ``` show "?g x = l" by simp ``` huffman@21164 ` 215` ``` qed ``` huffman@21164 ` 216` ```next ``` huffman@21164 ` 217` ``` assume "?rhs" ``` huffman@21164 ` 218` ``` then obtain g where ``` huffman@21784 ` 219` ``` "(\z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast ``` huffman@21164 ` 220` ``` thus "(DERIV f x :> l)" ``` nipkow@23413 ` 221` ``` by (auto simp add: isCont_iff DERIV_iff cong: LIM_cong) ``` huffman@21164 ` 222` ```qed ``` huffman@21164 ` 223` huffman@21164 ` 224` ```lemma DERIV_chain': ``` huffman@21164 ` 225` ``` assumes f: "DERIV f x :> D" ``` huffman@21164 ` 226` ``` assumes g: "DERIV g (f x) :> E" ``` huffman@21784 ` 227` ``` shows "DERIV (\x. g (f x)) x :> E * D" ``` huffman@21164 ` 228` ```proof (unfold DERIV_iff2) ``` huffman@21784 ` 229` ``` obtain d where d: "\y. g y - g (f x) = d y * (y - f x)" ``` huffman@21164 ` 230` ``` and cont_d: "isCont d (f x)" and dfx: "d (f x) = E" ``` huffman@21164 ` 231` ``` using CARAT_DERIV [THEN iffD1, OF g] by fast ``` huffman@21164 ` 232` ``` from f have "f -- x --> f x" ``` huffman@21164 ` 233` ``` by (rule DERIV_isCont [unfolded isCont_def]) ``` huffman@21164 ` 234` ``` with cont_d have "(\z. d (f z)) -- x --> d (f x)" ``` huffman@44568 ` 235` ``` by (rule isCont_tendsto_compose) ``` huffman@21784 ` 236` ``` hence "(\z. d (f z) * ((f z - f x) / (z - x))) ``` huffman@21784 ` 237` ``` -- x --> d (f x) * D" ``` huffman@44568 ` 238` ``` by (rule tendsto_mult [OF _ f [unfolded DERIV_iff2]]) ``` huffman@21784 ` 239` ``` thus "(\z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D" ``` huffman@35216 ` 240` ``` by (simp add: d dfx) ``` huffman@21164 ` 241` ```qed ``` huffman@21164 ` 242` wenzelm@31899 ` 243` ```text {* ``` wenzelm@31899 ` 244` ``` Let's do the standard proof, though theorem ``` wenzelm@31899 ` 245` ``` @{text "LIM_mult2"} follows from a NS proof ``` wenzelm@31899 ` 246` ```*} ``` huffman@21164 ` 247` huffman@21164 ` 248` ```lemma DERIV_cmult: ``` huffman@21164 ` 249` ``` "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D" ``` huffman@21164 ` 250` ```by (drule DERIV_mult' [OF DERIV_const], simp) ``` huffman@21164 ` 251` paulson@33654 ` 252` ```lemma DERIV_cdivide: "DERIV f x :> D ==> DERIV (%x. f x / c) x :> D / c" ``` paulson@33654 ` 253` ``` apply (subgoal_tac "DERIV (%x. (1 / c) * f x) x :> (1 / c) * D", force) ``` paulson@33654 ` 254` ``` apply (erule DERIV_cmult) ``` paulson@33654 ` 255` ``` done ``` paulson@33654 ` 256` wenzelm@31899 ` 257` ```text {* Standard version *} ``` huffman@21164 ` 258` ```lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db" ``` huffman@35216 ` 259` ```by (drule (1) DERIV_chain', simp add: o_def mult_commute) ``` huffman@21164 ` 260` huffman@21164 ` 261` ```lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db" ``` huffman@21164 ` 262` ```by (auto dest: DERIV_chain simp add: o_def) ``` huffman@21164 ` 263` wenzelm@31899 ` 264` ```text {* Derivative of linear multiplication *} ``` huffman@21164 ` 265` ```lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c" ``` huffman@23069 ` 266` ```by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp) ``` huffman@21164 ` 267` huffman@21164 ` 268` ```lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))" ``` huffman@23069 ` 269` ```apply (cut_tac DERIV_power [OF DERIV_ident]) ``` huffman@35216 ` 270` ```apply (simp add: real_of_nat_def) ``` huffman@21164 ` 271` ```done ``` huffman@21164 ` 272` wenzelm@31899 ` 273` ```text {* Power of @{text "-1"} *} ``` huffman@21164 ` 274` huffman@21784 ` 275` ```lemma DERIV_inverse: ``` haftmann@31017 ` 276` ``` fixes x :: "'a::{real_normed_field}" ``` huffman@21784 ` 277` ``` shows "x \ 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))" ``` huffman@30273 ` 278` ```by (drule DERIV_inverse' [OF DERIV_ident]) simp ``` huffman@21164 ` 279` wenzelm@31899 ` 280` ```text {* Derivative of inverse *} ``` huffman@21784 ` 281` ```lemma DERIV_inverse_fun: ``` haftmann@31017 ` 282` ``` fixes x :: "'a::{real_normed_field}" ``` huffman@21784 ` 283` ``` shows "[| DERIV f x :> d; f(x) \ 0 |] ``` huffman@21784 ` 284` ``` ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))" ``` huffman@30273 ` 285` ```by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib) ``` huffman@21164 ` 286` wenzelm@31899 ` 287` ```text {* Derivative of quotient *} ``` huffman@21784 ` 288` ```lemma DERIV_quotient: ``` haftmann@31017 ` 289` ``` fixes x :: "'a::{real_normed_field}" ``` huffman@21784 ` 290` ``` shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \ 0 |] ``` huffman@21784 ` 291` ``` ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))" ``` huffman@30273 ` 292` ```by (drule (2) DERIV_divide) (simp add: mult_commute) ``` huffman@21164 ` 293` wenzelm@31899 ` 294` ```text {* @{text "DERIV_intros"} *} ``` wenzelm@31899 ` 295` ```ML {* ``` wenzelm@31902 ` 296` ```structure Deriv_Intros = Named_Thms ``` wenzelm@31899 ` 297` ```( ``` wenzelm@45294 ` 298` ``` val name = @{binding DERIV_intros} ``` wenzelm@31899 ` 299` ``` val description = "DERIV introduction rules" ``` wenzelm@31899 ` 300` ```) ``` wenzelm@31899 ` 301` ```*} ``` hoelzl@31880 ` 302` wenzelm@31902 ` 303` ```setup Deriv_Intros.setup ``` hoelzl@31880 ` 304` hoelzl@31880 ` 305` ```lemma DERIV_cong: "\ DERIV f x :> X ; X = Y \ \ DERIV f x :> Y" ``` hoelzl@31880 ` 306` ``` by simp ``` hoelzl@31880 ` 307` hoelzl@31880 ` 308` ```declare ``` hoelzl@31880 ` 309` ``` DERIV_const[THEN DERIV_cong, DERIV_intros] ``` hoelzl@31880 ` 310` ``` DERIV_ident[THEN DERIV_cong, DERIV_intros] ``` hoelzl@31880 ` 311` ``` DERIV_add[THEN DERIV_cong, DERIV_intros] ``` hoelzl@31880 ` 312` ``` DERIV_minus[THEN DERIV_cong, DERIV_intros] ``` hoelzl@31880 ` 313` ``` DERIV_mult[THEN DERIV_cong, DERIV_intros] ``` hoelzl@31880 ` 314` ``` DERIV_diff[THEN DERIV_cong, DERIV_intros] ``` hoelzl@31880 ` 315` ``` DERIV_inverse'[THEN DERIV_cong, DERIV_intros] ``` hoelzl@31880 ` 316` ``` DERIV_divide[THEN DERIV_cong, DERIV_intros] ``` hoelzl@31880 ` 317` ``` DERIV_power[where 'a=real, THEN DERIV_cong, ``` hoelzl@31880 ` 318` ``` unfolded real_of_nat_def[symmetric], DERIV_intros] ``` hoelzl@31880 ` 319` ``` DERIV_setsum[THEN DERIV_cong, DERIV_intros] ``` huffman@22984 ` 320` wenzelm@31899 ` 321` huffman@22984 ` 322` ```subsection {* Differentiability predicate *} ``` huffman@21164 ` 323` huffman@29169 ` 324` ```definition ``` huffman@29169 ` 325` ``` differentiable :: "['a::real_normed_field \ 'a, 'a] \ bool" ``` huffman@29169 ` 326` ``` (infixl "differentiable" 60) where ``` huffman@29169 ` 327` ``` "f differentiable x = (\D. DERIV f x :> D)" ``` huffman@29169 ` 328` huffman@29169 ` 329` ```lemma differentiableE [elim?]: ``` huffman@29169 ` 330` ``` assumes "f differentiable x" ``` huffman@29169 ` 331` ``` obtains df where "DERIV f x :> df" ``` wenzelm@41550 ` 332` ``` using assms unfolding differentiable_def .. ``` huffman@29169 ` 333` huffman@21164 ` 334` ```lemma differentiableD: "f differentiable x ==> \D. DERIV f x :> D" ``` huffman@21164 ` 335` ```by (simp add: differentiable_def) ``` huffman@21164 ` 336` huffman@21164 ` 337` ```lemma differentiableI: "DERIV f x :> D ==> f differentiable x" ``` huffman@21164 ` 338` ```by (force simp add: differentiable_def) ``` huffman@21164 ` 339` huffman@29169 ` 340` ```lemma differentiable_ident [simp]: "(\x. x) differentiable x" ``` huffman@29169 ` 341` ``` by (rule DERIV_ident [THEN differentiableI]) ``` huffman@29169 ` 342` huffman@29169 ` 343` ```lemma differentiable_const [simp]: "(\z. a) differentiable x" ``` huffman@29169 ` 344` ``` by (rule DERIV_const [THEN differentiableI]) ``` huffman@21164 ` 345` huffman@29169 ` 346` ```lemma differentiable_compose: ``` huffman@29169 ` 347` ``` assumes f: "f differentiable (g x)" ``` huffman@29169 ` 348` ``` assumes g: "g differentiable x" ``` huffman@29169 ` 349` ``` shows "(\x. f (g x)) differentiable x" ``` huffman@29169 ` 350` ```proof - ``` huffman@29169 ` 351` ``` from `f differentiable (g x)` obtain df where "DERIV f (g x) :> df" .. ``` huffman@29169 ` 352` ``` moreover ``` huffman@29169 ` 353` ``` from `g differentiable x` obtain dg where "DERIV g x :> dg" .. ``` huffman@29169 ` 354` ``` ultimately ``` huffman@29169 ` 355` ``` have "DERIV (\x. f (g x)) x :> df * dg" by (rule DERIV_chain2) ``` huffman@29169 ` 356` ``` thus ?thesis by (rule differentiableI) ``` huffman@29169 ` 357` ```qed ``` huffman@29169 ` 358` huffman@29169 ` 359` ```lemma differentiable_sum [simp]: ``` huffman@21164 ` 360` ``` assumes "f differentiable x" ``` huffman@21164 ` 361` ``` and "g differentiable x" ``` huffman@21164 ` 362` ``` shows "(\x. f x + g x) differentiable x" ``` huffman@21164 ` 363` ```proof - ``` huffman@29169 ` 364` ``` from `f differentiable x` obtain df where "DERIV f x :> df" .. ``` huffman@29169 ` 365` ``` moreover ``` huffman@29169 ` 366` ``` from `g differentiable x` obtain dg where "DERIV g x :> dg" .. ``` huffman@29169 ` 367` ``` ultimately ``` huffman@29169 ` 368` ``` have "DERIV (\x. f x + g x) x :> df + dg" by (rule DERIV_add) ``` huffman@29169 ` 369` ``` thus ?thesis by (rule differentiableI) ``` huffman@29169 ` 370` ```qed ``` huffman@29169 ` 371` huffman@29169 ` 372` ```lemma differentiable_minus [simp]: ``` huffman@29169 ` 373` ``` assumes "f differentiable x" ``` huffman@29169 ` 374` ``` shows "(\x. - f x) differentiable x" ``` huffman@29169 ` 375` ```proof - ``` huffman@29169 ` 376` ``` from `f differentiable x` obtain df where "DERIV f x :> df" .. ``` huffman@29169 ` 377` ``` hence "DERIV (\x. - f x) x :> - df" by (rule DERIV_minus) ``` huffman@29169 ` 378` ``` thus ?thesis by (rule differentiableI) ``` huffman@21164 ` 379` ```qed ``` huffman@21164 ` 380` huffman@29169 ` 381` ```lemma differentiable_diff [simp]: ``` huffman@21164 ` 382` ``` assumes "f differentiable x" ``` huffman@29169 ` 383` ``` assumes "g differentiable x" ``` huffman@21164 ` 384` ``` shows "(\x. f x - g x) differentiable x" ``` wenzelm@41550 ` 385` ``` unfolding diff_minus using assms by simp ``` huffman@29169 ` 386` huffman@29169 ` 387` ```lemma differentiable_mult [simp]: ``` huffman@29169 ` 388` ``` assumes "f differentiable x" ``` huffman@29169 ` 389` ``` assumes "g differentiable x" ``` huffman@29169 ` 390` ``` shows "(\x. f x * g x) differentiable x" ``` huffman@21164 ` 391` ```proof - ``` huffman@29169 ` 392` ``` from `f differentiable x` obtain df where "DERIV f x :> df" .. ``` huffman@21164 ` 393` ``` moreover ``` huffman@29169 ` 394` ``` from `g differentiable x` obtain dg where "DERIV g x :> dg" .. ``` huffman@29169 ` 395` ``` ultimately ``` huffman@29169 ` 396` ``` have "DERIV (\x. f x * g x) x :> df * g x + dg * f x" by (rule DERIV_mult) ``` huffman@29169 ` 397` ``` thus ?thesis by (rule differentiableI) ``` huffman@21164 ` 398` ```qed ``` huffman@21164 ` 399` huffman@29169 ` 400` ```lemma differentiable_inverse [simp]: ``` huffman@29169 ` 401` ``` assumes "f differentiable x" and "f x \ 0" ``` huffman@29169 ` 402` ``` shows "(\x. inverse (f x)) differentiable x" ``` huffman@21164 ` 403` ```proof - ``` huffman@29169 ` 404` ``` from `f differentiable x` obtain df where "DERIV f x :> df" .. ``` huffman@29169 ` 405` ``` hence "DERIV (\x. inverse (f x)) x :> - (inverse (f x) * df * inverse (f x))" ``` huffman@29169 ` 406` ``` using `f x \ 0` by (rule DERIV_inverse') ``` huffman@29169 ` 407` ``` thus ?thesis by (rule differentiableI) ``` huffman@21164 ` 408` ```qed ``` huffman@21164 ` 409` huffman@29169 ` 410` ```lemma differentiable_divide [simp]: ``` huffman@29169 ` 411` ``` assumes "f differentiable x" ``` huffman@29169 ` 412` ``` assumes "g differentiable x" and "g x \ 0" ``` huffman@29169 ` 413` ``` shows "(\x. f x / g x) differentiable x" ``` wenzelm@41550 ` 414` ``` unfolding divide_inverse using assms by simp ``` huffman@29169 ` 415` huffman@29169 ` 416` ```lemma differentiable_power [simp]: ``` haftmann@31017 ` 417` ``` fixes f :: "'a::{real_normed_field} \ 'a" ``` huffman@29169 ` 418` ``` assumes "f differentiable x" ``` huffman@29169 ` 419` ``` shows "(\x. f x ^ n) differentiable x" ``` wenzelm@41550 ` 420` ``` apply (induct n) ``` wenzelm@41550 ` 421` ``` apply simp ``` wenzelm@41550 ` 422` ``` apply (simp add: assms) ``` wenzelm@41550 ` 423` ``` done ``` huffman@29169 ` 424` huffman@22984 ` 425` huffman@21164 ` 426` ```subsection {* Nested Intervals and Bisection *} ``` huffman@21164 ` 427` hoelzl@51477 ` 428` ```lemma nested_sequence_unique: ``` hoelzl@51477 ` 429` ``` assumes "\n. f n \ f (Suc n)" "\n. g (Suc n) \ g n" "\n. f n \ g n" "(\n. f n - g n) ----> 0" ``` hoelzl@51477 ` 430` ``` shows "\l::real. ((\n. f n \ l) \ f ----> l) \ ((\n. l \ g n) \ g ----> l)" ``` hoelzl@51477 ` 431` ```proof - ``` hoelzl@51477 ` 432` ``` have "incseq f" unfolding incseq_Suc_iff by fact ``` hoelzl@51477 ` 433` ``` have "decseq g" unfolding decseq_Suc_iff by fact ``` huffman@21164 ` 434` hoelzl@51477 ` 435` ``` { fix n ``` hoelzl@51477 ` 436` ``` from `decseq g` have "g n \ g 0" by (rule decseqD) simp ``` hoelzl@51477 ` 437` ``` with `\n. f n \ g n`[THEN spec, of n] have "f n \ g 0" by auto } ``` hoelzl@51477 ` 438` ``` then obtain u where "f ----> u" "\i. f i \ u" ``` hoelzl@51477 ` 439` ``` using incseq_convergent[OF `incseq f`] by auto ``` hoelzl@51477 ` 440` ``` moreover ``` hoelzl@51477 ` 441` ``` { fix n ``` hoelzl@51477 ` 442` ``` from `incseq f` have "f 0 \ f n" by (rule incseqD) simp ``` hoelzl@51477 ` 443` ``` with `\n. f n \ g n`[THEN spec, of n] have "f 0 \ g n" by simp } ``` hoelzl@51477 ` 444` ``` then obtain l where "g ----> l" "\i. l \ g i" ``` hoelzl@51477 ` 445` ``` using decseq_convergent[OF `decseq g`] by auto ``` hoelzl@51477 ` 446` ``` moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF `f ----> u` `g ----> l`]] ``` hoelzl@51477 ` 447` ``` ultimately show ?thesis by auto ``` hoelzl@51477 ` 448` ```qed ``` huffman@21164 ` 449` hoelzl@51476 ` 450` ```lemma Bolzano[consumes 1, case_names trans local]: ``` hoelzl@51476 ` 451` ``` fixes P :: "real \ real \ bool" ``` hoelzl@51476 ` 452` ``` assumes [arith]: "a \ b" ``` hoelzl@51476 ` 453` ``` assumes trans: "\a b c. \P a b; P b c; a \ b; b \ c\ \ P a c" ``` hoelzl@51476 ` 454` ``` assumes local: "\x. a \ x \ x \ b \ \d>0. \a b. a \ x \ x \ b \ b - a < d \ P a b" ``` hoelzl@51476 ` 455` ``` shows "P a b" ``` hoelzl@51476 ` 456` ```proof - ``` hoelzl@51476 ` 457` ``` def bisect \ "nat_rec (a, b) (\n (x, y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2))" ``` hoelzl@51476 ` 458` ``` def l \ "\n. fst (bisect n)" and u \ "\n. snd (bisect n)" ``` hoelzl@51476 ` 459` ``` have l[simp]: "l 0 = a" "\n. l (Suc n) = (if P (l n) ((l n + u n) / 2) then (l n + u n) / 2 else l n)" ``` hoelzl@51476 ` 460` ``` and u[simp]: "u 0 = b" "\n. u (Suc n) = (if P (l n) ((l n + u n) / 2) then u n else (l n + u n) / 2)" ``` hoelzl@51476 ` 461` ``` by (simp_all add: l_def u_def bisect_def split: prod.split) ``` huffman@21164 ` 462` hoelzl@51476 ` 463` ``` { fix n have "l n \ u n" by (induct n) auto } note this[simp] ``` huffman@21164 ` 464` hoelzl@51476 ` 465` ``` have "\x. ((\n. l n \ x) \ l ----> x) \ ((\n. x \ u n) \ u ----> x)" ``` hoelzl@51477 ` 466` ``` proof (safe intro!: nested_sequence_unique) ``` hoelzl@51476 ` 467` ``` fix n show "l n \ l (Suc n)" "u (Suc n) \ u n" by (induct n) auto ``` hoelzl@51476 ` 468` ``` next ``` hoelzl@51476 ` 469` ``` { fix n have "l n - u n = (a - b) / 2^n" by (induct n) (auto simp: field_simps) } ``` hoelzl@51476 ` 470` ``` then show "(\n. l n - u n) ----> 0" by (simp add: LIMSEQ_divide_realpow_zero) ``` hoelzl@51476 ` 471` ``` qed fact ``` hoelzl@51476 ` 472` ``` then obtain x where x: "\n. l n \ x" "\n. x \ u n" and "l ----> x" "u ----> x" by auto ``` hoelzl@51476 ` 473` ``` obtain d where "0 < d" and d: "\a b. a \ x \ x \ b \ b - a < d \ P a b" ``` hoelzl@51476 ` 474` ``` using `l 0 \ x` `x \ u 0` local[of x] by auto ``` huffman@21164 ` 475` hoelzl@51476 ` 476` ``` show "P a b" ``` hoelzl@51476 ` 477` ``` proof (rule ccontr) ``` hoelzl@51476 ` 478` ``` assume "\ P a b" ``` hoelzl@51476 ` 479` ``` { fix n have "\ P (l n) (u n)" ``` hoelzl@51476 ` 480` ``` proof (induct n) ``` hoelzl@51476 ` 481` ``` case (Suc n) with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case by auto ``` hoelzl@51476 ` 482` ``` qed (simp add: `\ P a b`) } ``` hoelzl@51476 ` 483` ``` moreover ``` hoelzl@51476 ` 484` ``` { have "eventually (\n. x - d / 2 < l n) sequentially" ``` hoelzl@51476 ` 485` ``` using `0 < d` `l ----> x` by (intro order_tendstoD[of _ x]) auto ``` hoelzl@51476 ` 486` ``` moreover have "eventually (\n. u n < x + d / 2) sequentially" ``` hoelzl@51476 ` 487` ``` using `0 < d` `u ----> x` by (intro order_tendstoD[of _ x]) auto ``` hoelzl@51476 ` 488` ``` ultimately have "eventually (\n. P (l n) (u n)) sequentially" ``` hoelzl@51476 ` 489` ``` proof eventually_elim ``` hoelzl@51476 ` 490` ``` fix n assume "x - d / 2 < l n" "u n < x + d / 2" ``` hoelzl@51476 ` 491` ``` from add_strict_mono[OF this] have "u n - l n < d" by simp ``` hoelzl@51476 ` 492` ``` with x show "P (l n) (u n)" by (rule d) ``` hoelzl@51476 ` 493` ``` qed } ``` hoelzl@51476 ` 494` ``` ultimately show False by simp ``` hoelzl@51476 ` 495` ``` qed ``` huffman@21164 ` 496` ```qed ``` huffman@21164 ` 497` huffman@21164 ` 498` ```(*HOL style here: object-level formulations*) ``` huffman@21164 ` 499` ```lemma IVT_objl: "(f(a::real) \ (y::real) & y \ f(b) & a \ b & ``` huffman@21164 ` 500` ``` (\x. a \ x & x \ b --> isCont f x)) ``` huffman@21164 ` 501` ``` --> (\x. a \ x & x \ b & f(x) = y)" ``` huffman@21164 ` 502` ```apply (blast intro: IVT) ``` huffman@21164 ` 503` ```done ``` huffman@21164 ` 504` huffman@21164 ` 505` ```lemma IVT2_objl: "(f(b::real) \ (y::real) & y \ f(a) & a \ b & ``` huffman@21164 ` 506` ``` (\x. a \ x & x \ b --> isCont f x)) ``` huffman@21164 ` 507` ``` --> (\x. a \ x & x \ b & f(x) = y)" ``` huffman@21164 ` 508` ```apply (blast intro: IVT2) ``` huffman@21164 ` 509` ```done ``` huffman@21164 ` 510` huffman@29975 ` 511` hoelzl@51479 ` 512` ```lemma compact_Icc[simp, intro]: "compact {a .. b::real}" ``` hoelzl@51479 ` 513` ```proof (cases "a \ b", rule compactI) ``` hoelzl@51479 ` 514` ``` fix C assume C: "a \ b" "\t\C. open t" "{a..b} \ \C" ``` hoelzl@51479 ` 515` ``` def T == "{a .. b}" ``` hoelzl@51479 ` 516` ``` from C(1,3) show "\C'\C. finite C' \ {a..b} \ \C'" ``` hoelzl@51479 ` 517` ``` proof (induct rule: Bolzano) ``` hoelzl@51479 ` 518` ``` case (trans a b c) ``` hoelzl@51479 ` 519` ``` then have *: "{a .. c} = {a .. b} \ {b .. c}" by auto ``` hoelzl@51479 ` 520` ``` from trans obtain C1 C2 where "C1\C \ finite C1 \ {a..b} \ \C1" "C2\C \ finite C2 \ {b..c} \ \C2" ``` hoelzl@51479 ` 521` ``` by (auto simp: *) ``` hoelzl@51479 ` 522` ``` with trans show ?case ``` hoelzl@51479 ` 523` ``` unfolding * by (intro exI[of _ "C1 \ C2"]) auto ``` hoelzl@51479 ` 524` ``` next ``` hoelzl@51479 ` 525` ``` case (local x) ``` hoelzl@51479 ` 526` ``` then have "x \ \C" using C by auto ``` hoelzl@51479 ` 527` ``` with C(2) obtain c where "x \ c" "open c" "c \ C" by auto ``` hoelzl@51479 ` 528` ``` then obtain e where "0 < e" "{x - e <..< x + e} \ c" ``` hoelzl@51479 ` 529` ``` by (auto simp: open_real_def dist_real_def subset_eq Ball_def abs_less_iff) ``` hoelzl@51479 ` 530` ``` with `c \ C` show ?case ``` hoelzl@51479 ` 531` ``` by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto ``` hoelzl@51479 ` 532` ``` qed ``` hoelzl@51479 ` 533` ```qed simp ``` hoelzl@51479 ` 534` huffman@29975 ` 535` ```subsection {* Boundedness of continuous functions *} ``` huffman@29975 ` 536` huffman@21164 ` 537` ```text{*By bisection, function continuous on closed interval is bounded above*} ``` huffman@21164 ` 538` hoelzl@51479 ` 539` ```lemma isCont_eq_Ub: ``` hoelzl@51479 ` 540` ``` fixes f :: "real \ 'a::linorder_topology" ``` hoelzl@51479 ` 541` ``` shows "a \ b \ \x::real. a \ x \ x \ b \ isCont f x \ ``` hoelzl@51479 ` 542` ``` \M. (\x. a \ x \ x \ b \ f x \ M) \ (\x. a \ x \ x \ b \ f x = M)" ``` hoelzl@51479 ` 543` ``` using continuous_attains_sup[of "{a .. b}" f] ``` hoelzl@51479 ` 544` ``` apply (simp add: continuous_at_imp_continuous_on Ball_def) ``` hoelzl@51479 ` 545` ``` apply safe ``` hoelzl@51479 ` 546` ``` apply (rule_tac x="f x" in exI) ``` hoelzl@51479 ` 547` ``` apply auto ``` hoelzl@51479 ` 548` ``` done ``` hoelzl@51479 ` 549` hoelzl@51479 ` 550` ```lemma isCont_eq_Lb: ``` hoelzl@51479 ` 551` ``` fixes f :: "real \ 'a::linorder_topology" ``` hoelzl@51479 ` 552` ``` shows "a \ b \ \x. a \ x \ x \ b \ isCont f x \ ``` hoelzl@51479 ` 553` ``` \M. (\x. a \ x \ x \ b \ M \ f x) \ (\x. a \ x \ x \ b \ f x = M)" ``` hoelzl@51479 ` 554` ``` using continuous_attains_inf[of "{a .. b}" f] ``` hoelzl@51479 ` 555` ``` apply (simp add: continuous_at_imp_continuous_on Ball_def) ``` hoelzl@51479 ` 556` ``` apply safe ``` hoelzl@51479 ` 557` ``` apply (rule_tac x="f x" in exI) ``` hoelzl@51479 ` 558` ``` apply auto ``` hoelzl@51479 ` 559` ``` done ``` hoelzl@51479 ` 560` huffman@21164 ` 561` ```lemma isCont_bounded: ``` hoelzl@51479 ` 562` ``` fixes f :: "real \ 'a::linorder_topology" ``` hoelzl@51479 ` 563` ``` shows "a \ b \ \x. a \ x \ x \ b \ isCont f x \ \M. \x. a \ x \ x \ b \ f x \ M" ``` hoelzl@51479 ` 564` ``` using isCont_eq_Ub[of a b f] by auto ``` hoelzl@51479 ` 565` hoelzl@51479 ` 566` ```lemma isCont_has_Ub: ``` hoelzl@51479 ` 567` ``` fixes f :: "real \ 'a::linorder_topology" ``` hoelzl@51479 ` 568` ``` shows "a \ b \ \x. a \ x \ x \ b \ isCont f x \ ``` hoelzl@51479 ` 569` ``` \M. (\x. a \ x \ x \ b \ f x \ M) \ (\N. N < M \ (\x. a \ x \ x \ b \ N < f x))" ``` hoelzl@51479 ` 570` ``` using isCont_eq_Ub[of a b f] by auto ``` huffman@21164 ` 571` huffman@21164 ` 572` ```text{*Refine the above to existence of least upper bound*} ``` huffman@21164 ` 573` huffman@21164 ` 574` ```lemma lemma_reals_complete: "((\x. x \ S) & (\y. isUb UNIV S (y::real))) --> ``` huffman@21164 ` 575` ``` (\t. isLub UNIV S t)" ``` huffman@21164 ` 576` ```by (blast intro: reals_complete) ``` huffman@21164 ` 577` huffman@21164 ` 578` huffman@21164 ` 579` ```text{*Another version.*} ``` huffman@21164 ` 580` huffman@21164 ` 581` ```lemma isCont_Lb_Ub: "[|a \ b; \x. a \ x & x \ b --> isCont f x |] ``` huffman@21164 ` 582` ``` ==> \L M::real. (\x::real. a \ x & x \ b --> L \ f(x) & f(x) \ M) & ``` huffman@21164 ` 583` ``` (\y. L \ y & y \ M --> (\x. a \ x & x \ b & (f(x) = y)))" ``` huffman@21164 ` 584` ```apply (frule isCont_eq_Lb) ``` huffman@21164 ` 585` ```apply (frule_tac [2] isCont_eq_Ub) ``` huffman@21164 ` 586` ```apply (assumption+, safe) ``` huffman@21164 ` 587` ```apply (rule_tac x = "f x" in exI) ``` huffman@21164 ` 588` ```apply (rule_tac x = "f xa" in exI, simp, safe) ``` huffman@21164 ` 589` ```apply (cut_tac x = x and y = xa in linorder_linear, safe) ``` huffman@21164 ` 590` ```apply (cut_tac f = f and a = x and b = xa and y = y in IVT_objl) ``` huffman@21164 ` 591` ```apply (cut_tac [2] f = f and a = xa and b = x and y = y in IVT2_objl, safe) ``` huffman@21164 ` 592` ```apply (rule_tac [2] x = xb in exI) ``` huffman@21164 ` 593` ```apply (rule_tac [4] x = xb in exI, simp_all) ``` huffman@21164 ` 594` ```done ``` huffman@21164 ` 595` huffman@21164 ` 596` huffman@29975 ` 597` ```subsection {* Local extrema *} ``` huffman@29975 ` 598` huffman@21164 ` 599` ```text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*} ``` huffman@21164 ` 600` paulson@33654 ` 601` ```lemma DERIV_pos_inc_right: ``` huffman@21164 ` 602` ``` fixes f :: "real => real" ``` huffman@21164 ` 603` ``` assumes der: "DERIV f x :> l" ``` huffman@21164 ` 604` ``` and l: "0 < l" ``` huffman@21164 ` 605` ``` shows "\d > 0. \h > 0. h < d --> f(x) < f(x + h)" ``` huffman@21164 ` 606` ```proof - ``` huffman@21164 ` 607` ``` from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]] ``` huffman@21164 ` 608` ``` have "\s > 0. (\z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < l)" ``` huffman@21164 ` 609` ``` by (simp add: diff_minus) ``` huffman@21164 ` 610` ``` then obtain s ``` huffman@21164 ` 611` ``` where s: "0 < s" ``` huffman@21164 ` 612` ``` and all: "!!z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < l" ``` huffman@21164 ` 613` ``` by auto ``` huffman@21164 ` 614` ``` thus ?thesis ``` huffman@21164 ` 615` ``` proof (intro exI conjI strip) ``` huffman@23441 ` 616` ``` show "0 real" ``` huffman@21164 ` 633` ``` assumes der: "DERIV f x :> l" ``` huffman@21164 ` 634` ``` and l: "l < 0" ``` huffman@21164 ` 635` ``` shows "\d > 0. \h > 0. h < d --> f(x) < f(x-h)" ``` huffman@21164 ` 636` ```proof - ``` huffman@21164 ` 637` ``` from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]] ``` huffman@21164 ` 638` ``` have "\s > 0. (\z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < -l)" ``` huffman@21164 ` 639` ``` by (simp add: diff_minus) ``` huffman@21164 ` 640` ``` then obtain s ``` huffman@21164 ` 641` ``` where s: "0 < s" ``` huffman@21164 ` 642` ``` and all: "!!z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < -l" ``` huffman@21164 ` 643` ``` by auto ``` huffman@21164 ` 644` ``` thus ?thesis ``` huffman@21164 ` 645` ``` proof (intro exI conjI strip) ``` huffman@23441 ` 646` ``` show "0 real" ``` paulson@33654 ` 664` ``` shows "DERIV f x :> l \ 0 < l \ \d > 0. \h > 0. h < d --> f(x - h) < f(x)" ``` paulson@33654 ` 665` ``` apply (rule DERIV_neg_dec_left [of "%x. - f x" x "-l", simplified]) ``` hoelzl@41368 ` 666` ``` apply (auto simp add: DERIV_minus) ``` paulson@33654 ` 667` ``` done ``` paulson@33654 ` 668` paulson@33654 ` 669` ```lemma DERIV_neg_dec_right: ``` paulson@33654 ` 670` ``` fixes f :: "real => real" ``` paulson@33654 ` 671` ``` shows "DERIV f x :> l \ l < 0 \ \d > 0. \h > 0. h < d --> f(x) > f(x + h)" ``` paulson@33654 ` 672` ``` apply (rule DERIV_pos_inc_right [of "%x. - f x" x "-l", simplified]) ``` hoelzl@41368 ` 673` ``` apply (auto simp add: DERIV_minus) ``` paulson@33654 ` 674` ``` done ``` paulson@33654 ` 675` huffman@21164 ` 676` ```lemma DERIV_local_max: ``` huffman@21164 ` 677` ``` fixes f :: "real => real" ``` huffman@21164 ` 678` ``` assumes der: "DERIV f x :> l" ``` huffman@21164 ` 679` ``` and d: "0 < d" ``` huffman@21164 ` 680` ``` and le: "\y. \x-y\ < d --> f(y) \ f(x)" ``` huffman@21164 ` 681` ``` shows "l = 0" ``` huffman@21164 ` 682` ```proof (cases rule: linorder_cases [of l 0]) ``` huffman@23441 ` 683` ``` case equal thus ?thesis . ``` huffman@21164 ` 684` ```next ``` huffman@21164 ` 685` ``` case less ``` paulson@33654 ` 686` ``` from DERIV_neg_dec_left [OF der less] ``` huffman@21164 ` 687` ``` obtain d' where d': "0 < d'" ``` huffman@21164 ` 688` ``` and lt: "\h > 0. h < d' \ f x < f (x-h)" by blast ``` huffman@21164 ` 689` ``` from real_lbound_gt_zero [OF d d'] ``` huffman@21164 ` 690` ``` obtain e where "0 < e \ e < d \ e < d'" .. ``` huffman@21164 ` 691` ``` with lt le [THEN spec [where x="x-e"]] ``` huffman@21164 ` 692` ``` show ?thesis by (auto simp add: abs_if) ``` huffman@21164 ` 693` ```next ``` huffman@21164 ` 694` ``` case greater ``` paulson@33654 ` 695` ``` from DERIV_pos_inc_right [OF der greater] ``` huffman@21164 ` 696` ``` obtain d' where d': "0 < d'" ``` huffman@21164 ` 697` ``` and lt: "\h > 0. h < d' \ f x < f (x + h)" by blast ``` huffman@21164 ` 698` ``` from real_lbound_gt_zero [OF d d'] ``` huffman@21164 ` 699` ``` obtain e where "0 < e \ e < d \ e < d'" .. ``` huffman@21164 ` 700` ``` with lt le [THEN spec [where x="x+e"]] ``` huffman@21164 ` 701` ``` show ?thesis by (auto simp add: abs_if) ``` huffman@21164 ` 702` ```qed ``` huffman@21164 ` 703` huffman@21164 ` 704` huffman@21164 ` 705` ```text{*Similar theorem for a local minimum*} ``` huffman@21164 ` 706` ```lemma DERIV_local_min: ``` huffman@21164 ` 707` ``` fixes f :: "real => real" ``` huffman@21164 ` 708` ``` shows "[| DERIV f x :> l; 0 < d; \y. \x-y\ < d --> f(x) \ f(y) |] ==> l = 0" ``` huffman@21164 ` 709` ```by (drule DERIV_minus [THEN DERIV_local_max], auto) ``` huffman@21164 ` 710` huffman@21164 ` 711` huffman@21164 ` 712` ```text{*In particular, if a function is locally flat*} ``` huffman@21164 ` 713` ```lemma DERIV_local_const: ``` huffman@21164 ` 714` ``` fixes f :: "real => real" ``` huffman@21164 ` 715` ``` shows "[| DERIV f x :> l; 0 < d; \y. \x-y\ < d --> f(x) = f(y) |] ==> l = 0" ``` huffman@21164 ` 716` ```by (auto dest!: DERIV_local_max) ``` huffman@21164 ` 717` huffman@29975 ` 718` huffman@29975 ` 719` ```subsection {* Rolle's Theorem *} ``` huffman@29975 ` 720` huffman@21164 ` 721` ```text{*Lemma about introducing open ball in open interval*} ``` huffman@21164 ` 722` ```lemma lemma_interval_lt: ``` huffman@21164 ` 723` ``` "[| a < x; x < b |] ``` huffman@21164 ` 724` ``` ==> \d::real. 0 < d & (\y. \x-y\ < d --> a < y & y < b)" ``` chaieb@27668 ` 725` huffman@22998 ` 726` ```apply (simp add: abs_less_iff) ``` huffman@21164 ` 727` ```apply (insert linorder_linear [of "x-a" "b-x"], safe) ``` huffman@21164 ` 728` ```apply (rule_tac x = "x-a" in exI) ``` huffman@21164 ` 729` ```apply (rule_tac [2] x = "b-x" in exI, auto) ``` huffman@21164 ` 730` ```done ``` huffman@21164 ` 731` huffman@21164 ` 732` ```lemma lemma_interval: "[| a < x; x < b |] ==> ``` huffman@21164 ` 733` ``` \d::real. 0 < d & (\y. \x-y\ < d --> a \ y & y \ b)" ``` huffman@21164 ` 734` ```apply (drule lemma_interval_lt, auto) ``` huffman@44921 ` 735` ```apply force ``` huffman@21164 ` 736` ```done ``` huffman@21164 ` 737` huffman@21164 ` 738` ```text{*Rolle's Theorem. ``` huffman@21164 ` 739` ``` If @{term f} is defined and continuous on the closed interval ``` huffman@21164 ` 740` ``` @{text "[a,b]"} and differentiable on the open interval @{text "(a,b)"}, ``` huffman@21164 ` 741` ``` and @{term "f(a) = f(b)"}, ``` huffman@21164 ` 742` ``` then there exists @{text "x0 \ (a,b)"} such that @{term "f'(x0) = 0"}*} ``` huffman@21164 ` 743` ```theorem Rolle: ``` huffman@21164 ` 744` ``` assumes lt: "a < b" ``` huffman@21164 ` 745` ``` and eq: "f(a) = f(b)" ``` huffman@21164 ` 746` ``` and con: "\x. a \ x & x \ b --> isCont f x" ``` huffman@21164 ` 747` ``` and dif [rule_format]: "\x. a < x & x < b --> f differentiable x" ``` huffman@21784 ` 748` ``` shows "\z::real. a < z & z < b & DERIV f z :> 0" ``` huffman@21164 ` 749` ```proof - ``` huffman@21164 ` 750` ``` have le: "a \ b" using lt by simp ``` huffman@21164 ` 751` ``` from isCont_eq_Ub [OF le con] ``` huffman@21164 ` 752` ``` obtain x where x_max: "\z. a \ z \ z \ b \ f z \ f x" ``` huffman@21164 ` 753` ``` and alex: "a \ x" and xleb: "x \ b" ``` huffman@21164 ` 754` ``` by blast ``` huffman@21164 ` 755` ``` from isCont_eq_Lb [OF le con] ``` huffman@21164 ` 756` ``` obtain x' where x'_min: "\z. a \ z \ z \ b \ f x' \ f z" ``` huffman@21164 ` 757` ``` and alex': "a \ x'" and x'leb: "x' \ b" ``` huffman@21164 ` 758` ``` by blast ``` huffman@21164 ` 759` ``` show ?thesis ``` huffman@21164 ` 760` ``` proof cases ``` huffman@21164 ` 761` ``` assume axb: "a < x & x < b" ``` huffman@21164 ` 762` ``` --{*@{term f} attains its maximum within the interval*} ``` chaieb@27668 ` 763` ``` hence ax: "ay. \x-y\ < d \ a \ y \ y \ b" ``` huffman@21164 ` 766` ``` by blast ``` huffman@21164 ` 767` ``` hence bound': "\y. \x-y\ < d \ f y \ f x" using x_max ``` huffman@21164 ` 768` ``` by blast ``` huffman@21164 ` 769` ``` from differentiableD [OF dif [OF axb]] ``` huffman@21164 ` 770` ``` obtain l where der: "DERIV f x :> l" .. ``` huffman@21164 ` 771` ``` have "l=0" by (rule DERIV_local_max [OF der d bound']) ``` huffman@21164 ` 772` ``` --{*the derivative at a local maximum is zero*} ``` huffman@21164 ` 773` ``` thus ?thesis using ax xb der by auto ``` huffman@21164 ` 774` ``` next ``` huffman@21164 ` 775` ``` assume notaxb: "~ (a < x & x < b)" ``` huffman@21164 ` 776` ``` hence xeqab: "x=a | x=b" using alex xleb by arith ``` huffman@21164 ` 777` ``` hence fb_eq_fx: "f b = f x" by (auto simp add: eq) ``` huffman@21164 ` 778` ``` show ?thesis ``` huffman@21164 ` 779` ``` proof cases ``` huffman@21164 ` 780` ``` assume ax'b: "a < x' & x' < b" ``` huffman@21164 ` 781` ``` --{*@{term f} attains its minimum within the interval*} ``` chaieb@27668 ` 782` ``` hence ax': "ay. \x'-y\ < d \ a \ y \ y \ b" ``` huffman@21164 ` 785` ``` by blast ``` huffman@21164 ` 786` ``` hence bound': "\y. \x'-y\ < d \ f x' \ f y" using x'_min ``` huffman@21164 ` 787` ``` by blast ``` huffman@21164 ` 788` ``` from differentiableD [OF dif [OF ax'b]] ``` huffman@21164 ` 789` ``` obtain l where der: "DERIV f x' :> l" .. ``` huffman@21164 ` 790` ``` have "l=0" by (rule DERIV_local_min [OF der d bound']) ``` huffman@21164 ` 791` ``` --{*the derivative at a local minimum is zero*} ``` huffman@21164 ` 792` ``` thus ?thesis using ax' x'b der by auto ``` huffman@21164 ` 793` ``` next ``` huffman@21164 ` 794` ``` assume notax'b: "~ (a < x' & x' < b)" ``` huffman@21164 ` 795` ``` --{*@{term f} is constant througout the interval*} ``` huffman@21164 ` 796` ``` hence x'eqab: "x'=a | x'=b" using alex' x'leb by arith ``` huffman@21164 ` 797` ``` hence fb_eq_fx': "f b = f x'" by (auto simp add: eq) ``` huffman@21164 ` 798` ``` from dense [OF lt] ``` huffman@21164 ` 799` ``` obtain r where ar: "a < r" and rb: "r < b" by blast ``` huffman@21164 ` 800` ``` from lemma_interval [OF ar rb] ``` huffman@21164 ` 801` ``` obtain d where d: "0y. \r-y\ < d \ a \ y \ y \ b" ``` huffman@21164 ` 802` ``` by blast ``` huffman@21164 ` 803` ``` have eq_fb: "\z. a \ z --> z \ b --> f z = f b" ``` huffman@21164 ` 804` ``` proof (clarify) ``` huffman@21164 ` 805` ``` fix z::real ``` huffman@21164 ` 806` ``` assume az: "a \ z" and zb: "z \ b" ``` huffman@21164 ` 807` ``` show "f z = f b" ``` huffman@21164 ` 808` ``` proof (rule order_antisym) ``` huffman@21164 ` 809` ``` show "f z \ f b" by (simp add: fb_eq_fx x_max az zb) ``` huffman@21164 ` 810` ``` show "f b \ f z" by (simp add: fb_eq_fx' x'_min az zb) ``` huffman@21164 ` 811` ``` qed ``` huffman@21164 ` 812` ``` qed ``` huffman@21164 ` 813` ``` have bound': "\y. \r-y\ < d \ f r = f y" ``` huffman@21164 ` 814` ``` proof (intro strip) ``` huffman@21164 ` 815` ``` fix y::real ``` huffman@21164 ` 816` ``` assume lt: "\r-y\ < d" ``` huffman@21164 ` 817` ``` hence "f y = f b" by (simp add: eq_fb bound) ``` huffman@21164 ` 818` ``` thus "f r = f y" by (simp add: eq_fb ar rb order_less_imp_le) ``` huffman@21164 ` 819` ``` qed ``` huffman@21164 ` 820` ``` from differentiableD [OF dif [OF conjI [OF ar rb]]] ``` huffman@21164 ` 821` ``` obtain l where der: "DERIV f r :> l" .. ``` huffman@21164 ` 822` ``` have "l=0" by (rule DERIV_local_const [OF der d bound']) ``` huffman@21164 ` 823` ``` --{*the derivative of a constant function is zero*} ``` huffman@21164 ` 824` ``` thus ?thesis using ar rb der by auto ``` huffman@21164 ` 825` ``` qed ``` huffman@21164 ` 826` ``` qed ``` huffman@21164 ` 827` ```qed ``` huffman@21164 ` 828` huffman@21164 ` 829` huffman@21164 ` 830` ```subsection{*Mean Value Theorem*} ``` huffman@21164 ` 831` huffman@21164 ` 832` ```lemma lemma_MVT: ``` huffman@21164 ` 833` ``` "f a - (f b - f a)/(b-a) * a = f b - (f b - f a)/(b-a) * (b::real)" ``` hoelzl@51481 ` 834` ``` by (cases "a = b") (simp_all add: field_simps) ``` huffman@21164 ` 835` huffman@21164 ` 836` ```theorem MVT: ``` huffman@21164 ` 837` ``` assumes lt: "a < b" ``` huffman@21164 ` 838` ``` and con: "\x. a \ x & x \ b --> isCont f x" ``` huffman@21164 ` 839` ``` and dif [rule_format]: "\x. a < x & x < b --> f differentiable x" ``` huffman@21784 ` 840` ``` shows "\l z::real. a < z & z < b & DERIV f z :> l & ``` huffman@21164 ` 841` ``` (f(b) - f(a) = (b-a) * l)" ``` huffman@21164 ` 842` ```proof - ``` huffman@21164 ` 843` ``` let ?F = "%x. f x - ((f b - f a) / (b-a)) * x" ``` huffman@44233 ` 844` ``` have contF: "\x. a \ x \ x \ b \ isCont ?F x" ``` huffman@44233 ` 845` ``` using con by (fast intro: isCont_intros) ``` huffman@21164 ` 846` ``` have difF: "\x. a < x \ x < b \ ?F differentiable x" ``` huffman@21164 ` 847` ``` proof (clarify) ``` huffman@21164 ` 848` ``` fix x::real ``` huffman@21164 ` 849` ``` assume ax: "a < x" and xb: "x < b" ``` huffman@21164 ` 850` ``` from differentiableD [OF dif [OF conjI [OF ax xb]]] ``` huffman@21164 ` 851` ``` obtain l where der: "DERIV f x :> l" .. ``` huffman@21164 ` 852` ``` show "?F differentiable x" ``` huffman@21164 ` 853` ``` by (rule differentiableI [where D = "l - (f b - f a)/(b-a)"], ``` huffman@21164 ` 854` ``` blast intro: DERIV_diff DERIV_cmult_Id der) ``` huffman@21164 ` 855` ``` qed ``` huffman@21164 ` 856` ``` from Rolle [where f = ?F, OF lt lemma_MVT contF difF] ``` huffman@21164 ` 857` ``` obtain z where az: "a < z" and zb: "z < b" and der: "DERIV ?F z :> 0" ``` huffman@21164 ` 858` ``` by blast ``` huffman@21164 ` 859` ``` have "DERIV (%x. ((f b - f a)/(b-a)) * x) z :> (f b - f a)/(b-a)" ``` huffman@21164 ` 860` ``` by (rule DERIV_cmult_Id) ``` huffman@21164 ` 861` ``` hence derF: "DERIV (\x. ?F x + (f b - f a) / (b - a) * x) z ``` huffman@21164 ` 862` ``` :> 0 + (f b - f a) / (b - a)" ``` huffman@21164 ` 863` ``` by (rule DERIV_add [OF der]) ``` huffman@21164 ` 864` ``` show ?thesis ``` huffman@21164 ` 865` ``` proof (intro exI conjI) ``` huffman@23441 ` 866` ``` show "a < z" using az . ``` huffman@23441 ` 867` ``` show "z < b" using zb . ``` huffman@21164 ` 868` ``` show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by (simp) ``` huffman@21164 ` 869` ``` show "DERIV f z :> ((f b - f a)/(b-a))" using derF by simp ``` huffman@21164 ` 870` ``` qed ``` huffman@21164 ` 871` ```qed ``` huffman@21164 ` 872` hoelzl@29803 ` 873` ```lemma MVT2: ``` hoelzl@29803 ` 874` ``` "[| a < b; \x. a \ x & x \ b --> DERIV f x :> f'(x) |] ``` hoelzl@29803 ` 875` ``` ==> \z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))" ``` hoelzl@29803 ` 876` ```apply (drule MVT) ``` hoelzl@29803 ` 877` ```apply (blast intro: DERIV_isCont) ``` hoelzl@29803 ` 878` ```apply (force dest: order_less_imp_le simp add: differentiable_def) ``` hoelzl@29803 ` 879` ```apply (blast dest: DERIV_unique order_less_imp_le) ``` hoelzl@29803 ` 880` ```done ``` hoelzl@29803 ` 881` huffman@21164 ` 882` huffman@21164 ` 883` ```text{*A function is constant if its derivative is 0 over an interval.*} ``` huffman@21164 ` 884` huffman@21164 ` 885` ```lemma DERIV_isconst_end: ``` huffman@21164 ` 886` ``` fixes f :: "real => real" ``` huffman@21164 ` 887` ``` shows "[| a < b; ``` huffman@21164 ` 888` ``` \x. a \ x & x \ b --> isCont f x; ``` huffman@21164 ` 889` ``` \x. a < x & x < b --> DERIV f x :> 0 |] ``` huffman@21164 ` 890` ``` ==> f b = f a" ``` huffman@21164 ` 891` ```apply (drule MVT, assumption) ``` huffman@21164 ` 892` ```apply (blast intro: differentiableI) ``` huffman@21164 ` 893` ```apply (auto dest!: DERIV_unique simp add: diff_eq_eq) ``` huffman@21164 ` 894` ```done ``` huffman@21164 ` 895` huffman@21164 ` 896` ```lemma DERIV_isconst1: ``` huffman@21164 ` 897` ``` fixes f :: "real => real" ``` huffman@21164 ` 898` ``` shows "[| a < b; ``` huffman@21164 ` 899` ``` \x. a \ x & x \ b --> isCont f x; ``` huffman@21164 ` 900` ``` \x. a < x & x < b --> DERIV f x :> 0 |] ``` huffman@21164 ` 901` ``` ==> \x. a \ x & x \ b --> f x = f a" ``` huffman@21164 ` 902` ```apply safe ``` huffman@21164 ` 903` ```apply (drule_tac x = a in order_le_imp_less_or_eq, safe) ``` huffman@21164 ` 904` ```apply (drule_tac b = x in DERIV_isconst_end, auto) ``` huffman@21164 ` 905` ```done ``` huffman@21164 ` 906` huffman@21164 ` 907` ```lemma DERIV_isconst2: ``` huffman@21164 ` 908` ``` fixes f :: "real => real" ``` huffman@21164 ` 909` ``` shows "[| a < b; ``` huffman@21164 ` 910` ``` \x. a \ x & x \ b --> isCont f x; ``` huffman@21164 ` 911` ``` \x. a < x & x < b --> DERIV f x :> 0; ``` huffman@21164 ` 912` ``` a \ x; x \ b |] ``` huffman@21164 ` 913` ``` ==> f x = f a" ``` huffman@21164 ` 914` ```apply (blast dest: DERIV_isconst1) ``` huffman@21164 ` 915` ```done ``` huffman@21164 ` 916` hoelzl@29803 ` 917` ```lemma DERIV_isconst3: fixes a b x y :: real ``` hoelzl@29803 ` 918` ``` assumes "a < b" and "x \ {a <..< b}" and "y \ {a <..< b}" ``` hoelzl@29803 ` 919` ``` assumes derivable: "\x. x \ {a <..< b} \ DERIV f x :> 0" ``` hoelzl@29803 ` 920` ``` shows "f x = f y" ``` hoelzl@29803 ` 921` ```proof (cases "x = y") ``` hoelzl@29803 ` 922` ``` case False ``` hoelzl@29803 ` 923` ``` let ?a = "min x y" ``` hoelzl@29803 ` 924` ``` let ?b = "max x y" ``` hoelzl@29803 ` 925` ``` ``` hoelzl@29803 ` 926` ``` have "\z. ?a \ z \ z \ ?b \ DERIV f z :> 0" ``` hoelzl@29803 ` 927` ``` proof (rule allI, rule impI) ``` hoelzl@29803 ` 928` ``` fix z :: real assume "?a \ z \ z \ ?b" ``` hoelzl@29803 ` 929` ``` hence "a < z" and "z < b" using `x \ {a <..< b}` and `y \ {a <..< b}` by auto ``` hoelzl@29803 ` 930` ``` hence "z \ {a<.. 0" by (rule derivable) ``` hoelzl@29803 ` 932` ``` qed ``` hoelzl@29803 ` 933` ``` hence isCont: "\z. ?a \ z \ z \ ?b \ isCont f z" ``` hoelzl@29803 ` 934` ``` and DERIV: "\z. ?a < z \ z < ?b \ DERIV f z :> 0" using DERIV_isCont by auto ``` hoelzl@29803 ` 935` hoelzl@29803 ` 936` ``` have "?a < ?b" using `x \ y` by auto ``` hoelzl@29803 ` 937` ``` from DERIV_isconst2[OF this isCont DERIV, of x] and DERIV_isconst2[OF this isCont DERIV, of y] ``` hoelzl@29803 ` 938` ``` show ?thesis by auto ``` hoelzl@29803 ` 939` ```qed auto ``` hoelzl@29803 ` 940` huffman@21164 ` 941` ```lemma DERIV_isconst_all: ``` huffman@21164 ` 942` ``` fixes f :: "real => real" ``` huffman@21164 ` 943` ``` shows "\x. DERIV f x :> 0 ==> f(x) = f(y)" ``` huffman@21164 ` 944` ```apply (rule linorder_cases [of x y]) ``` huffman@21164 ` 945` ```apply (blast intro: sym DERIV_isCont DERIV_isconst_end)+ ``` huffman@21164 ` 946` ```done ``` huffman@21164 ` 947` huffman@21164 ` 948` ```lemma DERIV_const_ratio_const: ``` huffman@21784 ` 949` ``` fixes f :: "real => real" ``` huffman@21784 ` 950` ``` shows "[|a \ b; \x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b-a) * k" ``` huffman@21164 ` 951` ```apply (rule linorder_cases [of a b], auto) ``` huffman@21164 ` 952` ```apply (drule_tac [!] f = f in MVT) ``` huffman@21164 ` 953` ```apply (auto dest: DERIV_isCont DERIV_unique simp add: differentiable_def) ``` nipkow@23477 ` 954` ```apply (auto dest: DERIV_unique simp add: ring_distribs diff_minus) ``` huffman@21164 ` 955` ```done ``` huffman@21164 ` 956` huffman@21164 ` 957` ```lemma DERIV_const_ratio_const2: ``` huffman@21784 ` 958` ``` fixes f :: "real => real" ``` huffman@21784 ` 959` ``` shows "[|a \ b; \x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k" ``` huffman@21164 ` 960` ```apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1]) ``` huffman@21164 ` 961` ```apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc) ``` huffman@21164 ` 962` ```done ``` huffman@21164 ` 963` huffman@21164 ` 964` ```lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)" ``` huffman@21164 ` 965` ```by (simp) ``` huffman@21164 ` 966` huffman@21164 ` 967` ```lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)" ``` huffman@21164 ` 968` ```by (simp) ``` huffman@21164 ` 969` huffman@21164 ` 970` ```text{*Gallileo's "trick": average velocity = av. of end velocities*} ``` huffman@21164 ` 971` huffman@21164 ` 972` ```lemma DERIV_const_average: ``` huffman@21164 ` 973` ``` fixes v :: "real => real" ``` huffman@21164 ` 974` ``` assumes neq: "a \ (b::real)" ``` huffman@21164 ` 975` ``` and der: "\x. DERIV v x :> k" ``` huffman@21164 ` 976` ``` shows "v ((a + b)/2) = (v a + v b)/2" ``` huffman@21164 ` 977` ```proof (cases rule: linorder_cases [of a b]) ``` huffman@21164 ` 978` ``` case equal with neq show ?thesis by simp ``` huffman@21164 ` 979` ```next ``` huffman@21164 ` 980` ``` case less ``` huffman@21164 ` 981` ``` have "(v b - v a) / (b - a) = k" ``` huffman@21164 ` 982` ``` by (rule DERIV_const_ratio_const2 [OF neq der]) ``` huffman@21164 ` 983` ``` hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp ``` huffman@21164 ` 984` ``` moreover have "(v ((a + b) / 2) - v a) / ((a + b) / 2 - a) = k" ``` huffman@21164 ` 985` ``` by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq) ``` huffman@21164 ` 986` ``` ultimately show ?thesis using neq by force ``` huffman@21164 ` 987` ```next ``` huffman@21164 ` 988` ``` case greater ``` huffman@21164 ` 989` ``` have "(v b - v a) / (b - a) = k" ``` huffman@21164 ` 990` ``` by (rule DERIV_const_ratio_const2 [OF neq der]) ``` huffman@21164 ` 991` ``` hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp ``` huffman@21164 ` 992` ``` moreover have " (v ((b + a) / 2) - v a) / ((b + a) / 2 - a) = k" ``` huffman@21164 ` 993` ``` by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq) ``` huffman@21164 ` 994` ``` ultimately show ?thesis using neq by (force simp add: add_commute) ``` huffman@21164 ` 995` ```qed ``` huffman@21164 ` 996` paulson@33654 ` 997` ```(* A function with positive derivative is increasing. ``` paulson@33654 ` 998` ``` A simple proof using the MVT, by Jeremy Avigad. And variants. ``` paulson@33654 ` 999` ```*) ``` paulson@33654 ` 1000` ```lemma DERIV_pos_imp_increasing: ``` paulson@33654 ` 1001` ``` fixes a::real and b::real and f::"real => real" ``` paulson@33654 ` 1002` ``` assumes "a < b" and "\x. a \ x & x \ b --> (EX y. DERIV f x :> y & y > 0)" ``` paulson@33654 ` 1003` ``` shows "f a < f b" ``` paulson@33654 ` 1004` ```proof (rule ccontr) ``` wenzelm@41550 ` 1005` ``` assume f: "~ f a < f b" ``` wenzelm@33690 ` 1006` ``` have "EX l z. a < z & z < b & DERIV f z :> l ``` paulson@33654 ` 1007` ``` & f b - f a = (b - a) * l" ``` wenzelm@33690 ` 1008` ``` apply (rule MVT) ``` wenzelm@33690 ` 1009` ``` using assms ``` wenzelm@33690 ` 1010` ``` apply auto ``` wenzelm@33690 ` 1011` ``` apply (metis DERIV_isCont) ``` huffman@36777 ` 1012` ``` apply (metis differentiableI less_le) ``` wenzelm@33690 ` 1013` ``` done ``` wenzelm@41550 ` 1014` ``` then obtain l z where z: "a < z" "z < b" "DERIV f z :> l" ``` paulson@33654 ` 1015` ``` and "f b - f a = (b - a) * l" ``` paulson@33654 ` 1016` ``` by auto ``` wenzelm@41550 ` 1017` ``` with assms f have "~(l > 0)" ``` huffman@36777 ` 1018` ``` by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le) ``` wenzelm@41550 ` 1019` ``` with assms z show False ``` huffman@36777 ` 1020` ``` by (metis DERIV_unique less_le) ``` paulson@33654 ` 1021` ```qed ``` paulson@33654 ` 1022` noschinl@45791 ` 1023` ```lemma DERIV_nonneg_imp_nondecreasing: ``` paulson@33654 ` 1024` ``` fixes a::real and b::real and f::"real => real" ``` paulson@33654 ` 1025` ``` assumes "a \ b" and ``` paulson@33654 ` 1026` ``` "\x. a \ x & x \ b --> (\y. DERIV f x :> y & y \ 0)" ``` paulson@33654 ` 1027` ``` shows "f a \ f b" ``` paulson@33654 ` 1028` ```proof (rule ccontr, cases "a = b") ``` wenzelm@41550 ` 1029` ``` assume "~ f a \ f b" and "a = b" ``` wenzelm@41550 ` 1030` ``` then show False by auto ``` haftmann@37891 ` 1031` ```next ``` haftmann@37891 ` 1032` ``` assume A: "~ f a \ f b" ``` haftmann@37891 ` 1033` ``` assume B: "a ~= b" ``` paulson@33654 ` 1034` ``` with assms have "EX l z. a < z & z < b & DERIV f z :> l ``` paulson@33654 ` 1035` ``` & f b - f a = (b - a) * l" ``` wenzelm@33690 ` 1036` ``` apply - ``` wenzelm@33690 ` 1037` ``` apply (rule MVT) ``` wenzelm@33690 ` 1038` ``` apply auto ``` wenzelm@33690 ` 1039` ``` apply (metis DERIV_isCont) ``` huffman@36777 ` 1040` ``` apply (metis differentiableI less_le) ``` paulson@33654 ` 1041` ``` done ``` wenzelm@41550 ` 1042` ``` then obtain l z where z: "a < z" "z < b" "DERIV f z :> l" ``` haftmann@37891 ` 1043` ``` and C: "f b - f a = (b - a) * l" ``` paulson@33654 ` 1044` ``` by auto ``` haftmann@37891 ` 1045` ``` with A have "a < b" "f b < f a" by auto ``` haftmann@37891 ` 1046` ``` with C have "\ l \ 0" by (auto simp add: not_le algebra_simps) ``` huffman@45051 ` 1047` ``` (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono add_left_mono linear order_refl) ``` wenzelm@41550 ` 1048` ``` with assms z show False ``` paulson@33654 ` 1049` ``` by (metis DERIV_unique order_less_imp_le) ``` paulson@33654 ` 1050` ```qed ``` paulson@33654 ` 1051` paulson@33654 ` 1052` ```lemma DERIV_neg_imp_decreasing: ``` paulson@33654 ` 1053` ``` fixes a::real and b::real and f::"real => real" ``` paulson@33654 ` 1054` ``` assumes "a < b" and ``` paulson@33654 ` 1055` ``` "\x. a \ x & x \ b --> (\y. DERIV f x :> y & y < 0)" ``` paulson@33654 ` 1056` ``` shows "f a > f b" ``` paulson@33654 ` 1057` ```proof - ``` paulson@33654 ` 1058` ``` have "(%x. -f x) a < (%x. -f x) b" ``` paulson@33654 ` 1059` ``` apply (rule DERIV_pos_imp_increasing [of a b "%x. -f x"]) ``` wenzelm@33690 ` 1060` ``` using assms ``` wenzelm@33690 ` 1061` ``` apply auto ``` paulson@33654 ` 1062` ``` apply (metis DERIV_minus neg_0_less_iff_less) ``` paulson@33654 ` 1063` ``` done ``` paulson@33654 ` 1064` ``` thus ?thesis ``` paulson@33654 ` 1065` ``` by simp ``` paulson@33654 ` 1066` ```qed ``` paulson@33654 ` 1067` paulson@33654 ` 1068` ```lemma DERIV_nonpos_imp_nonincreasing: ``` paulson@33654 ` 1069` ``` fixes a::real and b::real and f::"real => real" ``` paulson@33654 ` 1070` ``` assumes "a \ b" and ``` paulson@33654 ` 1071` ``` "\x. a \ x & x \ b --> (\y. DERIV f x :> y & y \ 0)" ``` paulson@33654 ` 1072` ``` shows "f a \ f b" ``` paulson@33654 ` 1073` ```proof - ``` paulson@33654 ` 1074` ``` have "(%x. -f x) a \ (%x. -f x) b" ``` noschinl@45791 ` 1075` ``` apply (rule DERIV_nonneg_imp_nondecreasing [of a b "%x. -f x"]) ``` wenzelm@33690 ` 1076` ``` using assms ``` wenzelm@33690 ` 1077` ``` apply auto ``` paulson@33654 ` 1078` ``` apply (metis DERIV_minus neg_0_le_iff_le) ``` paulson@33654 ` 1079` ``` done ``` paulson@33654 ` 1080` ``` thus ?thesis ``` paulson@33654 ` 1081` ``` by simp ``` paulson@33654 ` 1082` ```qed ``` huffman@21164 ` 1083` huffman@21164 ` 1084` ```text{*Continuity of inverse function*} ``` huffman@21164 ` 1085` huffman@21164 ` 1086` ```lemma isCont_inverse_function: ``` huffman@21164 ` 1087` ``` fixes f g :: "real \ real" ``` huffman@21164 ` 1088` ``` assumes d: "0 < d" ``` hoelzl@51481 ` 1089` ``` and inj: "\z. \z-x\ \ d \ g (f z) = z" ``` hoelzl@51481 ` 1090` ``` and cont: "\z. \z-x\ \ d \ isCont f z" ``` huffman@21164 ` 1091` ``` shows "isCont g (f x)" ``` hoelzl@51481 ` 1092` ```proof - ``` hoelzl@51481 ` 1093` ``` let ?A = "f (x - d)" and ?B = "f (x + d)" and ?D = "{x - d..x + d}" ``` hoelzl@51481 ` 1094` hoelzl@51481 ` 1095` ``` have f: "continuous_on ?D f" ``` hoelzl@51481 ` 1096` ``` using cont by (intro continuous_at_imp_continuous_on ballI) auto ``` hoelzl@51481 ` 1097` ``` then have g: "continuous_on (f`?D) g" ``` hoelzl@51481 ` 1098` ``` using inj by (intro continuous_on_inv) auto ``` hoelzl@51481 ` 1099` hoelzl@51481 ` 1100` ``` from d f have "{min ?A ?B <..< max ?A ?B} \ f ` ?D" ``` hoelzl@51481 ` 1101` ``` by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max) ``` hoelzl@51481 ` 1102` ``` with g have "continuous_on {min ?A ?B <..< max ?A ?B} g" ``` hoelzl@51481 ` 1103` ``` by (rule continuous_on_subset) ``` hoelzl@51481 ` 1104` ``` moreover ``` hoelzl@51481 ` 1105` ``` have "(?A < f x \ f x < ?B) \ (?B < f x \ f x < ?A)" ``` hoelzl@51481 ` 1106` ``` using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto ``` hoelzl@51481 ` 1107` ``` then have "f x \ {min ?A ?B <..< max ?A ?B}" ``` hoelzl@51481 ` 1108` ``` by auto ``` hoelzl@51481 ` 1109` ``` ultimately ``` hoelzl@51481 ` 1110` ``` show ?thesis ``` hoelzl@51481 ` 1111` ``` by (simp add: continuous_on_eq_continuous_at) ``` huffman@21164 ` 1112` ```qed ``` huffman@21164 ` 1113` hoelzl@51481 ` 1114` ```lemma isCont_inverse_function2: ``` hoelzl@51481 ` 1115` ``` fixes f g :: "real \ real" shows ``` hoelzl@51481 ` 1116` ``` "\a < x; x < b; ``` hoelzl@51481 ` 1117` ``` \z. a \ z \ z \ b \ g (f z) = z; ``` hoelzl@51481 ` 1118` ``` \z. a \ z \ z \ b \ isCont f z\ ``` hoelzl@51481 ` 1119` ``` \ isCont g (f x)" ``` hoelzl@51481 ` 1120` ```apply (rule isCont_inverse_function ``` hoelzl@51481 ` 1121` ``` [where f=f and d="min (x - a) (b - x)"]) ``` hoelzl@51481 ` 1122` ```apply (simp_all add: abs_le_iff) ``` hoelzl@51481 ` 1123` ```done ``` hoelzl@51481 ` 1124` huffman@23041 ` 1125` ```text {* Derivative of inverse function *} ``` huffman@23041 ` 1126` huffman@23041 ` 1127` ```lemma DERIV_inverse_function: ``` huffman@23041 ` 1128` ``` fixes f g :: "real \ real" ``` huffman@23041 ` 1129` ``` assumes der: "DERIV f (g x) :> D" ``` huffman@23041 ` 1130` ``` assumes neq: "D \ 0" ``` huffman@23044 ` 1131` ``` assumes a: "a < x" and b: "x < b" ``` huffman@23044 ` 1132` ``` assumes inj: "\y. a < y \ y < b \ f (g y) = y" ``` huffman@23041 ` 1133` ``` assumes cont: "isCont g x" ``` huffman@23041 ` 1134` ``` shows "DERIV g x :> inverse D" ``` huffman@23041 ` 1135` ```unfolding DERIV_iff2 ``` huffman@23044 ` 1136` ```proof (rule LIM_equal2) ``` huffman@23044 ` 1137` ``` show "0 < min (x - a) (b - x)" ``` chaieb@27668 ` 1138` ``` using a b by arith ``` huffman@23044 ` 1139` ```next ``` huffman@23041 ` 1140` ``` fix y ``` huffman@23044 ` 1141` ``` assume "norm (y - x) < min (x - a) (b - x)" ``` chaieb@27668 ` 1142` ``` hence "a < y" and "y < b" ``` huffman@23044 ` 1143` ``` by (simp_all add: abs_less_iff) ``` huffman@23041 ` 1144` ``` thus "(g y - g x) / (y - x) = ``` huffman@23041 ` 1145` ``` inverse ((f (g y) - x) / (g y - g x))" ``` huffman@23041 ` 1146` ``` by (simp add: inj) ``` huffman@23041 ` 1147` ```next ``` huffman@23041 ` 1148` ``` have "(\z. (f z - f (g x)) / (z - g x)) -- g x --> D" ``` huffman@23041 ` 1149` ``` by (rule der [unfolded DERIV_iff2]) ``` huffman@23041 ` 1150` ``` hence 1: "(\z. (f z - x) / (z - g x)) -- g x --> D" ``` huffman@23044 ` 1151` ``` using inj a b by simp ``` huffman@23041 ` 1152` ``` have 2: "\d>0. \y. y \ x \ norm (y - x) < d \ g y \ g x" ``` huffman@23041 ` 1153` ``` proof (safe intro!: exI) ``` huffman@23044 ` 1154` ``` show "0 < min (x - a) (b - x)" ``` huffman@23044 ` 1155` ``` using a b by simp ``` huffman@23041 ` 1156` ``` next ``` huffman@23041 ` 1157` ``` fix y ``` huffman@23044 ` 1158` ``` assume "norm (y - x) < min (x - a) (b - x)" ``` huffman@23044 ` 1159` ``` hence y: "a < y" "y < b" ``` huffman@23044 ` 1160` ``` by (simp_all add: abs_less_iff) ``` huffman@23041 ` 1161` ``` assume "g y = g x" ``` huffman@23041 ` 1162` ``` hence "f (g y) = f (g x)" by simp ``` huffman@23044 ` 1163` ``` hence "y = x" using inj y a b by simp ``` huffman@23041 ` 1164` ``` also assume "y \ x" ``` huffman@23041 ` 1165` ``` finally show False by simp ``` huffman@23041 ` 1166` ``` qed ``` huffman@23041 ` 1167` ``` have "(\y. (f (g y) - x) / (g y - g x)) -- x --> D" ``` huffman@23041 ` 1168` ``` using cont 1 2 by (rule isCont_LIM_compose2) ``` huffman@23041 ` 1169` ``` thus "(\y. inverse ((f (g y) - x) / (g y - g x))) ``` huffman@23041 ` 1170` ``` -- x --> inverse D" ``` huffman@44568 ` 1171` ``` using neq by (rule tendsto_inverse) ``` huffman@23041 ` 1172` ```qed ``` huffman@23041 ` 1173` huffman@29975 ` 1174` ```subsection {* Generalized Mean Value Theorem *} ``` huffman@29975 ` 1175` huffman@21164 ` 1176` ```theorem GMVT: ``` huffman@21784 ` 1177` ``` fixes a b :: real ``` huffman@21164 ` 1178` ``` assumes alb: "a < b" ``` wenzelm@41550 ` 1179` ``` and fc: "\x. a \ x \ x \ b \ isCont f x" ``` wenzelm@41550 ` 1180` ``` and fd: "\x. a < x \ x < b \ f differentiable x" ``` wenzelm@41550 ` 1181` ``` and gc: "\x. a \ x \ x \ b \ isCont g x" ``` wenzelm@41550 ` 1182` ``` and gd: "\x. a < x \ x < b \ g differentiable x" ``` huffman@21164 ` 1183` ``` shows "\g'c f'c c. DERIV g c :> g'c \ DERIV f c :> f'c \ a < c \ c < b \ ((f b - f a) * g'c) = ((g b - g a) * f'c)" ``` huffman@21164 ` 1184` ```proof - ``` huffman@21164 ` 1185` ``` let ?h = "\x. (f b - f a)*(g x) - (g b - g a)*(f x)" ``` wenzelm@41550 ` 1186` ``` from assms have "a < b" by simp ``` huffman@21164 ` 1187` ``` moreover have "\x. a \ x \ x \ b \ isCont ?h x" ``` huffman@44233 ` 1188` ``` using fc gc by simp ``` huffman@44233 ` 1189` ``` moreover have "\x. a < x \ x < b \ ?h differentiable x" ``` huffman@44233 ` 1190` ``` using fd gd by simp ``` huffman@21164 ` 1191` ``` ultimately have "\l z. a < z \ z < b \ DERIV ?h z :> l \ ?h b - ?h a = (b - a) * l" by (rule MVT) ``` huffman@21164 ` 1192` ``` then obtain l where ldef: "\z. a < z \ z < b \ DERIV ?h z :> l \ ?h b - ?h a = (b - a) * l" .. ``` huffman@21164 ` 1193` ``` then obtain c where cdef: "a < c \ c < b \ DERIV ?h c :> l \ ?h b - ?h a = (b - a) * l" .. ``` huffman@21164 ` 1194` huffman@21164 ` 1195` ``` from cdef have cint: "a < c \ c < b" by auto ``` huffman@21164 ` 1196` ``` with gd have "g differentiable c" by simp ``` huffman@21164 ` 1197` ``` hence "\D. DERIV g c :> D" by (rule differentiableD) ``` huffman@21164 ` 1198` ``` then obtain g'c where g'cdef: "DERIV g c :> g'c" .. ``` huffman@21164 ` 1199` huffman@21164 ` 1200` ``` from cdef have "a < c \ c < b" by auto ``` huffman@21164 ` 1201` ``` with fd have "f differentiable c" by simp ``` huffman@21164 ` 1202` ``` hence "\D. DERIV f c :> D" by (rule differentiableD) ``` huffman@21164 ` 1203` ``` then obtain f'c where f'cdef: "DERIV f c :> f'c" .. ``` huffman@21164 ` 1204` huffman@21164 ` 1205` ``` from cdef have "DERIV ?h c :> l" by auto ``` hoelzl@41368 ` 1206` ``` moreover have "DERIV ?h c :> g'c * (f b - f a) - f'c * (g b - g a)" ``` hoelzl@41368 ` 1207` ``` using g'cdef f'cdef by (auto intro!: DERIV_intros) ``` huffman@21164 ` 1208` ``` ultimately have leq: "l = g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique) ``` huffman@21164 ` 1209` huffman@21164 ` 1210` ``` { ``` huffman@21164 ` 1211` ``` from cdef have "?h b - ?h a = (b - a) * l" by auto ``` huffman@21164 ` 1212` ``` also with leq have "\ = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp ``` huffman@21164 ` 1213` ``` finally have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp ``` huffman@21164 ` 1214` ``` } ``` huffman@21164 ` 1215` ``` moreover ``` huffman@21164 ` 1216` ``` { ``` huffman@21164 ` 1217` ``` have "?h b - ?h a = ``` huffman@21164 ` 1218` ``` ((f b)*(g b) - (f a)*(g b) - (g b)*(f b) + (g a)*(f b)) - ``` huffman@21164 ` 1219` ``` ((f b)*(g a) - (f a)*(g a) - (g b)*(f a) + (g a)*(f a))" ``` nipkow@29667 ` 1220` ``` by (simp add: algebra_simps) ``` huffman@21164 ` 1221` ``` hence "?h b - ?h a = 0" by auto ``` huffman@21164 ` 1222` ``` } ``` huffman@21164 ` 1223` ``` ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto ``` huffman@21164 ` 1224` ``` with alb have "g'c * (f b - f a) - f'c * (g b - g a) = 0" by simp ``` huffman@21164 ` 1225` ``` hence "g'c * (f b - f a) = f'c * (g b - g a)" by simp ``` huffman@21164 ` 1226` ``` hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: mult_ac) ``` huffman@21164 ` 1227` huffman@21164 ` 1228` ``` with g'cdef f'cdef cint show ?thesis by auto ``` huffman@21164 ` 1229` ```qed ``` huffman@21164 ` 1230` huffman@29470 ` 1231` huffman@29166 ` 1232` ```subsection {* Theorems about Limits *} ``` huffman@29166 ` 1233` huffman@29166 ` 1234` ```(* need to rename second isCont_inverse *) ``` huffman@29166 ` 1235` huffman@29166 ` 1236` ```lemma isCont_inv_fun: ``` huffman@29166 ` 1237` ``` fixes f g :: "real \ real" ``` huffman@29166 ` 1238` ``` shows "[| 0 < d; \z. \z - x\ \ d --> g(f(z)) = z; ``` huffman@29166 ` 1239` ``` \z. \z - x\ \ d --> isCont f z |] ``` huffman@29166 ` 1240` ``` ==> isCont g (f x)" ``` huffman@29166 ` 1241` ```by (rule isCont_inverse_function) ``` huffman@29166 ` 1242` huffman@29166 ` 1243` ```text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*} ``` huffman@29166 ` 1244` ```lemma LIM_fun_gt_zero: ``` huffman@29166 ` 1245` ``` "[| f -- c --> (l::real); 0 < l |] ``` huffman@29166 ` 1246` ``` ==> \r. 0 < r & (\x::real. x \ c & \c - x\ < r --> 0 < f x)" ``` huffman@44209 ` 1247` ```apply (drule (1) LIM_D, clarify) ``` huffman@29166 ` 1248` ```apply (rule_tac x = s in exI) ``` huffman@44209 ` 1249` ```apply (simp add: abs_less_iff) ``` huffman@29166 ` 1250` ```done ``` huffman@29166 ` 1251` huffman@29166 ` 1252` ```lemma LIM_fun_less_zero: ``` huffman@29166 ` 1253` ``` "[| f -- c --> (l::real); l < 0 |] ``` huffman@29166 ` 1254` ``` ==> \r. 0 < r & (\x::real. x \ c & \c - x\ < r --> f x < 0)" ``` huffman@44209 ` 1255` ```apply (drule LIM_D [where r="-l"], simp, clarify) ``` huffman@29166 ` 1256` ```apply (rule_tac x = s in exI) ``` huffman@44209 ` 1257` ```apply (simp add: abs_less_iff) ``` huffman@29166 ` 1258` ```done ``` huffman@29166 ` 1259` huffman@29166 ` 1260` ```lemma LIM_fun_not_zero: ``` huffman@29166 ` 1261` ``` "[| f -- c --> (l::real); l \ 0 |] ``` huffman@29166 ` 1262` ``` ==> \r. 0 < r & (\x::real. x \ c & \c - x\ < r --> f x \ 0)" ``` huffman@44209 ` 1263` ```apply (rule linorder_cases [of l 0]) ``` huffman@44209 ` 1264` ```apply (drule (1) LIM_fun_less_zero, force) ``` huffman@44209 ` 1265` ```apply simp ``` huffman@44209 ` 1266` ```apply (drule (1) LIM_fun_gt_zero, force) ``` huffman@29166 ` 1267` ```done ``` huffman@29166 ` 1268` hoelzl@50327 ` 1269` ```lemma GMVT': ``` hoelzl@50327 ` 1270` ``` fixes f g :: "real \ real" ``` hoelzl@50327 ` 1271` ``` assumes "a < b" ``` hoelzl@50327 ` 1272` ``` assumes isCont_f: "\z. a \ z \ z \ b \ isCont f z" ``` hoelzl@50327 ` 1273` ``` assumes isCont_g: "\z. a \ z \ z \ b \ isCont g z" ``` hoelzl@50327 ` 1274` ``` assumes DERIV_g: "\z. a < z \ z < b \ DERIV g z :> (g' z)" ``` hoelzl@50327 ` 1275` ``` assumes DERIV_f: "\z. a < z \ z < b \ DERIV f z :> (f' z)" ``` hoelzl@50327 ` 1276` ``` shows "\c. a < c \ c < b \ (f b - f a) * g' c = (g b - g a) * f' c" ``` hoelzl@50327 ` 1277` ```proof - ``` hoelzl@50327 ` 1278` ``` have "\g'c f'c c. DERIV g c :> g'c \ DERIV f c :> f'c \ ``` hoelzl@50327 ` 1279` ``` a < c \ c < b \ (f b - f a) * g'c = (g b - g a) * f'c" ``` hoelzl@50327 ` 1280` ``` using assms by (intro GMVT) (force simp: differentiable_def)+ ``` hoelzl@50327 ` 1281` ``` then obtain c where "a < c" "c < b" "(f b - f a) * g' c = (g b - g a) * f' c" ``` hoelzl@50327 ` 1282` ``` using DERIV_f DERIV_g by (force dest: DERIV_unique) ``` hoelzl@50327 ` 1283` ``` then show ?thesis ``` hoelzl@50327 ` 1284` ``` by auto ``` hoelzl@50327 ` 1285` ```qed ``` hoelzl@50327 ` 1286` hoelzl@50329 ` 1287` ```lemma DERIV_cong_ev: "x = y \ eventually (\x. f x = g x) (nhds x) \ u = v \ ``` hoelzl@50329 ` 1288` ``` DERIV f x :> u \ DERIV g y :> v" ``` hoelzl@50329 ` 1289` ``` unfolding DERIV_iff2 ``` hoelzl@50329 ` 1290` ```proof (rule filterlim_cong) ``` hoelzl@50329 ` 1291` ``` assume "eventually (\x. f x = g x) (nhds x)" ``` hoelzl@50329 ` 1292` ``` moreover then have "f x = g x" by (auto simp: eventually_nhds) ``` hoelzl@50329 ` 1293` ``` moreover assume "x = y" "u = v" ``` hoelzl@50329 ` 1294` ``` ultimately show "eventually (\xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)" ``` hoelzl@50329 ` 1295` ``` by (auto simp: eventually_within at_def elim: eventually_elim1) ``` hoelzl@50329 ` 1296` ```qed simp_all ``` hoelzl@50329 ` 1297` hoelzl@50330 ` 1298` ```lemma DERIV_shift: ``` hoelzl@50330 ` 1299` ``` "(DERIV f (x + z) :> y) \ (DERIV (\x. f (x + z)) x :> y)" ``` hoelzl@50330 ` 1300` ``` by (simp add: DERIV_iff field_simps) ``` hoelzl@50329 ` 1301` hoelzl@50330 ` 1302` ```lemma DERIV_mirror: ``` hoelzl@50330 ` 1303` ``` "(DERIV f (- x) :> y) \ (DERIV (\x. f (- x::real) :: real) x :> - y)" ``` hoelzl@50330 ` 1304` ``` by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right ``` hoelzl@50330 ` 1305` ``` tendsto_minus_cancel_left field_simps conj_commute) ``` hoelzl@50329 ` 1306` hoelzl@50327 ` 1307` ```lemma lhopital_right_0: ``` hoelzl@50329 ` 1308` ``` fixes f0 g0 :: "real \ real" ``` hoelzl@50329 ` 1309` ``` assumes f_0: "(f0 ---> 0) (at_right 0)" ``` hoelzl@50329 ` 1310` ``` assumes g_0: "(g0 ---> 0) (at_right 0)" ``` hoelzl@50327 ` 1311` ``` assumes ev: ``` hoelzl@50329 ` 1312` ``` "eventually (\x. g0 x \ 0) (at_right 0)" ``` hoelzl@50327 ` 1313` ``` "eventually (\x. g' x \ 0) (at_right 0)" ``` hoelzl@50329 ` 1314` ``` "eventually (\x. DERIV f0 x :> f' x) (at_right 0)" ``` hoelzl@50329 ` 1315` ``` "eventually (\x. DERIV g0 x :> g' x) (at_right 0)" ``` hoelzl@50327 ` 1316` ``` assumes lim: "((\ x. (f' x / g' x)) ---> x) (at_right 0)" ``` hoelzl@50329 ` 1317` ``` shows "((\ x. f0 x / g0 x) ---> x) (at_right 0)" ``` hoelzl@50327 ` 1318` ```proof - ``` hoelzl@50329 ` 1319` ``` def f \ "\x. if x \ 0 then 0 else f0 x" ``` hoelzl@50329 ` 1320` ``` then have "f 0 = 0" by simp ``` hoelzl@50329 ` 1321` hoelzl@50329 ` 1322` ``` def g \ "\x. if x \ 0 then 0 else g0 x" ``` hoelzl@50329 ` 1323` ``` then have "g 0 = 0" by simp ``` hoelzl@50329 ` 1324` hoelzl@50329 ` 1325` ``` have "eventually (\x. g0 x \ 0 \ g' x \ 0 \ ``` hoelzl@50329 ` 1326` ``` DERIV f0 x :> (f' x) \ DERIV g0 x :> (g' x)) (at_right 0)" ``` hoelzl@50329 ` 1327` ``` using ev by eventually_elim auto ``` hoelzl@50329 ` 1328` ``` then obtain a where [arith]: "0 < a" ``` hoelzl@50329 ` 1329` ``` and g0_neq_0: "\x. 0 < x \ x < a \ g0 x \ 0" ``` hoelzl@50327 ` 1330` ``` and g'_neq_0: "\x. 0 < x \ x < a \ g' x \ 0" ``` hoelzl@50329 ` 1331` ``` and f0: "\x. 0 < x \ x < a \ DERIV f0 x :> (f' x)" ``` hoelzl@50329 ` 1332` ``` and g0: "\x. 0 < x \ x < a \ DERIV g0 x :> (g' x)" ``` hoelzl@50327 ` 1333` ``` unfolding eventually_within eventually_at by (auto simp: dist_real_def) ``` hoelzl@50327 ` 1334` hoelzl@50329 ` 1335` ``` have g_neq_0: "\x. 0 < x \ x < a \ g x \ 0" ``` hoelzl@50329 ` 1336` ``` using g0_neq_0 by (simp add: g_def) ``` hoelzl@50329 ` 1337` hoelzl@50329 ` 1338` ``` { fix x assume x: "0 < x" "x < a" then have "DERIV f x :> (f' x)" ``` hoelzl@50329 ` 1339` ``` by (intro DERIV_cong_ev[THEN iffD1, OF _ _ _ f0[OF x]]) ``` hoelzl@50329 ` 1340` ``` (auto simp: f_def eventually_nhds_metric dist_real_def intro!: exI[of _ x]) } ``` hoelzl@50329 ` 1341` ``` note f = this ``` hoelzl@50329 ` 1342` hoelzl@50329 ` 1343` ``` { fix x assume x: "0 < x" "x < a" then have "DERIV g x :> (g' x)" ``` hoelzl@50329 ` 1344` ``` by (intro DERIV_cong_ev[THEN iffD1, OF _ _ _ g0[OF x]]) ``` hoelzl@50329 ` 1345` ``` (auto simp: g_def eventually_nhds_metric dist_real_def intro!: exI[of _ x]) } ``` hoelzl@50329 ` 1346` ``` note g = this ``` hoelzl@50329 ` 1347` hoelzl@50329 ` 1348` ``` have "isCont f 0" ``` hoelzl@50329 ` 1349` ``` using tendsto_const[of "0::real" "at 0"] f_0 ``` hoelzl@50329 ` 1350` ``` unfolding isCont_def f_def ``` hoelzl@50329 ` 1351` ``` by (intro filterlim_split_at_real) ``` hoelzl@50329 ` 1352` ``` (auto elim: eventually_elim1 ``` hoelzl@50329 ` 1353` ``` simp add: filterlim_def le_filter_def eventually_within eventually_filtermap) ``` hoelzl@50329 ` 1354` ``` ``` hoelzl@50329 ` 1355` ``` have "isCont g 0" ``` hoelzl@50329 ` 1356` ``` using tendsto_const[of "0::real" "at 0"] g_0 ``` hoelzl@50329 ` 1357` ``` unfolding isCont_def g_def ``` hoelzl@50329 ` 1358` ``` by (intro filterlim_split_at_real) ``` hoelzl@50329 ` 1359` ``` (auto elim: eventually_elim1 ``` hoelzl@50329 ` 1360` ``` simp add: filterlim_def le_filter_def eventually_within eventually_filtermap) ``` hoelzl@50329 ` 1361` hoelzl@50327 ` 1362` ``` have "\\. \x\{0 <..< a}. 0 < \ x \ \ x < x \ f x / g x = f' (\ x) / g' (\ x)" ``` hoelzl@50327 ` 1363` ``` proof (rule bchoice, rule) ``` hoelzl@50327 ` 1364` ``` fix x assume "x \ {0 <..< a}" ``` hoelzl@50327 ` 1365` ``` then have x[arith]: "0 < x" "x < a" by auto ``` hoelzl@50327 ` 1366` ``` with g'_neq_0 g_neq_0 `g 0 = 0` have g': "\x. 0 < x \ x < a \ 0 \ g' x" "g 0 \ g x" ``` hoelzl@50327 ` 1367` ``` by auto ``` hoelzl@50328 ` 1368` ``` have "\x. 0 \ x \ x < a \ isCont f x" ``` hoelzl@50328 ` 1369` ``` using `isCont f 0` f by (auto intro: DERIV_isCont simp: le_less) ``` hoelzl@50328 ` 1370` ``` moreover have "\x. 0 \ x \ x < a \ isCont g x" ``` hoelzl@50328 ` 1371` ``` using `isCont g 0` g by (auto intro: DERIV_isCont simp: le_less) ``` hoelzl@50328 ` 1372` ``` ultimately have "\c. 0 < c \ c < x \ (f x - f 0) * g' c = (g x - g 0) * f' c" ``` hoelzl@50328 ` 1373` ``` using f g `x < a` by (intro GMVT') auto ``` hoelzl@50327 ` 1374` ``` then guess c .. ``` hoelzl@50327 ` 1375` ``` moreover ``` hoelzl@50327 ` 1376` ``` with g'(1)[of c] g'(2) have "(f x - f 0) / (g x - g 0) = f' c / g' c" ``` hoelzl@50327 ` 1377` ``` by (simp add: field_simps) ``` hoelzl@50327 ` 1378` ``` ultimately show "\y. 0 < y \ y < x \ f x / g x = f' y / g' y" ``` hoelzl@50327 ` 1379` ``` using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c]) ``` hoelzl@50327 ` 1380` ``` qed ``` hoelzl@50327 ` 1381` ``` then guess \ .. ``` hoelzl@50327 ` 1382` ``` then have \: "eventually (\x. 0 < \ x \ \ x < x \ f x / g x = f' (\ x) / g' (\ x)) (at_right 0)" ``` hoelzl@50327 ` 1383` ``` unfolding eventually_within eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def) ``` hoelzl@50327 ` 1384` ``` moreover ``` hoelzl@50327 ` 1385` ``` from \ have "eventually (\x. norm (\ x) \ x) (at_right 0)" ``` hoelzl@50327 ` 1386` ``` by eventually_elim auto ``` hoelzl@50327 ` 1387` ``` then have "((\x. norm (\ x)) ---> 0) (at_right 0)" ``` hoelzl@50327 ` 1388` ``` by (rule_tac real_tendsto_sandwich[where f="\x. 0" and h="\x. x"]) ``` hoelzl@50327 ` 1389` ``` (auto intro: tendsto_const tendsto_ident_at_within) ``` hoelzl@50327 ` 1390` ``` then have "(\ ---> 0) (at_right 0)" ``` hoelzl@50327 ` 1391` ``` by (rule tendsto_norm_zero_cancel) ``` hoelzl@50327 ` 1392` ``` with \ have "filterlim \ (at_right 0) (at_right 0)" ``` hoelzl@50327 ` 1393` ``` by (auto elim!: eventually_elim1 simp: filterlim_within filterlim_at) ``` hoelzl@50327 ` 1394` ``` from this lim have "((\t. f' (\ t) / g' (\ t)) ---> x) (at_right 0)" ``` hoelzl@50327 ` 1395` ``` by (rule_tac filterlim_compose[of _ _ _ \]) ``` hoelzl@50329 ` 1396` ``` ultimately have "((\t. f t / g t) ---> x) (at_right 0)" (is ?P) ``` hoelzl@50328 ` 1397` ``` by (rule_tac filterlim_cong[THEN iffD1, OF refl refl]) ``` hoelzl@50328 ` 1398` ``` (auto elim: eventually_elim1) ``` hoelzl@50329 ` 1399` ``` also have "?P \ ?thesis" ``` hoelzl@50329 ` 1400` ``` by (rule filterlim_cong) (auto simp: f_def g_def eventually_within) ``` hoelzl@50329 ` 1401` ``` finally show ?thesis . ``` hoelzl@50327 ` 1402` ```qed ``` hoelzl@50327 ` 1403` hoelzl@50330 ` 1404` ```lemma lhopital_right: ``` hoelzl@50330 ` 1405` ``` "((f::real \ real) ---> 0) (at_right x) \ (g ---> 0) (at_right x) \ ``` hoelzl@50330 ` 1406` ``` eventually (\x. g x \ 0) (at_right x) \ ``` hoelzl@50330 ` 1407` ``` eventually (\x. g' x \ 0) (at_right x) \ ``` hoelzl@50330 ` 1408` ``` eventually (\x. DERIV f x :> f' x) (at_right x) \ ``` hoelzl@50330 ` 1409` ``` eventually (\x. DERIV g x :> g' x) (at_right x) \ ``` hoelzl@50330 ` 1410` ``` ((\ x. (f' x / g' x)) ---> y) (at_right x) \ ``` hoelzl@50330 ` 1411` ``` ((\ x. f x / g x) ---> y) (at_right x)" ``` hoelzl@50330 ` 1412` ``` unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift ``` hoelzl@50330 ` 1413` ``` by (rule lhopital_right_0) ``` hoelzl@50330 ` 1414` hoelzl@50330 ` 1415` ```lemma lhopital_left: ``` hoelzl@50330 ` 1416` ``` "((f::real \ real) ---> 0) (at_left x) \ (g ---> 0) (at_left x) \ ``` hoelzl@50330 ` 1417` ``` eventually (\x. g x \ 0) (at_left x) \ ``` hoelzl@50330 ` 1418` ``` eventually (\x. g' x \ 0) (at_left x) \ ``` hoelzl@50330 ` 1419` ``` eventually (\x. DERIV f x :> f' x) (at_left x) \ ``` hoelzl@50330 ` 1420` ``` eventually (\x. DERIV g x :> g' x) (at_left x) \ ``` hoelzl@50330 ` 1421` ``` ((\ x. (f' x / g' x)) ---> y) (at_left x) \ ``` hoelzl@50330 ` 1422` ``` ((\ x. f x / g x) ---> y) (at_left x)" ``` hoelzl@50330 ` 1423` ``` unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror ``` hoelzl@50330 ` 1424` ``` by (rule lhopital_right[where f'="\x. - f' (- x)"]) (auto simp: DERIV_mirror) ``` hoelzl@50330 ` 1425` hoelzl@50330 ` 1426` ```lemma lhopital: ``` hoelzl@50330 ` 1427` ``` "((f::real \ real) ---> 0) (at x) \ (g ---> 0) (at x) \ ``` hoelzl@50330 ` 1428` ``` eventually (\x. g x \ 0) (at x) \ ``` hoelzl@50330 ` 1429` ``` eventually (\x. g' x \ 0) (at x) \ ``` hoelzl@50330 ` 1430` ``` eventually (\x. DERIV f x :> f' x) (at x) \ ``` hoelzl@50330 ` 1431` ``` eventually (\x. DERIV g x :> g' x) (at x) \ ``` hoelzl@50330 ` 1432` ``` ((\ x. (f' x / g' x)) ---> y) (at x) \ ``` hoelzl@50330 ` 1433` ``` ((\ x. f x / g x) ---> y) (at x)" ``` hoelzl@50330 ` 1434` ``` unfolding eventually_at_split filterlim_at_split ``` hoelzl@50330 ` 1435` ``` by (auto intro!: lhopital_right[of f x g g' f'] lhopital_left[of f x g g' f']) ``` hoelzl@50330 ` 1436` hoelzl@50327 ` 1437` ```lemma lhopital_right_0_at_top: ``` hoelzl@50327 ` 1438` ``` fixes f g :: "real \ real" ``` hoelzl@50327 ` 1439` ``` assumes g_0: "LIM x at_right 0. g x :> at_top" ``` hoelzl@50327 ` 1440` ``` assumes ev: ``` hoelzl@50327 ` 1441` ``` "eventually (\x. g' x \ 0) (at_right 0)" ``` hoelzl@50327 ` 1442` ``` "eventually (\x. DERIV f x :> f' x) (at_right 0)" ``` hoelzl@50327 ` 1443` ``` "eventually (\x. DERIV g x :> g' x) (at_right 0)" ``` hoelzl@50327 ` 1444` ``` assumes lim: "((\ x. (f' x / g' x)) ---> x) (at_right 0)" ``` hoelzl@50327 ` 1445` ``` shows "((\ x. f x / g x) ---> x) (at_right 0)" ``` hoelzl@50327 ` 1446` ``` unfolding tendsto_iff ``` hoelzl@50327 ` 1447` ```proof safe ``` hoelzl@50327 ` 1448` ``` fix e :: real assume "0 < e" ``` hoelzl@50327 ` 1449` hoelzl@50327 ` 1450` ``` with lim[unfolded tendsto_iff, rule_format, of "e / 4"] ``` hoelzl@50327 ` 1451` ``` have "eventually (\t. dist (f' t / g' t) x < e / 4) (at_right 0)" by simp ``` hoelzl@50327 ` 1452` ``` from eventually_conj[OF eventually_conj[OF ev(1) ev(2)] eventually_conj[OF ev(3) this]] ``` hoelzl@50327 ` 1453` ``` obtain a where [arith]: "0 < a" ``` hoelzl@50327 ` 1454` ``` and g'_neq_0: "\x. 0 < x \ x < a \ g' x \ 0" ``` hoelzl@50327 ` 1455` ``` and f0: "\x. 0 < x \ x \ a \ DERIV f x :> (f' x)" ``` hoelzl@50327 ` 1456` ``` and g0: "\x. 0 < x \ x \ a \ DERIV g x :> (g' x)" ``` hoelzl@50327 ` 1457` ``` and Df: "\t. 0 < t \ t < a \ dist (f' t / g' t) x < e / 4" ``` hoelzl@50327 ` 1458` ``` unfolding eventually_within_le by (auto simp: dist_real_def) ``` hoelzl@50327 ` 1459` hoelzl@50327 ` 1460` ``` from Df have ``` hoelzl@50328 ` 1461` ``` "eventually (\t. t < a) (at_right 0)" "eventually (\t::real. 0 < t) (at_right 0)" ``` hoelzl@50327 ` 1462` ``` unfolding eventually_within eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def) ``` hoelzl@50327 ` 1463` hoelzl@50327 ` 1464` ``` moreover ``` hoelzl@50328 ` 1465` ``` have "eventually (\t. 0 < g t) (at_right 0)" "eventually (\t. g a < g t) (at_right 0)" ``` hoelzl@50346 ` 1466` ``` using g_0 by (auto elim: eventually_elim1 simp: filterlim_at_top_dense) ``` hoelzl@50327 ` 1467` hoelzl@50327 ` 1468` ``` moreover ``` hoelzl@50327 ` 1469` ``` have inv_g: "((\x. inverse (g x)) ---> 0) (at_right 0)" ``` hoelzl@50327 ` 1470` ``` using tendsto_inverse_0 filterlim_mono[OF g_0 at_top_le_at_infinity order_refl] ``` hoelzl@50327 ` 1471` ``` by (rule filterlim_compose) ``` hoelzl@50327 ` 1472` ``` then have "((\x. norm (1 - g a * inverse (g x))) ---> norm (1 - g a * 0)) (at_right 0)" ``` hoelzl@50327 ` 1473` ``` by (intro tendsto_intros) ``` hoelzl@50327 ` 1474` ``` then have "((\x. norm (1 - g a / g x)) ---> 1) (at_right 0)" ``` hoelzl@50327 ` 1475` ``` by (simp add: inverse_eq_divide) ``` hoelzl@50327 ` 1476` ``` from this[unfolded tendsto_iff, rule_format, of 1] ``` hoelzl@50327 ` 1477` ``` have "eventually (\x. norm (1 - g a / g x) < 2) (at_right 0)" ``` hoelzl@50327 ` 1478` ``` by (auto elim!: eventually_elim1 simp: dist_real_def) ``` hoelzl@50327 ` 1479` hoelzl@50327 ` 1480` ``` moreover ``` hoelzl@50327 ` 1481` ``` from inv_g have "((\t. norm ((f a - x * g a) * inverse (g t))) ---> norm ((f a - x * g a) * 0)) (at_right 0)" ``` hoelzl@50327 ` 1482` ``` by (intro tendsto_intros) ``` hoelzl@50327 ` 1483` ``` then have "((\t. norm (f a - x * g a) / norm (g t)) ---> 0) (at_right 0)" ``` hoelzl@50327 ` 1484` ``` by (simp add: inverse_eq_divide) ``` hoelzl@50327 ` 1485` ``` from this[unfolded tendsto_iff, rule_format, of "e / 2"] `0 < e` ``` hoelzl@50327 ` 1486` ``` have "eventually (\t. norm (f a - x * g a) / norm (g t) < e / 2) (at_right 0)" ``` hoelzl@50327 ` 1487` ``` by (auto simp: dist_real_def) ``` hoelzl@50327 ` 1488` hoelzl@50327 ` 1489` ``` ultimately show "eventually (\t. dist (f t / g t) x < e) (at_right 0)" ``` hoelzl@50327 ` 1490` ``` proof eventually_elim ``` hoelzl@50327 ` 1491` ``` fix t assume t[arith]: "0 < t" "t < a" "g a < g t" "0 < g t" ``` hoelzl@50327 ` 1492` ``` assume ineq: "norm (1 - g a / g t) < 2" "norm (f a - x * g a) / norm (g t) < e / 2" ``` hoelzl@50327 ` 1493` hoelzl@50327 ` 1494` ``` have "\y. t < y \ y < a \ (g a - g t) * f' y = (f a - f t) * g' y" ``` hoelzl@50327 ` 1495` ``` using f0 g0 t(1,2) by (intro GMVT') (force intro!: DERIV_isCont)+ ``` hoelzl@50327 ` 1496` ``` then guess y .. ``` hoelzl@50327 ` 1497` ``` from this ``` hoelzl@50327 ` 1498` ``` have [arith]: "t < y" "y < a" and D_eq: "(f t - f a) / (g t - g a) = f' y / g' y" ``` hoelzl@50327 ` 1499` ``` using `g a < g t` g'_neq_0[of y] by (auto simp add: field_simps) ``` hoelzl@50327 ` 1500` hoelzl@50327 ` 1501` ``` have *: "f t / g t - x = ((f t - f a) / (g t - g a) - x) * (1 - g a / g t) + (f a - x * g a) / g t" ``` hoelzl@50327 ` 1502` ``` by (simp add: field_simps) ``` hoelzl@50327 ` 1503` ``` have "norm (f t / g t - x) \ ``` hoelzl@50327 ` 1504` ``` norm (((f t - f a) / (g t - g a) - x) * (1 - g a / g t)) + norm ((f a - x * g a) / g t)" ``` hoelzl@50327 ` 1505` ``` unfolding * by (rule norm_triangle_ineq) ``` hoelzl@50327 ` 1506` ``` also have "\ = dist (f' y / g' y) x * norm (1 - g a / g t) + norm (f a - x * g a) / norm (g t)" ``` hoelzl@50327 ` 1507` ``` by (simp add: abs_mult D_eq dist_real_def) ``` hoelzl@50327 ` 1508` ``` also have "\ < (e / 4) * 2 + e / 2" ``` hoelzl@50327 ` 1509` ``` using ineq Df[of y] `0 < e` by (intro add_le_less_mono mult_mono) auto ``` hoelzl@50327 ` 1510` ``` finally show "dist (f t / g t) x < e" ``` hoelzl@50327 ` 1511` ``` by (simp add: dist_real_def) ``` hoelzl@50327 ` 1512` ``` qed ``` hoelzl@50327 ` 1513` ```qed ``` hoelzl@50327 ` 1514` hoelzl@50330 ` 1515` ```lemma lhopital_right_at_top: ``` hoelzl@50330 ` 1516` ``` "LIM x at_right x. (g::real \ real) x :> at_top \ ``` hoelzl@50330 ` 1517` ``` eventually (\x. g' x \ 0) (at_right x) \ ``` hoelzl@50330 ` 1518` ``` eventually (\x. DERIV f x :> f' x) (at_right x) \ ``` hoelzl@50330 ` 1519` ``` eventually (\x. DERIV g x :> g' x) (at_right x) \ ``` hoelzl@50330 ` 1520` ``` ((\ x. (f' x / g' x)) ---> y) (at_right x) \ ``` hoelzl@50330 ` 1521` ``` ((\ x. f x / g x) ---> y) (at_right x)" ``` hoelzl@50330 ` 1522` ``` unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift ``` hoelzl@50330 ` 1523` ``` by (rule lhopital_right_0_at_top) ``` hoelzl@50330 ` 1524` hoelzl@50330 ` 1525` ```lemma lhopital_left_at_top: ``` hoelzl@50330 ` 1526` ``` "LIM x at_left x. (g::real \ real) x :> at_top \ ``` hoelzl@50330 ` 1527` ``` eventually (\x. g' x \ 0) (at_left x) \ ``` hoelzl@50330 ` 1528` ``` eventually (\x. DERIV f x :> f' x) (at_left x) \ ``` hoelzl@50330 ` 1529` ``` eventually (\x. DERIV g x :> g' x) (at_left x) \ ``` hoelzl@50330 ` 1530` ``` ((\ x. (f' x / g' x)) ---> y) (at_left x) \ ``` hoelzl@50330 ` 1531` ``` ((\ x. f x / g x) ---> y) (at_left x)" ``` hoelzl@50330 ` 1532` ``` unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror ``` hoelzl@50330 ` 1533` ``` by (rule lhopital_right_at_top[where f'="\x. - f' (- x)"]) (auto simp: DERIV_mirror) ``` hoelzl@50330 ` 1534` hoelzl@50330 ` 1535` ```lemma lhopital_at_top: ``` hoelzl@50330 ` 1536` ``` "LIM x at x. (g::real \ real) x :> at_top \ ``` hoelzl@50330 ` 1537` ``` eventually (\x. g' x \ 0) (at x) \ ``` hoelzl@50330 ` 1538` ``` eventually (\x. DERIV f x :> f' x) (at x) \ ``` hoelzl@50330 ` 1539` ``` eventually (\x. DERIV g x :> g' x) (at x) \ ``` hoelzl@50330 ` 1540` ``` ((\ x. (f' x / g' x)) ---> y) (at x) \ ``` hoelzl@50330 ` 1541` ``` ((\ x. f x / g x) ---> y) (at x)" ``` hoelzl@50330 ` 1542` ``` unfolding eventually_at_split filterlim_at_split ``` hoelzl@50330 ` 1543` ``` by (auto intro!: lhopital_right_at_top[of g x g' f f'] lhopital_left_at_top[of g x g' f f']) ``` hoelzl@50330 ` 1544` hoelzl@50347 ` 1545` ```lemma lhospital_at_top_at_top: ``` hoelzl@50347 ` 1546` ``` fixes f g :: "real \ real" ``` hoelzl@50347 ` 1547` ``` assumes g_0: "LIM x at_top. g x :> at_top" ``` hoelzl@50347 ` 1548` ``` assumes g': "eventually (\x. g' x \ 0) at_top" ``` hoelzl@50347 ` 1549` ``` assumes Df: "eventually (\x. DERIV f x :> f' x) at_top" ``` hoelzl@50347 ` 1550` ``` assumes Dg: "eventually (\x. DERIV g x :> g' x) at_top" ``` hoelzl@50347 ` 1551` ``` assumes lim: "((\ x. (f' x / g' x)) ---> x) at_top" ``` hoelzl@50347 ` 1552` ``` shows "((\ x. f x / g x) ---> x) at_top" ``` hoelzl@50347 ` 1553` ``` unfolding filterlim_at_top_to_right ``` hoelzl@50347 ` 1554` ```proof (rule lhopital_right_0_at_top) ``` hoelzl@50347 ` 1555` ``` let ?F = "\x. f (inverse x)" ``` hoelzl@50347 ` 1556` ``` let ?G = "\x. g (inverse x)" ``` hoelzl@50347 ` 1557` ``` let ?R = "at_right (0::real)" ``` hoelzl@50347 ` 1558` ``` let ?D = "\f' x. f' (inverse x) * - (inverse x ^ Suc (Suc 0))" ``` hoelzl@50347 ` 1559` hoelzl@50347 ` 1560` ``` show "LIM x ?R. ?G x :> at_top" ``` hoelzl@50347 ` 1561` ``` using g_0 unfolding filterlim_at_top_to_right . ``` hoelzl@50347 ` 1562` hoelzl@50347 ` 1563` ``` show "eventually (\x. DERIV ?G x :> ?D g' x) ?R" ``` hoelzl@50347 ` 1564` ``` unfolding eventually_at_right_to_top ``` hoelzl@50347 ` 1565` ``` using Dg eventually_ge_at_top[where c="1::real"] ``` hoelzl@50347 ` 1566` ``` apply eventually_elim ``` hoelzl@50347 ` 1567` ``` apply (rule DERIV_cong) ``` hoelzl@50347 ` 1568` ``` apply (rule DERIV_chain'[where f=inverse]) ``` hoelzl@50347 ` 1569` ``` apply (auto intro!: DERIV_inverse) ``` hoelzl@50347 ` 1570` ``` done ``` hoelzl@50347 ` 1571` hoelzl@50347 ` 1572` ``` show "eventually (\x. DERIV ?F x :> ?D f' x) ?R" ``` hoelzl@50347 ` 1573` ``` unfolding eventually_at_right_to_top ``` hoelzl@50347 ` 1574` ``` using Df eventually_ge_at_top[where c="1::real"] ``` hoelzl@50347 ` 1575` ``` apply eventually_elim ``` hoelzl@50347 ` 1576` ``` apply (rule DERIV_cong) ``` hoelzl@50347 ` 1577` ``` apply (rule DERIV_chain'[where f=inverse]) ``` hoelzl@50347 ` 1578` ``` apply (auto intro!: DERIV_inverse) ``` hoelzl@50347 ` 1579` ``` done ``` hoelzl@50347 ` 1580` hoelzl@50347 ` 1581` ``` show "eventually (\x. ?D g' x \ 0) ?R" ``` hoelzl@50347 ` 1582` ``` unfolding eventually_at_right_to_top ``` hoelzl@50347 ` 1583` ``` using g' eventually_ge_at_top[where c="1::real"] ``` hoelzl@50347 ` 1584` ``` by eventually_elim auto ``` hoelzl@50347 ` 1585` ``` ``` hoelzl@50347 ` 1586` ``` show "((\x. ?D f' x / ?D g' x) ---> x) ?R" ``` hoelzl@50347 ` 1587` ``` unfolding filterlim_at_right_to_top ``` hoelzl@50347 ` 1588` ``` apply (intro filterlim_cong[THEN iffD2, OF refl refl _ lim]) ``` hoelzl@50347 ` 1589` ``` using eventually_ge_at_top[where c="1::real"] ``` hoelzl@50347 ` 1590` ``` by eventually_elim simp ``` hoelzl@50347 ` 1591` ```qed ``` hoelzl@50347 ` 1592` huffman@21164 ` 1593` ```end ```