# HG changeset patch # User huffman # Date 1235015499 28800 # Node ID 6b1ccda8bf19731c0388d8e0961b75d64f676fc0 # Parent 57975b45ab70e60407e4c1c6b46a3bf262804c88 move FrechetDeriv.thy to Library diff -r 57975b45ab70 -r 6b1ccda8bf19 src/HOL/Complex_Main.thy --- a/src/HOL/Complex_Main.thy Wed Feb 18 19:32:26 2009 -0800 +++ b/src/HOL/Complex_Main.thy Wed Feb 18 19:51:39 2009 -0800 @@ -9,7 +9,6 @@ Ln Taylor Integration - FrechetDeriv begin end diff -r 57975b45ab70 -r 6b1ccda8bf19 src/HOL/FrechetDeriv.thy --- a/src/HOL/FrechetDeriv.thy Wed Feb 18 19:32:26 2009 -0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,503 +0,0 @@ -(* Title : FrechetDeriv.thy - ID : $Id$ - Author : Brian Huffman -*) - -header {* Frechet Derivative *} - -theory FrechetDeriv -imports Lim -begin - -definition - fderiv :: - "['a::real_normed_vector \ 'b::real_normed_vector, 'a, 'a \ 'b] \ bool" - -- {* Frechet derivative: D is derivative of function f at x *} - ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where - "FDERIV f x :> D = (bounded_linear D \ - (\h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)" - -lemma FDERIV_I: - "\bounded_linear D; (\h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0\ - \ FDERIV f x :> D" -by (simp add: fderiv_def) - -lemma FDERIV_D: - "FDERIV f x :> D \ (\h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0" -by (simp add: fderiv_def) - -lemma FDERIV_bounded_linear: "FDERIV f x :> D \ bounded_linear D" -by (simp add: fderiv_def) - -lemma bounded_linear_zero: - "bounded_linear (\x::'a::real_normed_vector. 0::'b::real_normed_vector)" -proof - show "(0::'b) = 0 + 0" by simp - fix r show "(0::'b) = scaleR r 0" by simp - have "\x::'a. norm (0::'b) \ norm x * 0" by simp - thus "\K. \x::'a. norm (0::'b) \ norm x * K" .. -qed - -lemma FDERIV_const: "FDERIV (\x. k) x :> (\h. 0)" -by (simp add: fderiv_def bounded_linear_zero) - -lemma bounded_linear_ident: - "bounded_linear (\x::'a::real_normed_vector. x)" -proof - fix x y :: 'a show "x + y = x + y" by simp - fix r and x :: 'a show "scaleR r x = scaleR r x" by simp - have "\x::'a. norm x \ norm x * 1" by simp - thus "\K. \x::'a. norm x \ norm x * K" .. -qed - -lemma FDERIV_ident: "FDERIV (\x. x) x :> (\h. h)" -by (simp add: fderiv_def bounded_linear_ident) - -subsection {* Addition *} - -lemma add_diff_add: - fixes a b c d :: "'a::ab_group_add" - shows "(a + c) - (b + d) = (a - b) + (c - d)" -by simp - -lemma bounded_linear_add: - assumes "bounded_linear f" - assumes "bounded_linear g" - shows "bounded_linear (\x. f x + g x)" -proof - - interpret f: bounded_linear f by fact - interpret g: bounded_linear g by fact - show ?thesis apply (unfold_locales) - apply (simp only: f.add g.add add_ac) - apply (simp only: f.scaleR g.scaleR scaleR_right_distrib) - apply (rule f.pos_bounded [THEN exE], rename_tac Kf) - apply (rule g.pos_bounded [THEN exE], rename_tac Kg) - apply (rule_tac x="Kf + Kg" in exI, safe) - apply (subst right_distrib) - apply (rule order_trans [OF norm_triangle_ineq]) - apply (rule add_mono, erule spec, erule spec) - done -qed - -lemma norm_ratio_ineq: - fixes x y :: "'a::real_normed_vector" - fixes h :: "'b::real_normed_vector" - shows "norm (x + y) / norm h \ norm x / norm h + norm y / norm h" -apply (rule ord_le_eq_trans) -apply (rule divide_right_mono) -apply (rule norm_triangle_ineq) -apply (rule norm_ge_zero) -apply (rule add_divide_distrib) -done - -lemma FDERIV_add: - assumes f: "FDERIV f x :> F" - assumes g: "FDERIV g x :> G" - shows "FDERIV (\x. f x + g x) x :> (\h. F h + G h)" -proof (rule FDERIV_I) - show "bounded_linear (\h. F h + G h)" - apply (rule bounded_linear_add) - apply (rule FDERIV_bounded_linear [OF f]) - apply (rule FDERIV_bounded_linear [OF g]) - done -next - have f': "(\h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0" - using f by (rule FDERIV_D) - have g': "(\h. norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0" - using g by (rule FDERIV_D) - from f' g' - have "(\h. norm (f (x + h) - f x - F h) / norm h - + norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0" - by (rule LIM_add_zero) - thus "(\h. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h)) - / norm h) -- 0 --> 0" - apply (rule real_LIM_sandwich_zero) - apply (simp add: divide_nonneg_pos) - apply (simp only: add_diff_add) - apply (rule norm_ratio_ineq) - done -qed - -subsection {* Subtraction *} - -lemma bounded_linear_minus: - assumes "bounded_linear f" - shows "bounded_linear (\x. - f x)" -proof - - interpret f: bounded_linear f by fact - show ?thesis apply (unfold_locales) - apply (simp add: f.add) - apply (simp add: f.scaleR) - apply (simp add: f.bounded) - done -qed - -lemma FDERIV_minus: - "FDERIV f x :> F \ FDERIV (\x. - f x) x :> (\h. - F h)" -apply (rule FDERIV_I) -apply (rule bounded_linear_minus) -apply (erule FDERIV_bounded_linear) -apply (simp only: fderiv_def minus_diff_minus norm_minus_cancel) -done - -lemma FDERIV_diff: - "\FDERIV f x :> F; FDERIV g x :> G\ - \ FDERIV (\x. f x - g x) x :> (\h. F h - G h)" -by (simp only: diff_minus FDERIV_add FDERIV_minus) - -subsection {* Continuity *} - -lemma FDERIV_isCont: - assumes f: "FDERIV f x :> F" - shows "isCont f x" -proof - - from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear) - have "(\h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0" - by (rule FDERIV_D [OF f]) - hence "(\h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0" - by (intro LIM_mult_zero LIM_norm_zero LIM_ident) - hence "(\h. norm (f (x + h) - f x - F h)) -- 0 --> 0" - by (simp cong: LIM_cong) - hence "(\h. f (x + h) - f x - F h) -- 0 --> 0" - by (rule LIM_norm_zero_cancel) - hence "(\h. f (x + h) - f x - F h + F h) -- 0 --> 0" - by (intro LIM_add_zero F.LIM_zero LIM_ident) - hence "(\h. f (x + h) - f x) -- 0 --> 0" - by simp - thus "isCont f x" - unfolding isCont_iff by (rule LIM_zero_cancel) -qed - -subsection {* Composition *} - -lemma real_divide_cancel_lemma: - fixes a b c :: real - shows "(b = 0 \ a = 0) \ (a / b) * (b / c) = a / c" -by simp - -lemma bounded_linear_compose: - assumes "bounded_linear f" - assumes "bounded_linear g" - shows "bounded_linear (\x. f (g x))" -proof - - interpret f: bounded_linear f by fact - interpret g: bounded_linear g by fact - show ?thesis proof (unfold_locales) - fix x y show "f (g (x + y)) = f (g x) + f (g y)" - by (simp only: f.add g.add) - next - fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))" - by (simp only: f.scaleR g.scaleR) - next - from f.pos_bounded - obtain Kf where f: "\x. norm (f x) \ norm x * Kf" and Kf: "0 < Kf" by fast - from g.pos_bounded - obtain Kg where g: "\x. norm (g x) \ norm x * Kg" by fast - show "\K. \x. norm (f (g x)) \ norm x * K" - proof (intro exI allI) - fix x - have "norm (f (g x)) \ norm (g x) * Kf" - using f . - also have "\ \ (norm x * Kg) * Kf" - using g Kf [THEN order_less_imp_le] by (rule mult_right_mono) - also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)" - by (rule mult_assoc) - finally show "norm (f (g x)) \ norm x * (Kg * Kf)" . - qed - qed -qed - -lemma FDERIV_compose: - fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" - fixes g :: "'b::real_normed_vector \ 'c::real_normed_vector" - assumes f: "FDERIV f x :> F" - assumes g: "FDERIV g (f x) :> G" - shows "FDERIV (\x. g (f x)) x :> (\h. G (F h))" -proof (rule FDERIV_I) - from FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f] - show "bounded_linear (\h. G (F h))" - by (rule bounded_linear_compose) -next - let ?Rf = "\h. f (x + h) - f x - F h" - let ?Rg = "\k. g (f x + k) - g (f x) - G k" - let ?k = "\h. f (x + h) - f x" - let ?Nf = "\h. norm (?Rf h) / norm h" - let ?Ng = "\h. norm (?Rg (?k h)) / norm (?k h)" - from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear) - from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear) - from F.bounded obtain kF where kF: "\x. norm (F x) \ norm x * kF" by fast - from G.bounded obtain kG where kG: "\x. norm (G x) \ norm x * kG" by fast - - let ?fun2 = "\h. ?Nf h * kG + ?Ng h * (?Nf h + kF)" - - show "(\h. norm (g (f (x + h)) - g (f x) - G (F h)) / norm h) -- 0 --> 0" - proof (rule real_LIM_sandwich_zero) - have Nf: "?Nf -- 0 --> 0" - using FDERIV_D [OF f] . - - have Ng1: "isCont (\k. norm (?Rg k) / norm k) 0" - by (simp add: isCont_def FDERIV_D [OF g]) - have Ng2: "?k -- 0 --> 0" - apply (rule LIM_zero) - apply (fold isCont_iff) - apply (rule FDERIV_isCont [OF f]) - done - have Ng: "?Ng -- 0 --> 0" - using isCont_LIM_compose [OF Ng1 Ng2] by simp - - have "(\h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) - -- 0 --> 0 * kG + 0 * (0 + kF)" - by (intro LIM_add LIM_mult LIM_const Nf Ng) - thus "(\h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0" - by simp - next - fix h::'a assume h: "h \ 0" - thus "0 \ norm (g (f (x + h)) - g (f x) - G (F h)) / norm h" - by (simp add: divide_nonneg_pos) - next - fix h::'a assume h: "h \ 0" - have "g (f (x + h)) - g (f x) - G (F h) = G (?Rf h) + ?Rg (?k h)" - by (simp add: G.diff) - hence "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h - = norm (G (?Rf h) + ?Rg (?k h)) / norm h" - by (rule arg_cong) - also have "\ \ norm (G (?Rf h)) / norm h + norm (?Rg (?k h)) / norm h" - by (rule norm_ratio_ineq) - also have "\ \ ?Nf h * kG + ?Ng h * (?Nf h + kF)" - proof (rule add_mono) - show "norm (G (?Rf h)) / norm h \ ?Nf h * kG" - apply (rule ord_le_eq_trans) - apply (rule divide_right_mono [OF kG norm_ge_zero]) - apply simp - done - next - have "norm (?Rg (?k h)) / norm h = ?Ng h * (norm (?k h) / norm h)" - apply (rule real_divide_cancel_lemma [symmetric]) - apply (simp add: G.zero) - done - also have "\ \ ?Ng h * (?Nf h + kF)" - proof (rule mult_left_mono) - have "norm (?k h) / norm h = norm (?Rf h + F h) / norm h" - by simp - also have "\ \ ?Nf h + norm (F h) / norm h" - by (rule norm_ratio_ineq) - also have "\ \ ?Nf h + kF" - apply (rule add_left_mono) - apply (subst pos_divide_le_eq, simp add: h) - apply (subst mult_commute) - apply (rule kF) - done - finally show "norm (?k h) / norm h \ ?Nf h + kF" . - next - show "0 \ ?Ng h" - apply (case_tac "f (x + h) - f x = 0", simp) - apply (rule divide_nonneg_pos [OF norm_ge_zero]) - apply simp - done - qed - finally show "norm (?Rg (?k h)) / norm h \ ?Ng h * (?Nf h + kF)" . - qed - finally show "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h - \ ?Nf h * kG + ?Ng h * (?Nf h + kF)" . - qed -qed - -subsection {* Product Rule *} - -lemma (in bounded_bilinear) FDERIV_lemma: - "a' ** b' - a ** b - (a ** B + A ** b) - = a ** (b' - b - B) + (a' - a - A) ** b' + A ** (b' - b)" -by (simp add: diff_left diff_right) - -lemma (in bounded_bilinear) FDERIV: - fixes x :: "'d::real_normed_vector" - assumes f: "FDERIV f x :> F" - assumes g: "FDERIV g x :> G" - shows "FDERIV (\x. f x ** g x) x :> (\h. f x ** G h + F h ** g x)" -proof (rule FDERIV_I) - show "bounded_linear (\h. f x ** G h + F h ** g x)" - apply (rule bounded_linear_add) - apply (rule bounded_linear_compose [OF bounded_linear_right]) - apply (rule FDERIV_bounded_linear [OF g]) - apply (rule bounded_linear_compose [OF bounded_linear_left]) - apply (rule FDERIV_bounded_linear [OF f]) - done -next - from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]] - obtain KF where norm_F: "\x. norm (F x) \ norm x * KF" by fast - - from pos_bounded obtain K where K: "0 < K" and norm_prod: - "\a b. norm (a ** b) \ norm a * norm b * K" by fast - - let ?Rf = "\h. f (x + h) - f x - F h" - let ?Rg = "\h. g (x + h) - g x - G h" - - let ?fun1 = "\h. - norm (f x ** ?Rg h + ?Rf h ** g (x + h) + F h ** (g (x + h) - g x)) / - norm h" - - let ?fun2 = "\h. - norm (f x) * (norm (?Rg h) / norm h) * K + - norm (?Rf h) / norm h * norm (g (x + h)) * K + - KF * norm (g (x + h) - g x) * K" - - have "?fun1 -- 0 --> 0" - proof (rule real_LIM_sandwich_zero) - from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]] - have "?fun2 -- 0 --> - norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K" - by (intro LIM_add LIM_mult LIM_const LIM_norm LIM_zero FDERIV_D) - thus "?fun2 -- 0 --> 0" - by simp - next - fix h::'d assume "h \ 0" - thus "0 \ ?fun1 h" - by (simp add: divide_nonneg_pos) - next - fix h::'d assume "h \ 0" - have "?fun1 h \ (norm (f x) * norm (?Rg h) * K + - norm (?Rf h) * norm (g (x + h)) * K + - norm h * KF * norm (g (x + h) - g x) * K) / norm h" - by (intro - divide_right_mono mult_mono' - order_trans [OF norm_triangle_ineq add_mono] - order_trans [OF norm_prod mult_right_mono] - mult_nonneg_nonneg order_refl norm_ge_zero norm_F - K [THEN order_less_imp_le] - ) - also have "\ = ?fun2 h" - by (simp add: add_divide_distrib) - finally show "?fun1 h \ ?fun2 h" . - qed - thus "(\h. - norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x)) - / norm h) -- 0 --> 0" - by (simp only: FDERIV_lemma) -qed - -lemmas FDERIV_mult = mult.FDERIV - -lemmas FDERIV_scaleR = scaleR.FDERIV - - -subsection {* Powers *} - -lemma FDERIV_power_Suc: - fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}" - shows "FDERIV (\x. x ^ Suc n) x :> (\h. (1 + of_nat n) * x ^ n * h)" - apply (induct n) - apply (simp add: power_Suc FDERIV_ident) - apply (drule FDERIV_mult [OF FDERIV_ident]) - apply (simp only: of_nat_Suc left_distrib mult_1_left) - apply (simp only: power_Suc right_distrib add_ac mult_ac) -done - -lemma FDERIV_power: - fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}" - shows "FDERIV (\x. x ^ n) x :> (\h. of_nat n * x ^ (n - 1) * h)" - apply (cases n) - apply (simp add: FDERIV_const) - apply (simp add: FDERIV_power_Suc) - done - - -subsection {* Inverse *} - -lemma inverse_diff_inverse: - "\(a::'a::division_ring) \ 0; b \ 0\ - \ inverse a - inverse b = - (inverse a * (a - b) * inverse b)" -by (simp add: right_diff_distrib left_diff_distrib mult_assoc) - -lemmas bounded_linear_mult_const = - mult.bounded_linear_left [THEN bounded_linear_compose] - -lemmas bounded_linear_const_mult = - mult.bounded_linear_right [THEN bounded_linear_compose] - -lemma FDERIV_inverse: - fixes x :: "'a::real_normed_div_algebra" - assumes x: "x \ 0" - shows "FDERIV inverse x :> (\h. - (inverse x * h * inverse x))" - (is "FDERIV ?inv _ :> _") -proof (rule FDERIV_I) - show "bounded_linear (\h. - (?inv x * h * ?inv x))" - apply (rule bounded_linear_minus) - apply (rule bounded_linear_mult_const) - apply (rule bounded_linear_const_mult) - apply (rule bounded_linear_ident) - done -next - show "(\h. norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h) - -- 0 --> 0" - proof (rule LIM_equal2) - show "0 < norm x" using x by simp - next - fix h::'a - assume 1: "h \ 0" - assume "norm (h - 0) < norm x" - hence "h \ -x" by clarsimp - hence 2: "x + h \ 0" - apply (rule contrapos_nn) - apply (rule sym) - apply (erule equals_zero_I) - done - show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h - = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h" - apply (subst inverse_diff_inverse [OF 2 x]) - apply (subst minus_diff_minus) - apply (subst norm_minus_cancel) - apply (simp add: left_diff_distrib) - done - next - show "(\h. norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h) - -- 0 --> 0" - proof (rule real_LIM_sandwich_zero) - show "(\h. norm (?inv (x + h) - ?inv x) * norm (?inv x)) - -- 0 --> 0" - apply (rule LIM_mult_left_zero) - apply (rule LIM_norm_zero) - apply (rule LIM_zero) - apply (rule LIM_offset_zero) - apply (rule LIM_inverse) - apply (rule LIM_ident) - apply (rule x) - done - next - fix h::'a assume h: "h \ 0" - show "0 \ norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h" - apply (rule divide_nonneg_pos) - apply (rule norm_ge_zero) - apply (simp add: h) - done - next - fix h::'a assume h: "h \ 0" - have "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h - \ norm (?inv (x + h) - ?inv x) * norm h * norm (?inv x) / norm h" - apply (rule divide_right_mono [OF _ norm_ge_zero]) - apply (rule order_trans [OF norm_mult_ineq]) - apply (rule mult_right_mono [OF _ norm_ge_zero]) - apply (rule norm_mult_ineq) - done - also have "\ = norm (?inv (x + h) - ?inv x) * norm (?inv x)" - by simp - finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h - \ norm (?inv (x + h) - ?inv x) * norm (?inv x)" . - qed - qed -qed - -subsection {* Alternate definition *} - -lemma field_fderiv_def: - fixes x :: "'a::real_normed_field" shows - "FDERIV f x :> (\h. h * D) = (\h. (f (x + h) - f x) / h) -- 0 --> D" - apply (unfold fderiv_def) - apply (simp add: mult.bounded_linear_left) - apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric]) - apply (subst diff_divide_distrib) - apply (subst times_divide_eq_left [symmetric]) - apply (simp cong: LIM_cong) - apply (simp add: LIM_norm_zero_iff LIM_zero_iff) -done - -end diff -r 57975b45ab70 -r 6b1ccda8bf19 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Feb 18 19:32:26 2009 -0800 +++ b/src/HOL/IsaMakefile Wed Feb 18 19:51:39 2009 -0800 @@ -271,7 +271,6 @@ Complex.thy \ Deriv.thy \ Fact.thy \ - FrechetDeriv.thy \ Integration.thy \ Lim.thy \ Ln.thy \ @@ -315,6 +314,7 @@ Library/Executable_Set.thy Library/Infinite_Set.thy \ Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\ Library/Finite_Cartesian_Product.thy \ + Library/FrechetDeriv.thy \ Library/Fundamental_Theorem_Algebra.thy \ Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy \ Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy \ diff -r 57975b45ab70 -r 6b1ccda8bf19 src/HOL/Library/FrechetDeriv.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/FrechetDeriv.thy Wed Feb 18 19:51:39 2009 -0800 @@ -0,0 +1,503 @@ +(* Title : FrechetDeriv.thy + ID : $Id$ + Author : Brian Huffman +*) + +header {* Frechet Derivative *} + +theory FrechetDeriv +imports Lim +begin + +definition + fderiv :: + "['a::real_normed_vector \ 'b::real_normed_vector, 'a, 'a \ 'b] \ bool" + -- {* Frechet derivative: D is derivative of function f at x *} + ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where + "FDERIV f x :> D = (bounded_linear D \ + (\h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)" + +lemma FDERIV_I: + "\bounded_linear D; (\h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0\ + \ FDERIV f x :> D" +by (simp add: fderiv_def) + +lemma FDERIV_D: + "FDERIV f x :> D \ (\h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0" +by (simp add: fderiv_def) + +lemma FDERIV_bounded_linear: "FDERIV f x :> D \ bounded_linear D" +by (simp add: fderiv_def) + +lemma bounded_linear_zero: + "bounded_linear (\x::'a::real_normed_vector. 0::'b::real_normed_vector)" +proof + show "(0::'b) = 0 + 0" by simp + fix r show "(0::'b) = scaleR r 0" by simp + have "\x::'a. norm (0::'b) \ norm x * 0" by simp + thus "\K. \x::'a. norm (0::'b) \ norm x * K" .. +qed + +lemma FDERIV_const: "FDERIV (\x. k) x :> (\h. 0)" +by (simp add: fderiv_def bounded_linear_zero) + +lemma bounded_linear_ident: + "bounded_linear (\x::'a::real_normed_vector. x)" +proof + fix x y :: 'a show "x + y = x + y" by simp + fix r and x :: 'a show "scaleR r x = scaleR r x" by simp + have "\x::'a. norm x \ norm x * 1" by simp + thus "\K. \x::'a. norm x \ norm x * K" .. +qed + +lemma FDERIV_ident: "FDERIV (\x. x) x :> (\h. h)" +by (simp add: fderiv_def bounded_linear_ident) + +subsection {* Addition *} + +lemma add_diff_add: + fixes a b c d :: "'a::ab_group_add" + shows "(a + c) - (b + d) = (a - b) + (c - d)" +by simp + +lemma bounded_linear_add: + assumes "bounded_linear f" + assumes "bounded_linear g" + shows "bounded_linear (\x. f x + g x)" +proof - + interpret f: bounded_linear f by fact + interpret g: bounded_linear g by fact + show ?thesis apply (unfold_locales) + apply (simp only: f.add g.add add_ac) + apply (simp only: f.scaleR g.scaleR scaleR_right_distrib) + apply (rule f.pos_bounded [THEN exE], rename_tac Kf) + apply (rule g.pos_bounded [THEN exE], rename_tac Kg) + apply (rule_tac x="Kf + Kg" in exI, safe) + apply (subst right_distrib) + apply (rule order_trans [OF norm_triangle_ineq]) + apply (rule add_mono, erule spec, erule spec) + done +qed + +lemma norm_ratio_ineq: + fixes x y :: "'a::real_normed_vector" + fixes h :: "'b::real_normed_vector" + shows "norm (x + y) / norm h \ norm x / norm h + norm y / norm h" +apply (rule ord_le_eq_trans) +apply (rule divide_right_mono) +apply (rule norm_triangle_ineq) +apply (rule norm_ge_zero) +apply (rule add_divide_distrib) +done + +lemma FDERIV_add: + assumes f: "FDERIV f x :> F" + assumes g: "FDERIV g x :> G" + shows "FDERIV (\x. f x + g x) x :> (\h. F h + G h)" +proof (rule FDERIV_I) + show "bounded_linear (\h. F h + G h)" + apply (rule bounded_linear_add) + apply (rule FDERIV_bounded_linear [OF f]) + apply (rule FDERIV_bounded_linear [OF g]) + done +next + have f': "(\h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0" + using f by (rule FDERIV_D) + have g': "(\h. norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0" + using g by (rule FDERIV_D) + from f' g' + have "(\h. norm (f (x + h) - f x - F h) / norm h + + norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0" + by (rule LIM_add_zero) + thus "(\h. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h)) + / norm h) -- 0 --> 0" + apply (rule real_LIM_sandwich_zero) + apply (simp add: divide_nonneg_pos) + apply (simp only: add_diff_add) + apply (rule norm_ratio_ineq) + done +qed + +subsection {* Subtraction *} + +lemma bounded_linear_minus: + assumes "bounded_linear f" + shows "bounded_linear (\x. - f x)" +proof - + interpret f: bounded_linear f by fact + show ?thesis apply (unfold_locales) + apply (simp add: f.add) + apply (simp add: f.scaleR) + apply (simp add: f.bounded) + done +qed + +lemma FDERIV_minus: + "FDERIV f x :> F \ FDERIV (\x. - f x) x :> (\h. - F h)" +apply (rule FDERIV_I) +apply (rule bounded_linear_minus) +apply (erule FDERIV_bounded_linear) +apply (simp only: fderiv_def minus_diff_minus norm_minus_cancel) +done + +lemma FDERIV_diff: + "\FDERIV f x :> F; FDERIV g x :> G\ + \ FDERIV (\x. f x - g x) x :> (\h. F h - G h)" +by (simp only: diff_minus FDERIV_add FDERIV_minus) + +subsection {* Continuity *} + +lemma FDERIV_isCont: + assumes f: "FDERIV f x :> F" + shows "isCont f x" +proof - + from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear) + have "(\h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0" + by (rule FDERIV_D [OF f]) + hence "(\h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0" + by (intro LIM_mult_zero LIM_norm_zero LIM_ident) + hence "(\h. norm (f (x + h) - f x - F h)) -- 0 --> 0" + by (simp cong: LIM_cong) + hence "(\h. f (x + h) - f x - F h) -- 0 --> 0" + by (rule LIM_norm_zero_cancel) + hence "(\h. f (x + h) - f x - F h + F h) -- 0 --> 0" + by (intro LIM_add_zero F.LIM_zero LIM_ident) + hence "(\h. f (x + h) - f x) -- 0 --> 0" + by simp + thus "isCont f x" + unfolding isCont_iff by (rule LIM_zero_cancel) +qed + +subsection {* Composition *} + +lemma real_divide_cancel_lemma: + fixes a b c :: real + shows "(b = 0 \ a = 0) \ (a / b) * (b / c) = a / c" +by simp + +lemma bounded_linear_compose: + assumes "bounded_linear f" + assumes "bounded_linear g" + shows "bounded_linear (\x. f (g x))" +proof - + interpret f: bounded_linear f by fact + interpret g: bounded_linear g by fact + show ?thesis proof (unfold_locales) + fix x y show "f (g (x + y)) = f (g x) + f (g y)" + by (simp only: f.add g.add) + next + fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))" + by (simp only: f.scaleR g.scaleR) + next + from f.pos_bounded + obtain Kf where f: "\x. norm (f x) \ norm x * Kf" and Kf: "0 < Kf" by fast + from g.pos_bounded + obtain Kg where g: "\x. norm (g x) \ norm x * Kg" by fast + show "\K. \x. norm (f (g x)) \ norm x * K" + proof (intro exI allI) + fix x + have "norm (f (g x)) \ norm (g x) * Kf" + using f . + also have "\ \ (norm x * Kg) * Kf" + using g Kf [THEN order_less_imp_le] by (rule mult_right_mono) + also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)" + by (rule mult_assoc) + finally show "norm (f (g x)) \ norm x * (Kg * Kf)" . + qed + qed +qed + +lemma FDERIV_compose: + fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" + fixes g :: "'b::real_normed_vector \ 'c::real_normed_vector" + assumes f: "FDERIV f x :> F" + assumes g: "FDERIV g (f x) :> G" + shows "FDERIV (\x. g (f x)) x :> (\h. G (F h))" +proof (rule FDERIV_I) + from FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f] + show "bounded_linear (\h. G (F h))" + by (rule bounded_linear_compose) +next + let ?Rf = "\h. f (x + h) - f x - F h" + let ?Rg = "\k. g (f x + k) - g (f x) - G k" + let ?k = "\h. f (x + h) - f x" + let ?Nf = "\h. norm (?Rf h) / norm h" + let ?Ng = "\h. norm (?Rg (?k h)) / norm (?k h)" + from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear) + from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear) + from F.bounded obtain kF where kF: "\x. norm (F x) \ norm x * kF" by fast + from G.bounded obtain kG where kG: "\x. norm (G x) \ norm x * kG" by fast + + let ?fun2 = "\h. ?Nf h * kG + ?Ng h * (?Nf h + kF)" + + show "(\h. norm (g (f (x + h)) - g (f x) - G (F h)) / norm h) -- 0 --> 0" + proof (rule real_LIM_sandwich_zero) + have Nf: "?Nf -- 0 --> 0" + using FDERIV_D [OF f] . + + have Ng1: "isCont (\k. norm (?Rg k) / norm k) 0" + by (simp add: isCont_def FDERIV_D [OF g]) + have Ng2: "?k -- 0 --> 0" + apply (rule LIM_zero) + apply (fold isCont_iff) + apply (rule FDERIV_isCont [OF f]) + done + have Ng: "?Ng -- 0 --> 0" + using isCont_LIM_compose [OF Ng1 Ng2] by simp + + have "(\h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) + -- 0 --> 0 * kG + 0 * (0 + kF)" + by (intro LIM_add LIM_mult LIM_const Nf Ng) + thus "(\h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0" + by simp + next + fix h::'a assume h: "h \ 0" + thus "0 \ norm (g (f (x + h)) - g (f x) - G (F h)) / norm h" + by (simp add: divide_nonneg_pos) + next + fix h::'a assume h: "h \ 0" + have "g (f (x + h)) - g (f x) - G (F h) = G (?Rf h) + ?Rg (?k h)" + by (simp add: G.diff) + hence "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h + = norm (G (?Rf h) + ?Rg (?k h)) / norm h" + by (rule arg_cong) + also have "\ \ norm (G (?Rf h)) / norm h + norm (?Rg (?k h)) / norm h" + by (rule norm_ratio_ineq) + also have "\ \ ?Nf h * kG + ?Ng h * (?Nf h + kF)" + proof (rule add_mono) + show "norm (G (?Rf h)) / norm h \ ?Nf h * kG" + apply (rule ord_le_eq_trans) + apply (rule divide_right_mono [OF kG norm_ge_zero]) + apply simp + done + next + have "norm (?Rg (?k h)) / norm h = ?Ng h * (norm (?k h) / norm h)" + apply (rule real_divide_cancel_lemma [symmetric]) + apply (simp add: G.zero) + done + also have "\ \ ?Ng h * (?Nf h + kF)" + proof (rule mult_left_mono) + have "norm (?k h) / norm h = norm (?Rf h + F h) / norm h" + by simp + also have "\ \ ?Nf h + norm (F h) / norm h" + by (rule norm_ratio_ineq) + also have "\ \ ?Nf h + kF" + apply (rule add_left_mono) + apply (subst pos_divide_le_eq, simp add: h) + apply (subst mult_commute) + apply (rule kF) + done + finally show "norm (?k h) / norm h \ ?Nf h + kF" . + next + show "0 \ ?Ng h" + apply (case_tac "f (x + h) - f x = 0", simp) + apply (rule divide_nonneg_pos [OF norm_ge_zero]) + apply simp + done + qed + finally show "norm (?Rg (?k h)) / norm h \ ?Ng h * (?Nf h + kF)" . + qed + finally show "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h + \ ?Nf h * kG + ?Ng h * (?Nf h + kF)" . + qed +qed + +subsection {* Product Rule *} + +lemma (in bounded_bilinear) FDERIV_lemma: + "a' ** b' - a ** b - (a ** B + A ** b) + = a ** (b' - b - B) + (a' - a - A) ** b' + A ** (b' - b)" +by (simp add: diff_left diff_right) + +lemma (in bounded_bilinear) FDERIV: + fixes x :: "'d::real_normed_vector" + assumes f: "FDERIV f x :> F" + assumes g: "FDERIV g x :> G" + shows "FDERIV (\x. f x ** g x) x :> (\h. f x ** G h + F h ** g x)" +proof (rule FDERIV_I) + show "bounded_linear (\h. f x ** G h + F h ** g x)" + apply (rule bounded_linear_add) + apply (rule bounded_linear_compose [OF bounded_linear_right]) + apply (rule FDERIV_bounded_linear [OF g]) + apply (rule bounded_linear_compose [OF bounded_linear_left]) + apply (rule FDERIV_bounded_linear [OF f]) + done +next + from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]] + obtain KF where norm_F: "\x. norm (F x) \ norm x * KF" by fast + + from pos_bounded obtain K where K: "0 < K" and norm_prod: + "\a b. norm (a ** b) \ norm a * norm b * K" by fast + + let ?Rf = "\h. f (x + h) - f x - F h" + let ?Rg = "\h. g (x + h) - g x - G h" + + let ?fun1 = "\h. + norm (f x ** ?Rg h + ?Rf h ** g (x + h) + F h ** (g (x + h) - g x)) / + norm h" + + let ?fun2 = "\h. + norm (f x) * (norm (?Rg h) / norm h) * K + + norm (?Rf h) / norm h * norm (g (x + h)) * K + + KF * norm (g (x + h) - g x) * K" + + have "?fun1 -- 0 --> 0" + proof (rule real_LIM_sandwich_zero) + from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]] + have "?fun2 -- 0 --> + norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K" + by (intro LIM_add LIM_mult LIM_const LIM_norm LIM_zero FDERIV_D) + thus "?fun2 -- 0 --> 0" + by simp + next + fix h::'d assume "h \ 0" + thus "0 \ ?fun1 h" + by (simp add: divide_nonneg_pos) + next + fix h::'d assume "h \ 0" + have "?fun1 h \ (norm (f x) * norm (?Rg h) * K + + norm (?Rf h) * norm (g (x + h)) * K + + norm h * KF * norm (g (x + h) - g x) * K) / norm h" + by (intro + divide_right_mono mult_mono' + order_trans [OF norm_triangle_ineq add_mono] + order_trans [OF norm_prod mult_right_mono] + mult_nonneg_nonneg order_refl norm_ge_zero norm_F + K [THEN order_less_imp_le] + ) + also have "\ = ?fun2 h" + by (simp add: add_divide_distrib) + finally show "?fun1 h \ ?fun2 h" . + qed + thus "(\h. + norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x)) + / norm h) -- 0 --> 0" + by (simp only: FDERIV_lemma) +qed + +lemmas FDERIV_mult = mult.FDERIV + +lemmas FDERIV_scaleR = scaleR.FDERIV + + +subsection {* Powers *} + +lemma FDERIV_power_Suc: + fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}" + shows "FDERIV (\x. x ^ Suc n) x :> (\h. (1 + of_nat n) * x ^ n * h)" + apply (induct n) + apply (simp add: power_Suc FDERIV_ident) + apply (drule FDERIV_mult [OF FDERIV_ident]) + apply (simp only: of_nat_Suc left_distrib mult_1_left) + apply (simp only: power_Suc right_distrib add_ac mult_ac) +done + +lemma FDERIV_power: + fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}" + shows "FDERIV (\x. x ^ n) x :> (\h. of_nat n * x ^ (n - 1) * h)" + apply (cases n) + apply (simp add: FDERIV_const) + apply (simp add: FDERIV_power_Suc) + done + + +subsection {* Inverse *} + +lemma inverse_diff_inverse: + "\(a::'a::division_ring) \ 0; b \ 0\ + \ inverse a - inverse b = - (inverse a * (a - b) * inverse b)" +by (simp add: right_diff_distrib left_diff_distrib mult_assoc) + +lemmas bounded_linear_mult_const = + mult.bounded_linear_left [THEN bounded_linear_compose] + +lemmas bounded_linear_const_mult = + mult.bounded_linear_right [THEN bounded_linear_compose] + +lemma FDERIV_inverse: + fixes x :: "'a::real_normed_div_algebra" + assumes x: "x \ 0" + shows "FDERIV inverse x :> (\h. - (inverse x * h * inverse x))" + (is "FDERIV ?inv _ :> _") +proof (rule FDERIV_I) + show "bounded_linear (\h. - (?inv x * h * ?inv x))" + apply (rule bounded_linear_minus) + apply (rule bounded_linear_mult_const) + apply (rule bounded_linear_const_mult) + apply (rule bounded_linear_ident) + done +next + show "(\h. norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h) + -- 0 --> 0" + proof (rule LIM_equal2) + show "0 < norm x" using x by simp + next + fix h::'a + assume 1: "h \ 0" + assume "norm (h - 0) < norm x" + hence "h \ -x" by clarsimp + hence 2: "x + h \ 0" + apply (rule contrapos_nn) + apply (rule sym) + apply (erule equals_zero_I) + done + show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h + = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h" + apply (subst inverse_diff_inverse [OF 2 x]) + apply (subst minus_diff_minus) + apply (subst norm_minus_cancel) + apply (simp add: left_diff_distrib) + done + next + show "(\h. norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h) + -- 0 --> 0" + proof (rule real_LIM_sandwich_zero) + show "(\h. norm (?inv (x + h) - ?inv x) * norm (?inv x)) + -- 0 --> 0" + apply (rule LIM_mult_left_zero) + apply (rule LIM_norm_zero) + apply (rule LIM_zero) + apply (rule LIM_offset_zero) + apply (rule LIM_inverse) + apply (rule LIM_ident) + apply (rule x) + done + next + fix h::'a assume h: "h \ 0" + show "0 \ norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h" + apply (rule divide_nonneg_pos) + apply (rule norm_ge_zero) + apply (simp add: h) + done + next + fix h::'a assume h: "h \ 0" + have "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h + \ norm (?inv (x + h) - ?inv x) * norm h * norm (?inv x) / norm h" + apply (rule divide_right_mono [OF _ norm_ge_zero]) + apply (rule order_trans [OF norm_mult_ineq]) + apply (rule mult_right_mono [OF _ norm_ge_zero]) + apply (rule norm_mult_ineq) + done + also have "\ = norm (?inv (x + h) - ?inv x) * norm (?inv x)" + by simp + finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h + \ norm (?inv (x + h) - ?inv x) * norm (?inv x)" . + qed + qed +qed + +subsection {* Alternate definition *} + +lemma field_fderiv_def: + fixes x :: "'a::real_normed_field" shows + "FDERIV f x :> (\h. h * D) = (\h. (f (x + h) - f x) / h) -- 0 --> D" + apply (unfold fderiv_def) + apply (simp add: mult.bounded_linear_left) + apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric]) + apply (subst diff_divide_distrib) + apply (subst times_divide_eq_left [symmetric]) + apply (simp cong: LIM_cong) + apply (simp add: LIM_norm_zero_iff LIM_zero_iff) +done + +end diff -r 57975b45ab70 -r 6b1ccda8bf19 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Feb 18 19:32:26 2009 -0800 +++ b/src/HOL/Library/Library.thy Wed Feb 18 19:51:39 2009 -0800 @@ -22,6 +22,7 @@ Executable_Set Float Formal_Power_Series + FrechetDeriv FuncSet Fundamental_Theorem_Algebra Infinite_Set