author | huffman |
Thu, 13 Mar 2014 16:07:27 -0700 | |
changeset 56117 | 2dbf84ee3deb |
parent 55970 | 6d123f0ae358 |
child 56133 | 304e37faf1ac |
permissions | -rw-r--r-- |
53781 | 1 |
(* Title: HOL/Multivariate_Analysis/Derivative.thy |
2 |
Author: John Harrison |
|
3 |
Author: Robert Himmelmann, TU Muenchen (translation from HOL Light) |
|
36350 | 4 |
*) |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
5 |
|
53781 | 6 |
header {* Multivariate calculus in Euclidean space *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
7 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
8 |
theory Derivative |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
9 |
imports Brouwer_Fixpoint Operator_Norm |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
10 |
begin |
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
11 |
|
53781 | 12 |
lemma bounded_linear_imp_linear: (* TODO: move elsewhere *) |
13 |
assumes "bounded_linear f" |
|
14 |
shows "linear f" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
15 |
proof - |
53781 | 16 |
interpret f: bounded_linear f |
17 |
using assms . |
|
18 |
show ?thesis |
|
53600
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53374
diff
changeset
|
19 |
by (simp add: f.add f.scaleR linear_iff) |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
20 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
21 |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
22 |
lemma netlimit_at_vector: (* TODO: move *) |
37730 | 23 |
fixes a :: "'a::real_normed_vector" |
24 |
shows "netlimit (at a) = a" |
|
25 |
proof (cases "\<exists>x. x \<noteq> a") |
|
26 |
case True then obtain x where x: "x \<noteq> a" .. |
|
27 |
have "\<not> trivial_limit (at a)" |
|
28 |
unfolding trivial_limit_def eventually_at dist_norm |
|
29 |
apply clarsimp |
|
30 |
apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI) |
|
31 |
apply (simp add: norm_sgn sgn_zero_iff x) |
|
32 |
done |
|
53781 | 33 |
then show ?thesis |
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51478
diff
changeset
|
34 |
by (rule netlimit_within [of a UNIV]) |
37730 | 35 |
qed simp |
36 |
||
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
37 |
(* Because I do not want to type this all the time *) |
53781 | 38 |
lemmas linear_linear = linear_conv_bounded_linear[symmetric] |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
39 |
|
53781 | 40 |
lemma derivative_linear[dest]: "(f has_derivative f') net \<Longrightarrow> bounded_linear f'" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
41 |
unfolding has_derivative_def by auto |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
42 |
|
53781 | 43 |
lemma derivative_is_linear: "(f has_derivative f') net \<Longrightarrow> linear f'" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
44 |
by (rule derivative_linear [THEN bounded_linear_imp_linear]) |
44137 | 45 |
|
53781 | 46 |
lemma DERIV_conv_has_derivative: "(DERIV f x :> f') \<longleftrightarrow> (f has_derivative op * f') (at x)" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
47 |
using deriv_fderiv[of f x UNIV f'] by (subst (asm) mult_commute) |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
48 |
|
53781 | 49 |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
50 |
subsection {* Derivatives *} |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
51 |
|
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
52 |
subsubsection {* Combining theorems. *} |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
53 |
|
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
54 |
lemmas has_derivative_id = FDERIV_ident |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
55 |
lemmas has_derivative_const = FDERIV_const |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
56 |
lemmas has_derivative_neg = FDERIV_minus |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
57 |
lemmas has_derivative_add = FDERIV_add |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
58 |
lemmas has_derivative_sub = FDERIV_diff |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
59 |
lemmas has_derivative_setsum = FDERIV_setsum |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
60 |
lemmas scaleR_right_has_derivative = FDERIV_scaleR_right |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
61 |
lemmas scaleR_left_has_derivative = FDERIV_scaleR_left |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
62 |
lemmas inner_right_has_derivative = FDERIV_inner_right |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
63 |
lemmas inner_left_has_derivative = FDERIV_inner_left |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
64 |
lemmas mult_right_has_derivative = FDERIV_mult_right |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
65 |
lemmas mult_left_has_derivative = FDERIV_mult_left |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
66 |
|
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
67 |
lemma has_derivative_add_const: |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
68 |
"(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
69 |
by (intro FDERIV_eq_intros) auto |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
70 |
|
53781 | 71 |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
72 |
subsection {* Derivative with composed bilinear function. *} |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
73 |
|
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
74 |
lemma has_derivative_bilinear_within: |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
75 |
assumes "(f has_derivative f') (at x within s)" |
53781 | 76 |
and "(g has_derivative g') (at x within s)" |
77 |
and "bounded_bilinear h" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
78 |
shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
79 |
using bounded_bilinear.FDERIV[OF assms(3,1,2)] . |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
80 |
|
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
81 |
lemma has_derivative_bilinear_at: |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
82 |
assumes "(f has_derivative f') (at x)" |
53781 | 83 |
and "(g has_derivative g') (at x)" |
84 |
and "bounded_bilinear h" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
85 |
shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
86 |
using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
87 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
88 |
text {* These are the only cases we'll care about, probably. *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
89 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
90 |
lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow> |
53781 | 91 |
bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)" |
92 |
unfolding has_derivative_def Lim |
|
93 |
by (auto simp add: netlimit_within inverse_eq_divide field_simps) |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
94 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
95 |
lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow> |
53781 | 96 |
bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)" |
97 |
using has_derivative_within [of f f' x UNIV] |
|
98 |
by simp |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
99 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
100 |
text {* More explicit epsilon-delta forms. *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
101 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
102 |
lemma has_derivative_within': |
53781 | 103 |
"(f has_derivative f')(at x within s) \<longleftrightarrow> |
104 |
bounded_linear f' \<and> |
|
105 |
(\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow> |
|
106 |
norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)" |
|
36587 | 107 |
unfolding has_derivative_within Lim_within dist_norm |
53781 | 108 |
unfolding diff_0_right |
109 |
by (simp add: diff_diff_eq) |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
110 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
111 |
lemma has_derivative_at': |
53781 | 112 |
"(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and> |
113 |
(\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow> |
|
114 |
norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)" |
|
115 |
using has_derivative_within' [of f f' x UNIV] |
|
116 |
by simp |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
117 |
|
53781 | 118 |
lemma has_derivative_at_within: |
119 |
"(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)" |
|
120 |
unfolding has_derivative_within' has_derivative_at' |
|
121 |
by blast |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
122 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
123 |
lemma has_derivative_within_open: |
53781 | 124 |
"a \<in> s \<Longrightarrow> open s \<Longrightarrow> |
125 |
(f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a)" |
|
37730 | 126 |
by (simp only: at_within_interior interior_open) |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
127 |
|
43338 | 128 |
lemma has_derivative_right: |
53781 | 129 |
fixes f :: "real \<Rightarrow> real" |
130 |
and y :: "real" |
|
43338 | 131 |
shows "(f has_derivative (op * y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow> |
132 |
((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x <..} \<inter> I))" |
|
133 |
proof - |
|
134 |
have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) ---> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow> |
|
135 |
((\<lambda>t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \<inter> I))" |
|
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset
|
136 |
by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib) |
43338 | 137 |
also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))" |
138 |
by (simp add: Lim_null[symmetric]) |
|
139 |
also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))" |
|
44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset
|
140 |
by (intro Lim_cong_within) (simp_all add: field_simps) |
43338 | 141 |
finally show ?thesis |
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset
|
142 |
by (simp add: bounded_linear_mult_right has_derivative_within) |
43338 | 143 |
qed |
144 |
||
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
145 |
subsubsection {*Caratheodory characterization*} |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
146 |
|
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
147 |
lemma DERIV_within_iff: |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
148 |
"(DERIV f a : s :> D) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) ---> D) (at a within s)" |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
149 |
proof - |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
150 |
have 1: "\<And>w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)" |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
151 |
by (metis divide_diff_eq_iff eq_iff_diff_eq_0) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
152 |
show ?thesis |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
153 |
apply (simp add: deriv_fderiv has_derivative_within bounded_linear_mult_left) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
154 |
apply (simp add: LIM_zero_iff [where l = D, symmetric]) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
155 |
apply (simp add: Lim_within dist_norm) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
156 |
apply (simp add: nonzero_norm_divide [symmetric]) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
157 |
apply (simp add: 1 diff_add_eq_diff_diff) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
158 |
done |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
159 |
qed |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
160 |
|
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
161 |
lemma DERIV_caratheodory_within: |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
162 |
"(DERIV f x : s :> l) \<longleftrightarrow> |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
163 |
(\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)" |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
164 |
(is "?lhs = ?rhs") |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
165 |
proof |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
166 |
assume der: "DERIV f x : s :> l" |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
167 |
show ?rhs |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
168 |
proof (intro exI conjI) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
169 |
let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))" |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
170 |
show "\<forall>z. f z - f x = ?g z * (z-x)" by simp |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
171 |
show "continuous (at x within s) ?g" using der |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
172 |
by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
173 |
show "?g x = l" by simp |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
174 |
qed |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
175 |
next |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
176 |
assume ?rhs |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
177 |
then obtain g where |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
178 |
"(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within s) g" and "g x = l" by blast |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
179 |
thus "(DERIV f x : s :> l)" |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
180 |
by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
181 |
qed |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
182 |
|
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
183 |
lemma CARAT_DERIV: (*FIXME: REPLACES THE ONE IN Deriv.thy*) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
184 |
"(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)" |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
185 |
by (rule DERIV_caratheodory_within) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
186 |
|
53781 | 187 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
188 |
subsubsection {* Limit transformation for derivatives *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
189 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
190 |
lemma has_derivative_transform_within: |
53781 | 191 |
assumes "0 < d" |
192 |
and "x \<in> s" |
|
193 |
and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'" |
|
194 |
and "(f has_derivative f') (at x within s)" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
195 |
shows "(g has_derivative f') (at x within s)" |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
196 |
using assms |
53781 | 197 |
unfolding has_derivative_within |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
198 |
apply clarify |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
199 |
apply (rule Lim_transform_within, auto) |
53781 | 200 |
done |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
201 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
202 |
lemma has_derivative_transform_at: |
53781 | 203 |
assumes "0 < d" |
204 |
and "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'" |
|
205 |
and "(f has_derivative f') (at x)" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
206 |
shows "(g has_derivative f') (at x)" |
53781 | 207 |
using has_derivative_transform_within [of d x UNIV f g f'] assms |
208 |
by simp |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
209 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
210 |
lemma has_derivative_transform_within_open: |
53781 | 211 |
assumes "open s" |
212 |
and "x \<in> s" |
|
213 |
and "\<forall>y\<in>s. f y = g y" |
|
214 |
and "(f has_derivative f') (at x)" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
215 |
shows "(g has_derivative f') (at x)" |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
216 |
using assms |
53781 | 217 |
unfolding has_derivative_at |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
218 |
apply clarify |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
219 |
apply (rule Lim_transform_within_open[OF assms(1,2)], auto) |
53781 | 220 |
done |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
221 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
222 |
subsection {* Differentiability *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
223 |
|
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36334
diff
changeset
|
224 |
no_notation Deriv.differentiable (infixl "differentiable" 60) |
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36334
diff
changeset
|
225 |
|
53781 | 226 |
abbreviation |
227 |
differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" |
|
228 |
(infixr "differentiable" 30) |
|
229 |
where "f differentiable net \<equiv> isDiff net f" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
230 |
|
53781 | 231 |
definition |
232 |
differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" |
|
233 |
(infixr "differentiable'_on" 30) |
|
234 |
where "f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable (at x within s))" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
235 |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
236 |
lemmas differentiable_def = isDiff_def |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
237 |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
238 |
lemma differentiableI: "(f has_derivative f') net \<Longrightarrow> f differentiable net" |
53781 | 239 |
unfolding differentiable_def |
240 |
by auto |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
241 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
242 |
lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)" |
53781 | 243 |
unfolding differentiable_def |
244 |
using has_derivative_at_within |
|
245 |
by blast |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
246 |
|
44123 | 247 |
lemma differentiable_within_open: (* TODO: delete *) |
53781 | 248 |
assumes "a \<in> s" |
249 |
and "open s" |
|
250 |
shows "f differentiable (at a within s) \<longleftrightarrow> f differentiable (at a)" |
|
251 |
using assms |
|
252 |
by (simp only: at_within_interior interior_open) |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
253 |
|
44123 | 254 |
lemma differentiable_on_eq_differentiable_at: |
53781 | 255 |
"open s \<Longrightarrow> f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x)" |
44123 | 256 |
unfolding differentiable_on_def |
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51478
diff
changeset
|
257 |
by (metis at_within_interior interior_open) |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
258 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
259 |
lemma differentiable_transform_within: |
53781 | 260 |
assumes "0 < d" |
261 |
and "x \<in> s" |
|
262 |
and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'" |
|
44123 | 263 |
assumes "f differentiable (at x within s)" |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
264 |
shows "g differentiable (at x within s)" |
53781 | 265 |
using assms(4) |
266 |
unfolding differentiable_def |
|
44123 | 267 |
by (auto intro!: has_derivative_transform_within[OF assms(1-3)]) |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
268 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
269 |
lemma differentiable_transform_at: |
53781 | 270 |
assumes "0 < d" |
271 |
and "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'" |
|
272 |
and "f differentiable at x" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
273 |
shows "g differentiable at x" |
53781 | 274 |
using assms(3) |
275 |
unfolding differentiable_def |
|
276 |
using has_derivative_transform_at[OF assms(1-2)] |
|
277 |
by auto |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
278 |
|
53781 | 279 |
|
280 |
subsection {* Frechet derivative and Jacobian matrix *} |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
281 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
282 |
definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)" |
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
283 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
284 |
lemma frechet_derivative_works: |
53781 | 285 |
"f differentiable net \<longleftrightarrow> (f has_derivative (frechet_derivative f net)) net" |
286 |
unfolding frechet_derivative_def differentiable_def |
|
287 |
unfolding some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] .. |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
288 |
|
53781 | 289 |
lemma linear_frechet_derivative: "f differentiable net \<Longrightarrow> linear(frechet_derivative f net)" |
44123 | 290 |
unfolding frechet_derivative_works has_derivative_def |
291 |
by (auto intro: bounded_linear_imp_linear) |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
292 |
|
53781 | 293 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
294 |
subsection {* Differentiability implies continuity *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
295 |
|
44123 | 296 |
lemma Lim_mul_norm_within: |
53781 | 297 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
298 |
shows "(f ---> 0) (at a within s) \<Longrightarrow> ((\<lambda>x. norm(x - a) *\<^sub>R f x) ---> 0) (at a within s)" |
|
299 |
unfolding Lim_within |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
300 |
apply (auto simp: ) |
53781 | 301 |
apply (erule_tac x=e in allE) |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
302 |
apply (auto simp: ) |
53781 | 303 |
apply (rule_tac x="min d 1" in exI) |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
304 |
apply (auto simp: ) |
53781 | 305 |
apply (erule_tac x=x in ballE) |
306 |
unfolding dist_norm diff_0_right |
|
307 |
apply (auto intro!: mult_strict_mono[of _ "1::real", unfolded mult_1_left]) |
|
308 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
309 |
|
44123 | 310 |
lemma differentiable_imp_continuous_within: |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
311 |
"f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
312 |
by (auto simp: differentiable_def intro: FDERIV_continuous) |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
313 |
|
44123 | 314 |
lemma differentiable_imp_continuous_on: |
315 |
"f differentiable_on s \<Longrightarrow> continuous_on s f" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
316 |
unfolding differentiable_on_def continuous_on_eq_continuous_within |
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
317 |
using differentiable_imp_continuous_within by blast |
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
318 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
319 |
lemma has_derivative_within_subset: |
53781 | 320 |
"(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> |
321 |
(f has_derivative f') (at x within t)" |
|
322 |
unfolding has_derivative_within |
|
323 |
using tendsto_within_subset |
|
324 |
by blast |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
325 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
326 |
lemma differentiable_within_subset: |
53781 | 327 |
"f differentiable (at x within t) \<Longrightarrow> s \<subseteq> t \<Longrightarrow> |
328 |
f differentiable (at x within s)" |
|
329 |
unfolding differentiable_def |
|
330 |
using has_derivative_within_subset |
|
331 |
by blast |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
332 |
|
44123 | 333 |
lemma differentiable_on_subset: |
334 |
"f differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable_on s" |
|
53781 | 335 |
unfolding differentiable_on_def |
336 |
using differentiable_within_subset |
|
337 |
by blast |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
338 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
339 |
lemma differentiable_on_empty: "f differentiable_on {}" |
53781 | 340 |
unfolding differentiable_on_def |
341 |
by auto |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
342 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
343 |
text {* Several results are easier using a "multiplied-out" variant. |
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
344 |
(I got this idea from Dieudonne's proof of the chain rule). *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
345 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
346 |
lemma has_derivative_within_alt: |
53781 | 347 |
"(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and> |
348 |
(\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm(y - x) < d \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> e * norm (y - x))" |
|
349 |
(is "?lhs \<longleftrightarrow> ?rhs") |
|
44123 | 350 |
proof |
53781 | 351 |
assume ?lhs |
352 |
then show ?rhs |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
353 |
unfolding has_derivative_within Lim_within |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
354 |
apply clarify |
53781 | 355 |
apply (erule_tac x=e in allE) |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
356 |
apply safe |
53781 | 357 |
apply (rule_tac x=d in exI) |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
358 |
apply clarify |
44123 | 359 |
proof- |
53781 | 360 |
fix x y e d |
361 |
assume as: |
|
362 |
"0 < e" |
|
363 |
"0 < d" |
|
364 |
"norm (y - x) < d" |
|
365 |
"\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> |
|
366 |
dist ((1 / norm (xa - x)) *\<^sub>R (f xa - (f x + f' (xa - x)))) 0 < e" |
|
367 |
"y \<in> s" |
|
368 |
"bounded_linear f'" |
|
369 |
then interpret bounded_linear f' |
|
370 |
by auto |
|
371 |
show "norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)" |
|
372 |
proof (cases "y = x") |
|
373 |
case True |
|
374 |
then show ?thesis |
|
375 |
using `bounded_linear f'` by (auto simp add: zero) |
|
44123 | 376 |
next |
53781 | 377 |
case False |
378 |
then have "norm (f y - (f x + f' (y - x))) < e * norm (y - x)" |
|
379 |
using as(4)[rule_format, OF `y \<in> s`] |
|
380 |
unfolding dist_norm diff_0_right |
|
381 |
using as(3) |
|
41958 | 382 |
using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded dist_norm] |
383 |
by (auto simp add: linear_0 linear_sub) |
|
53781 | 384 |
then show ?thesis |
385 |
by (auto simp add: algebra_simps) |
|
44123 | 386 |
qed |
387 |
qed |
|
388 |
next |
|
53781 | 389 |
assume ?rhs |
390 |
then show ?lhs |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
391 |
apply (auto simp: has_derivative_within Lim_within) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
392 |
apply (erule_tac x="e/2" in allE, auto) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
393 |
apply (rule_tac x=d in exI, auto) |
44123 | 394 |
unfolding dist_norm diff_0_right norm_scaleR |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
395 |
apply (erule_tac x=xa in ballE, auto) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
396 |
apply (rule_tac y="e/2" in le_less_trans) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
397 |
apply (auto intro!: mult_imp_div_pos_le simp add: algebra_simps) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
398 |
done |
44123 | 399 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
400 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
401 |
lemma has_derivative_at_alt: |
53781 | 402 |
"(f has_derivative f') (at x) \<longleftrightarrow> |
403 |
bounded_linear f' \<and> |
|
404 |
(\<forall>e>0. \<exists>d>0. \<forall>y. norm(y - x) < d \<longrightarrow> norm (f y - f x - f'(y - x)) \<le> e * norm (y - x))" |
|
405 |
using has_derivative_within_alt[where s=UNIV] |
|
406 |
by simp |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
407 |
|
53781 | 408 |
|
409 |
subsection {* The chain rule *} |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
410 |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
411 |
lemma diff_chain_within[FDERIV_intros]: |
44123 | 412 |
assumes "(f has_derivative f') (at x within s)" |
53781 | 413 |
and "(g has_derivative g') (at (f x) within (f ` s))" |
414 |
shows "((g \<circ> f) has_derivative (g' \<circ> f'))(at x within s)" |
|
415 |
using FDERIV_in_compose[OF assms] |
|
416 |
by (simp add: comp_def) |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
417 |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
418 |
lemma diff_chain_at[FDERIV_intros]: |
53781 | 419 |
"(f has_derivative f') (at x) \<Longrightarrow> |
420 |
(g has_derivative g') (at (f x)) \<Longrightarrow> ((g \<circ> f) has_derivative (g' \<circ> f')) (at x)" |
|
421 |
using FDERIV_compose[of f f' x UNIV g g'] |
|
422 |
by (simp add: comp_def) |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
423 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
424 |
|
53781 | 425 |
subsection {* Composition rules stated just for differentiability *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
426 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
427 |
lemma differentiable_chain_at: |
53781 | 428 |
"f differentiable (at x) \<Longrightarrow> |
429 |
g differentiable (at (f x)) \<Longrightarrow> (g \<circ> f) differentiable (at x)" |
|
430 |
unfolding differentiable_def |
|
431 |
by (meson diff_chain_at) |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
432 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
433 |
lemma differentiable_chain_within: |
53781 | 434 |
"f differentiable (at x within s) \<Longrightarrow> |
435 |
g differentiable (at(f x) within (f ` s)) \<Longrightarrow> (g \<circ> f) differentiable (at x within s)" |
|
436 |
unfolding differentiable_def |
|
437 |
by (meson diff_chain_within) |
|
438 |
||
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
439 |
|
37730 | 440 |
subsection {* Uniqueness of derivative *} |
441 |
||
442 |
text {* |
|
443 |
The general result is a bit messy because we need approachability of the |
|
444 |
limit point from any direction. But OK for nontrivial intervals etc. |
|
445 |
*} |
|
51363
d4d00c804645
changed has_derivative_intros into a named theorems collection
hoelzl
parents:
50939
diff
changeset
|
446 |
|
44123 | 447 |
lemma frechet_derivative_unique_within: |
448 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
|
449 |
assumes "(f has_derivative f') (at x within s)" |
|
53781 | 450 |
and "(f has_derivative f'') (at x within s)" |
451 |
and "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < abs d \<and> abs d < e \<and> (x + d *\<^sub>R i) \<in> s" |
|
44123 | 452 |
shows "f' = f''" |
53781 | 453 |
proof - |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
454 |
note as = assms(1,2)[unfolded has_derivative_def] |
44123 | 455 |
then interpret f': bounded_linear f' by auto |
456 |
from as interpret f'': bounded_linear f'' by auto |
|
457 |
have "x islimpt s" unfolding islimpt_approachable |
|
53781 | 458 |
proof (rule, rule) |
459 |
fix e :: real |
|
460 |
assume "e > 0" |
|
55665 | 461 |
obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> s" |
462 |
using assms(3) SOME_Basis `e>0` by blast |
|
53781 | 463 |
then show "\<exists>x'\<in>s. x' \<noteq> x \<and> dist x' x < e" |
464 |
apply (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI) |
|
465 |
unfolding dist_norm |
|
466 |
apply (auto simp: SOME_Basis nonzero_Basis) |
|
467 |
done |
|
44123 | 468 |
qed |
53781 | 469 |
then have *: "netlimit (at x within s) = x" |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
470 |
apply (auto intro!: netlimit_within) |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
471 |
by (metis trivial_limit_within) |
53781 | 472 |
show ?thesis |
473 |
apply (rule linear_eq_stdbasis) |
|
44123 | 474 |
unfolding linear_conv_bounded_linear |
53781 | 475 |
apply (rule as(1,2)[THEN conjunct1])+ |
476 |
proof (rule, rule ccontr) |
|
477 |
fix i :: 'a |
|
478 |
assume i: "i \<in> Basis" |
|
479 |
def e \<equiv> "norm (f' i - f'' i)" |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
480 |
assume "f' i \<noteq> f'' i" |
53781 | 481 |
then have "e > 0" |
482 |
unfolding e_def by auto |
|
55665 | 483 |
obtain d where d: |
484 |
"0 < d" |
|
485 |
"(\<And>xa. xa\<in>s \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> |
|
486 |
dist ((f xa - f x - f' (xa - x)) /\<^sub>R norm (xa - x) - |
|
487 |
(f xa - f x - f'' (xa - x)) /\<^sub>R norm (xa - x)) (0 - 0) < e)" |
|
488 |
using tendsto_diff [OF as(1,2)[THEN conjunct2]] |
|
489 |
unfolding * Lim_within |
|
490 |
using `e>0` by blast |
|
491 |
obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> s" |
|
492 |
using assms(3) i d(1) by blast |
|
53781 | 493 |
have *: "norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) = |
494 |
norm ((1 / abs c) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
495 |
unfolding scaleR_right_distrib by auto |
53781 | 496 |
also have "\<dots> = norm ((1 / abs c) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))" |
44123 | 497 |
unfolding f'.scaleR f''.scaleR |
53781 | 498 |
unfolding scaleR_right_distrib scaleR_minus_right |
499 |
by auto |
|
500 |
also have "\<dots> = e" |
|
501 |
unfolding e_def |
|
55665 | 502 |
using c(1) |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
503 |
using norm_minus_cancel[of "f' i - f'' i"] |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53799
diff
changeset
|
504 |
by auto |
53781 | 505 |
finally show False |
506 |
using c |
|
55665 | 507 |
using d(2)[of "x + c *\<^sub>R i"] |
44123 | 508 |
unfolding dist_norm |
509 |
unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff |
|
510 |
scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib |
|
53781 | 511 |
using i |
512 |
by (auto simp: inverse_eq_divide) |
|
44123 | 513 |
qed |
514 |
qed |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
515 |
|
37730 | 516 |
lemma frechet_derivative_unique_at: |
53781 | 517 |
"(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''" |
37730 | 518 |
by (rule FDERIV_unique) |
41829 | 519 |
|
44123 | 520 |
lemma frechet_derivative_unique_within_closed_interval: |
521 |
fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector" |
|
53781 | 522 |
assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" |
523 |
and "x \<in> {a..b}" |
|
524 |
and "(f has_derivative f' ) (at x within {a..b})" |
|
525 |
and "(f has_derivative f'') (at x within {a..b})" |
|
44123 | 526 |
shows "f' = f''" |
527 |
apply(rule frechet_derivative_unique_within) |
|
528 |
apply(rule assms(3,4))+ |
|
53781 | 529 |
proof (rule, rule, rule) |
530 |
fix e :: real |
|
531 |
fix i :: 'a |
|
532 |
assume "e > 0" and i: "i \<in> Basis" |
|
533 |
then show "\<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> {a..b}" |
|
534 |
proof (cases "x\<bullet>i = a\<bullet>i") |
|
535 |
case True |
|
536 |
then show ?thesis |
|
537 |
apply (rule_tac x="(min (b\<bullet>i - a\<bullet>i) e) / 2" in exI) |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
538 |
using assms(1)[THEN bspec[where x=i]] and `e>0` and assms(2) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
539 |
unfolding mem_interval |
53781 | 540 |
using i |
541 |
apply (auto simp add: field_simps inner_simps inner_Basis) |
|
542 |
done |
|
543 |
next |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
544 |
note * = assms(2)[unfolded mem_interval, THEN bspec, OF i] |
53781 | 545 |
case False |
546 |
moreover have "a \<bullet> i < x \<bullet> i" |
|
547 |
using False * by auto |
|
44123 | 548 |
moreover { |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
549 |
have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> a\<bullet>i *2 + x\<bullet>i - a\<bullet>i" |
44123 | 550 |
by auto |
53781 | 551 |
also have "\<dots> = a\<bullet>i + x\<bullet>i" |
552 |
by auto |
|
553 |
also have "\<dots> \<le> 2 * (x\<bullet>i)" |
|
554 |
using * by auto |
|
555 |
finally have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> x \<bullet> i * 2" |
|
556 |
by auto |
|
44123 | 557 |
} |
53781 | 558 |
moreover have "min (x \<bullet> i - a \<bullet> i) e \<ge> 0" |
559 |
using * and `e>0` by auto |
|
560 |
then have "x \<bullet> i * 2 \<le> b \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e" |
|
561 |
using * by auto |
|
44123 | 562 |
ultimately show ?thesis |
53781 | 563 |
apply (rule_tac x="- (min (x\<bullet>i - a\<bullet>i) e) / 2" in exI) |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
564 |
using assms(1)[THEN bspec, OF i] and `e>0` and assms(2) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
565 |
unfolding mem_interval |
53781 | 566 |
using i |
567 |
apply (auto simp add: field_simps inner_simps inner_Basis) |
|
568 |
done |
|
44123 | 569 |
qed |
570 |
qed |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
571 |
|
44123 | 572 |
lemma frechet_derivative_unique_within_open_interval: |
573 |
fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector" |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
574 |
assumes "x \<in> box a b" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
575 |
and "(f has_derivative f' ) (at x within box a b)" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
576 |
and "(f has_derivative f'') (at x within box a b)" |
37650 | 577 |
shows "f' = f''" |
578 |
proof - |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
579 |
from assms(1) have *: "at x within box a b = at x" |
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51478
diff
changeset
|
580 |
by (metis at_within_interior interior_open open_interval) |
37650 | 581 |
from assms(2,3) [unfolded *] show "f' = f''" |
582 |
by (rule frechet_derivative_unique_at) |
|
583 |
qed |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
584 |
|
37730 | 585 |
lemma frechet_derivative_at: |
53781 | 586 |
"(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)" |
587 |
apply (rule frechet_derivative_unique_at[of f]) |
|
588 |
apply assumption |
|
589 |
unfolding frechet_derivative_works[symmetric] |
|
590 |
using differentiable_def |
|
591 |
apply auto |
|
592 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
593 |
|
44123 | 594 |
lemma frechet_derivative_within_closed_interval: |
53781 | 595 |
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector" |
596 |
assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" |
|
597 |
and "x \<in> {a..b}" |
|
598 |
and "(f has_derivative f') (at x within {a..b})" |
|
599 |
shows "frechet_derivative f (at x within {a..b}) = f'" |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
600 |
using assms |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
601 |
by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works) |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
602 |
|
53781 | 603 |
|
604 |
subsection {* The traditional Rolle theorem in one dimension *} |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
605 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
606 |
lemma linear_componentwise: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
607 |
fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
608 |
assumes lf: "linear f" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
609 |
shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs") |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
610 |
proof - |
53781 | 611 |
have fA: "finite Basis" |
612 |
by simp |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
613 |
have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
614 |
by (simp add: inner_setsum_left) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
615 |
then show ?thesis |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
616 |
unfolding linear_setsum_mul[OF lf fA, symmetric] |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
617 |
unfolding euclidean_representation .. |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
618 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
619 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
620 |
text {* We do not introduce @{text jacobian}, which is defined on matrices, instead we use |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
621 |
the unfolding of it. *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
622 |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
623 |
lemma jacobian_works: |
53781 | 624 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
625 |
shows "f differentiable net \<longleftrightarrow> |
|
626 |
(f has_derivative (\<lambda>h. \<Sum>i\<in>Basis. |
|
627 |
(\<Sum>j\<in>Basis. frechet_derivative f net j \<bullet> i * (h \<bullet> j)) *\<^sub>R i)) net" |
|
628 |
(is "?differentiable \<longleftrightarrow> (f has_derivative (\<lambda>h. \<Sum>i\<in>Basis. ?SUM h i *\<^sub>R i)) net") |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
629 |
proof |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
630 |
assume *: ?differentiable |
53781 | 631 |
{ |
632 |
fix h i |
|
633 |
have "?SUM h i = frechet_derivative f net h \<bullet> i" |
|
634 |
using * |
|
635 |
by (auto intro!: setsum_cong simp: linear_componentwise[of _ h i] linear_frechet_derivative) |
|
636 |
} |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
637 |
with * show "(f has_derivative (\<lambda>h. \<Sum>i\<in>Basis. ?SUM h i *\<^sub>R i)) net" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
638 |
by (simp add: frechet_derivative_works euclidean_representation) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
639 |
qed (auto intro!: differentiableI) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
640 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
641 |
lemma differential_zero_maxmin_component: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
642 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
643 |
assumes k: "k \<in> Basis" |
53781 | 644 |
and ball: "0 < e" "(\<forall>y \<in> ball x e. (f y)\<bullet>k \<le> (f x)\<bullet>k) \<or> (\<forall>y\<in>ball x e. (f x)\<bullet>k \<le> (f y)\<bullet>k)" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
645 |
and diff: "f differentiable (at x)" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
646 |
shows "(\<Sum>j\<in>Basis. (frechet_derivative f (at x) j \<bullet> k) *\<^sub>R j) = (0::'a)" (is "?D k = 0") |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
647 |
proof (rule ccontr) |
53781 | 648 |
assume "\<not> ?thesis" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
649 |
then obtain j where j: "?D k \<bullet> j \<noteq> 0" "j \<in> Basis" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
650 |
unfolding euclidean_eq_iff[of _ "0::'a"] by auto |
53781 | 651 |
then have *: "\<bar>?D k \<bullet> j\<bar> / 2 > 0" |
652 |
by auto |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
653 |
note as = diff[unfolded jacobian_works has_derivative_at_alt] |
55665 | 654 |
obtain e' where e': |
655 |
"0 < e'" |
|
656 |
"(\<And>y. norm (y - x) < e' \<Longrightarrow> |
|
657 |
norm (f y - f x - |
|
658 |
(\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative f (at x) j \<bullet> i * ((y - x) \<bullet> j)) *\<^sub>R i)) |
|
659 |
\<le> \<bar>(\<Sum>j\<in>Basis. (frechet_derivative f (at x) j \<bullet> k) *\<^sub>R j) \<bullet> j\<bar> / 2 * norm (y - x))" |
|
660 |
using as[THEN conjunct2] * by blast |
|
661 |
obtain d where d: "0 < d" "d < e" "d < e'" |
|
662 |
using real_lbound_gt_zero[OF ball(1) e'(1)] by blast |
|
53781 | 663 |
{ |
664 |
fix c |
|
665 |
assume "abs c \<le> d" |
|
666 |
then have *: "norm (x + c *\<^sub>R j - x) < e'" |
|
667 |
using norm_Basis[OF j(2)] d by auto |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
668 |
let ?v = "(\<Sum>i\<in>Basis. (\<Sum>l\<in>Basis. ?D i \<bullet> l * ((c *\<^sub>R j :: 'a) \<bullet> l)) *\<^sub>R i)" |
53781 | 669 |
have if_dist: "\<And> P a b c. a * (if P then b else c) = (if P then a * b else a * c)" |
670 |
by auto |
|
671 |
have "\<bar>(f (x + c *\<^sub>R j) - f x - ?v) \<bullet> k\<bar> \<le> norm (f (x + c *\<^sub>R j) - f x - ?v)" |
|
672 |
by (rule Basis_le_norm[OF k]) |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
673 |
also have "\<dots> \<le> \<bar>?D k \<bullet> j\<bar> / 2 * \<bar>c\<bar>" |
55665 | 674 |
using e'(2)[OF *] and norm_Basis[OF j(2)] j |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
675 |
by simp |
53781 | 676 |
finally have "\<bar>(f (x + c *\<^sub>R j) - f x - ?v) \<bullet> k\<bar> \<le> \<bar>?D k \<bullet> j\<bar> / 2 * \<bar>c\<bar>" |
677 |
by simp |
|
678 |
then have "\<bar>f (x + c *\<^sub>R j) \<bullet> k - f x \<bullet> k - c * (?D k \<bullet> j)\<bar> \<le> \<bar>?D k \<bullet> j\<bar> / 2 * \<bar>c\<bar>" |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
679 |
using j k |
53781 | 680 |
by (simp add: inner_simps field_simps inner_Basis setsum_cases if_dist) |
681 |
} |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
682 |
note * = this |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
683 |
have "x + d *\<^sub>R j \<in> ball x e" "x - d *\<^sub>R j \<in> ball x e" |
53781 | 684 |
unfolding mem_ball dist_norm |
685 |
using norm_Basis[OF j(2)] d |
|
686 |
by auto |
|
687 |
then have **: "((f (x - d *\<^sub>R j))\<bullet>k \<le> (f x)\<bullet>k \<and> (f (x + d *\<^sub>R j))\<bullet>k \<le> (f x)\<bullet>k) \<or> |
|
688 |
((f (x - d *\<^sub>R j))\<bullet>k \<ge> (f x)\<bullet>k \<and> (f (x + d *\<^sub>R j))\<bullet>k \<ge> (f x)\<bullet>k)" |
|
689 |
using ball by auto |
|
690 |
have ***: "\<And>y y1 y2 d dx :: real. y1 \<le> y \<and> y2 \<le> y \<or> y \<le> y1 \<and> y \<le> y2 \<Longrightarrow> |
|
691 |
d < abs dx \<Longrightarrow> abs (y1 - y - - dx) \<le> d \<Longrightarrow> abs (y2 - y - dx) \<le> d \<Longrightarrow> False" |
|
692 |
by arith |
|
693 |
show False |
|
694 |
apply (rule ***[OF **, where dx="d * (?D k \<bullet> j)" and d="\<bar>?D k \<bullet> j\<bar> / 2 * \<bar>d\<bar>"]) |
|
55665 | 695 |
using *[of "-d"] and *[of d] and d(1) and j |
44123 | 696 |
unfolding mult_minus_left |
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset
|
697 |
unfolding abs_mult diff_minus_eq_add scaleR_minus_left |
53781 | 698 |
unfolding algebra_simps |
699 |
apply (auto intro: mult_pos_pos) |
|
700 |
done |
|
34906 | 701 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
702 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
703 |
text {* In particular if we have a mapping into @{typ "real"}. *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
704 |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
705 |
lemma differential_zero_maxmin: |
53781 | 706 |
fixes f::"'a::euclidean_space \<Rightarrow> real" |
707 |
assumes "x \<in> s" |
|
708 |
and "open s" |
|
709 |
and deriv: "(f has_derivative f') (at x)" |
|
710 |
and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
711 |
shows "f' = (\<lambda>v. 0)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
712 |
proof - |
53781 | 713 |
obtain e where e: "e > 0" "ball x e \<subseteq> s" |
44123 | 714 |
using `open s`[unfolded open_contains_ball] and `x \<in> s` by auto |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
715 |
with differential_zero_maxmin_component[where 'b=real, of 1 e x f] mono deriv |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
716 |
have "(\<Sum>j\<in>Basis. frechet_derivative f (at x) j *\<^sub>R j) = (0::'a)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
717 |
by (auto simp: Basis_real_def differentiable_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
718 |
with frechet_derivative_at[OF deriv, symmetric] |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
719 |
have "\<forall>i\<in>Basis. f' i = 0" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
720 |
by (simp add: euclidean_eq_iff[of _ "0::'a"] inner_setsum_left_Basis) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
721 |
with derivative_is_linear[OF deriv, THEN linear_componentwise, of _ 1] |
53781 | 722 |
show ?thesis |
723 |
by (simp add: fun_eq_iff) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
724 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
725 |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
726 |
lemma rolle: |
53781 | 727 |
fixes f :: "real \<Rightarrow> real" |
728 |
assumes "a < b" |
|
729 |
and "f a = f b" |
|
730 |
and "continuous_on {a..b} f" |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
731 |
and "\<forall>x\<in>box a b. (f has_derivative f' x) (at x)" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
732 |
shows "\<exists>x\<in>box a b. f' x = (\<lambda>v. 0)" |
53781 | 733 |
proof - |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
734 |
have "\<exists>x\<in>box a b. (\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)" |
53781 | 735 |
proof - |
736 |
have "(a + b) / 2 \<in> {a .. b}" |
|
737 |
using assms(1) by auto |
|
738 |
then have *: "{a..b} \<noteq> {}" |
|
739 |
by auto |
|
55665 | 740 |
obtain d where d: |
741 |
"d \<in> {a..b}" |
|
742 |
"\<forall>y\<in>{a..b}. f y \<le> f d" |
|
743 |
using continuous_attains_sup[OF compact_interval * assms(3)] .. |
|
744 |
obtain c where c: |
|
745 |
"c \<in> {a..b}" |
|
746 |
"\<forall>y\<in>{a..b}. f c \<le> f y" |
|
747 |
using continuous_attains_inf[OF compact_interval * assms(3)] .. |
|
44123 | 748 |
show ?thesis |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
749 |
proof (cases "d \<in> box a b \<or> c \<in> box a b") |
53781 | 750 |
case True |
751 |
then show ?thesis |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
752 |
by (metis c(2) d(2) interval_open_subset_closed subset_iff) |
44123 | 753 |
next |
754 |
def e \<equiv> "(a + b) /2" |
|
53781 | 755 |
case False |
756 |
then have "f d = f c" |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
757 |
using d c assms(2) by (auto simp: box_real) |
53781 | 758 |
then have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d" |
759 |
using c d |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
760 |
by force |
53781 | 761 |
then show ?thesis |
762 |
apply (rule_tac x=e in bexI) |
|
763 |
unfolding e_def |
|
764 |
using assms(1) |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
765 |
apply (auto simp: box_real) |
53781 | 766 |
done |
44123 | 767 |
qed |
768 |
qed |
|
55665 | 769 |
then obtain x where x: "x \<in> box a b" "(\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)" .. |
53781 | 770 |
then have "f' x = (\<lambda>v. 0)" |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
771 |
apply (rule_tac differential_zero_maxmin[of x "box a b" f "f' x"]) |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
772 |
using assms |
53781 | 773 |
apply auto |
774 |
done |
|
775 |
then show ?thesis |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
776 |
by (metis x(1)) |
44123 | 777 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
778 |
|
53781 | 779 |
|
780 |
subsection {* One-dimensional mean value theorem *} |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
781 |
|
53781 | 782 |
lemma mvt: |
783 |
fixes f :: "real \<Rightarrow> real" |
|
784 |
assumes "a < b" |
|
785 |
and "continuous_on {a..b} f" |
|
44123 | 786 |
assumes "\<forall>x\<in>{a<..<b}. (f has_derivative (f' x)) (at x)" |
53781 | 787 |
shows "\<exists>x\<in>{a<..<b}. f b - f a = (f' x) (b - a)" |
788 |
proof - |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
789 |
have "\<exists>x\<in>box a b. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" |
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51363
diff
changeset
|
790 |
proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI) |
53781 | 791 |
fix x |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
792 |
assume "x \<in> box a b" hence x: "x \<in> {a<..<b}" by (simp add: box_real) |
53781 | 793 |
show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative |
794 |
(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
795 |
by (intro FDERIV_intros assms(3)[rule_format,OF x] mult_right_has_derivative) |
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51363
diff
changeset
|
796 |
qed (insert assms(1,2), auto intro!: continuous_on_intros simp: field_simps) |
55665 | 797 |
then obtain x where |
798 |
"x \<in> box a b" |
|
799 |
"(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" .. |
|
53781 | 800 |
then show ?thesis |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
801 |
by (metis (erased, hide_lams) assms(1) box_real diff_less_iff(1) eq_iff_diff_eq_0 linordered_field_class.sign_simps(41) nonzero_mult_divide_cancel_right not_real_square_gt_zero times_divide_eq_left) |
44123 | 802 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
803 |
|
44123 | 804 |
lemma mvt_simple: |
53781 | 805 |
fixes f :: "real \<Rightarrow> real" |
806 |
assumes "a < b" |
|
807 |
and "\<forall>x\<in>{a..b}. (f has_derivative f' x) (at x within {a..b})" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
808 |
shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)" |
53781 | 809 |
apply (rule mvt) |
810 |
apply (rule assms(1)) |
|
811 |
apply (rule differentiable_imp_continuous_on) |
|
812 |
unfolding differentiable_on_def differentiable_def |
|
813 |
defer |
|
44123 | 814 |
proof |
53781 | 815 |
fix x |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
816 |
assume x: "x \<in> {a<..<b}" hence x: "x \<in> box a b" by (simp add: box_real) |
53781 | 817 |
show "(f has_derivative f' x) (at x)" |
818 |
unfolding has_derivative_within_open[OF x open_interval,symmetric] |
|
819 |
apply (rule has_derivative_within_subset) |
|
820 |
apply (rule assms(2)[rule_format]) |
|
821 |
using x |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
822 |
apply (auto simp: box_real) |
53781 | 823 |
done |
824 |
qed (insert assms(2), auto) |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
825 |
|
44123 | 826 |
lemma mvt_very_simple: |
53781 | 827 |
fixes f :: "real \<Rightarrow> real" |
828 |
assumes "a \<le> b" |
|
829 |
and "\<forall>x\<in>{a..b}. (f has_derivative f' x) (at x within {a..b})" |
|
44123 | 830 |
shows "\<exists>x\<in>{a..b}. f b - f a = f' x (b - a)" |
831 |
proof (cases "a = b") |
|
53781 | 832 |
interpret bounded_linear "f' b" |
833 |
using assms(2) assms(1) by auto |
|
834 |
case True |
|
835 |
then show ?thesis |
|
836 |
apply (rule_tac x=a in bexI) |
|
837 |
using assms(2)[THEN bspec[where x=a]] |
|
838 |
unfolding has_derivative_def |
|
839 |
unfolding True |
|
840 |
using zero |
|
841 |
apply auto |
|
842 |
done |
|
843 |
next |
|
844 |
case False |
|
845 |
then show ?thesis |
|
846 |
using mvt_simple[OF _ assms(2)] |
|
847 |
using assms(1) |
|
848 |
by auto |
|
44123 | 849 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
850 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
851 |
text {* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
852 |
|
44123 | 853 |
lemma mvt_general: |
53781 | 854 |
fixes f :: "real \<Rightarrow> 'a::euclidean_space" |
855 |
assumes "a < b" |
|
856 |
and "continuous_on {a..b} f" |
|
857 |
and "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)" |
|
858 |
shows "\<exists>x\<in>{a<..<b}. norm (f b - f a) \<le> norm (f' x (b - a))" |
|
859 |
proof - |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
860 |
have "\<exists>x\<in>{a<..<b}. (op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)" |
53781 | 861 |
apply (rule mvt) |
862 |
apply (rule assms(1)) |
|
863 |
apply (rule continuous_on_inner continuous_on_intros assms(2) ballI)+ |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
864 |
unfolding o_def |
53781 | 865 |
apply (rule FDERIV_inner_right) |
866 |
using assms(3) |
|
867 |
apply auto |
|
868 |
done |
|
55665 | 869 |
then obtain x where x: |
870 |
"x \<in> {a<..<b}" |
|
871 |
"(op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)" .. |
|
53781 | 872 |
show ?thesis |
873 |
proof (cases "f a = f b") |
|
36844 | 874 |
case False |
53077 | 875 |
have "norm (f b - f a) * norm (f b - f a) = (norm (f b - f a))\<^sup>2" |
44123 | 876 |
by (simp add: power2_eq_square) |
53781 | 877 |
also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" |
878 |
unfolding power2_norm_eq_inner .. |
|
44123 | 879 |
also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" |
53781 | 880 |
using x |
881 |
unfolding inner_simps |
|
882 |
by (auto simp add: inner_diff_left) |
|
44123 | 883 |
also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" |
884 |
by (rule norm_cauchy_schwarz) |
|
53781 | 885 |
finally show ?thesis |
886 |
using False x(1) |
|
44123 | 887 |
by (auto simp add: real_mult_left_cancel) |
888 |
next |
|
53781 | 889 |
case True |
890 |
then show ?thesis |
|
891 |
using assms(1) |
|
892 |
apply (rule_tac x="(a + b) /2" in bexI) |
|
893 |
apply auto |
|
894 |
done |
|
44123 | 895 |
qed |
896 |
qed |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
897 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
898 |
text {* Still more general bound theorem. *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
899 |
|
44123 | 900 |
lemma differentiable_bound: |
53781 | 901 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
902 |
assumes "convex s" |
|
903 |
and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)" |
|
904 |
and "\<forall>x\<in>s. onorm (f' x) \<le> B" |
|
905 |
and x: "x \<in> s" |
|
906 |
and y: "y \<in> s" |
|
907 |
shows "norm (f x - f y) \<le> B * norm (x - y)" |
|
908 |
proof - |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
909 |
let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)" |
53781 | 910 |
have *: "\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s" |
44123 | 911 |
using assms(1)[unfolded convex_alt,rule_format,OF x y] |
912 |
unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib |
|
913 |
by (auto simp add: algebra_simps) |
|
53781 | 914 |
then have 1: "continuous_on {0..1} (f \<circ> ?p)" |
915 |
apply - |
|
916 |
apply (rule continuous_on_intros)+ |
|
44123 | 917 |
unfolding continuous_on_eq_continuous_within |
53781 | 918 |
apply rule |
919 |
apply (rule differentiable_imp_continuous_within) |
|
920 |
unfolding differentiable_def |
|
921 |
apply (rule_tac x="f' xa" in exI) |
|
922 |
apply (rule has_derivative_within_subset) |
|
923 |
apply (rule assms(2)[rule_format]) |
|
924 |
apply auto |
|
925 |
done |
|
926 |
have 2: "\<forall>u\<in>{0<..<1}. |
|
927 |
((f \<circ> ?p) has_derivative f' (x + u *\<^sub>R (y - x)) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u)" |
|
44123 | 928 |
proof rule |
929 |
case goal1 |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
930 |
let ?u = "x + u *\<^sub>R (y - x)" |
53781 | 931 |
have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within {0<..<1})" |
932 |
apply (rule diff_chain_within) |
|
933 |
apply (rule FDERIV_intros)+ |
|
934 |
apply (rule has_derivative_within_subset) |
|
935 |
apply (rule assms(2)[rule_format]) |
|
936 |
using goal1 * |
|
937 |
apply auto |
|
938 |
done |
|
939 |
then show ?case |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset
|
940 |
unfolding has_derivative_within_open[OF goal1 open_greaterThanLessThan] . |
44123 | 941 |
qed |
55665 | 942 |
obtain u where u: |
943 |
"u \<in> {0<..<1}" |
|
944 |
"norm ((f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 1 - (f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 0) |
|
945 |
\<le> norm ((f' (x + u *\<^sub>R (y - x)) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (1 - 0))" |
|
946 |
using mvt_general[OF zero_less_one 1 2] .. |
|
53781 | 947 |
have **: "\<And>x y. x \<in> s \<Longrightarrow> norm (f' x y) \<le> B * norm y" |
948 |
proof - |
|
44123 | 949 |
case goal1 |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
950 |
have "norm (f' x y) \<le> onorm (f' x) * norm y" |
53781 | 951 |
by (rule onorm(1)[OF derivative_is_linear[OF assms(2)[rule_format,OF goal1]]]) |
44123 | 952 |
also have "\<dots> \<le> B * norm y" |
53781 | 953 |
apply (rule mult_right_mono) |
44123 | 954 |
using assms(3)[rule_format,OF goal1] |
53781 | 955 |
apply (auto simp add: field_simps) |
956 |
done |
|
957 |
finally show ?case |
|
958 |
by simp |
|
44123 | 959 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
960 |
have "norm (f x - f y) = norm ((f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 1 - (f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 0)" |
53781 | 961 |
by (auto simp add: norm_minus_commute) |
962 |
also have "\<dots> \<le> norm (f' (x + u *\<^sub>R (y - x)) (y - x))" |
|
963 |
using u by auto |
|
964 |
also have "\<dots> \<le> B * norm(y - x)" |
|
965 |
apply (rule **) |
|
966 |
using * and u |
|
967 |
apply auto |
|
968 |
done |
|
969 |
finally show ?thesis |
|
970 |
by (auto simp add: norm_minus_commute) |
|
44123 | 971 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
972 |
|
44123 | 973 |
lemma differentiable_bound_real: |
53781 | 974 |
fixes f :: "real \<Rightarrow> real" |
975 |
assumes "convex s" |
|
976 |
and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)" |
|
977 |
and "\<forall>x\<in>s. onorm (f' x) \<le> B" |
|
978 |
and x: "x \<in> s" |
|
979 |
and y: "y \<in> s" |
|
980 |
shows "norm (f x - f y) \<le> B * norm (x - y)" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
981 |
using differentiable_bound[of s f f' B x y] |
53781 | 982 |
unfolding Ball_def image_iff o_def |
983 |
using assms |
|
984 |
by auto |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
985 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
986 |
text {* In particular. *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
987 |
|
44123 | 988 |
lemma has_derivative_zero_constant: |
53781 | 989 |
fixes f :: "real \<Rightarrow> real" |
990 |
assumes "convex s" |
|
991 |
and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)" |
|
44123 | 992 |
shows "\<exists>c. \<forall>x\<in>s. f x = c" |
53781 | 993 |
proof (cases "s={}") |
994 |
case False |
|
995 |
then obtain x where "x \<in> s" |
|
996 |
by auto |
|
997 |
have "\<And>y. y \<in> s \<Longrightarrow> f x = f y" |
|
998 |
proof - |
|
999 |
case goal1 |
|
1000 |
then show ?case |
|
1001 |
using differentiable_bound_real[OF assms(1-2), of 0 x y] and `x \<in> s` |
|
1002 |
unfolding onorm_const |
|
1003 |
by auto |
|
1004 |
qed |
|
1005 |
then show ?thesis |
|
1006 |
apply (rule_tac x="f x" in exI) |
|
1007 |
apply auto |
|
1008 |
done |
|
1009 |
next |
|
1010 |
case True |
|
1011 |
then show ?thesis by auto |
|
1012 |
qed |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1013 |
|
53781 | 1014 |
lemma has_derivative_zero_unique: |
1015 |
fixes f :: "real \<Rightarrow> real" |
|
1016 |
assumes "convex s" |
|
1017 |
and "a \<in> s" |
|
1018 |
and "f a = c" |
|
1019 |
and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)" |
|
1020 |
and "x \<in> s" |
|
44123 | 1021 |
shows "f x = c" |
53781 | 1022 |
using has_derivative_zero_constant[OF assms(1,4)] |
1023 |
using assms(2-3,5) |
|
1024 |
by auto |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1025 |
|
53781 | 1026 |
|
1027 |
subsection {* Differentiability of inverse function (most basic form) *} |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1028 |
|
44123 | 1029 |
lemma has_derivative_inverse_basic: |
53781 | 1030 |
fixes f :: "'b::euclidean_space \<Rightarrow> 'c::euclidean_space" |
44123 | 1031 |
assumes "(f has_derivative f') (at (g y))" |
53781 | 1032 |
and "bounded_linear g'" |
1033 |
and "g' \<circ> f' = id" |
|
1034 |
and "continuous (at y) g" |
|
1035 |
and "open t" |
|
1036 |
and "y \<in> t" |
|
1037 |
and "\<forall>z\<in>t. f (g z) = z" |
|
44123 | 1038 |
shows "(g has_derivative g') (at y)" |
53781 | 1039 |
proof - |
44123 | 1040 |
interpret f': bounded_linear f' |
1041 |
using assms unfolding has_derivative_def by auto |
|
53781 | 1042 |
interpret g': bounded_linear g' |
1043 |
using assms by auto |
|
55665 | 1044 |
obtain C where C: "0 < C" "\<And>x. norm (g' x) \<le> norm x * C" |
1045 |
using bounded_linear.pos_bounded[OF assms(2)] by blast |
|
53781 | 1046 |
have lem1: "\<forall>e>0. \<exists>d>0. \<forall>z. |
1047 |
norm (z - y) < d \<longrightarrow> norm (g z - g y - g'(z - y)) \<le> e * norm (g z - g y)" |
|
1048 |
proof (rule, rule) |
|
44123 | 1049 |
case goal1 |
53781 | 1050 |
have *: "e / C > 0" |
1051 |
apply (rule divide_pos_pos) |
|
55665 | 1052 |
using `e > 0` C(1) |
53781 | 1053 |
apply auto |
1054 |
done |
|
55665 | 1055 |
obtain d0 where d0: |
1056 |
"0 < d0" |
|
1057 |
"\<forall>ya. norm (ya - g y) < d0 \<longrightarrow> norm (f ya - f (g y) - f' (ya - g y)) \<le> e / C * norm (ya - g y)" |
|
1058 |
using assms(1) |
|
1059 |
unfolding has_derivative_at_alt |
|
1060 |
using * by blast |
|
1061 |
obtain d1 where d1: |
|
1062 |
"0 < d1" |
|
1063 |
"\<forall>x. 0 < dist x y \<and> dist x y < d1 \<longrightarrow> dist (g x) (g y) < d0" |
|
1064 |
using assms(4) |
|
1065 |
unfolding continuous_at Lim_at |
|
1066 |
using d0(1) by blast |
|
1067 |
obtain d2 where d2: |
|
1068 |
"0 < d2" |
|
1069 |
"\<forall>ya. dist ya y < d2 \<longrightarrow> ya \<in> t" |
|
1070 |
using assms(5) |
|
1071 |
unfolding open_dist |
|
1072 |
using assms(6) by blast |
|
1073 |
obtain d where d: "0 < d" "d < d1" "d < d2" |
|
1074 |
using real_lbound_gt_zero[OF d1(1) d2(1)] by blast |
|
53781 | 1075 |
then show ?case |
1076 |
apply (rule_tac x=d in exI) |
|
1077 |
apply rule |
|
1078 |
defer |
|
1079 |
apply rule |
|
1080 |
apply rule |
|
1081 |
proof - |
|
1082 |
fix z |
|
1083 |
assume as: "norm (z - y) < d" |
|
1084 |
then have "z \<in> t" |
|
44123 | 1085 |
using d2 d unfolding dist_norm by auto |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1086 |
have "norm (g z - g y - g' (z - y)) \<le> norm (g' (f (g z) - y - f' (g z - g y)))" |
44123 | 1087 |
unfolding g'.diff f'.diff |
53781 | 1088 |
unfolding assms(3)[unfolded o_def id_def, THEN fun_cong] |
44123 | 1089 |
unfolding assms(7)[rule_format,OF `z\<in>t`] |
53781 | 1090 |
apply (subst norm_minus_cancel[symmetric]) |
1091 |
apply auto |
|
1092 |
done |
|
1093 |
also have "\<dots> \<le> norm (f (g z) - y - f' (g z - g y)) * C" |
|
55665 | 1094 |
by (rule C(2)) |
44123 | 1095 |
also have "\<dots> \<le> (e / C) * norm (g z - g y) * C" |
53781 | 1096 |
apply (rule mult_right_mono) |
55665 | 1097 |
apply (rule d0(2)[rule_format,unfolded assms(7)[rule_format,OF `y\<in>t`]]) |
53781 | 1098 |
apply (cases "z = y") |
1099 |
defer |
|
55665 | 1100 |
apply (rule d1(2)[unfolded dist_norm,rule_format]) |
53781 | 1101 |
using as d C d0 |
1102 |
apply auto |
|
1103 |
done |
|
44123 | 1104 |
also have "\<dots> \<le> e * norm (g z - g y)" |
1105 |
using C by (auto simp add: field_simps) |
|
1106 |
finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)" |
|
1107 |
by simp |
|
1108 |
qed auto |
|
1109 |
qed |
|
53781 | 1110 |
have *: "(0::real) < 1 / 2" |
1111 |
by auto |
|
55665 | 1112 |
obtain d where d: |
1113 |
"0 < d" |
|
1114 |
"\<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> 1 / 2 * norm (g z - g y)" |
|
1115 |
using lem1 * by blast |
|
1116 |
def B \<equiv> "C * 2" |
|
53781 | 1117 |
have "B > 0" |
1118 |
unfolding B_def using C by auto |
|
1119 |
have lem2: "\<forall>z. norm(z - y) < d \<longrightarrow> norm (g z - g y) \<le> B * norm (z - y)" |
|
1120 |
proof (rule, rule) |
|
1121 |
case goal1 |
|
44123 | 1122 |
have "norm (g z - g y) \<le> norm(g' (z - y)) + norm ((g z - g y) - g'(z - y))" |
53781 | 1123 |
by (rule norm_triangle_sub) |
1124 |
also have "\<dots> \<le> norm (g' (z - y)) + 1 / 2 * norm (g z - g y)" |
|
1125 |
apply (rule add_left_mono) |
|
1126 |
using d and goal1 |
|
1127 |
apply auto |
|
1128 |
done |
|
44123 | 1129 |
also have "\<dots> \<le> norm (z - y) * C + 1 / 2 * norm (g z - g y)" |
53781 | 1130 |
apply (rule add_right_mono) |
1131 |
using C |
|
1132 |
apply auto |
|
1133 |
done |
|
1134 |
finally show ?case |
|
1135 |
unfolding B_def |
|
1136 |
by (auto simp add: field_simps) |
|
44123 | 1137 |
qed |
53781 | 1138 |
show ?thesis |
1139 |
unfolding has_derivative_at_alt |
|
1140 |
apply rule |
|
1141 |
apply (rule assms) |
|
1142 |
apply rule |
|
1143 |
apply rule |
|
1144 |
proof - |
|
1145 |
case goal1 |
|
1146 |
then have *: "e / B >0" |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
1147 |
by (metis `0 < B` divide_pos_pos) |
55665 | 1148 |
obtain d' where d': |
1149 |
"0 < d'" |
|
1150 |
"\<forall>z. norm (z - y) < d' \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)" |
|
1151 |
using lem1 * by blast |
|
1152 |
obtain k where k: "0 < k" "k < d" "k < d'" |
|
1153 |
using real_lbound_gt_zero[OF d(1) d'(1)] by blast |
|
44123 | 1154 |
show ?case |
53781 | 1155 |
apply (rule_tac x=k in exI) |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
1156 |
apply auto |
53781 | 1157 |
proof - |
1158 |
fix z |
|
1159 |
assume as: "norm (z - y) < k" |
|
1160 |
then have "norm (g z - g y - g' (z - y)) \<le> e / B * norm(g z - g y)" |
|
44123 | 1161 |
using d' k by auto |
53781 | 1162 |
also have "\<dots> \<le> e * norm (z - y)" |
44123 | 1163 |
unfolding times_divide_eq_left pos_divide_le_eq[OF `B>0`] |
53781 | 1164 |
using lem2[THEN spec[where x=z]] |
1165 |
using k as using `e > 0` |
|
44123 | 1166 |
by (auto simp add: field_simps) |
1167 |
finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (z - y)" |
|
53781 | 1168 |
by simp |
1169 |
qed(insert k, auto) |
|
44123 | 1170 |
qed |
1171 |
qed |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1172 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
1173 |
text {* Simply rewrite that based on the domain point x. *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1174 |
|
44123 | 1175 |
lemma has_derivative_inverse_basic_x: |
53781 | 1176 |
fixes f :: "'b::euclidean_space \<Rightarrow> 'c::euclidean_space" |
1177 |
assumes "(f has_derivative f') (at x)" |
|
1178 |
and "bounded_linear g'" |
|
1179 |
and "g' \<circ> f' = id" |
|
1180 |
and "continuous (at (f x)) g" |
|
1181 |
and "g (f x) = x" |
|
1182 |
and "open t" |
|
1183 |
and "f x \<in> t" |
|
1184 |
and "\<forall>y\<in>t. f (g y) = y" |
|
1185 |
shows "(g has_derivative g') (at (f x))" |
|
1186 |
apply (rule has_derivative_inverse_basic) |
|
1187 |
using assms |
|
1188 |
apply auto |
|
1189 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1190 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
1191 |
text {* This is the version in Dieudonne', assuming continuity of f and g. *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1192 |
|
44123 | 1193 |
lemma has_derivative_inverse_dieudonne: |
53781 | 1194 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
1195 |
assumes "open s" |
|
1196 |
and "open (f ` s)" |
|
1197 |
and "continuous_on s f" |
|
1198 |
and "continuous_on (f ` s) g" |
|
1199 |
and "\<forall>x\<in>s. g (f x) = x" |
|
1200 |
and "x \<in> s" |
|
1201 |
and "(f has_derivative f') (at x)" |
|
1202 |
and "bounded_linear g'" |
|
1203 |
and "g' \<circ> f' = id" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1204 |
shows "(g has_derivative g') (at (f x))" |
53781 | 1205 |
apply (rule has_derivative_inverse_basic_x[OF assms(7-9) _ _ assms(2)]) |
1206 |
using assms(3-6) |
|
1207 |
unfolding continuous_on_eq_continuous_at[OF assms(1)] continuous_on_eq_continuous_at[OF assms(2)] |
|
1208 |
apply auto |
|
1209 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1210 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
1211 |
text {* Here's the simplest way of not assuming much about g. *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1212 |
|
44123 | 1213 |
lemma has_derivative_inverse: |
53781 | 1214 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
1215 |
assumes "compact s" |
|
1216 |
and "x \<in> s" |
|
1217 |
and "f x \<in> interior (f ` s)" |
|
1218 |
and "continuous_on s f" |
|
1219 |
and "\<forall>y\<in>s. g (f y) = y" |
|
1220 |
and "(f has_derivative f') (at x)" |
|
1221 |
and "bounded_linear g'" |
|
1222 |
and "g' \<circ> f' = id" |
|
44123 | 1223 |
shows "(g has_derivative g') (at (f x))" |
53781 | 1224 |
proof - |
1225 |
{ |
|
1226 |
fix y |
|
1227 |
assume "y \<in> interior (f ` s)" |
|
1228 |
then obtain x where "x \<in> s" and *: "y = f x" |
|
1229 |
unfolding image_iff |
|
1230 |
using interior_subset |
|
1231 |
by auto |
|
1232 |
have "f (g y) = y" |
|
1233 |
unfolding * and assms(5)[rule_format,OF `x\<in>s`] .. |
|
44123 | 1234 |
} note * = this |
1235 |
show ?thesis |
|
53781 | 1236 |
apply (rule has_derivative_inverse_basic_x[OF assms(6-8)]) |
1237 |
apply (rule continuous_on_interior[OF _ assms(3)]) |
|
1238 |
apply (rule continuous_on_inv[OF assms(4,1)]) |
|
1239 |
apply (rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+ |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
1240 |
apply (metis *) |
53781 | 1241 |
done |
44123 | 1242 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1243 |
|
53781 | 1244 |
|
1245 |
subsection {* Proving surjectivity via Brouwer fixpoint theorem *} |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1246 |
|
44123 | 1247 |
lemma brouwer_surjective: |
56117
2dbf84ee3deb
remove ordered_euclidean_space constraint from brouwer/derivative lemmas;
huffman
parents:
55970
diff
changeset
|
1248 |
fixes f :: "'n::euclidean_space \<Rightarrow> 'n" |
53781 | 1249 |
assumes "compact t" |
1250 |
and "convex t" |
|
1251 |
and "t \<noteq> {}" |
|
1252 |
and "continuous_on t f" |
|
1253 |
and "\<forall>x\<in>s. \<forall>y\<in>t. x + (y - f y) \<in> t" |
|
1254 |
and "x \<in> s" |
|
44123 | 1255 |
shows "\<exists>y\<in>t. f y = x" |
53781 | 1256 |
proof - |
1257 |
have *: "\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y" |
|
1258 |
by (auto simp add: algebra_simps) |
|
44123 | 1259 |
show ?thesis |
1260 |
unfolding * |
|
53781 | 1261 |
apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"]) |
1262 |
apply (rule continuous_on_intros assms)+ |
|
1263 |
using assms(4-6) |
|
1264 |
apply auto |
|
1265 |
done |
|
44123 | 1266 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1267 |
|
44123 | 1268 |
lemma brouwer_surjective_cball: |
56117
2dbf84ee3deb
remove ordered_euclidean_space constraint from brouwer/derivative lemmas;
huffman
parents:
55970
diff
changeset
|
1269 |
fixes f :: "'n::euclidean_space \<Rightarrow> 'n" |
53781 | 1270 |
assumes "e > 0" |
1271 |
and "continuous_on (cball a e) f" |
|
1272 |
and "\<forall>x\<in>s. \<forall>y\<in>cball a e. x + (y - f y) \<in> cball a e" |
|
1273 |
and "x \<in> s" |
|
44123 | 1274 |
shows "\<exists>y\<in>cball a e. f y = x" |
53781 | 1275 |
apply (rule brouwer_surjective) |
1276 |
apply (rule compact_cball convex_cball)+ |
|
1277 |
unfolding cball_eq_empty |
|
1278 |
using assms |
|
1279 |
apply auto |
|
1280 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1281 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1282 |
text {* See Sussmann: "Multidifferential calculus", Theorem 2.1.1 *} |
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1283 |
|
44123 | 1284 |
lemma sussmann_open_mapping: |
56117
2dbf84ee3deb
remove ordered_euclidean_space constraint from brouwer/derivative lemmas;
huffman
parents:
55970
diff
changeset
|
1285 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
53781 | 1286 |
assumes "open s" |
1287 |
and "continuous_on s f" |
|
1288 |
and "x \<in> s" |
|
1289 |
and "(f has_derivative f') (at x)" |
|
1290 |
and "bounded_linear g'" "f' \<circ> g' = id" |
|
1291 |
and "t \<subseteq> s" |
|
1292 |
and "x \<in> interior t" |
|
44123 | 1293 |
shows "f x \<in> interior (f ` t)" |
53781 | 1294 |
proof - |
1295 |
interpret f': bounded_linear f' |
|
1296 |
using assms |
|
1297 |
unfolding has_derivative_def |
|
1298 |
by auto |
|
1299 |
interpret g': bounded_linear g' |
|
1300 |
using assms |
|
1301 |
by auto |
|
55665 | 1302 |
obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B" |
1303 |
using bounded_linear.pos_bounded[OF assms(5)] by blast |
|
53781 | 1304 |
then have *: "1 / (2 * B) > 0" |
1305 |
by (auto intro!: divide_pos_pos) |
|
55665 | 1306 |
obtain e0 where e0: |
1307 |
"0 < e0" |
|
1308 |
"\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)" |
|
1309 |
using assms(4) |
|
1310 |
unfolding has_derivative_at_alt |
|
1311 |
using * by blast |
|
1312 |
obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> t" |
|
1313 |
using assms(8) |
|
1314 |
unfolding mem_interior_cball |
|
1315 |
by blast |
|
53781 | 1316 |
have *: "0 < e0 / B" "0 < e1 / B" |
1317 |
apply (rule_tac[!] divide_pos_pos) |
|
1318 |
using e0 e1 B |
|
1319 |
apply auto |
|
1320 |
done |
|
55665 | 1321 |
obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B" |
1322 |
using real_lbound_gt_zero[OF *] by blast |
|
53781 | 1323 |
have "\<forall>z\<in>cball (f x) (e / 2). \<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z" |
1324 |
apply rule |
|
1325 |
apply (rule brouwer_surjective_cball[where s="cball (f x) (e/2)"]) |
|
1326 |
prefer 3 |
|
1327 |
apply rule |
|
1328 |
apply rule |
|
44123 | 1329 |
proof- |
1330 |
show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))" |
|
1331 |
unfolding g'.diff |
|
53781 | 1332 |
apply (rule continuous_on_compose[of _ _ f, unfolded o_def]) |
1333 |
apply (rule continuous_on_intros linear_continuous_on[OF assms(5)])+ |
|
1334 |
apply (rule continuous_on_subset[OF assms(2)]) |
|
1335 |
apply rule |
|
1336 |
apply (unfold image_iff) |
|
1337 |
apply (erule bexE) |
|
44123 | 1338 |
proof- |
53781 | 1339 |
fix y z |
1340 |
assume as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))" |
|
44123 | 1341 |
have "dist x z = norm (g' (f x) - g' y)" |
1342 |
unfolding as(2) and dist_norm by auto |
|
1343 |
also have "\<dots> \<le> norm (f x - y) * B" |
|
53781 | 1344 |
unfolding g'.diff[symmetric] |
1345 |
using B |
|
1346 |
by auto |
|
44123 | 1347 |
also have "\<dots> \<le> e * B" |
53781 | 1348 |
using as(1)[unfolded mem_cball dist_norm] |
1349 |
using B |
|
1350 |
by auto |
|
1351 |
also have "\<dots> \<le> e1" |
|
1352 |
using e |
|
1353 |
unfolding less_divide_eq |
|
1354 |
using B |
|
1355 |
by auto |
|
1356 |
finally have "z \<in> cball x e1" |
|
1357 |
unfolding mem_cball |
|
1358 |
by force |
|
1359 |
then show "z \<in> s" |
|
1360 |
using e1 assms(7) by auto |
|
44123 | 1361 |
qed |
1362 |
next |
|
53781 | 1363 |
fix y z |
1364 |
assume as: "y \<in> cball (f x) (e / 2)" "z \<in> cball (f x) e" |
|
1365 |
have "norm (g' (z - f x)) \<le> norm (z - f x) * B" |
|
1366 |
using B by auto |
|
1367 |
also have "\<dots> \<le> e * B" |
|
1368 |
apply (rule mult_right_mono) |
|
44123 | 1369 |
using as(2)[unfolded mem_cball dist_norm] and B |
53781 | 1370 |
unfolding norm_minus_commute |
1371 |
apply auto |
|
1372 |
done |
|
1373 |
also have "\<dots> < e0" |
|
1374 |
using e and B |
|
1375 |
unfolding less_divide_eq |
|
1376 |
by auto |
|
1377 |
finally have *: "norm (x + g' (z - f x) - x) < e0" |
|
1378 |
by auto |
|
1379 |
have **: "f x + f' (x + g' (z - f x) - x) = z" |
|
1380 |
using assms(6)[unfolded o_def id_def,THEN cong] |
|
1381 |
by auto |
|
1382 |
have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le> |
|
1383 |
norm (f (x + g' (z - f x)) - z) + norm (f x - y)" |
|
44123 | 1384 |
using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"] |
1385 |
by (auto simp add: algebra_simps) |
|
1386 |
also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)" |
|
55665 | 1387 |
using e0(2)[rule_format, OF *] |
53781 | 1388 |
unfolding algebra_simps ** |
1389 |
by auto |
|
44123 | 1390 |
also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2" |
53781 | 1391 |
using as(1)[unfolded mem_cball dist_norm] |
1392 |
by auto |
|
44123 | 1393 |
also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2" |
53781 | 1394 |
using * and B |
1395 |
by (auto simp add: field_simps) |
|
1396 |
also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2" |
|
1397 |
by auto |
|
1398 |
also have "\<dots> \<le> e/2 + e/2" |
|
1399 |
apply (rule add_right_mono) |
|
44123 | 1400 |
using as(2)[unfolded mem_cball dist_norm] |
53781 | 1401 |
unfolding norm_minus_commute |
1402 |
apply auto |
|
1403 |
done |
|
44123 | 1404 |
finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e" |
53781 | 1405 |
unfolding mem_cball dist_norm |
1406 |
by auto |
|
1407 |
qed (insert e, auto) note lem = this |
|
1408 |
show ?thesis |
|
1409 |
unfolding mem_interior |
|
1410 |
apply (rule_tac x="e/2" in exI) |
|
1411 |
apply rule |
|
1412 |
apply (rule divide_pos_pos) |
|
1413 |
prefer 3 |
|
44123 | 1414 |
proof |
53781 | 1415 |
fix y |
1416 |
assume "y \<in> ball (f x) (e / 2)" |
|
1417 |
then have *: "y \<in> cball (f x) (e / 2)" |
|
1418 |
by auto |
|
55665 | 1419 |
obtain z where z: "z \<in> cball (f x) e" "f (x + g' (z - f x)) = y" |
1420 |
using lem * by blast |
|
53781 | 1421 |
then have "norm (g' (z - f x)) \<le> norm (z - f x) * B" |
1422 |
using B |
|
1423 |
by (auto simp add: field_simps) |
|
44123 | 1424 |
also have "\<dots> \<le> e * B" |
53781 | 1425 |
apply (rule mult_right_mono) |
1426 |
using z(1) |
|
1427 |
unfolding mem_cball dist_norm norm_minus_commute |
|
1428 |
using B |
|
1429 |
apply auto |
|
1430 |
done |
|
1431 |
also have "\<dots> \<le> e1" |
|
1432 |
using e B unfolding less_divide_eq by auto |
|
1433 |
finally have "x + g'(z - f x) \<in> t" |
|
1434 |
apply - |
|
55665 | 1435 |
apply (rule e1(2)[unfolded subset_eq,rule_format]) |
53781 | 1436 |
unfolding mem_cball dist_norm |
1437 |
apply auto |
|
1438 |
done |
|
1439 |
then show "y \<in> f ` t" |
|
1440 |
using z by auto |
|
1441 |
qed (insert e, auto) |
|
44123 | 1442 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1443 |
|
53799 | 1444 |
text {* Hence the following eccentric variant of the inverse function theorem. |
1445 |
This has no continuity assumptions, but we do need the inverse function. |
|
1446 |
We could put @{text "f' \<circ> g = I"} but this happens to fit with the minimal linear |
|
1447 |
algebra theory I've set up so far. *} |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1448 |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
1449 |
(* move before left_inverse_linear in Euclidean_Space*) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
1450 |
|
53781 | 1451 |
lemma right_inverse_linear: |
1452 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'a" |
|
1453 |
assumes lf: "linear f" |
|
1454 |
and gf: "f \<circ> g = id" |
|
1455 |
shows "linear g" |
|
1456 |
proof - |
|
1457 |
from gf have fi: "surj f" |
|
1458 |
by (auto simp add: surj_def o_def id_def) metis |
|
1459 |
from linear_surjective_isomorphism[OF lf fi] |
|
1460 |
obtain h:: "'a \<Rightarrow> 'a" where h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x" |
|
1461 |
by blast |
|
1462 |
have "h = g" |
|
1463 |
apply (rule ext) |
|
1464 |
using gf h(2,3) |
|
1465 |
apply (simp add: o_def id_def fun_eq_iff) |
|
1466 |
apply metis |
|
1467 |
done |
|
1468 |
with h(1) show ?thesis by blast |
|
1469 |
qed |
|
1470 |
||
44123 | 1471 |
lemma has_derivative_inverse_strong: |
56117
2dbf84ee3deb
remove ordered_euclidean_space constraint from brouwer/derivative lemmas;
huffman
parents:
55970
diff
changeset
|
1472 |
fixes f :: "'n::euclidean_space \<Rightarrow> 'n" |
53781 | 1473 |
assumes "open s" |
1474 |
and "x \<in> s" |
|
1475 |
and "continuous_on s f" |
|
1476 |
and "\<forall>x\<in>s. g (f x) = x" |
|
1477 |
and "(f has_derivative f') (at x)" |
|
1478 |
and "f' \<circ> g' = id" |
|
44123 | 1479 |
shows "(g has_derivative g') (at (f x))" |
53781 | 1480 |
proof - |
1481 |
have linf: "bounded_linear f'" |
|
44123 | 1482 |
using assms(5) unfolding has_derivative_def by auto |
53781 | 1483 |
then have ling: "bounded_linear g'" |
1484 |
unfolding linear_conv_bounded_linear[symmetric] |
|
1485 |
apply - |
|
1486 |
apply (rule right_inverse_linear) |
|
1487 |
using assms(6) |
|
1488 |
apply auto |
|
1489 |
done |
|
1490 |
moreover have "g' \<circ> f' = id" |
|
1491 |
using assms(6) linf ling |
|
1492 |
unfolding linear_conv_bounded_linear[symmetric] |
|
1493 |
using linear_inverse_left |
|
1494 |
by auto |
|
1495 |
moreover have *:"\<forall>t\<subseteq>s. x \<in> interior t \<longrightarrow> f x \<in> interior (f ` t)" |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
1496 |
apply clarify |
53781 | 1497 |
apply (rule sussmann_open_mapping) |
1498 |
apply (rule assms ling)+ |
|
1499 |
apply auto |
|
1500 |
done |
|
1501 |
have "continuous (at (f x)) g" |
|
1502 |
unfolding continuous_at Lim_at |
|
1503 |
proof (rule, rule) |
|
1504 |
fix e :: real |
|
1505 |
assume "e > 0" |
|
1506 |
then have "f x \<in> interior (f ` (ball x e \<inter> s))" |
|
1507 |
using *[rule_format,of "ball x e \<inter> s"] `x \<in> s` |
|
1508 |
by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)]) |
|
55665 | 1509 |
then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> s)" |
1510 |
unfolding mem_interior by blast |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1511 |
show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e" |
53781 | 1512 |
apply (rule_tac x=d in exI) |
1513 |
apply rule |
|
55665 | 1514 |
apply (rule d(1)) |
53781 | 1515 |
apply rule |
1516 |
apply rule |
|
1517 |
proof - |
|
1518 |
case goal1 |
|
1519 |
then have "g y \<in> g ` f ` (ball x e \<inter> s)" |
|
55665 | 1520 |
using d(2)[unfolded subset_eq,THEN bspec[where x=y]] |
53781 | 1521 |
by (auto simp add: dist_commute) |
1522 |
then have "g y \<in> ball x e \<inter> s" |
|
1523 |
using assms(4) by auto |
|
1524 |
then show "dist (g y) (g (f x)) < e" |
|
1525 |
using assms(4)[rule_format,OF `x \<in> s`] |
|
44123 | 1526 |
by (auto simp add: dist_commute) |
1527 |
qed |
|
1528 |
qed |
|
1529 |
moreover have "f x \<in> interior (f ` s)" |
|
53781 | 1530 |
apply (rule sussmann_open_mapping) |
1531 |
apply (rule assms ling)+ |
|
1532 |
using interior_open[OF assms(1)] and `x \<in> s` |
|
1533 |
apply auto |
|
1534 |
done |
|
44123 | 1535 |
moreover have "\<And>y. y \<in> interior (f ` s) \<Longrightarrow> f (g y) = y" |
53781 | 1536 |
proof - |
1537 |
case goal1 |
|
1538 |
then have "y \<in> f ` s" |
|
1539 |
using interior_subset by auto |
|
55665 | 1540 |
then obtain z where "z \<in> s" "y = f z" unfolding image_iff .. |
53781 | 1541 |
then show ?case |
1542 |
using assms(4) by auto |
|
44123 | 1543 |
qed |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
1544 |
ultimately show ?thesis using assms |
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
1545 |
by (metis has_derivative_inverse_basic_x open_interior) |
44123 | 1546 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1547 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
1548 |
text {* A rewrite based on the other domain. *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1549 |
|
44123 | 1550 |
lemma has_derivative_inverse_strong_x: |
56117
2dbf84ee3deb
remove ordered_euclidean_space constraint from brouwer/derivative lemmas;
huffman
parents:
55970
diff
changeset
|
1551 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'a" |
53781 | 1552 |
assumes "open s" |
1553 |
and "g y \<in> s" |
|
1554 |
and "continuous_on s f" |
|
1555 |
and "\<forall>x\<in>s. g (f x) = x" |
|
1556 |
and "(f has_derivative f') (at (g y))" |
|
1557 |
and "f' \<circ> g' = id" |
|
1558 |
and "f (g y) = y" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1559 |
shows "(g has_derivative g') (at y)" |
53781 | 1560 |
using has_derivative_inverse_strong[OF assms(1-6)] |
1561 |
unfolding assms(7) |
|
1562 |
by simp |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1563 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
1564 |
text {* On a region. *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1565 |
|
44123 | 1566 |
lemma has_derivative_inverse_on: |
56117
2dbf84ee3deb
remove ordered_euclidean_space constraint from brouwer/derivative lemmas;
huffman
parents:
55970
diff
changeset
|
1567 |
fixes f :: "'n::euclidean_space \<Rightarrow> 'n" |
53781 | 1568 |
assumes "open s" |
1569 |
and "\<forall>x\<in>s. (f has_derivative f'(x)) (at x)" |
|
1570 |
and "\<forall>x\<in>s. g (f x) = x" |
|
1571 |
and "f' x \<circ> g' x = id" |
|
1572 |
and "x \<in> s" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1573 |
shows "(g has_derivative g'(x)) (at (f x))" |
53781 | 1574 |
apply (rule has_derivative_inverse_strong[where g'="g' x" and f=f]) |
1575 |
apply (rule assms)+ |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1576 |
unfolding continuous_on_eq_continuous_at[OF assms(1)] |
53781 | 1577 |
apply rule |
1578 |
apply (rule differentiable_imp_continuous_within) |
|
1579 |
unfolding differentiable_def |
|
1580 |
using assms |
|
1581 |
apply auto |
|
1582 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1583 |
|
44123 | 1584 |
text {* Invertible derivative continous at a point implies local |
1585 |
injectivity. It's only for this we need continuity of the derivative, |
|
1586 |
except of course if we want the fact that the inverse derivative is |
|
1587 |
also continuous. So if we know for some other reason that the inverse |
|
1588 |
function exists, it's OK. *} |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1589 |
|
53781 | 1590 |
lemma bounded_linear_sub: "bounded_linear f \<Longrightarrow> bounded_linear g \<Longrightarrow> bounded_linear (\<lambda>x. f x - g x)" |
44123 | 1591 |
using bounded_linear_add[of f "\<lambda>x. - g x"] bounded_linear_minus[of g] |
1592 |
by (auto simp add: algebra_simps) |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1593 |
|
44123 | 1594 |
lemma has_derivative_locally_injective: |
53781 | 1595 |
fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space" |
1596 |
assumes "a \<in> s" |
|
1597 |
and "open s" |
|
1598 |
and "bounded_linear g'" |
|
1599 |
and "g' \<circ> f' a = id" |
|
1600 |
and "\<forall>x\<in>s. (f has_derivative f' x) (at x)" |
|
1601 |
and "\<forall>e>0. \<exists>d>0. \<forall>x. dist a x < d \<longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < e" |
|
1602 |
obtains t where "a \<in> t" "open t" "\<forall>x\<in>t. \<forall>x'\<in>t. f x' = f x \<longrightarrow> x' = x" |
|
1603 |
proof - |
|
1604 |
interpret bounded_linear g' |
|
1605 |
using assms by auto |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1606 |
note f'g' = assms(4)[unfolded id_def o_def,THEN cong] |
53781 | 1607 |
have "g' (f' a (\<Sum>Basis)) = (\<Sum>Basis)" "(\<Sum>Basis) \<noteq> (0::'n)" |
1608 |
defer |
|
1609 |
apply (subst euclidean_eq_iff) |
|
1610 |
using f'g' |
|
1611 |
apply auto |
|
1612 |
done |
|
1613 |
then have *: "0 < onorm g'" |
|
1614 |
unfolding onorm_pos_lt[OF assms(3)[unfolded linear_linear]] |
|
1615 |
by fastforce |
|
1616 |
def k \<equiv> "1 / onorm g' / 2" |
|
1617 |
have *: "k > 0" |
|
1618 |
unfolding k_def using * by auto |
|
55665 | 1619 |
obtain d1 where d1: |
1620 |
"0 < d1" |
|
1621 |
"\<And>x. dist a x < d1 \<Longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < k" |
|
1622 |
using assms(6) * by blast |
|
53781 | 1623 |
from `open s` obtain d2 where "d2 > 0" "ball a d2 \<subseteq> s" |
1624 |
using `a\<in>s` .. |
|
1625 |
obtain d2 where "d2 > 0" "ball a d2 \<subseteq> s" |
|
1626 |
using assms(2,1) .. |
|
55665 | 1627 |
obtain d2 where d2: "0 < d2" "ball a d2 \<subseteq> s" |
1628 |
using assms(2) |
|
1629 |
unfolding open_contains_ball |
|
1630 |
using `a\<in>s` by blast |
|
1631 |
obtain d where d: "0 < d" "d < d1" "d < d2" |
|
1632 |
using real_lbound_gt_zero[OF d1(1) d2(1)] by blast |
|
44123 | 1633 |
show ?thesis |
1634 |
proof |
|
53781 | 1635 |
show "a \<in> ball a d" |
1636 |
using d by auto |
|
44123 | 1637 |
show "\<forall>x\<in>ball a d. \<forall>x'\<in>ball a d. f x' = f x \<longrightarrow> x' = x" |
1638 |
proof (intro strip) |
|
53781 | 1639 |
fix x y |
1640 |
assume as: "x \<in> ball a d" "y \<in> ball a d" "f x = f y" |
|
1641 |
def ph \<equiv> "\<lambda>w. w - g' (f w - f x)" |
|
44123 | 1642 |
have ph':"ph = g' \<circ> (\<lambda>w. f' a w - (f w - f x))" |
53781 | 1643 |
unfolding ph_def o_def |
1644 |
unfolding diff |
|
1645 |
using f'g' |
|
44123 | 1646 |
by (auto simp add: algebra_simps) |
53781 | 1647 |
have "norm (ph x - ph y) \<le> (1 / 2) * norm (x - y)" |
1648 |
apply (rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\<lambda>x v. v - g'(f' x v)"]) |
|
1649 |
apply (rule_tac[!] ballI) |
|
1650 |
proof - |
|
1651 |
fix u |
|
1652 |
assume u: "u \<in> ball a d" |
|
1653 |
then have "u \<in> s" |
|
1654 |
using d d2 by auto |
|
1655 |
have *: "(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)" |
|
1656 |
unfolding o_def and diff |
|
1657 |
using f'g' by auto |
|
41958 | 1658 |
show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
1659 |
unfolding ph' * |
53781 | 1660 |
apply (simp add: comp_def) |
1661 |
apply (rule bounded_linear.FDERIV[OF assms(3)]) |
|
1662 |
apply (rule FDERIV_intros) |
|
1663 |
defer |
|
1664 |
apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right]) |
|
1665 |
apply (rule has_derivative_at_within) |
|
1666 |
using assms(5) and `u \<in> s` `a \<in> s` |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
1667 |
apply (auto intro!: FDERIV_intros bounded_linear.FDERIV[of _ "\<lambda>x. x"] derivative_linear) |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
1668 |
done |
53781 | 1669 |
have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)" |
1670 |
apply (rule_tac[!] bounded_linear_sub) |
|
1671 |
apply (rule_tac[!] derivative_linear) |
|
1672 |
using assms(5) `u \<in> s` `a \<in> s` |
|
1673 |
apply auto |
|
1674 |
done |
|
44123 | 1675 |
have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)" |
53781 | 1676 |
unfolding * |
1677 |
apply (rule onorm_compose) |
|
1678 |
unfolding linear_conv_bounded_linear |
|
1679 |
apply (rule assms(3) **)+ |
|
1680 |
done |
|
44123 | 1681 |
also have "\<dots> \<le> onorm g' * k" |
53781 | 1682 |
apply (rule mult_left_mono) |
55665 | 1683 |
using d1(2)[of u] |
44123 | 1684 |
using onorm_neg[OF **(1)[unfolded linear_linear]] |
1685 |
using d and u and onorm_pos_le[OF assms(3)[unfolded linear_linear]] |
|
53781 | 1686 |
apply (auto simp add: algebra_simps) |
1687 |
done |
|
1688 |
also have "\<dots> \<le> 1 / 2" |
|
1689 |
unfolding k_def by auto |
|
1690 |
finally show "onorm (\<lambda>v. v - g' (f' u v)) \<le> 1 / 2" . |
|
44123 | 1691 |
qed |
1692 |
moreover have "norm (ph y - ph x) = norm (y - x)" |
|
53781 | 1693 |
apply (rule arg_cong[where f=norm]) |
1694 |
unfolding ph_def |
|
1695 |
using diff |
|
1696 |
unfolding as |
|
1697 |
apply auto |
|
1698 |
done |
|
1699 |
ultimately show "x = y" |
|
1700 |
unfolding norm_minus_commute by auto |
|
44123 | 1701 |
qed |
1702 |
qed auto |
|
1703 |
qed |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1704 |
|
53781 | 1705 |
|
1706 |
subsection {* Uniformly convergent sequence of derivatives *} |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1707 |
|
44123 | 1708 |
lemma has_derivative_sequence_lipschitz_lemma: |
53781 | 1709 |
fixes f :: "nat \<Rightarrow> 'm::euclidean_space \<Rightarrow> 'n::euclidean_space" |
44123 | 1710 |
assumes "convex s" |
53781 | 1711 |
and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)" |
1712 |
and "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h" |
|
1713 |
shows "\<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm ((f m x - f n x) - (f m y - f n y)) \<le> 2 * e * norm (x - y)" |
|
1714 |
proof rule+ |
|
1715 |
fix m n x y |
|
1716 |
assume as: "N \<le> m" "N \<le> n" "x \<in> s" "y \<in> s" |
|
1717 |
show "norm ((f m x - f n x) - (f m y - f n y)) \<le> 2 * e * norm (x - y)" |
|
1718 |
apply (rule differentiable_bound[where f'="\<lambda>x h. f' m x h - f' n x h", OF assms(1) _ _ as(3-4)]) |
|
1719 |
apply (rule_tac[!] ballI) |
|
1720 |
proof - |
|
1721 |
fix x |
|
1722 |
assume "x \<in> s" |
|
44123 | 1723 |
show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within s)" |
53781 | 1724 |
by (rule FDERIV_intros assms(2)[rule_format] `x\<in>s`)+ |
1725 |
{ |
|
1726 |
fix h |
|
44123 | 1727 |
have "norm (f' m x h - f' n x h) \<le> norm (f' m x h - g' x h) + norm (f' n x h - g' x h)" |
1728 |
using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"] |
|
53781 | 1729 |
unfolding norm_minus_commute |
1730 |
by (auto simp add: algebra_simps) |
|
1731 |
also have "\<dots> \<le> e * norm h + e * norm h" |
|
1732 |
using assms(3)[rule_format,OF `N \<le> m` `x \<in> s`, of h] |
|
1733 |
using assms(3)[rule_format,OF `N \<le> n` `x \<in> s`, of h] |
|
1734 |
by (auto simp add: field_simps) |
|
1735 |
finally have "norm (f' m x h - f' n x h) \<le> 2 * e * norm h" |
|
1736 |
by auto |
|
1737 |
} |
|
1738 |
then show "onorm (\<lambda>h. f' m x h - f' n x h) \<le> 2 * e" |
|
1739 |
apply - |
|
1740 |
apply (rule onorm(2)) |
|
1741 |
apply (rule linear_compose_sub) |
|
44123 | 1742 |
unfolding linear_conv_bounded_linear |
53781 | 1743 |
using assms(2)[rule_format,OF `x \<in> s`, THEN derivative_linear] |
1744 |
apply auto |
|
1745 |
done |
|
44123 | 1746 |
qed |
1747 |
qed |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1748 |
|
44123 | 1749 |
lemma has_derivative_sequence_lipschitz: |
53781 | 1750 |
fixes f :: "nat \<Rightarrow> 'm::euclidean_space \<Rightarrow> 'n::euclidean_space" |
44123 | 1751 |
assumes "convex s" |
53781 | 1752 |
and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)" |
1753 |
and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h" |
|
1754 |
and "e > 0" |
|
1755 |
shows "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. |
|
1756 |
norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)" |
|
1757 |
proof (rule, rule) |
|
1758 |
case goal1 have *: "2 * (1/2* e) = e" "1/2 * e >0" |
|
1759 |
using `e > 0` by auto |
|
55665 | 1760 |
obtain N where "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> 1 / 2 * e * norm h" |
1761 |
using assms(3) *(2) by blast |
|
53781 | 1762 |
then show ?case |
1763 |
apply (rule_tac x=N in exI) |
|
1764 |
apply (rule has_derivative_sequence_lipschitz_lemma[where e="1/2 *e", unfolded *]) |
|
1765 |
using assms |
|
1766 |
apply auto |
|
1767 |
done |
|
44123 | 1768 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1769 |
|
44123 | 1770 |
lemma has_derivative_sequence: |
1771 |
fixes f::"nat\<Rightarrow> 'm::euclidean_space \<Rightarrow> 'n::euclidean_space" |
|
1772 |
assumes "convex s" |
|
53781 | 1773 |
and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)" |
1774 |
and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h" |
|
1775 |
and "x0 \<in> s" |
|
1776 |
and "((\<lambda>n. f n x0) ---> l) sequentially" |
|
1777 |
shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) ---> g x) sequentially \<and> (g has_derivative g'(x)) (at x within s)" |
|
1778 |
proof - |
|
1779 |
have lem1: "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. |
|
1780 |
norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)" |
|
1781 |
apply (rule has_derivative_sequence_lipschitz[where e="42::nat"]) |
|
1782 |
apply (rule assms)+ |
|
1783 |
apply auto |
|
1784 |
done |
|
44123 | 1785 |
have "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) ---> g x) sequentially" |
53781 | 1786 |
apply (rule bchoice) |
1787 |
unfolding convergent_eq_cauchy |
|
44123 | 1788 |
proof |
53781 | 1789 |
fix x |
1790 |
assume "x \<in> s" |
|
1791 |
show "Cauchy (\<lambda>n. f n x)" |
|
1792 |
proof (cases "x = x0") |
|
1793 |
case True |
|
1794 |
then show ?thesis |
|
1795 |
using LIMSEQ_imp_Cauchy[OF assms(5)] by auto |
|
44123 | 1796 |
next |
53781 | 1797 |
case False |
1798 |
show ?thesis |
|
1799 |
unfolding Cauchy_def |
|
1800 |
proof (rule, rule) |
|
1801 |
fix e :: real |
|
1802 |
assume "e > 0" |
|
1803 |
then have *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0" |
|
44123 | 1804 |
using False by (auto intro!: divide_pos_pos) |
55665 | 1805 |
obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x0) (f n x0) < e / 2" |
1806 |
using LIMSEQ_imp_Cauchy[OF assms(5)] |
|
1807 |
unfolding Cauchy_def |
|
1808 |
using *(1) by blast |
|
1809 |
obtain N where N: |
|
1810 |
"\<forall>m\<ge>N. \<forall>n\<ge>N. |
|
1811 |
\<forall>xa\<in>s. \<forall>y\<in>s. norm (f m xa - f n xa - (f m y - f n y)) \<le> |
|
1812 |
e / 2 / norm (x - x0) * norm (xa - y)" |
|
1813 |
using lem1 *(2) by blast |
|
44123 | 1814 |
show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" |
53781 | 1815 |
apply (rule_tac x="max M N" in exI) |
1816 |
proof rule+ |
|
1817 |
fix m n |
|
1818 |
assume as: "max M N \<le>m" "max M N\<le>n" |
|
1819 |
have "dist (f m x) (f n x) \<le> |
|
1820 |
norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))" |
|
1821 |
unfolding dist_norm |
|
1822 |
by (rule norm_triangle_sub) |
|
44123 | 1823 |
also have "\<dots> \<le> norm (f m x0 - f n x0) + e / 2" |
1824 |
using N[rule_format,OF _ _ `x\<in>s` `x0\<in>s`, of m n] and as and False |
|
1825 |
by auto |
|
1826 |
also have "\<dots> < e / 2 + e / 2" |
|
53781 | 1827 |
apply (rule add_strict_right_mono) |
1828 |
using as and M[rule_format] |
|
1829 |
unfolding dist_norm |
|
1830 |
apply auto |
|
1831 |
done |
|
1832 |
finally show "dist (f m x) (f n x) < e" |
|
1833 |
by auto |
|
44123 | 1834 |
qed |
1835 |
qed |
|
1836 |
qed |
|
1837 |
qed |
|
55665 | 1838 |
then obtain g where g: "\<forall>x\<in>s. (\<lambda>n. f n x) ----> g x" .. |
53781 | 1839 |
have lem2: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm ((f n x - f n y) - (g x - g y)) \<le> e * norm (x - y)" |
1840 |
proof (rule, rule) |
|
1841 |
fix e :: real |
|
1842 |
assume *: "e > 0" |
|
55665 | 1843 |
obtain N where |
1844 |
N: "\<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)" |
|
1845 |
using lem1 * by blast |
|
44123 | 1846 |
show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)" |
53781 | 1847 |
apply (rule_tac x=N in exI) |
1848 |
proof rule+ |
|
1849 |
fix n x y |
|
1850 |
assume as: "N \<le> n" "x \<in> s" "y \<in> s" |
|
44123 | 1851 |
have "eventually (\<lambda>xa. norm (f n x - f n y - (f xa x - f xa y)) \<le> e * norm (x - y)) sequentially" |
1852 |
unfolding eventually_sequentially |
|
53781 | 1853 |
apply (rule_tac x=N in exI) |
1854 |
apply rule |
|
1855 |
apply rule |
|
1856 |
proof - |
|
1857 |
fix m |
|
1858 |
assume "N \<le> m" |
|
1859 |
then show "norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)" |
|
44123 | 1860 |
using N[rule_format, of n m x y] and as |
1861 |
by (auto simp add: algebra_simps) |
|
1862 |
qed |
|
53781 | 1863 |
then show "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)" |
1864 |
apply - |
|
1865 |
apply (rule Lim_norm_ubound[OF trivial_limit_sequentially, where f="\<lambda>m. (f n x - f n y) - (f m x - f m y)"]) |
|
1866 |
apply (rule tendsto_intros g[rule_format] as)+ |
|
1867 |
apply assumption |
|
1868 |
done |
|
44123 | 1869 |
qed |
1870 |
qed |
|
53781 | 1871 |
show ?thesis |
1872 |
unfolding has_derivative_within_alt |
|
1873 |
apply (rule_tac x=g in exI) |
|
1874 |
apply rule |
|
1875 |
apply rule |
|
1876 |
apply (rule g[rule_format]) |
|
1877 |
apply assumption |
|
1878 |
proof |
|
1879 |
fix x |
|
1880 |
assume "x \<in> s" |
|
1881 |
have lem3: "\<forall>u. ((\<lambda>n. f' n x u) ---> g' x u) sequentially" |
|
44907
93943da0a010
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
huffman
parents:
44890
diff
changeset
|
1882 |
unfolding LIMSEQ_def |
53781 | 1883 |
proof (rule, rule, rule) |
1884 |
fix u |
|
1885 |
fix e :: real |
|
1886 |
assume "e > 0" |
|
44123 | 1887 |
show "\<exists>N. \<forall>n\<ge>N. dist (f' n x u) (g' x u) < e" |
53781 | 1888 |
proof (cases "u = 0") |
1889 |
case True |
|
55665 | 1890 |
obtain N where N: "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h" |
1891 |
using assms(3) `e>0` by blast |
|
53781 | 1892 |
show ?thesis |
1893 |
apply (rule_tac x=N in exI) |
|
1894 |
unfolding True |
|
1895 |
using N[rule_format,OF _ `x\<in>s`,of _ 0] and `e>0` |
|
1896 |
apply auto |
|
1897 |
done |
|
44123 | 1898 |
next |
53781 | 1899 |
case False |
1900 |
then have *: "e / 2 / norm u > 0" |
|
1901 |
using `e > 0` |
|
1902 |
by (auto intro!: divide_pos_pos) |
|
55665 | 1903 |
obtain N where N: "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e / 2 / norm u * norm h" |
1904 |
using assms(3) * by blast |
|
53781 | 1905 |
show ?thesis |
1906 |
apply (rule_tac x=N in exI) |
|
1907 |
apply rule |
|
1908 |
apply rule |
|
1909 |
proof - |
|
1910 |
case goal1 |
|
1911 |
show ?case |
|
1912 |
unfolding dist_norm |
|
44123 | 1913 |
using N[rule_format,OF goal1 `x\<in>s`, of u] False `e>0` |
53781 | 1914 |
by (auto simp add: field_simps) |
44123 | 1915 |
qed |
1916 |
qed |
|
1917 |
qed |
|
1918 |
show "bounded_linear (g' x)" |
|
53600
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53374
diff
changeset
|
1919 |
unfolding linear_linear linear_iff |
53781 | 1920 |
apply rule |
1921 |
apply rule |
|
1922 |
apply rule |
|
1923 |
defer |
|
1924 |
apply rule |
|
1925 |
apply rule |
|
1926 |
proof - |
|
1927 |
fix x' y z :: 'm |
|
1928 |
fix c :: real |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1929 |
note lin = assms(2)[rule_format,OF `x\<in>s`,THEN derivative_linear] |
44123 | 1930 |
show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'" |
53781 | 1931 |
apply (rule tendsto_unique[OF trivial_limit_sequentially]) |
1932 |
apply (rule lem3[rule_format]) |
|
53600
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53374
diff
changeset
|
1933 |
unfolding lin[THEN bounded_linear_imp_linear, THEN linear_cmul] |
53781 | 1934 |
apply (intro tendsto_intros) |
1935 |
apply (rule lem3[rule_format]) |
|
1936 |
done |
|
44123 | 1937 |
show "g' x (y + z) = g' x y + g' x z" |
53781 | 1938 |
apply (rule tendsto_unique[OF trivial_limit_sequentially]) |
1939 |
apply (rule lem3[rule_format]) |
|
53600
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53374
diff
changeset
|
1940 |
unfolding lin[THEN bounded_linear_imp_linear, THEN linear_add] |
53781 | 1941 |
apply (rule tendsto_add) |
1942 |
apply (rule lem3[rule_format])+ |
|
1943 |
done |
|
44123 | 1944 |
qed |
1945 |
show "\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm (y - x) < d \<longrightarrow> norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)" |
|
53781 | 1946 |
proof (rule, rule) |
1947 |
case goal1 |
|
1948 |
have *: "e / 3 > 0" |
|
1949 |
using goal1 by auto |
|
55665 | 1950 |
obtain N1 where N1: "\<forall>n\<ge>N1. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e / 3 * norm h" |
1951 |
using assms(3) * by blast |
|
1952 |
obtain N2 where |
|
1953 |
N2: "\<forall>n\<ge>N2. \<forall>x\<in>s. \<forall>y\<in>s. norm (f n x - f n y - (g x - g y)) \<le> e / 3 * norm (x - y)" |
|
1954 |
using lem2 * by blast |
|
1955 |
obtain d1 where d1: |
|
1956 |
"0 < d1" |
|
1957 |
"\<forall>y\<in>s. norm (y - x) < d1 \<longrightarrow> |
|
1958 |
norm (f (max N1 N2) y - f (max N1 N2) x - f' (max N1 N2) x (y - x)) \<le> |
|
1959 |
e / 3 * norm (y - x)" |
|
1960 |
using assms(2)[unfolded has_derivative_within_alt, rule_format, |
|
1961 |
OF `x\<in>s`, of "max N1 N2", THEN conjunct2, rule_format, OF *] |
|
1962 |
by blast |
|
53781 | 1963 |
show ?case |
1964 |
apply (rule_tac x=d1 in exI) |
|
1965 |
apply rule |
|
55665 | 1966 |
apply (rule d1(1)) |
53781 | 1967 |
apply rule |
1968 |
apply rule |
|
1969 |
proof - |
|
1970 |
fix y |
|
1971 |
assume as: "y \<in> s" "norm (y - x) < d1" |
|
1972 |
let ?N = "max N1 N2" |
|
44123 | 1973 |
have "norm (g y - g x - (f ?N y - f ?N x)) \<le> e /3 * norm (y - x)" |
53781 | 1974 |
apply (subst norm_minus_cancel[symmetric]) |
1975 |
using N2[rule_format, OF _ `y \<in> s` `x \<in> s`, of ?N] |
|
1976 |
apply auto |
|
1977 |
done |
|
44123 | 1978 |
moreover |
1979 |
have "norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)" |
|
53781 | 1980 |
using d1 and as |
1981 |
by auto |
|
44123 | 1982 |
ultimately |
53781 | 1983 |
have "norm (g y - g x - f' ?N x (y - x)) \<le> 2 * e / 3 * norm (y - x)" |
44123 | 1984 |
using norm_triangle_le[of "g y - g x - (f ?N y - f ?N x)" "f ?N y - f ?N x - f' ?N x (y - x)" "2 * e / 3 * norm (y - x)"] |
53781 | 1985 |
by (auto simp add: algebra_simps) |
44123 | 1986 |
moreover |
1987 |
have " norm (f' ?N x (y - x) - g' x (y - x)) \<le> e / 3 * norm (y - x)" |
|
53781 | 1988 |
using N1 `x \<in> s` by auto |
41958 | 1989 |
ultimately show "norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)" |
44123 | 1990 |
using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"] |
53781 | 1991 |
by (auto simp add: algebra_simps) |
44123 | 1992 |
qed |
1993 |
qed |
|
1994 |
qed |
|
1995 |
qed |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1996 |
|
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset
|
1997 |
text {* Can choose to line up antiderivatives if we want. *} |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
1998 |
|
44123 | 1999 |
lemma has_antiderivative_sequence: |
53781 | 2000 |
fixes f :: "nat \<Rightarrow> 'm::euclidean_space \<Rightarrow> 'n::euclidean_space" |
44123 | 2001 |
assumes "convex s" |
53781 | 2002 |
and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)" |
2003 |
and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h" |
|
2004 |
shows "\<exists>g. \<forall>x\<in>s. (g has_derivative g' x) (at x within s)" |
|
2005 |
proof (cases "s = {}") |
|
2006 |
case False |
|
2007 |
then obtain a where "a \<in> s" |
|
2008 |
by auto |
|
2009 |
have *: "\<And>P Q. \<exists>g. \<forall>x\<in>s. P g x \<and> Q g x \<Longrightarrow> \<exists>g. \<forall>x\<in>s. Q g x" |
|
2010 |
by auto |
|
44123 | 2011 |
show ?thesis |
53781 | 2012 |
apply (rule *) |
2013 |
apply (rule has_derivative_sequence[OF assms(1) _ assms(3), of "\<lambda>n x. f n x + (f 0 a - f n a)"]) |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
2014 |
apply (metis assms(2) has_derivative_add_const) |
53781 | 2015 |
apply (rule `a \<in> s`) |
2016 |
apply auto |
|
2017 |
done |
|
44123 | 2018 |
qed auto |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2019 |
|
44123 | 2020 |
lemma has_antiderivative_limit: |
53781 | 2021 |
fixes g' :: "'m::euclidean_space \<Rightarrow> 'm \<Rightarrow> 'n::euclidean_space" |
44123 | 2022 |
assumes "convex s" |
53781 | 2023 |
and "\<forall>e>0. \<exists>f f'. \<forall>x\<in>s. |
2024 |
(f has_derivative (f' x)) (at x within s) \<and> (\<forall>h. norm (f' x h - g' x h) \<le> e * norm h)" |
|
2025 |
shows "\<exists>g. \<forall>x\<in>s. (g has_derivative g' x) (at x within s)" |
|
2026 |
proof - |
|
2027 |
have *: "\<forall>n. \<exists>f f'. \<forall>x\<in>s. |
|
2028 |
(f has_derivative (f' x)) (at x within s) \<and> |
|
2029 |
(\<forall>h. norm(f' x h - g' x h) \<le> inverse (real (Suc n)) * norm h)" |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
2030 |
by (metis assms(2) inverse_positive_iff_positive real_of_nat_Suc_gt_zero) |
55665 | 2031 |
obtain f where |
2032 |
*: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. FDERIV (f x) xa : s :> f' xa \<and> |
|
2033 |
(\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)" |
|
2034 |
using *[THEN choice] .. |
|
2035 |
obtain f' where |
|
2036 |
f: "\<forall>x. \<forall>xa\<in>s. FDERIV (f x) xa : s :> f' x xa \<and> |
|
2037 |
(\<forall>h. norm (f' x xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)" |
|
2038 |
using *[THEN choice] .. |
|
53781 | 2039 |
show ?thesis |
2040 |
apply (rule has_antiderivative_sequence[OF assms(1), of f f']) |
|
2041 |
defer |
|
2042 |
apply rule |
|
2043 |
apply rule |
|
2044 |
proof - |
|
2045 |
fix e :: real |
|
2046 |
assume "e > 0" |
|
55665 | 2047 |
obtain N where N: "inverse (real (Suc N)) < e" |
2048 |
using reals_Archimedean[OF `e>0`] .. |
|
44123 | 2049 |
show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h" |
53781 | 2050 |
apply (rule_tac x=N in exI) |
2051 |
proof rule+ |
|
44123 | 2052 |
case goal1 |
53781 | 2053 |
have *: "inverse (real (Suc n)) \<le> e" |
2054 |
apply (rule order_trans[OF _ N[THEN less_imp_le]]) |
|
2055 |
using goal1(1) |
|
2056 |
apply (auto simp add: field_simps) |
|
2057 |
done |
|
44123 | 2058 |
show ?case |
53781 | 2059 |
using f[rule_format,THEN conjunct2,OF goal1(2), of n, THEN spec[where x=h]] |
2060 |
apply (rule order_trans) |
|
2061 |
using N * |
|
2062 |
apply (cases "h = 0") |
|
2063 |
apply auto |
|
2064 |
done |
|
44123 | 2065 |
qed |
53781 | 2066 |
qed (insert f, auto) |
44123 | 2067 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2068 |
|
53781 | 2069 |
|
2070 |
subsection {* Differentiation of a series *} |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2071 |
|
53781 | 2072 |
definition sums_seq :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> nat set \<Rightarrow> bool" |
2073 |
(infixl "sums'_seq" 12) |
|
2074 |
where "(f sums_seq l) s \<longleftrightarrow> ((\<lambda>n. setsum f (s \<inter> {0..n})) ---> l) sequentially" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2075 |
|
44123 | 2076 |
lemma has_derivative_series: |
53781 | 2077 |
fixes f :: "nat \<Rightarrow> 'm::euclidean_space \<Rightarrow> 'n::euclidean_space" |
44123 | 2078 |
assumes "convex s" |
53781 | 2079 |
and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)" |
2080 |
and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (setsum (\<lambda>i. f' i x h) (k \<inter> {0..n}) - g' x h) \<le> e * norm h" |
|
2081 |
and "x \<in> s" |
|
2082 |
and "((\<lambda>n. f n x) sums_seq l) k" |
|
2083 |
shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) sums_seq (g x)) k \<and> (g has_derivative g' x) (at x within s)" |
|
44123 | 2084 |
unfolding sums_seq_def |
53781 | 2085 |
apply (rule has_derivative_sequence[OF assms(1) _ assms(3)]) |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
2086 |
apply (metis assms(2) has_derivative_setsum) |
53781 | 2087 |
using assms(4-5) |
2088 |
unfolding sums_seq_def |
|
2089 |
apply auto |
|
2090 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2091 |
|
53781 | 2092 |
|
2093 |
text {* Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector. *} |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2094 |
|
53781 | 2095 |
definition has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> real filter \<Rightarrow> bool" |
2096 |
(infixl "has'_vector'_derivative" 12) |
|
2097 |
where "(f has_vector_derivative f') net \<longleftrightarrow> (f has_derivative (\<lambda>x. x *\<^sub>R f')) net" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2098 |
|
53781 | 2099 |
definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)" |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2100 |
|
44123 | 2101 |
lemma vector_derivative_works: |
53781 | 2102 |
fixes f :: "real \<Rightarrow> 'a::real_normed_vector" |
2103 |
shows "f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net" |
|
2104 |
(is "?l = ?r") |
|
44123 | 2105 |
proof |
53781 | 2106 |
assume ?l |
55665 | 2107 |
obtain f' where f': "(f has_derivative f') net" |
2108 |
using `?l` unfolding differentiable_def .. |
|
53781 | 2109 |
then interpret bounded_linear f' |
2110 |
by auto |
|
2111 |
show ?r |
|
2112 |
unfolding vector_derivative_def has_vector_derivative_def |
|
2113 |
apply - |
|
2114 |
apply (rule someI_ex,rule_tac x="f' 1" in exI) |
|
2115 |
using f' |
|
2116 |
unfolding scaleR[symmetric] |
|
2117 |
apply auto |
|
2118 |
done |
|
44123 | 2119 |
next |
53781 | 2120 |
assume ?r |
2121 |
then show ?l |
|
44123 | 2122 |
unfolding vector_derivative_def has_vector_derivative_def differentiable_def |
2123 |
by auto |
|
2124 |
qed |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2125 |
|
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
46898
diff
changeset
|
2126 |
lemma has_vector_derivative_withinI_DERIV: |
53781 | 2127 |
assumes f: "DERIV f x :> y" |
2128 |
shows "(f has_vector_derivative y) (at x within s)" |
|
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
46898
diff
changeset
|
2129 |
unfolding has_vector_derivative_def real_scaleR_def |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
46898
diff
changeset
|
2130 |
apply (rule has_derivative_at_within) |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
46898
diff
changeset
|
2131 |
using DERIV_conv_has_derivative[THEN iffD1, OF f] |
53781 | 2132 |
apply (subst mult_commute) |
2133 |
apply assumption |
|
2134 |
done |
|
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
46898
diff
changeset
|
2135 |
|
37730 | 2136 |
lemma vector_derivative_unique_at: |
2137 |
assumes "(f has_vector_derivative f') (at x)" |
|
53781 | 2138 |
and "(f has_vector_derivative f'') (at x)" |
37730 | 2139 |
shows "f' = f''" |
53781 | 2140 |
proof - |
37730 | 2141 |
have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')" |
2142 |
using assms [unfolded has_vector_derivative_def] |
|
2143 |
by (rule frechet_derivative_unique_at) |
|
53781 | 2144 |
then show ?thesis |
2145 |
unfolding fun_eq_iff by auto |
|
37730 | 2146 |
qed |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2147 |
|
44123 | 2148 |
lemma vector_derivative_unique_within_closed_interval: |
53781 | 2149 |
assumes "a < b" |
2150 |
and "x \<in> {a..b}" |
|
44123 | 2151 |
assumes "(f has_vector_derivative f') (at x within {a..b})" |
2152 |
assumes "(f has_vector_derivative f'') (at x within {a..b})" |
|
2153 |
shows "f' = f''" |
|
53781 | 2154 |
proof - |
2155 |
have *: "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')" |
|
2156 |
apply (rule frechet_derivative_unique_within_closed_interval[of "a" "b"]) |
|
2157 |
using assms(3-)[unfolded has_vector_derivative_def] |
|
2158 |
using assms(1-2) |
|
2159 |
apply auto |
|
2160 |
done |
|
44123 | 2161 |
show ?thesis |
53781 | 2162 |
proof (rule ccontr) |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53077
diff
changeset
|
2163 |
assume **: "f' \<noteq> f''" |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53077
diff
changeset
|
2164 |
with * have "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1" |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53077
diff
changeset
|
2165 |
by (auto simp: fun_eq_iff) |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53077
diff
changeset
|
2166 |
with ** show False |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53077
diff
changeset
|
2167 |
unfolding o_def by auto |
44123 | 2168 |
qed |
2169 |
qed |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2170 |
|
37730 | 2171 |
lemma vector_derivative_at: |
53781 | 2172 |
"(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'" |
2173 |
apply (rule vector_derivative_unique_at) |
|
2174 |
defer |
|
2175 |
apply assumption |
|
2176 |
unfolding vector_derivative_works[symmetric] differentiable_def |
|
2177 |
unfolding has_vector_derivative_def |
|
2178 |
apply auto |
|
2179 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2180 |
|
44123 | 2181 |
lemma vector_derivative_within_closed_interval: |
53781 | 2182 |
assumes "a < b" |
2183 |
and "x \<in> {a..b}" |
|
44123 | 2184 |
assumes "(f has_vector_derivative f') (at x within {a..b})" |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2185 |
shows "vector_derivative f (at x within {a..b}) = f'" |
53781 | 2186 |
apply (rule vector_derivative_unique_within_closed_interval) |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2187 |
using vector_derivative_works[unfolded differentiable_def] |
53781 | 2188 |
using assms |
2189 |
apply (auto simp add:has_vector_derivative_def) |
|
2190 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2191 |
|
53781 | 2192 |
lemma has_vector_derivative_within_subset: |
2193 |
"(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> |
|
2194 |
(f has_vector_derivative f') (at x within t)" |
|
2195 |
unfolding has_vector_derivative_def |
|
2196 |
apply (rule has_derivative_within_subset) |
|
2197 |
apply auto |
|
2198 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2199 |
|
53781 | 2200 |
lemma has_vector_derivative_const: "((\<lambda>x. c) has_vector_derivative 0) net" |
2201 |
unfolding has_vector_derivative_def |
|
2202 |
using has_derivative_const |
|
2203 |
by auto |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2204 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2205 |
lemma has_vector_derivative_id: "((\<lambda>x::real. x) has_vector_derivative 1) net" |
53781 | 2206 |
unfolding has_vector_derivative_def |
2207 |
using has_derivative_id |
|
2208 |
by auto |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2209 |
|
44123 | 2210 |
lemma has_vector_derivative_cmul: |
53781 | 2211 |
"(f has_vector_derivative f') net \<Longrightarrow> |
2212 |
((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net" |
|
44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset
|
2213 |
unfolding has_vector_derivative_def |
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset
|
2214 |
apply (drule scaleR_right_has_derivative) |
53781 | 2215 |
apply (auto simp add: algebra_simps) |
2216 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2217 |
|
44123 | 2218 |
lemma has_vector_derivative_cmul_eq: |
2219 |
assumes "c \<noteq> 0" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2220 |
shows "(((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \<longleftrightarrow> (f has_vector_derivative f') net)" |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
2221 |
apply (rule iffI) |
53781 | 2222 |
apply (drule has_vector_derivative_cmul[where c="1/c"]) |
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset
|
2223 |
apply (rule_tac [2] has_vector_derivative_cmul) |
53781 | 2224 |
using assms |
2225 |
apply auto |
|
2226 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2227 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2228 |
lemma has_vector_derivative_neg: |
53781 | 2229 |
"(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. - f x) has_vector_derivative (- f')) net" |
2230 |
unfolding has_vector_derivative_def |
|
2231 |
apply (drule has_derivative_neg) |
|
2232 |
apply auto |
|
2233 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2234 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2235 |
lemma has_vector_derivative_add: |
44123 | 2236 |
assumes "(f has_vector_derivative f') net" |
53781 | 2237 |
and "(g has_vector_derivative g') net" |
2238 |
shows "((\<lambda>x. f x + g x) has_vector_derivative (f' + g')) net" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2239 |
using has_derivative_add[OF assms[unfolded has_vector_derivative_def]] |
53781 | 2240 |
unfolding has_vector_derivative_def |
2241 |
unfolding scaleR_right_distrib |
|
2242 |
by auto |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2243 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2244 |
lemma has_vector_derivative_sub: |
44123 | 2245 |
assumes "(f has_vector_derivative f') net" |
53781 | 2246 |
and "(g has_vector_derivative g') net" |
2247 |
shows "((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2248 |
using has_derivative_sub[OF assms[unfolded has_vector_derivative_def]] |
53781 | 2249 |
unfolding has_vector_derivative_def scaleR_right_diff_distrib |
2250 |
by auto |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2251 |
|
37650 | 2252 |
lemma has_vector_derivative_bilinear_within: |
44123 | 2253 |
assumes "(f has_vector_derivative f') (at x within s)" |
53781 | 2254 |
and "(g has_vector_derivative g') (at x within s)" |
44123 | 2255 |
assumes "bounded_bilinear h" |
2256 |
shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x within s)" |
|
53781 | 2257 |
proof - |
2258 |
interpret bounded_bilinear h |
|
2259 |
using assms by auto |
|
2260 |
show ?thesis |
|
2261 |
using has_derivative_bilinear_within[OF assms(1-2)[unfolded has_vector_derivative_def], of h] |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset
|
2262 |
unfolding o_def has_vector_derivative_def |
53781 | 2263 |
using assms(3) |
2264 |
unfolding scaleR_right scaleR_left scaleR_right_distrib |
|
44123 | 2265 |
by auto |
2266 |
qed |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2267 |
|
37650 | 2268 |
lemma has_vector_derivative_bilinear_at: |
44123 | 2269 |
assumes "(f has_vector_derivative f') (at x)" |
53781 | 2270 |
and "(g has_vector_derivative g') (at x)" |
44123 | 2271 |
assumes "bounded_bilinear h" |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2272 |
shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)" |
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51478
diff
changeset
|
2273 |
using has_vector_derivative_bilinear_within[OF assms] . |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2274 |
|
44123 | 2275 |
lemma has_vector_derivative_at_within: |
2276 |
"(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)" |
|
2277 |
unfolding has_vector_derivative_def |
|
45031 | 2278 |
by (rule has_derivative_at_within) |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2279 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2280 |
lemma has_vector_derivative_transform_within: |
53781 | 2281 |
assumes "0 < d" |
2282 |
and "x \<in> s" |
|
2283 |
and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'" |
|
44123 | 2284 |
assumes "(f has_vector_derivative f') (at x within s)" |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2285 |
shows "(g has_vector_derivative f') (at x within s)" |
53781 | 2286 |
using assms |
2287 |
unfolding has_vector_derivative_def |
|
44123 | 2288 |
by (rule has_derivative_transform_within) |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2289 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2290 |
lemma has_vector_derivative_transform_at: |
53781 | 2291 |
assumes "0 < d" |
2292 |
and "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'" |
|
2293 |
and "(f has_vector_derivative f') (at x)" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2294 |
shows "(g has_vector_derivative f') (at x)" |
53781 | 2295 |
using assms |
2296 |
unfolding has_vector_derivative_def |
|
44123 | 2297 |
by (rule has_derivative_transform_at) |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2298 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2299 |
lemma has_vector_derivative_transform_within_open: |
53781 | 2300 |
assumes "open s" |
2301 |
and "x \<in> s" |
|
2302 |
and "\<forall>y\<in>s. f y = g y" |
|
2303 |
and "(f has_vector_derivative f') (at x)" |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2304 |
shows "(g has_vector_derivative f') (at x)" |
53781 | 2305 |
using assms |
2306 |
unfolding has_vector_derivative_def |
|
44123 | 2307 |
by (rule has_derivative_transform_within_open) |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2308 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2309 |
lemma vector_diff_chain_at: |
44123 | 2310 |
assumes "(f has_vector_derivative f') (at x)" |
53781 | 2311 |
and "(g has_vector_derivative g') (at (f x))" |
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2312 |
shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x)" |
53781 | 2313 |
using assms(2) |
2314 |
unfolding has_vector_derivative_def |
|
2315 |
apply - |
|
2316 |
apply (drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]]) |
|
2317 |
apply (simp only: o_def real_scaleR_def scaleR_scaleR) |
|
2318 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2319 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2320 |
lemma vector_diff_chain_within: |
44123 | 2321 |
assumes "(f has_vector_derivative f') (at x within s)" |
53781 | 2322 |
and "(g has_vector_derivative g') (at (f x) within f ` s)" |
2323 |
shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x within s)" |
|
2324 |
using assms(2) |
|
2325 |
unfolding has_vector_derivative_def |
|
2326 |
apply - |
|
2327 |
apply (drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]]) |
|
2328 |
apply (simp only: o_def real_scaleR_def scaleR_scaleR) |
|
2329 |
done |
|
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2330 |
|
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff
changeset
|
2331 |
end |