author  paulson <lp15@cam.ac.uk> 
Sun, 20 May 2018 22:10:21 +0100  
changeset 68241  39a311f50344 
parent 68239  0764ee22a4d1 
child 68527  2f4e2aab190a 
permissions  rwrr 
63627  1 
(* Title: HOL/Analysis/Derivative.thy 
53781  2 
Author: John Harrison 
68239  3 
Author: Robert Himmelmann, TU Muenchen (translation from HOL Light); tidied by LCP 
36350  4 
*) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

5 

60420  6 
section \<open>Multivariate calculus in Euclidean space\<close> 
33741
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 
62207  9 
imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function 
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 

63938  12 
declare bounded_linear_inner_left [intro] 
61915
e9812a95d108
theory for type of bounded linear functions; differentiation under the integral sign
immler
parents:
61907
diff
changeset

13 

56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

14 
declare has_derivative_bounded_linear[dest] 
44137  15 

60420  16 
subsection \<open>Derivatives\<close> 
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

17 

400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

18 
lemma has_derivative_add_const: 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

19 
"(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net" 
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

20 
by (intro derivative_eq_intros) auto 
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

21 

53781  22 

67968  23 
subsection \<open>Derivative with composed bilinear function\<close> 
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

24 

60420  25 
text \<open>More explicit epsilondelta forms.\<close> 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

26 

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

27 
lemma has_derivative_within': 
53781  28 
"(f has_derivative f')(at x within s) \<longleftrightarrow> 
29 
bounded_linear f' \<and> 

30 
(\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm (x'  x) \<and> norm (x'  x) < d \<longrightarrow> 

31 
norm (f x'  f x  f'(x'  x)) / norm (x'  x) < e)" 

36587  32 
unfolding has_derivative_within Lim_within dist_norm 
53781  33 
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

34 

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

35 
lemma has_derivative_at': 
68239  36 
"(f has_derivative f') (at x) 
37 
\<longleftrightarrow> bounded_linear f' \<and> 

38 
(\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x'  x) \<and> norm (x'  x) < d \<longrightarrow> 

39 
norm (f x'  f x  f'(x'  x)) / norm (x'  x) < e)" 

40 
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

41 

67979
53323937ee25
new material about vec, real^1, etc.
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset

42 
lemma has_derivative_at_withinI: 
53781  43 
"(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)" 
44 
unfolding has_derivative_within' has_derivative_at' 

45 
by blast 

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

46 

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

47 
lemma has_derivative_within_open: 
68095
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

48 
"a \<in> S \<Longrightarrow> open S \<Longrightarrow> 
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

49 
(f has_derivative f') (at a within S) \<longleftrightarrow> (f has_derivative f') (at a)" 
37730  50 
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

51 

43338  52 
lemma has_derivative_right: 
53781  53 
fixes f :: "real \<Rightarrow> real" 
54 
and y :: "real" 

67399  55 
shows "(f has_derivative (( * ) y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow> 
68239  56 
((\<lambda>t. (f x  f t) / (x  t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))" 
43338  57 
proof  
61973  58 
have "((\<lambda>t. (f t  (f x + y * (t  x))) / \<bar>t  x\<bar>) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow> 
59 
((\<lambda>t. (f t  f x) / (t  x)  y) \<longlongrightarrow> 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

60 
by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib) 
61973  61 
also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t  f x) / (t  x)) \<longlongrightarrow> y) (at x within ({x<..} \<inter> I))" 
43338  62 
by (simp add: Lim_null[symmetric]) 
61973  63 
also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x  f t) / (x  t)) \<longlongrightarrow> y) (at x within ({x<..} \<inter> I))" 
44140
2c10c35dd4be
remove several redundant and unused theorems about derivatives
huffman
parents:
44137
diff
changeset

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

66 
by (simp add: bounded_linear_mult_right has_derivative_within) 
43338  67 
qed 
68 

60420  69 
subsubsection \<open>Caratheodory characterization\<close> 
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

70 

6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

71 
lemma DERIV_caratheodory_within: 
68095
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

72 
"(f has_field_derivative l) (at x within S) \<longleftrightarrow> 
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

73 
(\<exists>g. (\<forall>z. f z  f x = g z * (z  x)) \<and> continuous (at x within S) g \<and> g x = l)" 
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

74 
(is "?lhs = ?rhs") 
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

75 
proof 
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
56151
diff
changeset

76 
assume ?lhs 
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

77 
show ?rhs 
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

78 
proof (intro exI conjI) 
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

79 
let ?g = "(%z. if z = x then l else (f z  f x) / (zx))" 
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

80 
show "\<forall>z. f z  f x = ?g z * (zx)" by simp 
68095
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

81 
show "continuous (at x within S) ?g" using \<open>?lhs\<close> 
68239  82 
by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within) 
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

83 
show "?g x = l" by simp 
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

84 
qed 
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

85 
next 
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

86 
assume ?rhs 
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

87 
then obtain g where 
68095
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

88 
"(\<forall>z. f z  f x = g z * (zx))" and "continuous (at x within S) g" and "g x = l" by blast 
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
56151
diff
changeset

89 
thus ?lhs 
68239  90 
by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within) 
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

91 
qed 
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

92 

60420  93 
subsection \<open>Differentiability\<close> 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

94 

53781  95 
definition 
96 
differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" 

56182
528fae0816ea
update syntax of has_*derivative to infix 50; fixed proofs
hoelzl
parents:
56181
diff
changeset

97 
(infix "differentiable'_on" 50) 
53781  98 
where "f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable (at x within s))" 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

99 

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

100 
lemma differentiableI: "(f has_derivative f') net \<Longrightarrow> f differentiable net" 
53781  101 
unfolding differentiable_def 
102 
by auto 

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

103 

62533
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

104 
lemma differentiable_onD: "\<lbrakk>f differentiable_on S; x \<in> S\<rbrakk> \<Longrightarrow> f differentiable (at x within S)" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

105 
using differentiable_on_def by blast 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset

106 

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

107 
lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)" 
53781  108 
unfolding differentiable_def 
67979
53323937ee25
new material about vec, real^1, etc.
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset

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

111 

61104
3c2d4636cebc
new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents:
61076
diff
changeset

112 
lemma differentiable_at_imp_differentiable_on: 
3c2d4636cebc
new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents:
61076
diff
changeset

113 
"(\<And>x. x \<in> s \<Longrightarrow> f differentiable at x) \<Longrightarrow> f differentiable_on s" 
3c2d4636cebc
new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents:
61076
diff
changeset

114 
by (metis differentiable_at_withinI differentiable_on_def) 
3c2d4636cebc
new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents:
61076
diff
changeset

115 

3c2d4636cebc
new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents:
61076
diff
changeset

116 
corollary differentiable_iff_scaleR: 
3c2d4636cebc
new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents:
61076
diff
changeset

117 
fixes f :: "real \<Rightarrow> 'a::real_normed_vector" 
3c2d4636cebc
new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents:
61076
diff
changeset

118 
shows "f differentiable F \<longleftrightarrow> (\<exists>d. (f has_derivative (\<lambda>x. x *\<^sub>R d)) F)" 
3c2d4636cebc
new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents:
61076
diff
changeset

119 
by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR) 
3c2d4636cebc
new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents:
61076
diff
changeset

120 

44123  121 
lemma differentiable_on_eq_differentiable_at: 
53781  122 
"open s \<Longrightarrow> f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x)" 
44123  123 
unfolding differentiable_on_def 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51478
diff
changeset

124 
by (metis 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

125 

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

126 
lemma differentiable_transform_within: 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61975
diff
changeset

127 
assumes "f differentiable (at x within s)" 
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61975
diff
changeset

128 
and "0 < d" 
53781  129 
and "x \<in> s" 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61975
diff
changeset

130 
and "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'" 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

131 
shows "g differentiable (at x within s)" 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61975
diff
changeset

132 
using assms has_derivative_transform_within unfolding differentiable_def 
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61975
diff
changeset

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

134 

63469
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

135 
lemma differentiable_on_ident [simp, derivative_intros]: "(\<lambda>x. x) differentiable_on S" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

136 
by (simp add: differentiable_at_imp_differentiable_on) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

137 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

138 
lemma differentiable_on_id [simp, derivative_intros]: "id differentiable_on S" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

139 
by (simp add: id_def) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

140 

63955  141 
lemma differentiable_on_const [simp, derivative_intros]: "(\<lambda>z. c) differentiable_on S" 
142 
by (simp add: differentiable_on_def) 

143 

144 
lemma differentiable_on_mult [simp, derivative_intros]: 

145 
fixes f :: "'M::real_normed_vector \<Rightarrow> 'a::real_normed_algebra" 

146 
shows "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) differentiable_on S" 

68239  147 
unfolding differentiable_on_def differentiable_def 
63955  148 
using differentiable_def differentiable_mult by blast 
149 

63469
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

150 
lemma differentiable_on_compose: 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

151 
"\<lbrakk>g differentiable_on S; f differentiable_on (g ` S)\<rbrakk> \<Longrightarrow> (\<lambda>x. f (g x)) differentiable_on S" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

152 
by (simp add: differentiable_in_compose differentiable_on_def) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

153 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

154 
lemma bounded_linear_imp_differentiable_on: "bounded_linear f \<Longrightarrow> f differentiable_on S" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

155 
by (simp add: differentiable_on_def bounded_linear_imp_differentiable) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

156 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

157 
lemma linear_imp_differentiable_on: 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

158 
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

159 
shows "linear f \<Longrightarrow> f differentiable_on S" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

160 
by (simp add: differentiable_on_def linear_imp_differentiable) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

161 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

162 
lemma differentiable_on_minus [simp, derivative_intros]: 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

163 
"f differentiable_on S \<Longrightarrow> (\<lambda>z. (f z)) differentiable_on S" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

164 
by (simp add: differentiable_on_def) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

165 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

166 
lemma differentiable_on_add [simp, derivative_intros]: 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

167 
"\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z + g z) differentiable_on S" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

168 
by (simp add: differentiable_on_def) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

169 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

170 
lemma differentiable_on_diff [simp, derivative_intros]: 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

171 
"\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z  g z) differentiable_on S" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

172 
by (simp add: differentiable_on_def) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

173 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

174 
lemma differentiable_on_inverse [simp, derivative_intros]: 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

175 
fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

176 
shows "f differentiable_on S \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> f x \<noteq> 0) \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable_on S" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

177 
by (simp add: differentiable_on_def) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

178 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

179 
lemma differentiable_on_scaleR [derivative_intros, simp]: 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

180 
"\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) differentiable_on S" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

181 
unfolding differentiable_on_def 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

182 
by (blast intro: differentiable_scaleR) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

183 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

184 
lemma has_derivative_sqnorm_at [derivative_intros, simp]: 
68239  185 
"((\<lambda>x. (norm x)\<^sup>2) has_derivative (\<lambda>x. 2 *\<^sub>R (a \<bullet> x))) (at a)" 
186 
using bounded_bilinear.FDERIV [of "(\<bullet>)" id id a _ id id] 

187 
by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner) 

63469
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

188 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

189 
lemma differentiable_sqnorm_at [derivative_intros, simp]: 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

190 
fixes a :: "'a :: {real_normed_vector,real_inner}" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

191 
shows "(\<lambda>x. (norm x)\<^sup>2) differentiable (at a)" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

192 
by (force simp add: differentiable_def intro: has_derivative_sqnorm_at) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

193 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

194 
lemma differentiable_on_sqnorm [derivative_intros, simp]: 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

195 
fixes S :: "'a :: {real_normed_vector,real_inner} set" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

196 
shows "(\<lambda>x. (norm x)\<^sup>2) differentiable_on S" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

197 
by (simp add: differentiable_at_imp_differentiable_on) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

198 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

199 
lemma differentiable_norm_at [derivative_intros, simp]: 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

200 
fixes a :: "'a :: {real_normed_vector,real_inner}" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

201 
shows "a \<noteq> 0 \<Longrightarrow> norm differentiable (at a)" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

202 
using differentiableI has_derivative_norm by blast 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

203 

b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

204 
lemma differentiable_on_norm [derivative_intros, simp]: 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

205 
fixes S :: "'a :: {real_normed_vector,real_inner} set" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

206 
shows "0 \<notin> S \<Longrightarrow> norm differentiable_on S" 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

207 
by (metis differentiable_at_imp_differentiable_on differentiable_norm_at) 
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

208 

53781  209 

60420  210 
subsection \<open>Frechet derivative and Jacobian matrix\<close> 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

211 

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

212 
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

213 

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

214 
lemma frechet_derivative_works: 
53781  215 
"f differentiable net \<longleftrightarrow> (f has_derivative (frechet_derivative f net)) net" 
216 
unfolding frechet_derivative_def differentiable_def 

217 
unfolding some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] .. 

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

218 

56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
56151
diff
changeset

219 
lemma linear_frechet_derivative: "f differentiable net \<Longrightarrow> linear (frechet_derivative f net)" 
44123  220 
unfolding frechet_derivative_works has_derivative_def 
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

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

222 

53781  223 

60420  224 
subsection \<open>Differentiability implies continuity\<close> 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

225 

44123  226 
lemma differentiable_imp_continuous_within: 
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

227 
"f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f" 
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
56151
diff
changeset

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

229 

44123  230 
lemma differentiable_imp_continuous_on: 
231 
"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

232 
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

233 
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

234 

44123  235 
lemma differentiable_on_subset: 
236 
"f differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable_on s" 

53781  237 
unfolding differentiable_on_def 
238 
using differentiable_within_subset 

239 
by blast 

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

240 

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

241 
lemma differentiable_on_empty: "f differentiable_on {}" 
53781  242 
unfolding differentiable_on_def 
243 
by auto 

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

244 

67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

245 
lemma has_derivative_continuous_on: 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

246 
"(\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x within s)) \<Longrightarrow> continuous_on s f" 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

247 
by (auto intro!: differentiable_imp_continuous_on differentiableI simp: differentiable_on_def) 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

248 

60420  249 
text \<open>Results about neighborhoods filter.\<close> 
56151  250 

251 
lemma eventually_nhds_metric_le: 

252 
"eventually P (nhds a) = (\<exists>d>0. \<forall>x. dist x a \<le> d \<longrightarrow> P x)" 

253 
unfolding eventually_nhds_metric by (safe, rule_tac x="d / 2" in exI, auto) 

254 

255 
lemma le_nhds: "F \<le> nhds a \<longleftrightarrow> (\<forall>S. open S \<and> a \<in> S \<longrightarrow> eventually (\<lambda>x. x \<in> S) F)" 

61810  256 
unfolding le_filter_def eventually_nhds by (fast elim: eventually_mono) 
56151  257 

258 
lemma le_nhds_metric: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a < e) F)" 

61810  259 
unfolding le_filter_def eventually_nhds_metric by (fast elim: eventually_mono) 
56151  260 

261 
lemma le_nhds_metric_le: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a \<le> e) F)" 

61810  262 
unfolding le_filter_def eventually_nhds_metric_le by (fast elim: eventually_mono) 
56151  263 

60420  264 
text \<open>Several results are easier using a "multipliedout" variant. 
265 
(I got this idea from Dieudonne's proof of the chain rule).\<close> 

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

266 

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

267 
lemma has_derivative_within_alt: 
53781  268 
"(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and> 
269 
(\<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))" 

56151  270 
unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap 
59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59558
diff
changeset

271 
eventually_at dist_norm diff_diff_eq 
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

272 
by (force simp add: linear_0 bounded_linear.linear pos_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

273 

56320  274 
lemma has_derivative_within_alt2: 
275 
"(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and> 

276 
(\<forall>e>0. eventually (\<lambda>y. norm (f y  f x  f' (y  x)) \<le> e * norm (y  x)) (at x within s))" 

277 
unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap 

59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59558
diff
changeset

278 
eventually_at dist_norm diff_diff_eq 
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

279 
by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq) 
56320  280 

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

281 
lemma has_derivative_at_alt: 
53781  282 
"(f has_derivative f') (at x) \<longleftrightarrow> 
283 
bounded_linear f' \<and> 

284 
(\<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))" 

285 
using has_derivative_within_alt[where s=UNIV] 

286 
by simp 

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

287 

53781  288 

60420  289 
subsection \<open>The chain rule\<close> 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

290 

56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

291 
lemma diff_chain_within[derivative_intros]: 
44123  292 
assumes "(f has_derivative f') (at x within s)" 
53781  293 
and "(g has_derivative g') (at (f x) within (f ` s))" 
294 
shows "((g \<circ> f) has_derivative (g' \<circ> f'))(at x within s)" 

56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
56151
diff
changeset

295 
using has_derivative_in_compose[OF assms] 
53781  296 
by (simp add: comp_def) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

297 

56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

298 
lemma diff_chain_at[derivative_intros]: 
53781  299 
"(f has_derivative f') (at x) \<Longrightarrow> 
300 
(g has_derivative g') (at (f x)) \<Longrightarrow> ((g \<circ> f) has_derivative (g' \<circ> f')) (at x)" 

56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
56151
diff
changeset

301 
using has_derivative_compose[of f f' x UNIV g g'] 
53781  302 
by (simp add: comp_def) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

303 

68095
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

304 
lemma has_vector_derivative_within_open: 
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

305 
"a \<in> S \<Longrightarrow> open S \<Longrightarrow> 
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

306 
(f has_vector_derivative f') (at a within S) \<longleftrightarrow> (f has_vector_derivative f') (at a)" 
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

307 
by (simp only: at_within_interior interior_open) 
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

308 

64394  309 
lemma field_vector_diff_chain_within: 
68095
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

310 
assumes Df: "(f has_vector_derivative f') (at x within S)" 
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

311 
and Dg: "(g has_field_derivative g') (at (f x) within f ` S)" 
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

312 
shows "((g \<circ> f) has_vector_derivative (f' * g')) (at x within S)" 
64394  313 
using diff_chain_within[OF Df[unfolded has_vector_derivative_def] 
314 
Dg [unfolded has_field_derivative_def]] 

315 
by (auto simp: o_def mult.commute has_vector_derivative_def) 

316 

317 
lemma vector_derivative_diff_chain_within: 

68095
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

318 
assumes Df: "(f has_vector_derivative f') (at x within S)" 
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

319 
and Dg: "(g has_derivative g') (at (f x) within f`S)" 
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

320 
shows "((g \<circ> f) has_vector_derivative (g' f')) (at x within S)" 
64394  321 
using diff_chain_within[OF Df[unfolded has_vector_derivative_def] Dg] 
322 
linear.scaleR[OF has_derivative_linear[OF Dg]] 

323 
unfolding has_vector_derivative_def o_def 

324 
by (auto simp: o_def mult.commute has_vector_derivative_def) 

325 

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

326 

60420  327 
subsection \<open>Composition rules stated just for differentiability\<close> 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

328 

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

329 
lemma differentiable_chain_at: 
53781  330 
"f differentiable (at x) \<Longrightarrow> 
331 
g differentiable (at (f x)) \<Longrightarrow> (g \<circ> f) differentiable (at x)" 

332 
unfolding differentiable_def 

333 
by (meson diff_chain_at) 

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

334 

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

335 
lemma differentiable_chain_within: 
68095
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

336 
"f differentiable (at x within S) \<Longrightarrow> 
4fa3e63ecc7e
starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents:
68073
diff
changeset

337 
g differentiable (at(f x) within (f ` S)) \<Longrightarrow> (g \<circ> f) differentiable (at x within S)" 
53781  338 
unfolding differentiable_def 
339 
by (meson diff_chain_within) 

340 

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

341 

60420  342 
subsection \<open>Uniqueness of derivative\<close> 
37730  343 

56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

344 

60420  345 
text \<open> 
37730  346 
The general result is a bit messy because we need approachability of the 
347 
limit point from any direction. But OK for nontrivial intervals etc. 

60420  348 
\<close> 
51363
d4d00c804645
changed has_derivative_intros into a named theorems collection
hoelzl
parents:
50939
diff
changeset

349 

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

68239  352 
assumes 1: "(f has_derivative f') (at x within S)" 
353 
and 2: "(f has_derivative f'') (at x within S)" 

354 
and S: "\<And>i e. \<lbrakk>i\<in>Basis; e>0\<rbrakk> \<Longrightarrow> \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> S" 

44123  355 
shows "f' = f''" 
53781  356 
proof  
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

357 
note as = assms(1,2)[unfolded has_derivative_def] 
44123  358 
then interpret f': bounded_linear f' by auto 
359 
from as interpret f'': bounded_linear f'' by auto 

68058  360 
have "x islimpt S" unfolding islimpt_approachable 
68239  361 
proof (intro allI impI) 
53781  362 
fix e :: real 
363 
assume "e > 0" 

68058  364 
obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> S" 
60420  365 
using assms(3) SOME_Basis \<open>e>0\<close> by blast 
68058  366 
then show "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" 
68239  367 
by (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI) (auto simp: dist_norm SOME_Basis nonzero_Basis) qed 
68058  368 
then have *: "netlimit (at x within S) = x" 
68239  369 
by (simp add: Lim_ident_at trivial_limit_within) 
53781  370 
show ?thesis 
68058  371 
proof (rule linear_eq_stdbasis) 
372 
show "linear f'" "linear f''" 

373 
unfolding linear_conv_bounded_linear using as by auto 

374 
next 

53781  375 
fix i :: 'a 
376 
assume i: "i \<in> Basis" 

63040  377 
define e where "e = norm (f' i  f'' i)" 
68058  378 
show "f' i = f'' i" 
379 
proof (rule ccontr) 

380 
assume "f' i \<noteq> f'' i" 

381 
then have "e > 0" 

382 
unfolding e_def by auto 

383 
obtain d where d: 

384 
"0 < d" 

385 
"(\<And>y. y\<in>S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> 

386 
dist ((f y  f x  f' (y  x)) /\<^sub>R norm (y  x)  

387 
(f y  f x  f'' (y  x)) /\<^sub>R norm (y  x)) (0  0) < e)" 

388 
using tendsto_diff [OF as(1,2)[THEN conjunct2]] 

389 
unfolding * Lim_within 

390 
using \<open>e>0\<close> by blast 

391 
obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> S" 

392 
using assms(3) i d(1) by blast 

393 
have *: "norm ( ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) = 

61945  394 
norm ((1 / \<bar>c\<bar>) *\<^sub>R ( (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))" 
68058  395 
unfolding scaleR_right_distrib by auto 
396 
also have "\<dots> = norm ((1 / \<bar>c\<bar>) *\<^sub>R (c *\<^sub>R ( (f' i) + f'' i)))" 

397 
unfolding f'.scaleR f''.scaleR 

398 
unfolding scaleR_right_distrib scaleR_minus_right 

399 
by auto 

400 
also have "\<dots> = e" 

401 
unfolding e_def 

402 
using c(1) 

403 
using norm_minus_cancel[of "f' i  f'' i"] 

404 
by auto 

405 
finally show False 

406 
using c 

407 
using d(2)[of "x + c *\<^sub>R i"] 

408 
unfolding dist_norm 

409 
unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff 

410 
scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib 

411 
using i 

412 
by (auto simp: inverse_eq_divide) 

413 
qed 

44123  414 
qed 
415 
qed 

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

416 

44123  417 
lemma frechet_derivative_unique_within_closed_interval: 
56188  418 
fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" 
68239  419 
assumes ab: "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i" 
420 
and x: "x \<in> cbox a b" 

56188  421 
and "(f has_derivative f' ) (at x within cbox a b)" 
422 
and "(f has_derivative f'') (at x within cbox a b)" 

44123  423 
shows "f' = f''" 
68239  424 
proof (rule frechet_derivative_unique_within) 
53781  425 
fix e :: real 
426 
fix i :: 'a 

427 
assume "e > 0" and i: "i \<in> Basis" 

56188  428 
then show "\<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> cbox a b" 
53781  429 
proof (cases "x\<bullet>i = a\<bullet>i") 
430 
case True 

68239  431 
with ab[of i] \<open>e>0\<close> x i show ?thesis 
432 
by (rule_tac x="(min (b\<bullet>i  a\<bullet>i) e) / 2" in exI) 

433 
(auto simp add: mem_box field_simps inner_simps inner_Basis) 

53781  434 
next 
435 
case False 

436 
moreover have "a \<bullet> i < x \<bullet> i" 

68239  437 
using False i mem_box(2) x by force 
44123  438 
moreover { 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset

439 
have "a \<bullet> i * 2 + min (x \<bullet> i  a \<bullet> i) e \<le> a\<bullet>i *2 + x\<bullet>i  a\<bullet>i" 
44123  440 
by auto 
53781  441 
also have "\<dots> = a\<bullet>i + x\<bullet>i" 
442 
by auto 

443 
also have "\<dots> \<le> 2 * (x\<bullet>i)" 

68239  444 
using \<open>a \<bullet> i < x \<bullet> i\<close> by auto 
53781  445 
finally have "a \<bullet> i * 2 + min (x \<bullet> i  a \<bullet> i) e \<le> x \<bullet> i * 2" 
446 
by auto 

44123  447 
} 
53781  448 
moreover have "min (x \<bullet> i  a \<bullet> i) e \<ge> 0" 
68239  449 
by (simp add: \<open>0 < e\<close> \<open>a \<bullet> i < x \<bullet> i\<close> less_eq_real_def) 
53781  450 
then have "x \<bullet> i * 2 \<le> b \<bullet> i * 2 + min (x \<bullet> i  a \<bullet> i) e" 
68239  451 
using i mem_box(2) x by force 
44123  452 
ultimately show ?thesis 
68239  453 
using ab[of i] \<open>e>0\<close> x i 
454 
by (rule_tac x=" (min (x\<bullet>i  a\<bullet>i) e) / 2" in exI) 

455 
(auto simp add: mem_box field_simps inner_simps inner_Basis) 

44123  456 
qed 
68239  457 
qed (use assms in auto) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

458 

44123  459 
lemma frechet_derivative_unique_within_open_interval: 
56188  460 
fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" 
68239  461 
assumes x: "x \<in> box a b" 
462 
and f: "(f has_derivative f' ) (at x within box a b)" "(f has_derivative f'') (at x within box a b)" 

37650  463 
shows "f' = f''" 
464 
proof  

68239  465 
have "at x within box a b = at x" 
466 
by (metis x at_within_interior interior_open open_box) 

467 
with f show "f' = f''" 

468 
by (simp add: has_derivative_unique) 

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

470 

37730  471 
lemma frechet_derivative_at: 
53781  472 
"(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)" 
68239  473 
using differentiable_def frechet_derivative_works has_derivative_unique by blast 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

474 

56188  475 
lemma frechet_derivative_within_cbox: 
476 
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" 

68239  477 
assumes "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i" 
56188  478 
and "x \<in> cbox a b" 
479 
and "(f has_derivative f') (at x within cbox a b)" 

480 
shows "frechet_derivative f (at x within cbox a b) = f'" 

55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

481 
using assms 
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

482 
by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

483 

53781  484 

60420  485 
subsection \<open>The traditional Rolle theorem in one dimension\<close> 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

486 

60420  487 
text \<open>Derivatives of local minima and maxima are zero.\<close> 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

488 

56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

489 
lemma has_derivative_local_min: 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

490 
fixes f :: "'a::real_normed_vector \<Rightarrow> real" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

491 
assumes deriv: "(f has_derivative f') (at x)" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

492 
assumes min: "eventually (\<lambda>y. f x \<le> f y) (at x)" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

493 
shows "f' = (\<lambda>h. 0)" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

494 
proof 
56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

495 
fix h :: 'a 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

496 
interpret f': bounded_linear f' 
56182
528fae0816ea
update syntax of has_*derivative to infix 50; fixed proofs
hoelzl
parents:
56181
diff
changeset

497 
using deriv by (rule has_derivative_bounded_linear) 
56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

498 
show "f' h = 0" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

499 
proof (cases "h = 0") 
68239  500 
case False 
56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

501 
from min obtain d where d1: "0 < d" and d2: "\<forall>y\<in>ball x d. f x \<le> f y" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

502 
unfolding eventually_at by (force simp: dist_commute) 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

503 
have "FDERIV (\<lambda>r. x + r *\<^sub>R h) 0 :> (\<lambda>r. r *\<^sub>R h)" 
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

504 
by (intro derivative_eq_intros) auto 
56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

505 
then have "FDERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> (\<lambda>k. f' (k *\<^sub>R h))" 
56182
528fae0816ea
update syntax of has_*derivative to infix 50; fixed proofs
hoelzl
parents:
56181
diff
changeset

506 
by (rule has_derivative_compose, simp add: deriv) 
56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

507 
then have "DERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> f' h" 
56182
528fae0816ea
update syntax of has_*derivative to infix 50; fixed proofs
hoelzl
parents:
56181
diff
changeset

508 
unfolding has_field_derivative_def by (simp add: f'.scaleR mult_commute_abs) 
60420  509 
moreover have "0 < d / norm h" using d1 and \<open>h \<noteq> 0\<close> by simp 
56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

510 
moreover have "\<forall>y. \<bar>0  y\<bar> < d / norm h \<longrightarrow> f (x + 0 *\<^sub>R h) \<le> f (x + y *\<^sub>R h)" 
60420  511 
using \<open>h \<noteq> 0\<close> by (auto simp add: d2 dist_norm pos_less_divide_eq) 
56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

512 
ultimately show "f' h = 0" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

513 
by (rule DERIV_local_min) 
68239  514 
qed simp 
56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

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

516 

56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

517 
lemma has_derivative_local_max: 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

518 
fixes f :: "'a::real_normed_vector \<Rightarrow> real" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

519 
assumes "(f has_derivative f') (at x)" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

520 
assumes "eventually (\<lambda>y. f y \<le> f x) (at x)" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

521 
shows "f' = (\<lambda>h. 0)" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

522 
using has_derivative_local_min [of "\<lambda>x.  f x" "\<lambda>h.  f' h" "x"] 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

523 
using assms unfolding fun_eq_iff by simp 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

524 

304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

525 
lemma differential_zero_maxmin: 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

526 
fixes f::"'a::real_normed_vector \<Rightarrow> real" 
68239  527 
assumes "x \<in> S" 
528 
and "open S" 

56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

529 
and deriv: "(f has_derivative f') (at x)" 
68239  530 
and mono: "(\<forall>y\<in>S. f y \<le> f x) \<or> (\<forall>y\<in>S. f x \<le> f y)" 
56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

531 
shows "f' = (\<lambda>v. 0)" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

532 
using mono 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

533 
proof 
68239  534 
assume "\<forall>y\<in>S. f y \<le> f x" 
535 
with \<open>x \<in> S\<close> and \<open>open S\<close> have "eventually (\<lambda>y. f y \<le> f x) (at x)" 

56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

536 
unfolding eventually_at_topological by auto 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

537 
with deriv show ?thesis 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

538 
by (rule has_derivative_local_max) 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

539 
next 
68239  540 
assume "\<forall>y\<in>S. f x \<le> f y" 
541 
with \<open>x \<in> S\<close> and \<open>open S\<close> have "eventually (\<lambda>y. f x \<le> f y) (at x)" 

56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

542 
unfolding eventually_at_topological by auto 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

543 
with deriv show ?thesis 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

544 
by (rule has_derivative_local_min) 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

545 
qed 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

546 

304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

547 
lemma differential_zero_maxmin_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

548 
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset

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

551 
and diff: "f differentiable (at x)" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset

552 
shows "(\<Sum>j\<in>Basis. (frechet_derivative f (at x) j \<bullet> k) *\<^sub>R j) = (0::'a)" (is "?D k = 0") 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

553 
proof  
56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

554 
let ?f' = "frechet_derivative f (at x)" 
60420  555 
have "x \<in> ball x e" using \<open>0 < e\<close> by simp 
56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

556 
moreover have "open (ball x e)" by simp 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

557 
moreover have "((\<lambda>x. f x \<bullet> k) has_derivative (\<lambda>h. ?f' h \<bullet> k)) (at x)" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

558 
using bounded_linear_inner_left diff[unfolded frechet_derivative_works] 
56182
528fae0816ea
update syntax of has_*derivative to infix 50; fixed proofs
hoelzl
parents:
56181
diff
changeset

559 
by (rule bounded_linear.has_derivative) 
56133
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

560 
ultimately have "(\<lambda>h. frechet_derivative f (at x) h \<bullet> k) = (\<lambda>v. 0)" 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

561 
using ball(2) by (rule differential_zero_maxmin) 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

562 
then show ?thesis 
304e37faf1ac
generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents:
56117
diff
changeset

563 
unfolding fun_eq_iff 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

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

565 

68239  566 
theorem Rolle: 
53781  567 
fixes f :: "real \<Rightarrow> real" 
568 
assumes "a < b" 

68239  569 
and fab: "f a = f b" 
570 
and contf: "continuous_on {a..b} f" 

571 
and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)" 

56188  572 
shows "\<exists>x\<in>{a <..< b}. f' x = (\<lambda>v. 0)" 
53781  573 
proof  
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

574 
have "\<exists>x\<in>box a b. (\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)" 
53781  575 
proof  
68239  576 
have "(a + b) / 2 \<in> {a..b}" 
53781  577 
using assms(1) by auto 
68239  578 
then have *: "{a..b} \<noteq> {}" 
53781  579 
by auto 
68239  580 
obtain d where d: "d \<in>cbox a b" "\<forall>y\<in>cbox a b. f y \<le> f d" 
581 
using continuous_attains_sup[OF compact_Icc * contf] by auto 

582 
obtain c where c: "c \<in> cbox a b" "\<forall>y\<in>cbox a b. f c \<le> f y" 

583 
using continuous_attains_inf[OF compact_Icc * contf] by auto 

44123  584 
show ?thesis 
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

585 
proof (cases "d \<in> box a b \<or> c \<in> box a b") 
53781  586 
case True 
587 
then show ?thesis 

56188  588 
by (metis c(2) d(2) box_subset_cbox subset_iff) 
44123  589 
next 
63040  590 
define e where "e = (a + b) /2" 
53781  591 
case False 
592 
then have "f d = f c" 

68239  593 
using d c fab by auto 
594 
with c d have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d" 

55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

595 
by force 
53781  596 
then show ?thesis 
68239  597 
by (rule_tac x=e in bexI) (auto simp: e_def \<open>a < b\<close>) 
44123  598 
qed 
599 
qed 

56188  600 
then obtain x where x: "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)" 
601 
by auto 

53781  602 
then have "f' x = (\<lambda>v. 0)" 
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54230
diff
changeset

603 
apply (rule_tac differential_zero_maxmin[of x "box a b" f "f' x"]) 
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

604 
using assms 
53781  605 
apply auto 
606 
done 

607 
then show ?thesis 

55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55665
diff
changeset

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

610 

53781  611 

60420  612 
subsection \<open>Onedimensional mean value theorem\<close> 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

613 

53781  614 
lemma mvt: 
615 
fixes f :: "real \<Rightarrow> real" 

616 
assumes "a < b" 

68239  617 
and contf: "continuous_on {a..b} f" 
618 
and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)" 

53781  619 
shows "\<exists>x\<in>{a<..<b}. f b  f a = (f' x) (b  a)" 
620 
proof  

56188  621 
have "\<exists>x\<in>{a <..< b}. (\<lambda>xa. f' x xa  (f b  f a) / (b  a) * xa) = (\<lambda>v. 0)" 
68239  622 
proof (intro Rolle[OF \<open>a < b\<close>, of "\<lambda>x. f x  (f b  f a) / (b  a) * x"] ballI) 
53781  623 
fix x 
68239  624 
assume x: "a < x" "x < b" 
53781  625 
show "((\<lambda>x. f x  (f b  f a) / (b  a) * x) has_derivative 
626 
(\<lambda>xa. f' x xa  (f b  f a) / (b  a) * xa)) (at x)" 

68239  627 
by (intro derivative_intros derf[OF x]) 
628 
qed (use assms in \<open>auto intro!: continuous_intros simp: field_simps\<close>) 

55665  629 
then obtain x where 
56188  630 
"x \<in> {a <..< b}" 
55665  631 
"(\<lambda>xa. f' x xa  (f b  f a) / (b  a) * xa) = (\<lambda>v. 0)" .. 
53781  632 
then show ?thesis 
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61649
diff
changeset

633 
by (metis (hide_lams) assms(1) diff_gt_0_iff_gt eq_iff_diff_eq_0 
64240  634 
zero_less_mult_iff nonzero_mult_div_cancel_right not_real_square_gt_zero 
56188  635 
times_divide_eq_left) 
44123  636 
qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

637 

44123  638 
lemma mvt_simple: 
53781  639 
fixes f :: "real \<Rightarrow> real" 
640 
assumes "a < b" 

68241
39a311f50344
correcting the statements of the MVTs
paulson <lp15@cam.ac.uk>
parents:
68239
diff
changeset

641 
and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (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

642 
shows "\<exists>x\<in>{a<..<b}. f b  f a = f' x (b  a)" 
56264  643 
proof (rule mvt) 
644 
have "f differentiable_on {a..b}" 

68241
39a311f50344
correcting the statements of the MVTs
paulson <lp15@cam.ac.uk>
parents:
68239
diff
changeset

645 
using derf unfolding differentiable_on_def differentiable_def by force 
56264  646 
then show "continuous_on {a..b} f" 
647 
by (rule differentiable_imp_continuous_on) 

68239  648 
show "(f has_derivative f' x) (at x)" if "a < x" "x < b" for x 
68241
39a311f50344
correcting the statements of the MVTs
paulson <lp15@cam.ac.uk>
parents:
68239
diff
changeset

649 
by (metis at_within_Icc_at derf leI order.asym that) 
68239  650 
qed (rule assms) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

651 

44123  652 
lemma mvt_very_simple: 
53781  653 
fixes f :: "real \<Rightarrow> real" 
654 
assumes "a \<le> b" 

68241
39a311f50344
correcting the statements of the MVTs
paulson <lp15@cam.ac.uk>
parents:
68239
diff
changeset

655 
and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x within {a..b})" 
68239  656 
shows "\<exists>x\<in>{a..b}. f b  f a = f' x (b  a)" 
44123  657 
proof (cases "a = b") 
53781  658 
interpret bounded_linear "f' b" 
659 
using assms(2) assms(1) by auto 

660 
case True 

661 
then show ?thesis 

68239  662 
by force 
53781  663 
next 
664 
case False 

665 
then show ?thesis 

68239  666 
using mvt_simple[OF _ derf] 
667 
by (metis \<open>a \<le> b\<close> atLeastAtMost_iff dual_order.order_iff_strict greaterThanLessThan_iff) 

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

669 

60420  670 
text \<open>A nice generalization (see Havin's proof of 5.19 from Rudin's book).\<close> 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

671 

44123  672 
lemma mvt_general: 
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
56217
diff
changeset

673 
fixes f :: "real \<Rightarrow> 'a::real_inner" 
53781  674 
assumes "a < b" 
68239  675 
and contf: "continuous_on {a..b} f" 
676 
and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)" 

53781  677 
shows "\<exists>x\<in>{a<..<b}. norm (f b  f a) \<le> norm (f' x (b  a))" 
678 
proof  

56264  679 
have "\<exists>x\<in>{a<..<b}. (f b  f a) \<bullet> f b  (f b  f a) \<bullet> f a = (f b  f a) \<bullet> f' x (b  a)" 
68239  680 
apply (rule mvt [OF \<open>a < b\<close>]) 
681 
apply (intro continuous_intros contf) 

682 
using derf apply (blast intro: has_derivative_inner_right) 

53781  683 
done 
68239  684 
then obtain x where x: "x \<in> {a<..<b}" 
56264  685 
"(f b  f a) \<bullet> f b  (f b  f a) \<bullet> f a = (f b  f a) \<bullet> f' x (b  a)" .. 
53781  686 
show ?thesis 
687 
proof (cases "f a = f b") 

36844  688 
case False 
53077  689 
have "norm (f b  f a) * norm (f b  f a) = (norm (f b  f a))\<^sup>2" 
44123  690 
by (simp add: power2_eq_square) 
53781  691 
also have "\<dots> = (f b  f a) \<bullet> (f b  f a)" 
692 
unfolding power2_norm_eq_inner .. 

44123  693 
also have "\<dots> = (f b  f a) \<bullet> f' x (b  a)" 
56264  694 
using x(2) by (simp only: inner_diff_right) 
44123  695 
also have "\<dots> \<le> norm (f b  f a) * norm (f' x (b  a))" 
696 
by (rule norm_cauchy_schwarz) 

53781  697 
finally show ?thesis 
698 
using False x(1) 

56217
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
56196
diff
changeset

699 
by (auto simp add: mult_left_cancel) 
44123  700 
next 
53781  701 
case True 
702 
then show ?thesis 

68239  703 
using \<open>a < b\<close> by (rule_tac x="(a + b) /2" in bexI) auto 
44123  704 
qed 
705 
qed 

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

706 

60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

707 

60420  708 
subsection \<open>More general bound theorems\<close> 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

709 

68239  710 
proposition differentiable_bound_general: 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

711 
fixes f :: "real \<Rightarrow> 'a::real_normed_vector" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

712 
assumes "a < b" 
68239  713 
and f_cont: "continuous_on {a..b} f" 
714 
and phi_cont: "continuous_on {a..b} \<phi>" 

60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

715 
and f': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (f has_vector_derivative f' x) (at x)" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

716 
and phi': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<phi> has_vector_derivative \<phi>' x) (at x)" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

717 
and bnd: "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> norm (f' x) \<le> \<phi>' x" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

718 
shows "norm (f b  f a) \<le> \<phi> b  \<phi> a" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

719 
proof  
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

720 
{ 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

721 
fix x assume x: "a < x" "x < b" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

722 
have "0 \<le> norm (f' x)" by simp 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

723 
also have "\<dots> \<le> \<phi>' x" using x by (auto intro!: bnd) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

724 
finally have "0 \<le> \<phi>' x" . 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

725 
} note phi'_nonneg = this 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

726 
note f_tendsto = assms(2)[simplified continuous_on_def, rule_format] 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

727 
note phi_tendsto = assms(3)[simplified continuous_on_def, rule_format] 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

728 
{ 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

729 
fix e::real assume "e > 0" 
63040  730 
define e2 where "e2 = e / 2" 
731 
with \<open>e > 0\<close> have "e2 > 0" by simp 

60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

732 
let ?le = "\<lambda>x1. norm (f x1  f a) \<le> \<phi> x1  \<phi> a + e * (x1  a) + e" 
63040  733 
define A where "A = {x2. a \<le> x2 \<and> x2 \<le> b \<and> (\<forall>x1\<in>{a ..< x2}. ?le x1)}" 
68239  734 
have A_subset: "A \<subseteq> {a..b}" by (auto simp: A_def) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

735 
{ 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

736 
fix x2 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

737 
assume a: "a \<le> x2" "x2 \<le> b" and le: "\<forall>x1\<in>{a..<x2}. ?le x1" 
60420  738 
have "?le x2" using \<open>e > 0\<close> 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

739 
proof cases 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

740 
assume "x2 \<noteq> a" with a have "a < x2" by simp 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

741 
have "at x2 within {a <..<x2}\<noteq> bot" 
60420  742 
using \<open>a < x2\<close> 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

743 
by (auto simp: trivial_limit_within islimpt_in_closure) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

744 
moreover 
61973  745 
have "((\<lambda>x1. (\<phi> x1  \<phi> a) + e * (x1  a) + e) \<longlongrightarrow> (\<phi> x2  \<phi> a) + e * (x2  a) + e) (at x2 within {a <..<x2})" 
746 
"((\<lambda>x1. norm (f x1  f a)) \<longlongrightarrow> norm (f x2  f a)) (at x2 within {a <..<x2})" 

60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

747 
using a 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

748 
by (auto intro!: tendsto_eq_intros f_tendsto phi_tendsto 
68239  749 
intro: tendsto_within_subset[where S="{a..b}"]) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

750 
moreover 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

751 
have "eventually (\<lambda>x. x > a) (at x2 within {a <..<x2})" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

752 
by (auto simp: eventually_at_filter) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

753 
hence "eventually ?le (at x2 within {a <..<x2})" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

754 
unfolding eventually_at_filter 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

755 
by eventually_elim (insert le, auto) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

756 
ultimately 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

757 
show ?thesis 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

758 
by (rule tendsto_le) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

759 
qed simp 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

760 
} note le_cont = this 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

761 
have "a \<in> A" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

762 
using assms by (auto simp: A_def) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

763 
hence [simp]: "A \<noteq> {}" by auto 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

764 
have A_ivl: "\<And>x1 x2. x2 \<in> A \<Longrightarrow> x1 \<in> {a ..x2} \<Longrightarrow> x1 \<in> A" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

765 
by (simp add: A_def) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

766 
have [simp]: "bdd_above A" by (auto simp: A_def) 
63040  767 
define y where "y = Sup A" 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

768 
have "y \<le> b" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

769 
unfolding y_def 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

770 
by (simp add: cSup_le_iff) (simp add: A_def) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

771 
have leI: "\<And>x x1. a \<le> x1 \<Longrightarrow> x \<in> A \<Longrightarrow> x1 < x \<Longrightarrow> ?le x1" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

772 
by (auto simp: A_def intro!: le_cont) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

773 
have y_all_le: "\<forall>x1\<in>{a..<y}. ?le x1" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

774 
by (auto simp: y_def less_cSup_iff leI) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

775 
have "a \<le> y" 
60420  776 
by (metis \<open>a \<in> A\<close> \<open>bdd_above A\<close> cSup_upper y_def) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

777 
have "y \<in> A" 
60420  778 
using y_all_le \<open>a \<le> y\<close> \<open>y \<le> b\<close> 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

779 
by (auto simp: A_def) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

780 
hence "A = {a .. y}" 
68239  781 
using A_subset by (auto simp: subset_iff y_def cSup_upper intro: A_ivl) 
60420  782 
from le_cont[OF \<open>a \<le> y\<close> \<open>y \<le> b\<close> y_all_le] have le_y: "?le y" . 
68239  783 
have "y = b" 
784 
proof (cases "a = y") 

785 
case True 

60420  786 
with \<open>a < b\<close> have "y < b" by simp 
787 
with \<open>a = y\<close> f_cont phi_cont \<open>e2 > 0\<close> 

60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

788 
have 1: "\<forall>\<^sub>F x in at y within {y..b}. dist (f x) (f y) < e2" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

789 
and 2: "\<forall>\<^sub>F x in at y within {y..b}. dist (\<phi> x) (\<phi> y) < e2" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

790 
by (auto simp: continuous_on_def tendsto_iff) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

791 
have 3: "eventually (\<lambda>x. y < x) (at y within {y..b})" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

792 
by (auto simp: eventually_at_filter) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

793 
have 4: "eventually (\<lambda>x::real. x < b) (at y within {y..b})" 
60420  794 
using _ \<open>y < b\<close> 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

795 
by (rule order_tendstoD) (auto intro!: tendsto_eq_intros) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

796 
from 1 2 3 4 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

797 
have eventually_le: "eventually (\<lambda>x. ?le x) (at y within {y .. b})" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

798 
proof eventually_elim 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

799 
case (elim x1) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

800 
have "norm (f x1  f a) = norm (f x1  f y)" 
60420  801 
by (simp add: \<open>a = y\<close>) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

802 
also have "norm (f x1  f y) \<le> e2" 
60420  803 
using elim \<open>a = y\<close> by (auto simp : dist_norm intro!: less_imp_le) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

804 
also have "\<dots> \<le> e2 + (\<phi> x1  \<phi> a + e2 + e * (x1  a))" 
60420  805 
using \<open>0 < e\<close> elim 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

806 
by (intro add_increasing2[OF add_nonneg_nonneg order.refl]) 
60420  807 
(auto simp: \<open>a = y\<close> dist_norm intro!: mult_nonneg_nonneg) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

808 
also have "\<dots> = \<phi> x1  \<phi> a + e * (x1  a) + e" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

809 
by (simp add: e2_def) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

810 
finally show "?le x1" . 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

811 
qed 
60420  812 
from this[unfolded eventually_at_topological] \<open>?le y\<close> 
68239  813 
obtain S where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x" 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

814 
by metis 
60420  815 
from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0" 
62101  816 
by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>]) 
63040  817 
define d' where "d' = min b (y + (d/2))" 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

818 
have "d' \<in> A" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

819 
unfolding A_def 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

820 
proof safe 
60420  821 
show "a \<le> d'" using \<open>a = y\<close> \<open>0 < d\<close> \<open>y < b\<close> by (simp add: d'_def) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

822 
show "d' \<le> b" by (simp add: d'_def) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

823 
fix x1 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

824 
assume "x1 \<in> {a..<d'}" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

825 
hence "x1 \<in> S" "x1 \<in> {y..b}" 
60420  826 
by (auto simp: \<open>a = y\<close> d'_def dist_real_def intro!: d ) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

827 
thus "?le x1" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

828 
by (rule S) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

829 
qed 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

830 
hence "d' \<le> y" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

831 
unfolding y_def 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

832 
by (rule cSup_upper) simp 
68239  833 
then show "y = b" using \<open>d > 0\<close> \<open>y < b\<close> 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

834 
by (simp add: d'_def) 
68239  835 
next 
836 
case False 

837 
with \<open>a \<le> y\<close> have "a < y" by simp 

838 
show "y = b" 

839 
proof (rule ccontr) 

840 
assume "y \<noteq> b" 

841 
hence "y < b" using \<open>y \<le> b\<close> by simp 

842 
let ?F = "at y within {y..<b}" 

843 
from f' phi' 

844 
have "(f has_vector_derivative f' y) ?F" 

845 
and "(\<phi> has_vector_derivative \<phi>' y) ?F" 

846 
using \<open>a < y\<close> \<open>y < b\<close> 

847 
by (auto simp add: at_within_open[of _ "{a<..<b}"] has_vector_derivative_def 

848 
intro!: has_derivative_subset[where s="{a<..<b}" and t="{y..<b}"]) 

849 
hence "\<forall>\<^sub>F x1 in ?F. norm (f x1  f y  (x1  y) *\<^sub>R f' y) \<le> e2 * \<bar>x1  y\<bar>" 

850 
"\<forall>\<^sub>F x1 in ?F. norm (\<phi> x1  \<phi> y  (x1  y) *\<^sub>R \<phi>' y) \<le> e2 * \<bar>x1  y\<bar>" 

851 
using \<open>e2 > 0\<close> 

852 
by (auto simp: has_derivative_within_alt2 has_vector_derivative_def) 

853 
moreover 

854 
have "\<forall>\<^sub>F x1 in ?F. y \<le> x1" "\<forall>\<^sub>F x1 in ?F. x1 < b" 

855 
by (auto simp: eventually_at_filter) 

856 
ultimately 

857 
have "\<forall>\<^sub>F x1 in ?F. norm (f x1  f y) \<le> (\<phi> x1  \<phi> y) + e * \<bar>x1  y\<bar>" 

858 
(is "\<forall>\<^sub>F x1 in ?F. ?le' x1") 

859 
proof eventually_elim 

860 
case (elim x1) 

861 
from norm_triangle_ineq2[THEN order_trans, OF elim(1)] 

862 
have "norm (f x1  f y) \<le> norm (f' y) * \<bar>x1  y\<bar> + e2 * \<bar>x1  y\<bar>" 

863 
by (simp add: ac_simps) 

864 
also have "norm (f' y) \<le> \<phi>' y" using bnd \<open>a < y\<close> \<open>y < b\<close> by simp 

865 
also have "\<phi>' y * \<bar>x1  y\<bar> \<le> \<phi> x1  \<phi> y + e2 * \<bar>x1  y\<bar>" 

866 
using elim by (simp add: ac_simps) 

867 
finally 

868 
have "norm (f x1  f y) \<le> \<phi> x1  \<phi> y + e2 * \<bar>x1  y\<bar> + e2 * \<bar>x1  y\<bar>" 

869 
by (auto simp: mult_right_mono) 

870 
thus ?case by (simp add: e2_def) 

871 
qed 

872 
moreover have "?le' y" by simp 

873 
ultimately obtain S 

874 
where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..<b} \<Longrightarrow> ?le' x" 

875 
unfolding eventually_at_topological 

876 
by metis 

877 
from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0" 

878 
by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>]) 

879 
define d' where "d' = min ((y + b)/2) (y + (d/2))" 

880 
have "d' \<in> A" 

881 
unfolding A_def 

882 
proof safe 

883 
show "a \<le> d'" using \<open>a < y\<close> \<open>0 < d\<close> \<open>y < b\<close> by (simp add: d'_def) 

884 
show "d' \<le> b" using \<open>y < b\<close> by (simp add: d'_def min_def) 

885 
fix x1 

886 
assume x1: "x1 \<in> {a..<d'}" 

887 
show "?le x1" 

888 
proof (cases "x1 < y") 

889 
case True 

890 
then show ?thesis 

891 
using \<open>y \<in> A\<close> local.leI x1 by auto 

892 
next 

893 
case False 

894 
hence x1': "x1 \<in> S" "x1 \<in> {y..<b}" using x1 

895 
by (auto simp: d'_def dist_real_def intro!: d) 

896 
have "norm (f x1  f a) \<le> norm (f x1  f y) + norm (f y  f a)" 

897 
by (rule order_trans[OF _ norm_triangle_ineq]) simp 

898 
also note S(3)[OF x1'] 

899 
also note le_y 

900 
finally show "?le x1" 

901 
using False by (auto simp: algebra_simps) 

902 
qed 

903 
qed 

904 
hence "d' \<le> y" 

905 
unfolding y_def by (rule cSup_upper) simp 

906 
thus False using \<open>d > 0\<close> \<open>y < b\<close> 

907 
by (simp add: d'_def min_def split: if_split_asm) 

908 
qed 

909 
qed 

60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

910 
with le_y have "norm (f b  f a) \<le> \<phi> b  \<phi> a + e * (b  a + 1)" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

911 
by (simp add: algebra_simps) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

912 
} note * = this 
68239  913 
show ?thesis 
914 
proof (rule field_le_epsilon) 

60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

915 
fix e::real assume "e > 0" 
68239  916 
then show "norm (f b  f a) \<le> \<phi> b  \<phi> a + e" 
60420  917 
using *[of "e / (b  a + 1)"] \<open>a < b\<close> by simp 
68239  918 
qed 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

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

920 

44123  921 
lemma differentiable_bound: 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

922 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
68239  923 
assumes "convex S" 
924 
and derf: "\<And>x. x\<in>S \<Longrightarrow> (f has_derivative f' x) (at x within S)" 

925 
and B: "\<And>x. x \<in> S \<Longrightarrow> onorm (f' x) \<le> B" 

926 
and x: "x \<in> S" 

927 
and y: "y \<in> S" 

53781  928 
shows "norm (f x  f y) \<le> B * norm (x  y)" 
929 
proof  

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

930 
let ?p = "\<lambda>u. x + u *\<^sub>R (y  x)" 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

931 
let ?\<phi> = "\<lambda>h. h * B * norm (x  y)" 
68239  932 
have *: "x + u *\<^sub>R (y  x) \<in> S" if "u \<in> {0..1}" for u 
933 
proof  

934 
have "u *\<^sub>R y = u *\<^sub>R (y  x) + u *\<^sub>R x" 

935 
by (simp add: scale_right_diff_distrib) 

936 
then show "x + u *\<^sub>R (y  x) \<in> S" 

937 
using that \<open>convex S\<close> unfolding convex_alt by (metis (no_types) atLeastAtMost_iff linordered_field_class.sign_simps(2) pth_c(3) scaleR_collapse x y) 

938 
qed 

939 
have "\<And>z. z \<in> (\<lambda>u. x + u *\<^sub>R (y  x)) ` {0..1} \<Longrightarrow> 

940 
(f has_derivative f' z) (at z within (\<lambda>u. x + u *\<^sub>R (y  x)) ` {0..1})" 

941 
by (auto intro: * has_derivative_within_subset [OF derf]) 

942 
then have "continuous_on (?p ` {0..1}) f" 

60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

943 
unfolding continuous_on_eq_continuous_within 
68239  944 
by (meson has_derivative_continuous) 
945 
with * have 1: "continuous_on {0 .. 1} (f \<circ> ?p)" 

946 
by (intro continuous_intros)+ 

60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

947 
{ 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

948 
fix u::real assume u: "u \<in>{0 <..< 1}" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

949 
let ?u = "?p u" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

950 
interpret linear "(f' ?u)" 
68239  951 
using u by (auto intro!: has_derivative_linear derf *) 
56188  952 
have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y  x))) (at u within box 0 1)" 
68239  953 
by (intro derivative_intros has_derivative_within_subset [OF derf]) (use u * in auto) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

954 
hence "((f \<circ> ?p) has_vector_derivative f' ?u (y  x)) (at u)" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

955 
by (simp add: has_derivative_within_open[OF u open_greaterThanLessThan] 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

956 
scaleR has_vector_derivative_def o_def) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

957 
} note 2 = this 
68239  958 
have 3: "continuous_on {0..1} ?\<phi>" 
959 
by (rule continuous_intros)+ 

960 
have 4: "(?\<phi> has_vector_derivative B * norm (x  y)) (at u)" for u 

961 
by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros) 

60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

962 
{ 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

963 
fix u::real assume u: "u \<in>{0 <..< 1}" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

964 
let ?u = "?p u" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

965 
interpret bounded_linear "(f' ?u)" 
68239  966 
using u by (auto intro!: has_derivative_bounded_linear derf *) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

967 
have "norm (f' ?u (y  x)) \<le> onorm (f' ?u) * norm (y  x)" 
67682
00c436488398
tuned proofs  prefer explicit names for facts from 'interpret';
wenzelm
parents:
67399
diff
changeset

968 
by (rule onorm) (rule bounded_linear) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

969 
also have "onorm (f' ?u) \<le> B" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

970 
using u by (auto intro!: assms(3)[rule_format] *) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

971 
finally have "norm ((f' ?u) (y  x)) \<le> B * norm (x  y)" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

972 
by (simp add: mult_right_mono norm_minus_commute) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

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

974 
have "norm (f x  f y) = norm ((f \<circ> (\<lambda>u. x + u *\<^sub>R (y  x))) 1  (f \<circ> (\<lambda>u. x + u *\<^sub>R (y  x))) 0)" 
53781  975 
by (auto simp add: norm_minus_commute) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

976 
also 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

977 
from differentiable_bound_general[OF zero_less_one 1, OF 3 2 4 5] 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

978 
have "norm ((f \<circ> ?p) 1  (f \<circ> ?p) 0) \<le> B * norm (x  y)" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

979 
by simp 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

980 
finally show ?thesis . 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

981 
qed 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

982 

f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

983 
lemma 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

984 
differentiable_bound_segment: 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

985 
fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

986 
assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R a \<in> G" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

987 
assumes f': "\<And>x. x \<in> G \<Longrightarrow> (f has_derivative f' x) (at x within G)" 
68239  988 
assumes B: "\<And>x. x \<in> {0..1} \<Longrightarrow> onorm (f' (x0 + x *\<^sub>R a)) \<le> B" 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

989 
shows "norm (f (x0 + a)  f x0) \<le> norm a * B" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

990 
proof  
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

991 
let ?G = "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}" 
67399  992 
have "?G = (+) x0 ` (\<lambda>x. x *\<^sub>R a) ` {0..1}" by auto 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

993 
also have "convex \<dots>" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

994 
by (intro convex_translation convex_scaled convex_real_interval) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

995 
finally have "convex ?G" . 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

996 
moreover have "?G \<subseteq> G" "x0 \<in> ?G" "x0 + a \<in> ?G" using assms by (auto intro: image_eqI[where x=1]) 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

997 
ultimately show ?thesis 
60420  998 
using has_derivative_subset[OF f' \<open>?G \<subseteq> G\<close>] B 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

999 
differentiable_bound[of "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}" f f' B "x0 + a" x0] 
68239  1000 
by (force simp: ac_simps) 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1001 
qed 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1002 

f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1003 
lemma differentiable_bound_linearization: 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1004 
fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
68239  1005 
assumes S: "\<And>t. t \<in> {0..1} \<Longrightarrow> a + t *\<^sub>R (b  a) \<in> S" 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1006 
assumes f'[derivative_intros]: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" 
68239  1007 
assumes B: "\<And>x. x \<in> S \<Longrightarrow> onorm (f' x  f' x0) \<le> B" 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1008 
assumes "x0 \<in> S" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1009 
shows "norm (f b  f a  f' x0 (b  a)) \<le> norm (b  a) * B" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1010 
proof  
63040  1011 
define g where [abs_def]: "g x = f x  f' x0 x" for x 
60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1012 
have g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative (\<lambda>i. f' x i  f' x0 i)) (at x within S)" 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1013 
unfolding g_def using assms 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1014 
by (auto intro!: derivative_eq_intros 
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1015 
bounded_linear.has_derivative[OF has_derivative_bounded_linear, OF f']) 
68239  1016 
from B have "\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b  a)) i  f' x0 i) \<le> B" 
1017 
using assms by (auto simp: fun_diff_def) 

1018 
with differentiable_bound_segment[OF S g] \<open>x0 \<in> S\<close> 

60178
f620c70f9e9b
generalized differentiable_bound; some further variations of differentiable_bound
immler
parents:
60177
diff
changeset

1019 
show ?thesis 
63469
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

1020 
by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']]) 
44123  1021 
qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1022 

67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1023 
lemma vector_differentiable_bound_linearization: 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1024 
fixes f::"real \<Rightarrow> 'b::real_normed_vector" 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1025 
assumes f': "\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)" 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1026 
assumes "closed_segment a b \<subseteq> S" 
68239  1027 
assumes B: "\<And>x. x \<in> S \<Longrightarrow> norm (f' x  f' x0) \<le> B" 
67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1028 
assumes "x0 \<in> S" 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1029 
shows "norm (f b  f a  (b  a) *\<^sub>R f' x0) \<le> norm (b  a) * B" 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1030 
using assms 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1031 
by (intro differentiable_bound_linearization[of a b S f "\<lambda>x h. h *\<^sub>R f' x" x0 B]) 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1032 
(force simp: closed_segment_real_eq has_vector_derivative_def 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1033 
scaleR_diff_right[symmetric] mult.commute[of B] 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1034 
intro!: onorm_le mult_left_mono)+ 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1035 

bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1036 

60420  1037 
text \<open>In particular.\<close> 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1038 

44123  1039 
lemma has_derivative_zero_constant: 
60179  1040 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
53781  1041 
assumes "convex s" 
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1042 
and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)" 
44123  1043 
shows "\<exists>c. \<forall>x\<in>s. f x = c" 
56332  1044 
proof  
1045 
{ fix x y assume "x \<in> s" "y \<in> s" 

1046 
then have "norm (f x  f y) \<le> 0 * norm (x  y)" 

1047 
using assms by (intro differentiable_bound[of s]) (auto simp: onorm_zero) 

1048 
then have "f x = f y" 

1049 
by simp } 

53781  1050 
then show ?thesis 
56332  1051 
by metis 
53781  1052 
qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1053 

61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61520
diff
changeset

1054 
lemma has_field_derivative_zero_constant: 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61520
diff
changeset

1055 
assumes "convex s" "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative 0) (at x within s)" 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61520
diff
changeset

1056 
shows "\<exists>c. \<forall>x\<in>s. f (x) = (c :: 'a :: real_normed_field)" 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61520
diff
changeset

1057 
proof (rule has_derivative_zero_constant) 
67399  1058 
have A: "( * ) 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp 
61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61520
diff
changeset

1059 
fix x assume "x \<in> s" thus "(f has_derivative (\<lambda>h. 0)) (at x within s)" 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61520
diff
changeset

1060 
using assms(2)[of x] by (simp add: has_field_derivative_def A) 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61520
diff
changeset

1061 
qed fact 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61520
diff
changeset

1062 

67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1063 
lemma 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1064 
has_vector_derivative_zero_constant: 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1065 
assumes "convex s" 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1066 
assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_vector_derivative 0) (at x within s)" 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1067 
obtains c where "\<And>x. x \<in> s \<Longrightarrow> f x = c" 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1068 
using has_derivative_zero_constant[of s f] assms 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1069 
by (auto simp: has_vector_derivative_def) 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67682
diff
changeset

1070 

53781  1071 
lemma has_derivative_zero_unique: 
60179  1072 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
53781  1073 
assumes "convex s" 
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1074 
and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)" 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1075 
and "x \<in> s" "y \<in> s" 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1076 
shows "f x = f y" 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1077 
using has_derivative_zero_constant[OF assms(1,2)] assms(3) by force 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1078 

2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1079 
lemma has_derivative_zero_unique_connected: 
60179  1080 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1081 
assumes "open s" "connected s" 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1082 
assumes f: "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>x. 0)) (at x)" 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1083 
assumes "x \<in> s" "y \<in> s" 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1084 
shows "f x = f y" 
60420  1085 
proof (rule connected_local_const[where f=f, OF \<open>connected s\<close> \<open>x\<in>s\<close> \<open>y\<in>s\<close>]) 
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1086 
show "\<forall>a\<in>s. eventually (\<lambda>b. f a = f b) (at a within s)" 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1087 
proof 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1088 
fix a assume "a \<in> s" 
60420  1089 
with \<open>open s\<close> obtain e where "0 < e" "ball a e \<subseteq> s" 
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1090 
by (rule openE) 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1091 
then have "\<exists>c. \<forall>x\<in>ball a e. f x = c" 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1092 
by (intro has_derivative_zero_constant) 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1093 
(auto simp: at_within_open[OF _ open_ball] f convex_ball) 
60420  1094 
with \<open>0<e\<close> have "\<forall>x\<in>ball a e. f a = f x" 
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1095 
by auto 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1096 
then show "eventually (\<lambda>b. f a = f b) (at a within s)" 
60420  1097 
using \<open>0<e\<close> unfolding eventually_at_topological 
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1098 
by (intro exI[of _ "ball a e"]) auto 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1099 
qed 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1100 
qed 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56332
diff
changeset

1101 

60420  1102 
subsection \<open>Differentiability of inverse function (most basic form)\<close> 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1103 

44123  1104 
lemma has_derivative_inverse_basic: 
56226  1105 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
68055  1106 
assumes derf: "(f has_derivative f') (at (g y))" 
1107 
and ling': "bounded_linear g'" 

53781  1108 
and "g' \<circ> f' = id" 
68055  1109 
and contg: "continuous (at y) g" 
1110 
and "open T" 

1111 
and "y \<in> T" 

1112 
and fg: "\<And>z. z \<in> T \<Longrightarrow> f (g z) = z" 

44123  1113 
shows "(g has_derivative g') (at y)" 
53781  1114 
proof  
44123  1115 
interpret f': bounded_linear f' 
1116 
using assms unfolding has_derivative_def by auto 

53781  1117 
interpret g': bounded_linear g' 
1118 
using assms by auto 

55665  1119 
obtain C where C: "0 < C" "\<And>x. norm (g' x) \<le> norm x * C" 
1120 
using bounded_linear.pos_bounded[OF assms(2)] by blast 

53781  1121 
have lem1: "\<forall>e>0. \<exists>d>0. \<forall>z. 
1122 
norm (z  y) < d \<longrightarrow> norm (g z  g y  g'(z  y)) \<le> e * norm (g z  g y)" 

68055  1123 
proof (intro allI impI) 
61165  1124 
fix e :: real 
1125 
assume "e > 0" 

1126 
with C(1) have *: "e / C > 0" by auto 

68055  1127 
obtain d0 where "0 < d0" and d0: 