author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46898  1570b30ee040 
child 50418  bd68cf816dd3 
permissions  rwrr 
36350  1 
(* Title: HOL/Multivariate_Analysis/Derivative.thy 
2 
Author: John Harrison 

3 
Translation from HOL Light: Robert Himmelmann, TU Muenchen 

4 
*) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

5 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

6 
header {* Multivariate calculus in Euclidean space. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

7 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
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 HOLlight)
hoelzl
parents:
diff
changeset

10 
begin 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

11 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

12 
(* Because I do not want to type this all the time *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

13 
lemmas linear_linear = linear_conv_bounded_linear[THEN sym] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

14 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

15 
subsection {* Derivatives *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

16 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

17 
text {* The definition is slightly tricky since we make it work over 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

18 
nets of a particular form. This lets us prove theorems generally and use 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

19 
"at a" or "at a within s" for restriction to a set (1sided on R etc.) *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

20 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
43338
diff
changeset

21 
definition has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a filter \<Rightarrow> bool)" 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

22 
(infixl "(has'_derivative)" 12) where 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

23 
"(f has_derivative f') net \<equiv> bounded_linear f' \<and> ((\<lambda>y. (1 / (norm (y  netlimit net))) *\<^sub>R 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

24 
(f y  (f (netlimit net) + f'(y  netlimit net)))) > 0) net" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

25 

44137  26 
lemma derivative_linear[dest]: 
27 
"(f has_derivative f') net \<Longrightarrow> bounded_linear f'" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

28 
unfolding has_derivative_def by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

29 

37730  30 
lemma netlimit_at_vector: 
44137  31 
(* TODO: move *) 
37730  32 
fixes a :: "'a::real_normed_vector" 
33 
shows "netlimit (at a) = a" 

34 
proof (cases "\<exists>x. x \<noteq> a") 

35 
case True then obtain x where x: "x \<noteq> a" .. 

36 
have "\<not> trivial_limit (at a)" 

37 
unfolding trivial_limit_def eventually_at dist_norm 

38 
apply clarsimp 

39 
apply (rule_tac x="a + scaleR (d / 2) (sgn (x  a))" in exI) 

40 
apply (simp add: norm_sgn sgn_zero_iff x) 

41 
done 

42 
thus ?thesis 

43 
by (rule netlimit_within [of a UNIV, unfolded within_UNIV]) 

44 
qed simp 

45 

46 
lemma FDERIV_conv_has_derivative: 

44137  47 
shows "FDERIV f x :> f' = (f has_derivative f') (at x)" 
48 
unfolding fderiv_def has_derivative_def netlimit_at_vector 

49 
by (simp add: diff_diff_eq Lim_at_zero [where a=x] 

44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44531
diff
changeset

50 
tendsto_norm_zero_iff [where 'b='b, symmetric]) 
44137  51 

52 
lemma DERIV_conv_has_derivative: 

53 
"(DERIV f x :> f') = (f has_derivative op * f') (at x)" 

54 
unfolding deriv_fderiv FDERIV_conv_has_derivative 

55 
by (subst mult_commute, rule refl) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

56 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

57 
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 HOLlight)
hoelzl
parents:
diff
changeset

58 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

59 
lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

60 
bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y  x)) *\<^sub>R (f y  (f x + f' (y  x)))) > 0) (at x within s)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

61 
unfolding has_derivative_def and Lim by(auto simp add:netlimit_within) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

62 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

63 
lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

64 
bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y  x))) *\<^sub>R (f y  (f x + f' (y  x)))) > 0) (at x)" 
45031  65 
using has_derivative_within [of f f' x UNIV] by simp 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

66 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

67 
text {* More explicit epsilondelta forms. *} 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

68 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

69 
lemma has_derivative_within': 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

70 
"(f has_derivative f')(at x within s) \<longleftrightarrow> bounded_linear f' \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

71 
(\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm(x'  x) \<and> norm(x'  x) < d 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

72 
\<longrightarrow> norm(f x'  f x  f'(x'  x)) / norm(x'  x) < e)" 
36587  73 
unfolding has_derivative_within Lim_within dist_norm 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

74 
unfolding diff_0_right by (simp add: diff_diff_eq) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

75 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

76 
lemma has_derivative_at': 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

77 
"(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

78 
(\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm(x'  x) \<and> norm(x'  x) < d 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

79 
\<longrightarrow> norm(f x'  f x  f'(x'  x)) / norm(x'  x) < e)" 
45031  80 
using has_derivative_within' [of f f' x UNIV] by simp 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

81 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

82 
lemma has_derivative_at_within: "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

83 
unfolding has_derivative_within' has_derivative_at' by meson 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

84 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

85 
lemma has_derivative_within_open: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

86 
"a \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a))" 
37730  87 
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 HOLlight)
hoelzl
parents:
diff
changeset

88 

43338  89 
lemma has_derivative_right: 
90 
fixes f :: "real \<Rightarrow> real" and y :: "real" 

91 
shows "(f has_derivative (op * y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow> 

92 
((\<lambda>t. (f x  f t) / (x  t)) > y) (at x within ({x <..} \<inter> I))" 

93 
proof  

94 
have "((\<lambda>t. (f t  (f x + y * (t  x))) / \<bar>t  x\<bar>) > 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow> 

95 
((\<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

96 
by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib) 
43338  97 
also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t  f x) / (t  x)) > y) (at x within ({x<..} \<inter> I))" 
98 
by (simp add: Lim_null[symmetric]) 

99 
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

100 
by (intro Lim_cong_within) (simp_all add: field_simps) 
43338  101 
finally show ?thesis 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

102 
by (simp add: bounded_linear_mult_right has_derivative_within) 
43338  103 
qed 
104 

37648  105 
lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *) 
106 
proof  

107 
assume "bounded_linear f" 

108 
then interpret f: bounded_linear f . 

109 
show "linear f" 

110 
by (simp add: f.add f.scaleR linear_def) 

111 
qed 

112 

113 
lemma derivative_is_linear: 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

114 
"(f has_derivative f') net \<Longrightarrow> linear f'" 
37648  115 
by (rule derivative_linear [THEN bounded_linear_imp_linear]) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

116 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

117 
subsubsection {* Combining theorems. *} 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

118 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

119 
lemma has_derivative_id: "((\<lambda>x. x) has_derivative (\<lambda>h. h)) net" 
44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

120 
unfolding has_derivative_def 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

121 
by (simp add: bounded_linear_ident tendsto_const) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

122 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

123 
lemma has_derivative_const: "((\<lambda>x. c) has_derivative (\<lambda>h. 0)) net" 
44125  124 
unfolding has_derivative_def 
44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

125 
by (simp add: bounded_linear_zero tendsto_const) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

126 

44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

127 
lemma (in bounded_linear) has_derivative': "(f has_derivative f) net" 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

128 
unfolding has_derivative_def apply(rule,rule bounded_linear_axioms) 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

129 
unfolding diff by (simp add: tendsto_const) 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

130 

2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

131 
lemma (in bounded_linear) bounded_linear: "bounded_linear f" .. 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

132 

44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

133 
lemma (in bounded_linear) has_derivative: 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

134 
assumes "((\<lambda>x. g x) has_derivative (\<lambda>h. g' h)) net" 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

135 
shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>h. f (g' h))) net" 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

136 
using assms unfolding has_derivative_def 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

137 
apply safe 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

138 
apply (erule bounded_linear_compose [OF local.bounded_linear]) 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

139 
apply (drule local.tendsto) 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

140 
apply (simp add: local.scaleR local.diff local.add local.zero) 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

141 
done 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

142 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

143 
lemmas scaleR_right_has_derivative = 
45605  144 
bounded_linear.has_derivative [OF bounded_linear_scaleR_right] 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

145 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

146 
lemmas scaleR_left_has_derivative = 
45605  147 
bounded_linear.has_derivative [OF bounded_linear_scaleR_left] 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

148 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

149 
lemmas inner_right_has_derivative = 
45605  150 
bounded_linear.has_derivative [OF bounded_linear_inner_right] 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

151 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

152 
lemmas inner_left_has_derivative = 
45605  153 
bounded_linear.has_derivative [OF bounded_linear_inner_left] 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

154 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

155 
lemmas mult_right_has_derivative = 
45605  156 
bounded_linear.has_derivative [OF bounded_linear_mult_right] 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

157 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

158 
lemmas mult_left_has_derivative = 
45605  159 
bounded_linear.has_derivative [OF bounded_linear_mult_left] 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

160 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

161 
lemmas euclidean_component_has_derivative = 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

162 
bounded_linear.has_derivative [OF bounded_linear_euclidean_component] 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

163 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

164 
lemma has_derivative_neg: 
44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

165 
assumes "(f has_derivative f') net" 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

166 
shows "((\<lambda>x. (f x)) has_derivative (\<lambda>h. (f' h))) net" 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

167 
using scaleR_right_has_derivative [where r="1", OF assms] by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

168 

44123  169 
lemma has_derivative_add: 
170 
assumes "(f has_derivative f') net" and "(g has_derivative g') net" 

171 
shows "((\<lambda>x. f(x) + g(x)) has_derivative (\<lambda>h. f'(h) + g'(h))) net" 

172 
proof 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

173 
note as = assms[unfolded has_derivative_def] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

174 
show ?thesis unfolding has_derivative_def apply(rule,rule bounded_linear_add) 
44125  175 
using tendsto_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as 
44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

176 
by (auto simp add: algebra_simps) 
44123  177 
qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

178 

44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

179 
lemma has_derivative_add_const: 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

180 
"(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net" 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

181 
by (drule has_derivative_add, rule has_derivative_const, auto) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

182 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

183 
lemma has_derivative_sub: 
44123  184 
assumes "(f has_derivative f') net" and "(g has_derivative g') net" 
185 
shows "((\<lambda>x. f(x)  g(x)) has_derivative (\<lambda>h. f'(h)  g'(h))) net" 

186 
unfolding diff_minus by (intro has_derivative_add has_derivative_neg assms) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

187 

44123  188 
lemma has_derivative_setsum: 
189 
assumes "finite s" and "\<forall>a\<in>s. ((f a) has_derivative (f' a)) net" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

190 
shows "((\<lambda>x. setsum (\<lambda>a. f a x) s) has_derivative (\<lambda>h. setsum (\<lambda>a. f' a h) s)) net" 
44123  191 
using assms by (induct, simp_all add: has_derivative_const has_derivative_add) 
44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

192 
text {* Somewhat different results for derivative of scalar multiplier. *} 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

193 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

194 
(** move **) 
44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

195 
lemma linear_vmul_component: (* TODO: delete *) 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

196 
assumes lf: "linear f" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

197 
shows "linear (\<lambda>x. f x $$ k *\<^sub>R v)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

198 
using lf 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

199 
by (auto simp add: linear_def algebra_simps) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

200 

44123  201 
lemmas has_derivative_intros = 
44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

202 
has_derivative_id has_derivative_const 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

203 
has_derivative_add has_derivative_sub has_derivative_neg 
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

204 
has_derivative_add_const 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

205 
scaleR_left_has_derivative scaleR_right_has_derivative 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

206 
inner_left_has_derivative inner_right_has_derivative 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

207 
euclidean_component_has_derivative 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

208 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

209 
subsubsection {* Limit transformation for derivatives *} 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

210 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

211 
lemma has_derivative_transform_within: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

212 
assumes "0 < d" "x \<in> s" "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'" "(f has_derivative f') (at x within s)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

213 
shows "(g has_derivative f') (at x within s)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

214 
using assms(4) unfolding has_derivative_within apply apply(erule conjE,rule,assumption) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

215 
apply(rule Lim_transform_within[OF assms(1)]) defer apply assumption 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

216 
apply(rule,rule) apply(drule assms(3)[rule_format]) using assms(3)[rule_format, OF assms(2)] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

217 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

218 
lemma has_derivative_transform_at: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

219 
assumes "0 < d" "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'" "(f has_derivative f') (at x)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

220 
shows "(g has_derivative f') (at x)" 
45031  221 
using has_derivative_transform_within [of d x UNIV f g f'] assms by simp 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

222 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

223 
lemma has_derivative_transform_within_open: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

224 
assumes "open s" "x \<in> s" "\<forall>y\<in>s. f y = g y" "(f has_derivative f') (at x)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

225 
shows "(g has_derivative f') (at x)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

226 
using assms(4) unfolding has_derivative_at apply apply(erule conjE,rule,assumption) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

227 
apply(rule Lim_transform_within_open[OF assms(1,2)]) defer apply assumption 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

228 
apply(rule,rule) apply(drule assms(3)[rule_format]) using assms(3)[rule_format, OF assms(2)] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

229 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

230 
subsection {* Differentiability *} 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

231 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36334
diff
changeset

232 
no_notation Deriv.differentiable (infixl "differentiable" 60) 
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36334
diff
changeset

233 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
43338
diff
changeset

234 
definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" (infixr "differentiable" 30) where 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

235 
"f differentiable net \<equiv> (\<exists>f'. (f has_derivative f') net)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

236 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

237 
definition differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "differentiable'_on" 30) where 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

238 
"f differentiable_on s \<equiv> (\<forall>x\<in>s. f differentiable (at x within s))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

239 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

240 
lemma differentiableI: "(f has_derivative f') net \<Longrightarrow> f differentiable net" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

241 
unfolding differentiable_def by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

242 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

243 
lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

244 
unfolding differentiable_def using has_derivative_at_within by blast 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

245 

44123  246 
lemma differentiable_within_open: (* TODO: delete *) 
247 
assumes "a \<in> s" and "open s" 

248 
shows "f differentiable (at a within s) \<longleftrightarrow> (f differentiable (at a))" 

37730  249 
using assms 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 HOLlight)
hoelzl
parents:
diff
changeset

250 

44123  251 
lemma differentiable_on_eq_differentiable_at: 
252 
"open s \<Longrightarrow> (f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x))" 

253 
unfolding differentiable_on_def 

254 
by (auto simp add: at_within_interior interior_open) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

255 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

256 
lemma differentiable_transform_within: 
44123  257 
assumes "0 < d" and "x \<in> s" and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'" 
258 
assumes "f differentiable (at x within s)" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

259 
shows "g differentiable (at x within s)" 
44123  260 
using assms(4) unfolding differentiable_def 
261 
by (auto intro!: has_derivative_transform_within[OF assms(13)]) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

262 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

263 
lemma differentiable_transform_at: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

264 
assumes "0 < d" "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'" "f differentiable at x" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

265 
shows "g differentiable at x" 
44123  266 
using assms(3) unfolding differentiable_def 
267 
using has_derivative_transform_at[OF assms(12)] by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

268 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

269 
subsection {* Frechet derivative and Jacobian matrix. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

270 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

271 
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 HOLlight)
hoelzl
parents:
diff
changeset

272 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

273 
lemma frechet_derivative_works: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

274 
"f differentiable net \<longleftrightarrow> (f has_derivative (frechet_derivative f net)) net" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

275 
unfolding frechet_derivative_def differentiable_def and some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] .. 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

276 

37648  277 
lemma linear_frechet_derivative: 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

278 
shows "f differentiable net \<Longrightarrow> linear(frechet_derivative f net)" 
44123  279 
unfolding frechet_derivative_works has_derivative_def 
280 
by (auto intro: bounded_linear_imp_linear) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

281 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

282 
subsection {* Differentiability implies continuity *} 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

283 

44123  284 
lemma Lim_mul_norm_within: 
285 
fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

286 
shows "(f > 0) (at a within s) \<Longrightarrow> ((\<lambda>x. norm(x  a) *\<^sub>R f(x)) > 0) (at a within s)" 
44123  287 
unfolding Lim_within apply(rule,rule) 
288 
apply(erule_tac x=e in allE,erule impE,assumption,erule exE,erule conjE) 

289 
apply(rule_tac x="min d 1" in exI) apply rule defer 

290 
apply(rule,erule_tac x=x in ballE) unfolding dist_norm diff_0_right 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

291 
by(auto intro!: mult_strict_mono[of _ "1::real", unfolded mult_1_left]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

292 

44123  293 
lemma differentiable_imp_continuous_within: 
294 
assumes "f differentiable (at x within s)" 

295 
shows "continuous (at x within s) f" 

296 
proof 

297 
from assms guess f' unfolding differentiable_def has_derivative_within .. 

298 
note f'=this 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

299 
then interpret bounded_linear f' by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

300 
have *:"\<And>xa. x\<noteq>xa \<Longrightarrow> (f' \<circ> (\<lambda>y. y  x)) xa + norm (xa  x) *\<^sub>R ((1 / norm (xa  x)) *\<^sub>R (f xa  (f x + f' (xa  x))))  ((f' \<circ> (\<lambda>y. y  x)) x + 0) = f xa  f x" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

301 
using zero by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

302 
have **:"continuous (at x within s) (f' \<circ> (\<lambda>y. y  x))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

303 
apply(rule continuous_within_compose) apply(rule continuous_intros)+ 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

304 
by(rule linear_continuous_within[OF f'[THEN conjunct1]]) 
44123  305 
show ?thesis unfolding continuous_within 
306 
using f'[THEN conjunct2, THEN Lim_mul_norm_within] 

44125  307 
apply apply(drule tendsto_add) 
44123  308 
apply(rule **[unfolded continuous_within]) 
309 
unfolding Lim_within and dist_norm 

310 
apply (rule, rule) 

311 
apply (erule_tac x=e in allE) 

312 
apply (erule impE  assumption)+ 

313 
apply (erule exE, rule_tac x=d in exI) 

44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

314 
by (auto simp add: zero *) 
44123  315 
qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

316 

44123  317 
lemma differentiable_imp_continuous_at: 
318 
"f differentiable at x \<Longrightarrow> continuous (at x) f" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

319 
by(rule differentiable_imp_continuous_within[of _ x UNIV, unfolded within_UNIV]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

320 

44123  321 
lemma differentiable_imp_continuous_on: 
322 
"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 HOLlight)
hoelzl
parents:
diff
changeset

323 
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 HOLlight)
hoelzl
parents:
diff
changeset

324 
using differentiable_imp_continuous_within by blast 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

325 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

326 
lemma has_derivative_within_subset: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

327 
"(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

328 
unfolding has_derivative_within using Lim_within_subset by blast 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

329 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

330 
lemma differentiable_within_subset: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

331 
"f differentiable (at x within t) \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable (at x within s)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

332 
unfolding differentiable_def using has_derivative_within_subset by blast 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

333 

44123  334 
lemma differentiable_on_subset: 
335 
"f differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable_on s" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

336 
unfolding differentiable_on_def using differentiable_within_subset by blast 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

337 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

338 
lemma differentiable_on_empty: "f differentiable_on {}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

339 
unfolding differentiable_on_def by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

340 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

341 
text {* Several results are easier using a "multipliedout" variant. 
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

342 
(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 HOLlight)
hoelzl
parents:
diff
changeset

343 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

344 
lemma has_derivative_within_alt: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

345 
"(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

346 
(\<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))" (is "?lhs \<longleftrightarrow> ?rhs") 
44123  347 
proof 
348 
assume ?lhs thus ?rhs 

349 
unfolding has_derivative_within applyapply(erule conjE,rule,assumption) 

350 
unfolding Lim_within 

351 
apply(rule,erule_tac x=e in allE,rule,erule impE,assumption) 

352 
apply(erule exE,rule_tac x=d in exI) 

353 
apply(erule conjE,rule,assumption,rule,rule) 

354 
proof 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

355 
fix x y e d assume as:"0 < e" "0 < d" "norm (y  x) < d" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

356 
dist ((1 / norm (xa  x)) *\<^sub>R (f xa  (f x + f' (xa  x)))) 0 < e" "y \<in> s" "bounded_linear f'" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

357 
then interpret bounded_linear f' by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

358 
show "norm (f y  f x  f' (y  x)) \<le> e * norm (y  x)" proof(cases "y=x") 
44123  359 
case True thus ?thesis using `bounded_linear f'` by(auto simp add: zero) 
360 
next 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

361 
case False hence "norm (f y  (f x + f' (y  x))) < e * norm (y  x)" using as(4)[rule_format, OF `y\<in>s`] 
41958  362 
unfolding dist_norm diff_0_right using as(3) 
363 
using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded dist_norm] 

364 
by (auto simp add: linear_0 linear_sub) 

44123  365 
thus ?thesis by(auto simp add:algebra_simps) 
366 
qed 

367 
qed 

368 
next 

369 
assume ?rhs thus ?lhs unfolding has_derivative_within Lim_within 

370 
applyapply(erule conjE,rule,assumption) 

371 
apply(rule,erule_tac x="e/2" in allE,rule,erule impE) defer 

372 
apply(erule exE,rule_tac x=d in exI) 

373 
apply(erule conjE,rule,assumption,rule,rule) 

374 
unfolding dist_norm diff_0_right norm_scaleR 

375 
apply(erule_tac x=xa in ballE,erule impE) 

376 
proof 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

377 
fix e d y assume "bounded_linear f'" "0 < e" "0 < d" "y \<in> s" "0 < norm (y  x) \<and> norm (y  x) < d" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

378 
"norm (f y  f x  f' (y  x)) \<le> e / 2 * norm (y  x)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

379 
thus "\<bar>1 / norm (y  x)\<bar> * norm (f y  (f x + f' (y  x))) < e" 
44123  380 
apply(rule_tac le_less_trans[of _ "e/2"]) 
381 
by(auto intro!:mult_imp_div_pos_le simp add:algebra_simps) 

382 
qed auto 

383 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

384 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

385 
lemma has_derivative_at_alt: 
35172
579dd5570f96
Added integration to MultivariateAnalysis (upto FTC)
himmelma
parents:
35028
diff
changeset

386 
"(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and> 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

387 
(\<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))" 
45031  388 
using has_derivative_within_alt[where s=UNIV] by simp 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

389 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

390 
subsection {* The chain rule. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

391 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

392 
lemma diff_chain_within: 
44123  393 
assumes "(f has_derivative f') (at x within s)" 
394 
assumes "(g has_derivative g') (at (f x) within (f ` s))" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

395 
shows "((g o f) has_derivative (g' o f'))(at x within s)" 
44123  396 
unfolding has_derivative_within_alt 
397 
apply(rule,rule bounded_linear_compose[unfolded o_def[THEN sym]]) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

398 
apply(rule assms(2)[unfolded has_derivative_def,THEN conjE],assumption) 
44123  399 
apply(rule assms(1)[unfolded has_derivative_def,THEN conjE],assumption) 
400 
proof(rule,rule) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

401 
note assms = assms[unfolded has_derivative_within_alt] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

402 
fix e::real assume "0<e" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

403 
guess B1 using bounded_linear.pos_bounded[OF assms(1)[THEN conjunct1, rule_format]] .. note B1 = this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

404 
guess B2 using bounded_linear.pos_bounded[OF assms(2)[THEN conjunct1, rule_format]] .. note B2 = this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

405 
have *:"e / 2 / B2 > 0" using `e>0` B2 applyapply(rule divide_pos_pos) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

406 
guess d1 using assms(1)[THEN conjunct2, rule_format, OF *] .. note d1 = this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

407 
have *:"e / 2 / (1 + B1) > 0" using `e>0` B1 applyapply(rule divide_pos_pos) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

408 
guess de using assms(2)[THEN conjunct2, rule_format, OF *] .. note de = this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

409 
guess d2 using assms(1)[THEN conjunct2, rule_format, OF zero_less_one] .. note d2 = this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

410 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

411 
def d0 \<equiv> "(min d1 d2)/2" have d0:"d0>0" "d0 < d1" "d0 < d2" unfolding d0_def using d1 d2 by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

412 
def d \<equiv> "(min d0 (de / (B1 + 1))) / 2" have "de * 2 / (B1 + 1) > de / (B1 + 1)" apply(rule divide_strict_right_mono) using B1 de by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

413 
hence d:"d>0" "d < d1" "d < d2" "d < (de / (B1 + 1))" unfolding d_def using d0 d1 d2 de B1 by(auto intro!: divide_pos_pos simp add:min_less_iff_disj not_less) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

414 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

415 
show "\<exists>d>0. \<forall>y\<in>s. norm (y  x) < d \<longrightarrow> norm ((g \<circ> f) y  (g \<circ> f) x  (g' \<circ> f') (y  x)) \<le> e * norm (y  x)" apply(rule_tac x=d in exI) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

416 
proof(rule,rule `d>0`,rule,rule) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

417 
fix y assume as:"y \<in> s" "norm (y  x) < d" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

418 
hence 1:"norm (f y  f x  f' (y  x)) \<le> min (norm (y  x)) (e / 2 / B2 * norm (y  x))" using d1 d2 d by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

419 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

420 
have "norm (f y  f x) \<le> norm (f y  f x  f' (y  x)) + norm (f' (y  x))" 
44123  421 
using norm_triangle_sub[of "f y  f x" "f' (y  x)"] 
422 
by(auto simp add:algebra_simps) 

423 
also have "\<dots> \<le> norm (f y  f x  f' (y  x)) + B1 * norm (y  x)" 

424 
apply(rule add_left_mono) using B1 by(auto simp add:algebra_simps) 

425 
also have "\<dots> \<le> min (norm (y  x)) (e / 2 / B2 * norm (y  x)) + B1 * norm (y  x)" 

426 
apply(rule add_right_mono) using d1 d2 d as by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

427 
also have "\<dots> \<le> norm (y  x) + B1 * norm (y  x)" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

428 
also have "\<dots> = norm (y  x) * (1 + B1)" by(auto simp add:field_simps) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

429 
finally have 3:"norm (f y  f x) \<le> norm (y  x) * (1 + B1)" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

430 

44123  431 
hence "norm (f y  f x) \<le> d * (1 + B1)" apply 
432 
apply(rule order_trans,assumption,rule mult_right_mono) 

433 
using as B1 by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

434 
also have "\<dots> < de" using d B1 by(auto simp add:field_simps) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

435 
finally have "norm (g (f y)  g (f x)  g' (f y  f x)) \<le> e / 2 / (1 + B1) * norm (f y  f x)" 
44123  436 
applyapply(rule de[THEN conjunct2,rule_format]) 
437 
using `y\<in>s` using d as by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

438 
also have "\<dots> = (e / 2) * (1 / (1 + B1) * norm (f y  f x))" by auto 
44123  439 
also have "\<dots> \<le> e / 2 * norm (y  x)" apply(rule mult_left_mono) 
440 
using `e>0` and 3 using B1 and `e>0` by(auto simp add:divide_le_eq) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

441 
finally have 4:"norm (g (f y)  g (f x)  g' (f y  f x)) \<le> e / 2 * norm (y  x)" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

442 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

443 
interpret g': bounded_linear g' using assms(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

444 
interpret f': bounded_linear f' using assms(1) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

445 
have "norm ( g' (f' (y  x)) + g' (f y  f x)) = norm (g' (f y  f x  f' (y  x)))" 
36350  446 
by(auto simp add:algebra_simps f'.diff g'.diff g'.add) 
44123  447 
also have "\<dots> \<le> B2 * norm (f y  f x  f' (y  x))" using B2 
448 
by (auto simp add: algebra_simps) 

449 
also have "\<dots> \<le> B2 * (e / 2 / B2 * norm (y  x))" 

450 
apply (rule mult_left_mono) using as d1 d2 d B2 by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

451 
also have "\<dots> \<le> e / 2 * norm (y  x)" using B2 by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

452 
finally have 5:"norm ( g' (f' (y  x)) + g' (f y  f x)) \<le> e / 2 * norm (y  x)" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

453 

44123  454 
have "norm (g (f y)  g (f x)  g' (f y  f x)) + norm (g (f y)  g (f x)  g' (f' (y  x))  (g (f y)  g (f x)  g' (f y  f x))) \<le> e * norm (y  x)" 
455 
using 5 4 by auto 

456 
thus "norm ((g \<circ> f) y  (g \<circ> f) x  (g' \<circ> f') (y  x)) \<le> e * norm (y  x)" 

457 
unfolding o_def apply apply(rule order_trans, rule norm_triangle_sub) 

458 
by assumption 

459 
qed 

460 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

461 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

462 
lemma diff_chain_at: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

463 
"(f has_derivative f') (at x) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> ((g o f) has_derivative (g' o f')) (at x)" 
44123  464 
using diff_chain_within[of f f' x UNIV g g'] 
465 
using has_derivative_within_subset[of g g' "f x" UNIV "range f"] 

45031  466 
by simp 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

467 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

468 
subsection {* Composition rules stated just for differentiability. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

469 

44123  470 
lemma differentiable_const [intro]: 
471 
"(\<lambda>z. c) differentiable (net::'a::real_normed_vector filter)" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

472 
unfolding differentiable_def using has_derivative_const by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

473 

44123  474 
lemma differentiable_id [intro]: 
475 
"(\<lambda>z. z) differentiable (net::'a::real_normed_vector filter)" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

476 
unfolding differentiable_def using has_derivative_id by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

477 

44123  478 
lemma differentiable_cmul [intro]: 
479 
"f differentiable net \<Longrightarrow> 

480 
(\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)" 

481 
unfolding differentiable_def 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

482 
apply(erule exE, drule scaleR_right_has_derivative) by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

483 

44123  484 
lemma differentiable_neg [intro]: 
485 
"f differentiable net \<Longrightarrow> 

486 
(\<lambda>z. (f z)) differentiable (net::'a::real_normed_vector filter)" 

487 
unfolding differentiable_def 

488 
apply(erule exE, drule has_derivative_neg) by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

489 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

490 
lemma differentiable_add: "f differentiable net \<Longrightarrow> g differentiable net 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
43338
diff
changeset

491 
\<Longrightarrow> (\<lambda>z. f z + g z) differentiable (net::'a::real_normed_vector filter)" 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

492 
unfolding differentiable_def apply(erule exE)+ apply(rule_tac x="\<lambda>z. f' z + f'a z" in exI) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

493 
apply(rule has_derivative_add) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

494 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

495 
lemma differentiable_sub: "f differentiable net \<Longrightarrow> g differentiable net 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
43338
diff
changeset

496 
\<Longrightarrow> (\<lambda>z. f z  g z) differentiable (net::'a::real_normed_vector filter)" 
44123  497 
unfolding differentiable_def apply(erule exE)+ 
498 
apply(rule_tac x="\<lambda>z. f' z  f'a z" in exI) 

499 
apply(rule has_derivative_sub) by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

500 

37648  501 
lemma differentiable_setsum: 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

502 
assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net" 
44123  503 
shows "(\<lambda>x. setsum (\<lambda>a. f a x) s) differentiable net" 
504 
proof 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

505 
guess f' using bchoice[OF assms(2)[unfolded differentiable_def]] .. 
44123  506 
thus ?thesis unfolding differentiable_def apply 
507 
apply(rule,rule has_derivative_setsum[where f'=f'],rule assms(1)) by auto 

508 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

509 

37648  510 
lemma differentiable_setsum_numseg: 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

511 
shows "\<forall>i. m \<le> i \<and> i \<le> n \<longrightarrow> (f i) differentiable net \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) {m::nat..n}) differentiable net" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

512 
apply(rule differentiable_setsum) using finite_atLeastAtMost[of n m] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

513 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

514 
lemma differentiable_chain_at: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

515 
"f differentiable (at x) \<Longrightarrow> g differentiable (at(f x)) \<Longrightarrow> (g o f) differentiable (at x)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

516 
unfolding differentiable_def by(meson diff_chain_at) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

517 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

518 
lemma differentiable_chain_within: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

519 
"f differentiable (at x within s) \<Longrightarrow> g differentiable (at(f x) within (f ` s)) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

520 
\<Longrightarrow> (g o f) differentiable (at x within s)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

521 
unfolding differentiable_def by(meson diff_chain_within) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

522 

37730  523 
subsection {* Uniqueness of derivative *} 
524 

525 
text {* 

526 
The general result is a bit messy because we need approachability of the 

527 
limit point from any direction. But OK for nontrivial intervals etc. 

528 
*} 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

529 

44123  530 
lemma frechet_derivative_unique_within: 
531 
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" 

532 
assumes "(f has_derivative f') (at x within s)" 

533 
assumes "(f has_derivative f'') (at x within s)" 

534 
assumes "(\<forall>i<DIM('a). \<forall>e>0. \<exists>d. 0 < abs(d) \<and> abs(d) < e \<and> (x + d *\<^sub>R basis i) \<in> s)" 

535 
shows "f' = f''" 

536 
proof 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

537 
note as = assms(1,2)[unfolded has_derivative_def] 
44123  538 
then interpret f': bounded_linear f' by auto 
539 
from as interpret f'': bounded_linear f'' by auto 

540 
have "x islimpt s" unfolding islimpt_approachable 

541 
proof(rule,rule) 

542 
fix e::real assume "0<e" guess d 

543 
using assms(3)[rule_format,OF DIM_positive `e>0`] .. 

544 
thus "\<exists>x'\<in>s. x' \<noteq> x \<and> dist x' x < e" 

545 
apply(rule_tac x="x + d *\<^sub>R basis 0" in bexI) 

546 
unfolding dist_norm by auto 

547 
qed 

548 
hence *:"netlimit (at x within s) = x" applyapply(rule netlimit_within) 

549 
unfolding trivial_limit_within by simp 

550 
show ?thesis apply(rule linear_eq_stdbasis) 

551 
unfolding linear_conv_bounded_linear 

552 
apply(rule as(1,2)[THEN conjunct1])+ 

553 
proof(rule,rule,rule ccontr) 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

554 
fix i assume i:"i<DIM('a)" def e \<equiv> "norm (f' (basis i)  f'' (basis i))" 
44123  555 
assume "f' (basis i) \<noteq> f'' (basis i)" 
556 
hence "e>0" unfolding e_def by auto 

44125  557 
guess d using tendsto_diff [OF as(1,2)[THEN conjunct2], unfolded * Lim_within,rule_format,OF `e>0`] .. note d=this 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

558 
guess c using assms(3)[rule_format,OF i d[THEN conjunct1]] .. note c=this 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

559 
have *:"norm ( ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R basis i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R basis i)) = norm ((1 / abs c) *\<^sub>R ( (f' (c *\<^sub>R basis i)) + f'' (c *\<^sub>R basis i)))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

560 
unfolding scaleR_right_distrib by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

561 
also have "\<dots> = norm ((1 / abs c) *\<^sub>R (c *\<^sub>R ( (f' (basis i)) + f'' (basis i))))" 
44123  562 
unfolding f'.scaleR f''.scaleR 
563 
unfolding scaleR_right_distrib scaleR_minus_right by auto 

564 
also have "\<dots> = e" unfolding e_def using c[THEN conjunct1] 

565 
using norm_minus_cancel[of "f' (basis i)  f'' (basis i)"] 

566 
by (auto simp add: add.commute ab_diff_minus) 

567 
finally show False using c 

568 
using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R basis i"] 

569 
unfolding dist_norm 

570 
unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff 

571 
scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib 

572 
using i by auto 

573 
qed 

574 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

575 

37730  576 
lemma frechet_derivative_unique_at: 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

577 
shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''" 
37730  578 
unfolding FDERIV_conv_has_derivative [symmetric] 
579 
by (rule FDERIV_unique) 

41829  580 

44123  581 
lemma continuous_isCont: "isCont f x = continuous (at x) f" 
582 
unfolding isCont_def LIM_def 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

583 
unfolding continuous_at Lim_at unfolding dist_nz by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

584 

44123  585 
lemma frechet_derivative_unique_within_closed_interval: 
586 
fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector" 

587 
assumes "\<forall>i<DIM('a). a$$i < b$$i" "x \<in> {a..b}" (is "x\<in>?I") 

588 
assumes "(f has_derivative f' ) (at x within {a..b})" 

589 
assumes "(f has_derivative f'') (at x within {a..b})" 

590 
shows "f' = f''" 

591 
apply(rule frechet_derivative_unique_within) 

592 
apply(rule assms(3,4))+ 

593 
proof(rule,rule,rule,rule) 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

594 
fix e::real and i assume "e>0" and i:"i<DIM('a)" 
44123  595 
thus "\<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R basis i \<in> {a..b}" 
596 
proof(cases "x$$i=a$$i") 

597 
case True thus ?thesis 

598 
apply(rule_tac x="(min (b$$i  a$$i) e) / 2" in exI) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

599 
using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2) 
44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44282
diff
changeset

600 
unfolding mem_interval euclidean_simps 
44123  601 
using i by (auto simp add: field_simps) 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

602 
next note * = assms(2)[unfolded mem_interval,THEN spec[where x=i]] 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

603 
case False moreover have "a $$ i < x $$ i" using False * by auto 
44123  604 
moreover { 
605 
have "a $$ i * 2 + min (x $$ i  a $$ i) e \<le> a$$i *2 + x$$i  a$$i" 

606 
by auto 

607 
also have "\<dots> = a$$i + x$$i" by auto 

608 
also have "\<dots> \<le> 2 * x$$i" using * by auto 

609 
finally have "a $$ i * 2 + min (x $$ i  a $$ i) e \<le> x $$ i * 2" by auto 

610 
} 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

611 
moreover have "min (x $$ i  a $$ i) e \<ge> 0" using * and `e>0` by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

612 
hence "x $$ i * 2 \<le> b $$ i * 2 + min (x $$ i  a $$ i) e" using * by auto 
44123  613 
ultimately show ?thesis 
614 
apply(rule_tac x=" (min (x$$i  a$$i) e) / 2" in exI) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

615 
using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2) 
44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44282
diff
changeset

616 
unfolding mem_interval euclidean_simps 
44123  617 
using i by (auto simp add: field_simps) 
618 
qed 

619 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

620 

44123  621 
lemma frechet_derivative_unique_within_open_interval: 
622 
fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector" 

623 
assumes "x \<in> {a<..<b}" 

624 
assumes "(f has_derivative f' ) (at x within {a<..<b})" 

625 
assumes "(f has_derivative f'') (at x within {a<..<b})" 

37650  626 
shows "f' = f''" 
627 
proof  

628 
from assms(1) have *: "at x within {a<..<b} = at x" 

629 
by (simp add: at_within_interior interior_open open_interval) 

630 
from assms(2,3) [unfolded *] show "f' = f''" 

631 
by (rule frechet_derivative_unique_at) 

632 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

633 

37730  634 
lemma frechet_derivative_at: 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

635 
shows "(f has_derivative f') (at x) \<Longrightarrow> (f' = frechet_derivative f (at x))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

636 
apply(rule frechet_derivative_unique_at[of f],assumption) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

637 
unfolding frechet_derivative_works[THEN sym] using differentiable_def by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

638 

44123  639 
lemma frechet_derivative_within_closed_interval: 
640 
fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector" 

641 
assumes "\<forall>i<DIM('a). a$$i < b$$i" and "x \<in> {a..b}" 

642 
assumes "(f has_derivative f') (at x within {a.. b})" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

643 
shows "frechet_derivative f (at x within {a.. b}) = f'" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

644 
apply(rule frechet_derivative_unique_within_closed_interval[where f=f]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

645 
apply(rule assms(1,2))+ unfolding frechet_derivative_works[THEN sym] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

646 
unfolding differentiable_def using assms(3) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

647 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

648 
subsection {* The traditional Rolle theorem in one dimension. *} 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

649 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

650 
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

651 
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

652 
assumes lf: "linear f" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

653 
shows "(f x) $$ j = (\<Sum>i<DIM('a). (x$$i) * (f (basis i)$$j))" (is "?lhs = ?rhs") 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

654 
proof  
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

655 
have fA: "finite {..<DIM('a)}" by simp 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

656 
have "?rhs = (\<Sum>i<DIM('a). x$$i *\<^sub>R f (basis i))$$j" 
44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44282
diff
changeset

657 
by simp 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

658 
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

659 
unfolding linear_setsum_mul[OF lf fA, symmetric] 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

660 
unfolding euclidean_representation[symmetric] .. 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

661 
qed 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

662 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

663 
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

664 
the unfolding of it. *} 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

665 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

666 
lemma jacobian_works: 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

667 
"(f::('a::euclidean_space) \<Rightarrow> ('b::euclidean_space)) differentiable net \<longleftrightarrow> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

668 
(f has_derivative (\<lambda>h. \<chi>\<chi> i. 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

669 
\<Sum>j<DIM('a). frechet_derivative f net (basis j) $$ i * h $$ j)) net" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

670 
(is "?differentiable \<longleftrightarrow> (f has_derivative (\<lambda>h. \<chi>\<chi> i. ?SUM h i)) net") 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

671 
proof 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

672 
assume *: ?differentiable 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

673 
{ fix h i 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

674 
have "?SUM h i = frechet_derivative f net h $$ i" using * 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

675 
by (auto intro!: setsum_cong 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

676 
simp: linear_componentwise[of _ h i] linear_frechet_derivative) } 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

677 
thus "(f has_derivative (\<lambda>h. \<chi>\<chi> i. ?SUM h i)) net" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

678 
using * by (simp add: frechet_derivative_works) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

679 
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

680 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

681 
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

682 
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

683 
assumes k: "k < DIM('b)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

684 
and ball: "0 < e" "((\<forall>y \<in> ball x e. (f y)$$k \<le> (f x)$$k) \<or> (\<forall>y\<in>ball x e. (f x)$$k \<le> (f y)$$k))" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

685 
and diff: "f differentiable (at x)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

686 
shows "(\<chi>\<chi> j. frechet_derivative f (at x) (basis j) $$ k) = (0::'a)" (is "?D k = 0") 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

687 
proof (rule ccontr) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

688 
assume "?D k \<noteq> 0" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

689 
then obtain j where j: "?D k $$ j \<noteq> 0" "j < DIM('a)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

690 
unfolding euclidean_lambda_beta euclidean_eq[of _ "0::'a"] by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

691 
hence *: "\<bar>?D k $$ j\<bar> / 2 > 0" by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

692 
note as = diff[unfolded jacobian_works has_derivative_at_alt] 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

693 
guess e' using as[THEN conjunct2, rule_format, OF *] .. note e' = this 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

694 
guess d using real_lbound_gt_zero[OF ball(1) e'[THEN conjunct1]] .. note d = this 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

695 
{ fix c assume "abs c \<le> d" 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

696 
hence *:"norm (x + c *\<^sub>R basis j  x) < e'" using norm_basis[of j] d 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

697 
let ?v = "(\<chi>\<chi> i. \<Sum>l<DIM('a). ?D i $$ l * (c *\<^sub>R basis j :: 'a) $$ l)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

698 
have if_dist: "\<And> P a b c. a * (if P then b else c) = (if P then a * b else a * c)" by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

699 
have "\<bar>(f (x + c *\<^sub>R basis j)  f x  ?v) $$ k\<bar> \<le> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

700 
norm (f (x + c *\<^sub>R basis j)  f x  ?v)" by (rule component_le_norm) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

701 
also have "\<dots> \<le> \<bar>?D k $$ j\<bar> / 2 * \<bar>c\<bar>" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44647
diff
changeset

702 
using e'[THEN conjunct2, rule_format, OF *] and norm_basis[of j] by fastforce 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

703 
finally have "\<bar>(f (x + c *\<^sub>R basis j)  f x  ?v) $$ k\<bar> \<le> \<bar>?D k $$ j\<bar> / 2 * \<bar>c\<bar>" by simp 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

704 
hence "\<bar>f (x + c *\<^sub>R basis j) $$ k  f x $$ k  c * ?D k $$ j\<bar> \<le> \<bar>?D k $$ j\<bar> / 2 * \<bar>c\<bar>" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

705 
unfolding euclidean_simps euclidean_lambda_beta using j k 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

706 
by (simp add: if_dist setsum_cases field_simps) } note * = this 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

707 
have "x + d *\<^sub>R basis j \<in> ball x e" "x  d *\<^sub>R basis j \<in> ball x e" 
36587  708 
unfolding mem_ball dist_norm using norm_basis[of j] d 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

709 
hence **:"((f (x  d *\<^sub>R basis j))$$k \<le> (f x)$$k \<and> (f (x + d *\<^sub>R basis j))$$k \<le> (f x)$$k) \<or> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

710 
((f (x  d *\<^sub>R basis j))$$k \<ge> (f x)$$k \<and> (f (x + d *\<^sub>R basis j))$$k \<ge> (f x)$$k)" using ball by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

711 
have ***: "\<And>y y1 y2 d dx::real. 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

712 
(y1\<le>y\<and>y2\<le>y) \<or> (y\<le>y1\<and>y\<le>y2) \<Longrightarrow> d < abs dx \<Longrightarrow> abs(y1  y   dx) \<le> d \<Longrightarrow> (abs (y2  y  dx) \<le> d) \<Longrightarrow> False" by arith 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

713 
show False apply(rule ***[OF **, where dx="d * ?D k $$ j" and d="\<bar>?D k $$ j\<bar> / 2 * \<bar>d\<bar>"]) 
44123  714 
using *[of "d"] and *[of d] and d[THEN conjunct1] and j 
715 
unfolding mult_minus_left 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

716 
unfolding abs_mult diff_minus_eq_add scaleR_minus_left 
44123  717 
unfolding algebra_simps by (auto intro: mult_pos_pos) 
34906  718 
qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

719 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

720 
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 HOLlight)
hoelzl
parents:
diff
changeset

721 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

722 
lemma differential_zero_maxmin: 
37650  723 
fixes f::"'a\<Colon>euclidean_space \<Rightarrow> real" 
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 
assumes "x \<in> s" "open s" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

725 
and deriv: "(f has_derivative f') (at x)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

726 
and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

727 
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

728 
proof  
44123  729 
obtain e where e:"e>0" "ball x e \<subseteq> s" 
730 
using `open s`[unfolded open_contains_ball] and `x \<in> s` 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

731 
with differential_zero_maxmin_component[where 'b=real, of 0 e x f, simplified] 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

732 
have "(\<chi>\<chi> j. frechet_derivative f (at x) (basis j)) = (0::'a)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

733 
unfolding differentiable_def using mono deriv by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

734 
with frechet_derivative_at[OF deriv, symmetric] 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

735 
have "\<forall>i<DIM('a). f' (basis i) = 0" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

736 
by (simp add: euclidean_eq[of _ "0::'a"]) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

737 
with derivative_is_linear[OF deriv, THEN linear_componentwise, of _ 0] 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

738 
show ?thesis 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

739 
qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

740 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

741 
lemma rolle: fixes f::"real\<Rightarrow>real" 
44123  742 
assumes "a < b" and "f a = f b" and "continuous_on {a..b} f" 
743 
assumes "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)" 

744 
shows "\<exists>x\<in>{a<..<b}. f' x = (\<lambda>v. 0)" 

745 
proof 

746 
have "\<exists>x\<in>{a<..<b}. ((\<forall>y\<in>{a<..<b}. f x \<le> f y) \<or> (\<forall>y\<in>{a<..<b}. f y \<le> f x))" 

747 
proof 

748 
have "(a + b) / 2 \<in> {a .. b}" using assms(1) by auto 

749 
hence *:"{a .. b}\<noteq>{}" 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

750 
guess d using continuous_attains_sup[OF compact_interval * assms(3)] .. note d=this 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

751 
guess c using continuous_attains_inf[OF compact_interval * assms(3)] .. note c=this 
44123  752 
show ?thesis 
753 
proof(cases "d\<in>{a<..<b} \<or> c\<in>{a<..<b}") 

754 
case True thus ?thesis 

755 
apply(erule_tac disjE) apply(rule_tac x=d in bexI) 

756 
apply(rule_tac[3] x=c in bexI) 

757 
using d c by auto 

758 
next 

759 
def e \<equiv> "(a + b) /2" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

760 
case False hence "f d = f c" using d c assms(2) by auto 
44123  761 
hence "\<And>x. x\<in>{a..b} \<Longrightarrow> f x = f d" 
762 
using c d apply apply(erule_tac x=x in ballE)+ by auto 

763 
thus ?thesis 

764 
apply(rule_tac x=e in bexI) unfolding e_def using assms(1) by auto 

765 
qed 

766 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

767 
then guess x .. note x=this 
44123  768 
hence "f' x = (\<lambda>v. 0)" 
769 
apply(rule_tac differential_zero_maxmin[of x "{a<..<b}" f "f' x"]) 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

770 
defer apply(rule open_interval) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

771 
apply(rule assms(4)[unfolded has_derivative_at[THEN sym],THEN bspec[where x=x]],assumption) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

772 
unfolding o_def apply(erule disjE,rule disjI2) by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

773 
thus ?thesis apply(rule_tac x=x in bexI) unfolding o_def apply rule 
44123  774 
apply(drule_tac x=v in fun_cong) using x(1) by auto 
775 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

776 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

777 
subsection {* Onedimensional mean value theorem. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

778 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

779 
lemma mvt: fixes f::"real \<Rightarrow> real" 
44123  780 
assumes "a < b" and "continuous_on {a .. b} f" 
781 
assumes "\<forall>x\<in>{a<..<b}. (f has_derivative (f' x)) (at x)" 

782 
shows "\<exists>x\<in>{a<..<b}. (f b  f a = (f' x) (b  a))" 

783 
proof 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

784 
have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa  (f b  f a) / (b  a) * xa) = (\<lambda>v. 0)" 
44123  785 
apply(rule rolle[OF assms(1), of "\<lambda>x. f x  (f b  f a) / (b  a) * x"]) 
786 
defer 

44531
1d477a2b1572
replace some continuous_on lemmas with more general versions
huffman
parents:
44457
diff
changeset

787 
apply(rule continuous_on_intros assms(2))+ 
44123  788 
proof 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

789 
fix x assume x:"x \<in> {a<..<b}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

790 
show "((\<lambda>x. f x  (f b  f a) / (b  a) * x) has_derivative (\<lambda>xa. f' x xa  (f b  f a) / (b  a) * xa)) (at x)" 
44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

791 
by (intro has_derivative_intros assms(3)[rule_format,OF x] 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44140
diff
changeset

792 
mult_right_has_derivative) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

793 
qed(insert assms(1), auto simp add:field_simps) 
44123  794 
then guess x .. 
795 
thus ?thesis apply(rule_tac x=x in bexI) 

796 
apply(drule fun_cong[of _ _ "b  a"]) by auto 

797 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

798 

44123  799 
lemma mvt_simple: 
800 
fixes f::"real \<Rightarrow> real" 

801 
assumes "a<b" 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 HOLlight)
hoelzl
parents:
diff
changeset

802 
shows "\<exists>x\<in>{a<..<b}. f b  f a = f' x (b  a)" 
44123  803 
apply(rule mvt) 
804 
apply(rule assms(1), rule differentiable_imp_continuous_on) 

805 
unfolding differentiable_on_def differentiable_def defer 

806 
proof 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

807 
fix x assume x:"x \<in> {a<..<b}" show "(f has_derivative f' x) (at x)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

808 
unfolding has_derivative_within_open[OF x open_interval,THEN sym] 
44123  809 
apply(rule has_derivative_within_subset) 
810 
apply(rule assms(2)[rule_format]) 

811 
using x by auto 

812 
qed(insert assms(2), auto) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

813 

44123  814 
lemma mvt_very_simple: 
815 
fixes f::"real \<Rightarrow> real" 

816 
assumes "a \<le> b" and "\<forall>x\<in>{a..b}. (f has_derivative f'(x)) (at x within {a..b})" 

817 
shows "\<exists>x\<in>{a..b}. f b  f a = f' x (b  a)" 

818 
proof (cases "a = b") 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

819 
interpret bounded_linear "f' b" using assms(2) assms(1) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

820 
case True thus ?thesis apply(rule_tac x=a in bexI) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

821 
using assms(2)[THEN bspec[where x=a]] unfolding has_derivative_def 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

822 
unfolding True using zero by auto next 
44123  823 
case False thus ?thesis using mvt_simple[OF _ assms(2)] using assms(1) by auto 
824 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

825 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

826 
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 HOLlight)
hoelzl
parents:
diff
changeset

827 

44123  828 
lemma mvt_general: 
829 
fixes f::"real\<Rightarrow>'a::euclidean_space" 

830 
assumes "a<b" and "continuous_on {a..b} f" 

831 
assumes "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)" 

832 
shows "\<exists>x\<in>{a<..<b}. norm(f b  f a) \<le> norm(f'(x) (b  a))" 

833 
proof 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

834 
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)" 
44123  835 
apply(rule mvt) apply(rule assms(1)) 
836 
apply(rule continuous_on_inner continuous_on_intros assms(2))+ 

44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

837 
unfolding o_def apply(rule,rule has_derivative_intros) 
44123  838 
using assms(3) by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

839 
then guess x .. note x=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

840 
show ?thesis proof(cases "f a = f b") 
36844  841 
case False 
44123  842 
have "norm (f b  f a) * norm (f b  f a) = norm (f b  f a)^2" 
843 
by (simp add: power2_eq_square) 

35542  844 
also have "\<dots> = (f b  f a) \<bullet> (f b  f a)" unfolding power2_norm_eq_inner .. 
44123  845 
also have "\<dots> = (f b  f a) \<bullet> f' x (b  a)" 
846 
using x unfolding inner_simps by (auto simp add: inner_diff_left) 

847 
also have "\<dots> \<le> norm (f b  f a) * norm (f' x (b  a))" 

848 
by (rule norm_cauchy_schwarz) 

849 
finally show ?thesis using False x(1) 

850 
by (auto simp add: real_mult_left_cancel) 

851 
next 

852 
case True thus ?thesis using assms(1) 

853 
apply (rule_tac x="(a + b) /2" in bexI) by auto 

854 
qed 

855 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

856 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

857 
text {* Still more general bound theorem. *} 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

858 

44123  859 
lemma differentiable_bound: 
860 
fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space" 

861 
assumes "convex s" and "\<forall>x\<in>s. (f has_derivative f'(x)) (at x within s)" 

862 
assumes "\<forall>x\<in>s. onorm(f' x) \<le> B" and x:"x\<in>s" and y:"y\<in>s" 

863 
shows "norm(f x  f y) \<le> B * norm(x  y)" 

864 
proof 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

865 
let ?p = "\<lambda>u. x + u *\<^sub>R (y  x)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

866 
have *:"\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y  x) \<in> s" 
44123  867 
using assms(1)[unfolded convex_alt,rule_format,OF x y] 
868 
unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib 

869 
by (auto simp add: algebra_simps) 

870 
hence 1:"continuous_on {0..1} (f \<circ> ?p)" apply 

44531
1d477a2b1572
replace some continuous_on lemmas with more general versions
huffman
parents:
44457
diff
changeset

871 
apply(rule continuous_on_intros)+ 
44123  872 
unfolding continuous_on_eq_continuous_within 
873 
apply(rule,rule differentiable_imp_continuous_within) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

874 
unfolding differentiable_def apply(rule_tac x="f' xa" in exI) 
44123  875 
apply(rule has_derivative_within_subset) 
876 
apply(rule assms(2)[rule_format]) by auto 

877 
have 2:"\<forall>u\<in>{0<..<1}. ((f \<circ> ?p) has_derivative f' (x + u *\<^sub>R (y  x)) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y  x))) (at u)" 

878 
proof rule 

879 
case goal1 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

880 
let ?u = "x + u *\<^sub>R (y  x)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

881 
have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y  x))) (at u within {0<..<1})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

882 
apply(rule diff_chain_within) apply(rule has_derivative_intros)+ 
44123  883 
apply(rule has_derivative_within_subset) 
884 
apply(rule assms(2)[rule_format]) using goal1 * by auto 

885 
thus ?case 

886 
unfolding has_derivative_within_open[OF goal1 open_interval] by auto 

887 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

888 
guess u using mvt_general[OF zero_less_one 1 2] .. note u = this 
44123  889 
have **:"\<And>x y. x\<in>s \<Longrightarrow> norm (f' x y) \<le> B * norm y" 
890 
proof 

891 
case goal1 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

892 
have "norm (f' x y) \<le> onorm (f' x) * norm y" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

893 
using onorm(1)[OF derivative_is_linear[OF assms(2)[rule_format,OF goal1]]] by assumption 
44123  894 
also have "\<dots> \<le> B * norm y" 
895 
apply(rule mult_right_mono) 

896 
using assms(3)[rule_format,OF goal1] 

897 
by(auto simp add:field_simps) 

898 
finally show ?case by simp 

899 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

900 
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)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

901 
by(auto simp add:norm_minus_commute) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

902 
also have "\<dots> \<le> norm (f' (x + u *\<^sub>R (y  x)) (y  x))" using u by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

903 
also have "\<dots> \<le> B * norm(y  x)" apply(rule **) using * and u by auto 
44123  904 
finally show ?thesis by(auto simp add:norm_minus_commute) 
905 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

906 

44123  907 
lemma differentiable_bound_real: 
908 
fixes f::"real \<Rightarrow> real" 

909 
assumes "convex s" and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)" 

910 
assumes "\<forall>x\<in>s. onorm(f' x) \<le> B" and x:"x\<in>s" and y:"y\<in>s" 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

911 
shows "norm(f x  f y) \<le> B * norm(x  y)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

912 
using differentiable_bound[of s f f' B x y] 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

913 
unfolding Ball_def image_iff o_def using assms by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

914 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

915 
text {* In particular. *} 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

916 

44123  917 
lemma has_derivative_zero_constant: 
918 
fixes f::"real\<Rightarrow>real" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

919 
assumes "convex s" "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)" 
44123  920 
shows "\<exists>c. \<forall>x\<in>s. f x = c" 
921 
proof(cases "s={}") 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

922 
case False then obtain x where "x\<in>s" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

923 
have "\<And>y. y\<in>s \<Longrightarrow> f x = f y" proof case goal1 
44123  924 
thus ?case 
925 
using differentiable_bound_real[OF assms(12), of 0 x y] and `x\<in>s` 

926 
unfolding onorm_const by auto qed 

927 
thus ?thesis apply(rule_tac x="f x" in exI) by auto 

928 
qed auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

929 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

930 
lemma has_derivative_zero_unique: fixes f::"real\<Rightarrow>real" 
44123  931 
assumes "convex s" and "a \<in> s" and "f a = c" 
932 
assumes "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)" and "x\<in>s" 

933 
shows "f x = c" 

934 
using has_derivative_zero_constant[OF assms(1,4)] using assms(23,5) by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

935 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

936 
subsection {* Differentiability of inverse function (most basic form). *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

937 

44123  938 
lemma has_derivative_inverse_basic: 
939 
fixes f::"'b::euclidean_space \<Rightarrow> 'c::euclidean_space" 

940 
assumes "(f has_derivative f') (at (g y))" 

941 
assumes "bounded_linear g'" and "g' \<circ> f' = id" and "continuous (at y) g" 

942 
assumes "open t" and "y \<in> t" and "\<forall>z\<in>t. f(g z) = z" 

943 
shows "(g has_derivative g') (at y)" 

944 
proof 

945 
interpret f': bounded_linear f' 

946 
using assms unfolding has_derivative_def by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

947 
interpret g': bounded_linear g' using assms by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

948 
guess C using bounded_linear.pos_bounded[OF assms(2)] .. note C = this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

949 
(* have fgid:"\<And>x. g' (f' x) = x" using assms(3) unfolding o_def id_def apply()*) 
44123  950 
have lem1:"\<forall>e>0. \<exists>d>0. \<forall>z. norm(z  y) < d \<longrightarrow> norm(g z  g y  g'(z  y)) \<le> e * norm(g z  g y)" 
951 
proof(rule,rule) 

952 
case goal1 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

953 
have *:"e / C > 0" apply(rule divide_pos_pos) using `e>0` C by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

954 
guess d0 using assms(1)[unfolded has_derivative_at_alt,THEN conjunct2,rule_format,OF *] .. note d0=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

955 
guess d1 using assms(4)[unfolded continuous_at Lim_at,rule_format,OF d0[THEN conjunct1]] .. note d1=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

956 
guess d2 using assms(5)[unfolded open_dist,rule_format,OF assms(6)] .. note d2=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

957 
guess d using real_lbound_gt_zero[OF d1[THEN conjunct1] d2[THEN conjunct1]] .. note d=this 
44123  958 
thus ?case apply(rule_tac x=d in exI) apply rule defer 
959 
proof(rule,rule) 

960 
fix z assume as:"norm (z  y) < d" hence "z\<in>t" 

961 
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 HOLlight)
hoelzl
parents:
diff
changeset

962 
have "norm (g z  g y  g' (z  y)) \<le> norm (g' (f (g z)  y  f' (g z  g y)))" 
44123  963 
unfolding g'.diff f'.diff 
964 
unfolding assms(3)[unfolded o_def id_def, THEN fun_cong] 

965 
unfolding assms(7)[rule_format,OF `z\<in>t`] 

966 
apply(subst norm_minus_cancel[THEN sym]) by auto 

967 
also have "\<dots> \<le> norm(f (g z)  y  f' (g z  g y)) * C" 

968 
by (rule C [THEN conjunct2, rule_format]) 

969 
also have "\<dots> \<le> (e / C) * norm (g z  g y) * C" 

970 
apply(rule mult_right_mono) 

971 
apply(rule d0[THEN conjunct2,rule_format,unfolded assms(7)[rule_format,OF `y\<in>t`]]) 

972 
apply(cases "z=y") defer 

973 
apply(rule d1[THEN conjunct2, unfolded dist_norm,rule_format]) 

974 
using as d C d0 by auto 

975 
also have "\<dots> \<le> e * norm (g z  g y)" 

976 
using C by (auto simp add: field_simps) 

977 
finally show "norm (g z  g y  g' (z  y)) \<le> e * norm (g z  g y)" 

978 
by simp 

979 
qed auto 

980 
qed 

981 
have *:"(0::real) < 1 / 2" by auto 

982 
guess d using lem1[rule_format,OF *] .. note d=this 

983 
def B\<equiv>"C*2" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

984 
have "B>0" unfolding B_def using C by auto 
44123  985 
have lem2:"\<forall>z. norm(z  y) < d \<longrightarrow> norm(g z  g y) \<le> B * norm(z  y)" 
986 
proof(rule,rule) case goal1 

987 
have "norm (g z  g y) \<le> norm(g' (z  y)) + norm ((g z  g y)  g'(z  y))" 

988 
by(rule norm_triangle_sub) 

989 
also have "\<dots> \<le> norm(g' (z  y)) + 1 / 2 * norm (g z  g y)" 

990 
apply(rule add_left_mono) using d and goal1 by auto 

991 
also have "\<dots> \<le> norm (z  y) * C + 1 / 2 * norm (g z  g y)" 

992 
apply(rule add_right_mono) using C by auto 

993 
finally show ?case unfolding B_def by(auto simp add:field_simps) 

994 
qed 

995 
show ?thesis unfolding has_derivative_at_alt 

996 
proof(rule,rule assms,rule,rule) case goal1 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

997 
hence *:"e/B >0" applyapply(rule divide_pos_pos) using `B>0` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

998 
guess d' using lem1[rule_format,OF *] .. note d'=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

999 
guess k using real_lbound_gt_zero[OF d[THEN conjunct1] d'[THEN conjunct1]] .. note k=this 
44123  1000 
show ?case 
1001 
apply(rule_tac x=k in exI,rule) defer 

1002 
proof(rule,rule) 

1003 
fix z assume as:"norm(z  y) < k" 

1004 
hence "norm (g z  g y  g' (z  y)) \<le> e / B * norm(g z  g y)" 

1005 
using d' k by auto 

1006 
also have "\<dots> \<le> e * norm(z  y)" 

1007 
unfolding times_divide_eq_left pos_divide_le_eq[OF `B>0`] 

1008 
using lem2[THEN spec[where x=z]] using k as using `e>0` 

1009 
by (auto simp add: field_simps) 

1010 
finally show "norm (g z  g y  g' (z  y)) \<le> e * norm (z  y)" 

1011 
by simp qed(insert k, auto) 

1012 
qed 

1013 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1014 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

1015 
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 HOLlight)
hoelzl
parents:
diff
changeset

1016 

44123  1017 
lemma has_derivative_inverse_basic_x: 
1018 
fixes f::"'b::euclidean_space \<Rightarrow> 'c::euclidean_space" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1019 
assumes "(f has_derivative f') (at x)" "bounded_linear g'" "g' o f' = id" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1020 
"continuous (at (f x)) g" "g(f x) = x" "open t" "f x \<in> t" "\<forall>y\<in>t. f(g y) = y" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1021 
shows "(g has_derivative g') (at (f(x)))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1022 
apply(rule has_derivative_inverse_basic) using assms by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1023 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

1024 
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 HOLlight)
hoelzl
parents:
diff
changeset

1025 

44123  1026 
lemma has_derivative_inverse_dieudonne: 
1027 
fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1028 
assumes "open s" "open (f ` s)" "continuous_on s f" "continuous_on (f ` s) g" "\<forall>x\<in>s. g(f x) = x" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1029 
(**) "x\<in>s" "(f has_derivative f') (at x)" "bounded_linear g'" "g' o f' = id" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1030 
shows "(g has_derivative g') (at (f x))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1031 
apply(rule has_derivative_inverse_basic_x[OF assms(79) _ _ assms(2)]) 
44123  1032 
using assms(36) unfolding continuous_on_eq_continuous_at[OF assms(1)] 
1033 
continuous_on_eq_continuous_at[OF assms(2)] by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1034 

44124
4c2a61a897d8
Derivative.thy: more sensible subsection headings
huffman
parents:
44123
diff
changeset

1035 
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 HOLlight)
hoelzl
parents:
diff
changeset

1036 

44123  1037 
lemma has_derivative_inverse: 
1038 
fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1039 
assumes "compact s" "x \<in> s" "f x \<in> interior(f ` s)" "continuous_on s f" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1040 
"\<forall>y\<in>s. g(f y) = y" "(f has_derivative f') (at x)" "bounded_linear g'" "g' \<circ> f' = id" 
44123  1041 
shows "(g has_derivative g') (at (f x))" 
1042 
proof 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1043 
{ fix y assume "y\<in>interior (f ` s)" 
44123  1044 
then obtain x where "x\<in>s" and *:"y = f x" 
1045 
unfolding image_iff using interior_subset by auto 

1046 
have "f (g y) = y" unfolding * and assms(5)[rule_format,OF `x\<in>s`] .. 

1047 
} note * = this 

1048 
show ?thesis 

1049 
apply(rule has_derivative_inverse_basic_x[OF assms(68)]) 

1050 
apply(rule continuous_on_interior[OF _ assms(3)]) 

44647
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44568
diff
changeset

1051 
apply(rule continuous_on_inv[OF assms(4,1)]) 
44123  1052 
apply(rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+ 
1053 
by(rule, rule *, assumption) 

1054 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1055 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1056 
subsection {* Proving surjectivity via Brouwer fixpoint theorem. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1057 

44123  1058 
lemma brouwer_surjective: 
1059 
fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'n" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1060 
assumes "compact t" "convex t" "t \<noteq> {}" "continuous_on t f" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1061 
"\<forall>x\<in>s. \<forall>y\<in>t. x + (y  f y) \<in> t" "x\<in>s" 
44123  1062 
shows "\<exists>y\<in>t. f y = x" 
1063 
proof 

1064 
have *:"\<And>x y. f y = x \<longleftrightarrow> x + (y  f y) = y" 

1065 
by(auto simp add:algebra_simps) 

1066 
show ?thesis 

1067 
unfolding * 

1068 
apply(rule brouwer[OF assms(13), of "\<lambda>y. x + (y  f y)"]) 

1069 
apply(rule continuous_on_intros assms)+ using assms(46) by auto 

1070 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1071 

44123  1072 
lemma brouwer_surjective_cball: 
1073 
fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'n" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1074 
assumes "0 < e" "continuous_on (cball a e) f" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1075 
"\<forall>x\<in>s. \<forall>y\<in>cball a e. x + (y  f y) \<in> cball a e" "x\<in>s" 
44123  1076 
shows "\<exists>y\<in>cball a e. f y = x" 
1077 
apply(rule brouwer_surjective) 

1078 
apply(rule compact_cball convex_cball)+ 

1079 
unfolding cball_eq_empty using assms by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1080 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1081 
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 HOLlight)
hoelzl
parents:
diff
changeset

1082 

44123  1083 
lemma sussmann_open_mapping: 
1084 
fixes f::"'a::euclidean_space \<Rightarrow> 'b::ordered_euclidean_space" 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1085 
assumes "open s" "continuous_on s f" "x \<in> s" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1086 
"(f has_derivative f') (at x)" "bounded_linear g'" "f' \<circ> g' = id" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

1087 
"t \<subseteq> s" "x \<in> interior t" 
44123  1088 
shows "f x \<in> interior (f ` t)" 
1089 
proof 

1090 
interpret f':bounded_linear f' 

1091 
using assms unfolding has_derivative_def by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1092 
interpret g':bounded_linear g' using assms by auto 
44123  1093 
guess B using bounded_linear.pos_bounded[OF assms(5)] .. note B=this 
1094 
hence *:"1/(2*B)>0" by (auto intro!: divide_pos_pos) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1095 
guess e0 using assms(4)[unfolded has_derivative_at_alt,THEN conjunct2,rule_format,OF *] .. note e0=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1096 
guess e1 using assms(8)[unfolded mem_interior_cball] .. note e1=this 
44123  1097 
have *:"0<e0/B" "0<e1/B" 
1098 
apply(rule_tac[!] divide_pos_pos) using e0 e1 B by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1099 
guess e using real_lbound_gt_zero[OF *] .. note e=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1100 
have "\<forall>z\<in>cball (f x) (e/2). \<exists>y\<in>cball (f x) e. f (x + g' (y  f x)) = z" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1101 
apply(rule,rule brouwer_surjective_cball[where s="cball (f x) (e/2)"]) 
44123  1102 
prefer 3 apply(rule,rule) 
1103 
proof 

1104 
show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y  f x)))" 

1105 
unfolding g'.diff 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1106 
apply(rule continuous_on_compose[of _ _ f, unfolded o_def]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1107 
apply(rule continuous_on_intros linear_continuous_on[OF assms(5)])+ 
44123  1108 
apply(rule continuous_on_subset[OF assms(2)]) 
1109 
apply(rule,unfold image_iff,erule bexE) 

1110 
proof 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1111 
fix y z assume as:"y \<in>cball (f x) e" "z = x + (g' y  g' (f x))" 
44123  1112 
have "dist x z = norm (g' (f x)  g' y)" 
1113 
unfolding as(2) and dist_norm by auto 

1114 
also have "\<dots> \<le> norm (f x  y) * B" 

1115 
unfolding g'.diff[THEN sym] using B by auto 

1116 
also have "\<dots> \<le> e * B" 

1117 
using as(1)[unfolded mem_cball dist_norm] using B by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1118 
also have "\<dots> \<le> e1" using e unfolding less_divide_eq using B by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1119 
finally have "z\<in>cball x e1" unfolding mem_cball by force 
44123  1120 
thus "z \<in> s" using e1 assms(7) by auto 
1121 
qed 

1122 
next 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1123 
fix y z assume as:"y \<in> cball (f x) (e / 2)" "z \<in> cball (f x) e" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1124 
have "norm (g' (z  f x)) \<le> norm (z  f x) * B" using B by auto 
44123  1125 
also have "\<dots> \<le> e * B" apply(rule mult_right_mono) 
1126 
using as(2)[unfolded mem_cball dist_norm] and B 

1127 
unfolding norm_minus_commute by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1128 
also have "\<dots> < e0" using e and B unfolding less_divide_eq by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1129 
finally have *:"norm (x + g' (z  f x)  x) < e0" by auto 
44123  1130 
have **:"f x + f' (x + g' (z  f x)  x) = z" 
1131 
using assms(6)[unfolded o_def id_def,THEN cong] by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1132 
have "norm (f x  (y + (z  f (x + g' (z  f x))))) \<le> norm (f (x + g' (z  f x))  z) + norm (f x  y)" 
44123  1133 
using norm_triangle_ineq[of "f (x + g'(z  f x))  z" "f x  y"] 
1134 
by (auto simp add: algebra_simps) 

1135 
also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z  f x)) + norm (f x  y)" 

1136 
using e0[THEN conjunct2,rule_format,OF *] 

1137 
unfolding algebra_simps ** by auto 

1138 
also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z  f x)) + e/2" 

1139 
using as(1)[unfolded mem_cball dist_norm] by auto 

1140 
also have "\<dots> \<le> 1 / (B * 2) * B * norm (z  f x) + e/2" 

1141 
using * and B by (auto simp add: field_simps) 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1142 
also have "\<dots> \<le> 1 / 2 * norm (z  f x) + e/2" by auto 
44123  1143 
also have "\<dots> \<le> e/2 + e/2" apply(rule add_right_mono) 
1144 
using as(2)[unfolded mem_cball dist_norm] 

1145 
unfolding norm_minus_commute by auto 

1146 
finally show "y + (z  f (x + g' (z  f x))) \<in> cball (f x) e" 

1147 
unfolding mem_cball dist_norm by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1148 
qed(insert e, auto) note lem = this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1149 
show ?thesis unfolding mem_interior apply(rule_tac x="e/2" in exI) 
44123  1150 
apply(rule,rule divide_pos_pos) prefer 3 
1151 
proof 

1152 
fix y assume "y \<in> ball (f x) (e/2)" 

1153 
hence *:"y\<in>cball (f x) (e/2)" by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1154 
guess z using lem[rule_format,OF *] .. note z=this 
44123  1155 
hence "norm (g' (z  f x)) \<le> norm (z  f x) * B" 
1156 
using B by (auto simp add: field_simps) 

1157 
also have "\<dots> \<le> e * B" 

1158 
apply (rule mult_right_mono) using z(1) 

1159 
unfolding mem_cball dist_norm norm_minus_commute using B by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1160 
also have "\<dots> \<le> e1" using e B unfolding less_divide_eq by auto 
44123  1161 
finally have "x + g'(z  f x) \<in> t" apply 
1162 
apply(rule e1[THEN conjunct2,unfolded subset_eq,rule_format]) 

36587  1163 
unfolding mem_cball dist_norm by auto 
44123  1164 
thus "y \<in> f ` t" using z by auto 
1165 
qed(insert e, auto) 

1166 
qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1167 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1168 
text {* Hence the following eccentric variant of the inverse function theorem. *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1169 
(* This has no continuity assumptions, but we do need the inverse function. *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1170 
(* We could put f' o g = I but this happens to fit with the minimal linear *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1171 
(* algebra theory I've set up so far. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1172 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

1173 
(* 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

1174 

44123
