author | wenzelm |
Thu, 28 Jul 2016 20:39:46 +0200 | |
changeset 63558 | 0aa33085c8b1 |
parent 63469 | b6900858dcb9 |
child 63627 | 6ddb43c6b711 |
permissions | -rw-r--r-- |
63558 | 1 |
(* Title: HOL/Deriv.thy |
2 |
Author: Jacques D. Fleuriot, University of Cambridge, 1998 |
|
3 |
Author: Brian Huffman |
|
4 |
Author: Lawrence C Paulson, 2004 |
|
5 |
Author: Benjamin Porter, 2005 |
|
21164 | 6 |
*) |
7 |
||
63558 | 8 |
section \<open>Differentiation\<close> |
21164 | 9 |
|
10 |
theory Deriv |
|
63558 | 11 |
imports Limits |
21164 | 12 |
begin |
13 |
||
60758 | 14 |
subsection \<open>Frechet derivative\<close> |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
15 |
|
63558 | 16 |
definition has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> |
17 |
('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> bool" (infix "(has'_derivative)" 50) |
|
18 |
where "(f has_derivative f') F \<longleftrightarrow> |
|
19 |
bounded_linear f' \<and> |
|
20 |
((\<lambda>y. ((f y - f (Lim F (\<lambda>x. x))) - f' (y - Lim F (\<lambda>x. x))) /\<^sub>R norm (y - Lim F (\<lambda>x. x))) \<longlongrightarrow> 0) F" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
21 |
|
60758 | 22 |
text \<open> |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
23 |
Usually the filter @{term F} is @{term "at x within s"}. @{term "(f has_derivative D) |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
24 |
(at x within s)"} means: @{term D} is the derivative of function @{term f} at point @{term x} |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
25 |
within the set @{term s}. Where @{term s} is used to express left or right sided derivatives. In |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
26 |
most cases @{term s} is either a variable or @{term UNIV}. |
60758 | 27 |
\<close> |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
28 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
29 |
lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F" |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
30 |
by simp |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
31 |
|
63558 | 32 |
definition has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool" |
33 |
(infix "(has'_field'_derivative)" 50) |
|
34 |
where "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative op * D) F" |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
35 |
|
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
36 |
lemma DERIV_cong: "(f has_field_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) F" |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
37 |
by simp |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
38 |
|
63558 | 39 |
definition has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> real filter \<Rightarrow> bool" |
40 |
(infix "has'_vector'_derivative" 50) |
|
41 |
where "(f has_vector_derivative f') net \<longleftrightarrow> (f has_derivative (\<lambda>x. x *\<^sub>R f')) net" |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
42 |
|
63558 | 43 |
lemma has_vector_derivative_eq_rhs: |
44 |
"(f has_vector_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_vector_derivative Y) F" |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
45 |
by simp |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
46 |
|
57953 | 47 |
named_theorems derivative_intros "structural introduction rules for derivatives" |
60758 | 48 |
setup \<open> |
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
49 |
let |
57953 | 50 |
val eq_thms = @{thms has_derivative_eq_rhs DERIV_cong has_vector_derivative_eq_rhs} |
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
51 |
fun eq_rule thm = get_first (try (fn eq_thm => eq_thm OF [thm])) eq_thms |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
52 |
in |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
53 |
Global_Theory.add_thms_dynamic |
57953 | 54 |
(@{binding derivative_eq_intros}, |
55 |
fn context => |
|
56 |
Named_Theorems.get (Context.proof_of context) @{named_theorems derivative_intros} |
|
57 |
|> map_filter eq_rule) |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
58 |
end; |
60758 | 59 |
\<close> |
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
60 |
|
60758 | 61 |
text \<open> |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
62 |
The following syntax is only used as a legacy syntax. |
60758 | 63 |
\<close> |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
64 |
abbreviation (input) |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
65 |
FDERIV :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
66 |
("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) |
63558 | 67 |
where "FDERIV f x :> f' \<equiv> (f has_derivative f') (at x)" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
68 |
|
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
69 |
lemma has_derivative_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
70 |
by (simp add: has_derivative_def) |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
71 |
|
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56289
diff
changeset
|
72 |
lemma has_derivative_linear: "(f has_derivative f') F \<Longrightarrow> linear f'" |
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56289
diff
changeset
|
73 |
using bounded_linear.linear[OF has_derivative_bounded_linear] . |
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56289
diff
changeset
|
74 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
75 |
lemma has_derivative_ident[derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F" |
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57953
diff
changeset
|
76 |
by (simp add: has_derivative_def) |
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
|
77 |
|
63469
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63299
diff
changeset
|
78 |
lemma has_derivative_id [derivative_intros, simp]: "(id has_derivative id) (at a)" |
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63299
diff
changeset
|
79 |
by (metis eq_id_iff has_derivative_ident) |
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63299
diff
changeset
|
80 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
81 |
lemma has_derivative_const[derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F" |
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57953
diff
changeset
|
82 |
by (simp add: has_derivative_def) |
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
|
83 |
|
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
|
84 |
lemma (in bounded_linear) bounded_linear: "bounded_linear f" .. |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
85 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
86 |
lemma (in bounded_linear) has_derivative: |
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
|
87 |
"(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F" |
63092 | 88 |
unfolding has_derivative_def |
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
|
89 |
apply safe |
63558 | 90 |
apply (erule bounded_linear_compose [OF bounded_linear]) |
56219 | 91 |
apply (drule tendsto) |
92 |
apply (simp add: scaleR diff add zero) |
|
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
|
93 |
done |
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
|
94 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
95 |
lemmas has_derivative_scaleR_right [derivative_intros] = |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
96 |
bounded_linear.has_derivative [OF bounded_linear_scaleR_right] |
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
|
97 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
98 |
lemmas has_derivative_scaleR_left [derivative_intros] = |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
99 |
bounded_linear.has_derivative [OF bounded_linear_scaleR_left] |
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
|
100 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
101 |
lemmas has_derivative_mult_right [derivative_intros] = |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
102 |
bounded_linear.has_derivative [OF bounded_linear_mult_right] |
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
|
103 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
104 |
lemmas has_derivative_mult_left [derivative_intros] = |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
105 |
bounded_linear.has_derivative [OF bounded_linear_mult_left] |
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
|
106 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
107 |
lemma has_derivative_add[simp, derivative_intros]: |
63558 | 108 |
assumes f: "(f has_derivative f') F" |
109 |
and g: "(g has_derivative g') F" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
110 |
shows "((\<lambda>x. f x + g x) has_derivative (\<lambda>x. f' x + g' x)) F" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
111 |
unfolding has_derivative_def |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
112 |
proof safe |
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
|
113 |
let ?x = "Lim F (\<lambda>x. x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
114 |
let ?D = "\<lambda>f f' y. ((f y - f ?x) - f' (y - ?x)) /\<^sub>R norm (y - ?x)" |
61973 | 115 |
have "((\<lambda>x. ?D f f' x + ?D g g' x) \<longlongrightarrow> (0 + 0)) F" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
116 |
using f g by (intro tendsto_add) (auto simp: has_derivative_def) |
61973 | 117 |
then show "(?D (\<lambda>x. f x + g x) (\<lambda>x. f' x + g' x) \<longlongrightarrow> 0) F" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
118 |
by (simp add: field_simps scaleR_add_right scaleR_diff_right) |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
119 |
qed (blast intro: bounded_linear_add f g has_derivative_bounded_linear) |
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
|
120 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
121 |
lemma has_derivative_setsum[simp, derivative_intros]: |
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
|
122 |
assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
123 |
shows "((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F" |
63558 | 124 |
proof (cases "finite I") |
125 |
case True |
|
126 |
from this f show ?thesis |
|
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
|
127 |
by induct (simp_all add: f) |
63558 | 128 |
next |
129 |
case False |
|
130 |
then show ?thesis by simp |
|
131 |
qed |
|
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
|
132 |
|
63558 | 133 |
lemma has_derivative_minus[simp, derivative_intros]: |
134 |
"(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
135 |
using has_derivative_scaleR_right[of f f' F "-1"] by simp |
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
|
136 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
137 |
lemma has_derivative_diff[simp, derivative_intros]: |
63558 | 138 |
"(f has_derivative f') F \<Longrightarrow> (g has_derivative g') F \<Longrightarrow> |
139 |
((\<lambda>x. f x - g x) has_derivative (\<lambda>x. f' x - g' x)) F" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
140 |
by (simp only: diff_conv_add_uminus has_derivative_add has_derivative_minus) |
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
|
141 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
142 |
lemma has_derivative_at_within: |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
143 |
"(f has_derivative f') (at x within s) \<longleftrightarrow> |
61973 | 144 |
(bounded_linear f' \<and> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within s))" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
145 |
by (cases "at x within s = bot") (simp_all add: has_derivative_def Lim_ident_at) |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
146 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
147 |
lemma has_derivative_iff_norm: |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
148 |
"(f has_derivative f') (at x within s) \<longleftrightarrow> |
63558 | 149 |
bounded_linear f' \<and> ((\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x)) \<longlongrightarrow> 0) (at x within s)" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
150 |
using tendsto_norm_zero_iff[of _ "at x within s", where 'b="'b", symmetric] |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
151 |
by (simp add: has_derivative_at_within divide_inverse ac_simps) |
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
|
152 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
153 |
lemma has_derivative_at: |
63558 | 154 |
"(f has_derivative D) (at x) \<longleftrightarrow> |
155 |
(bounded_linear D \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) \<midarrow>0\<rightarrow> 0)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
156 |
unfolding has_derivative_iff_norm LIM_offset_zero_iff[of _ _ x] by simp |
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
|
157 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
158 |
lemma field_has_derivative_at: |
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
|
159 |
fixes x :: "'a::real_normed_field" |
61976 | 160 |
shows "(f has_derivative op * D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
161 |
apply (unfold has_derivative_at) |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
162 |
apply (simp add: bounded_linear_mult_right) |
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
|
163 |
apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric]) |
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
|
164 |
apply (subst diff_divide_distrib) |
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
|
165 |
apply (subst times_divide_eq_left [symmetric]) |
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
|
166 |
apply (simp cong: LIM_cong) |
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
|
167 |
apply (simp add: tendsto_norm_zero_iff LIM_zero_iff) |
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
|
168 |
done |
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
|
169 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
170 |
lemma has_derivativeI: |
63558 | 171 |
"bounded_linear f' \<Longrightarrow> |
172 |
((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within s) \<Longrightarrow> |
|
173 |
(f has_derivative f') (at x within s)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
174 |
by (simp add: has_derivative_at_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
|
175 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
176 |
lemma has_derivativeI_sandwich: |
63558 | 177 |
assumes e: "0 < e" |
178 |
and bounded: "bounded_linear f'" |
|
179 |
and sandwich: "(\<And>y. y \<in> s \<Longrightarrow> y \<noteq> x \<Longrightarrow> dist y x < e \<Longrightarrow> |
|
180 |
norm ((f y - f x) - f' (y - x)) / norm (y - x) \<le> H y)" |
|
61973 | 181 |
and "(H \<longlongrightarrow> 0) (at x within s)" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
182 |
shows "(f has_derivative f') (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
183 |
unfolding has_derivative_iff_norm |
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
|
184 |
proof safe |
61973 | 185 |
show "((\<lambda>y. norm (f y - f x - f' (y - x)) / norm (y - x)) \<longlongrightarrow> 0) (at x within s)" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
186 |
proof (rule tendsto_sandwich[where f="\<lambda>x. 0"]) |
61973 | 187 |
show "(H \<longlongrightarrow> 0) (at x within s)" by fact |
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
|
188 |
show "eventually (\<lambda>n. norm (f n - f x - f' (n - x)) / norm (n - x) \<le> H n) (at x within s)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
189 |
unfolding eventually_at using e sandwich by auto |
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57953
diff
changeset
|
190 |
qed (auto simp: le_divide_eq) |
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
|
191 |
qed fact |
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
|
192 |
|
63558 | 193 |
lemma has_derivative_subset: |
194 |
"(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
195 |
by (auto simp add: has_derivative_iff_norm intro: tendsto_within_subset) |
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
|
196 |
|
63558 | 197 |
lemmas has_derivative_within_subset = has_derivative_subset |
56261 | 198 |
|
199 |
||
60758 | 200 |
subsection \<open>Continuity\<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
|
201 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
202 |
lemma has_derivative_continuous: |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
203 |
assumes f: "(f has_derivative f') (at x within s)" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
204 |
shows "continuous (at x within s) f" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
205 |
proof - |
63558 | 206 |
from f interpret F: bounded_linear f' |
207 |
by (rule has_derivative_bounded_linear) |
|
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
|
208 |
note F.tendsto[tendsto_intros] |
61973 | 209 |
let ?L = "\<lambda>f. (f \<longlongrightarrow> 0) (at x within s)" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
210 |
have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x))" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
211 |
using f unfolding has_derivative_iff_norm by blast |
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
|
212 |
then have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x) * norm (y - x))" (is ?m) |
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
|
213 |
by (rule tendsto_mult_zero) (auto intro!: tendsto_eq_intros) |
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
|
214 |
also have "?m \<longleftrightarrow> ?L (\<lambda>y. norm ((f y - f x) - f' (y - x)))" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
215 |
by (intro filterlim_cong) (simp_all add: eventually_at_filter) |
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
|
216 |
finally have "?L (\<lambda>y. (f y - f x) - f' (y - x))" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
217 |
by (rule tendsto_norm_zero_cancel) |
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
|
218 |
then have "?L (\<lambda>y. ((f y - f x) - f' (y - x)) + f' (y - x))" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
219 |
by (rule tendsto_eq_intros) (auto intro!: tendsto_eq_intros simp: F.zero) |
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
|
220 |
then have "?L (\<lambda>y. f y - f x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
221 |
by simp |
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
|
222 |
from tendsto_add[OF this tendsto_const, of "f x"] show ?thesis |
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
|
223 |
by (simp add: continuous_within) |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
224 |
qed |
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
|
225 |
|
63558 | 226 |
|
60758 | 227 |
subsection \<open>Composition\<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
|
228 |
|
63558 | 229 |
lemma tendsto_at_iff_tendsto_nhds_within: |
230 |
"f x = y \<Longrightarrow> (f \<longlongrightarrow> y) (at x within s) \<longleftrightarrow> (f \<longlongrightarrow> y) (inf (nhds x) (principal s))" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
231 |
unfolding tendsto_def eventually_inf_principal eventually_at_filter |
61810 | 232 |
by (intro ext all_cong imp_cong) (auto elim!: eventually_mono) |
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
|
233 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
234 |
lemma has_derivative_in_compose: |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
235 |
assumes f: "(f has_derivative f') (at x within s)" |
63558 | 236 |
and g: "(g has_derivative g') (at (f x) within (f`s))" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
237 |
shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
238 |
proof - |
63558 | 239 |
from f interpret F: bounded_linear f' |
240 |
by (rule has_derivative_bounded_linear) |
|
241 |
from g interpret G: bounded_linear g' |
|
242 |
by (rule has_derivative_bounded_linear) |
|
243 |
from F.bounded obtain kF where kF: "\<And>x. norm (f' x) \<le> norm x * kF" |
|
244 |
by fast |
|
245 |
from G.bounded obtain kG where kG: "\<And>x. norm (g' x) \<le> norm x * kG" |
|
246 |
by fast |
|
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
|
247 |
note G.tendsto[tendsto_intros] |
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
|
248 |
|
61973 | 249 |
let ?L = "\<lambda>f. (f \<longlongrightarrow> 0) (at x within s)" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
250 |
let ?D = "\<lambda>f f' x y. (f y - f x) - f' (y - x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
251 |
let ?N = "\<lambda>f f' x y. norm (?D f f' x y) / norm (y - x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
252 |
let ?gf = "\<lambda>x. g (f x)" and ?gf' = "\<lambda>x. g' (f' x)" |
63040 | 253 |
define Nf where "Nf = ?N f f' x" |
254 |
define Ng where [abs_def]: "Ng y = ?N g g' (f x) (f y)" for y |
|
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
|
255 |
|
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
|
256 |
show ?thesis |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
257 |
proof (rule has_derivativeI_sandwich[of 1]) |
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
|
258 |
show "bounded_linear (\<lambda>x. g' (f' x))" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
259 |
using f g by (blast intro: bounded_linear_compose has_derivative_bounded_linear) |
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
|
260 |
next |
63558 | 261 |
fix y :: 'a |
262 |
assume neq: "y \<noteq> x" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
263 |
have "?N ?gf ?gf' x y = norm (g' (?D f f' x y) + ?D g g' (f x) (f y)) / norm (y - x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
264 |
by (simp add: G.diff G.add field_simps) |
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
|
265 |
also have "\<dots> \<le> norm (g' (?D f f' x y)) / norm (y - x) + Ng y * (norm (f y - f x) / norm (y - x))" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
266 |
by (simp add: add_divide_distrib[symmetric] divide_right_mono norm_triangle_ineq G.zero Ng_def) |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
267 |
also have "\<dots> \<le> Nf y * kG + Ng y * (Nf y + kF)" |
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
|
268 |
proof (intro add_mono mult_left_mono) |
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
|
269 |
have "norm (f y - f x) = norm (?D f f' x y + f' (y - x))" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
270 |
by simp |
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
|
271 |
also have "\<dots> \<le> norm (?D f f' x y) + norm (f' (y - x))" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
272 |
by (rule norm_triangle_ineq) |
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
|
273 |
also have "\<dots> \<le> norm (?D f f' x y) + norm (y - x) * kF" |
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
|
274 |
using kF by (intro add_mono) simp |
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
|
275 |
finally show "norm (f y - f x) / norm (y - x) \<le> Nf y + kF" |
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
|
276 |
by (simp add: neq Nf_def field_simps) |
63558 | 277 |
qed (use kG in \<open>simp_all add: Ng_def Nf_def neq zero_le_divide_iff field_simps\<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
|
278 |
finally show "?N ?gf ?gf' x y \<le> Nf y * kG + Ng y * (Nf y + kF)" . |
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
|
279 |
next |
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
|
280 |
have [tendsto_intros]: "?L Nf" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
281 |
using f unfolding has_derivative_iff_norm Nf_def .. |
61973 | 282 |
from f have "(f \<longlongrightarrow> f x) (at x within s)" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
283 |
by (blast intro: has_derivative_continuous continuous_within[THEN iffD1]) |
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
|
284 |
then have f': "LIM x at x within s. f x :> inf (nhds (f x)) (principal (f`s))" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
285 |
unfolding filterlim_def |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
286 |
by (simp add: eventually_filtermap eventually_at_filter le_principal) |
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
|
287 |
|
61973 | 288 |
have "((?N g g' (f x)) \<longlongrightarrow> 0) (at (f x) within f`s)" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
289 |
using g unfolding has_derivative_iff_norm .. |
61973 | 290 |
then have g': "((?N g g' (f x)) \<longlongrightarrow> 0) (inf (nhds (f x)) (principal (f`s)))" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
291 |
by (rule tendsto_at_iff_tendsto_nhds_within[THEN iffD1, rotated]) simp |
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
|
292 |
|
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
|
293 |
have [tendsto_intros]: "?L Ng" |
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
|
294 |
unfolding Ng_def by (rule filterlim_compose[OF g' f']) |
61973 | 295 |
show "((\<lambda>y. Nf y * kG + Ng y * (Nf y + kF)) \<longlongrightarrow> 0) (at x within s)" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
296 |
by (intro tendsto_eq_intros) auto |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
297 |
qed simp |
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
|
298 |
qed |
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
|
299 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
300 |
lemma has_derivative_compose: |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
301 |
"(f has_derivative f') (at x within s) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
302 |
((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
303 |
by (blast intro: has_derivative_in_compose has_derivative_subset) |
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
|
304 |
|
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
|
305 |
lemma (in bounded_bilinear) FDERIV: |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
306 |
assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
307 |
shows "((\<lambda>x. f x ** g x) has_derivative (\<lambda>h. f x ** g' h + f' h ** g x)) (at x within s)" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
308 |
proof - |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
309 |
from bounded_linear.bounded [OF has_derivative_bounded_linear [OF f]] |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
310 |
obtain KF where norm_F: "\<And>x. norm (f' x) \<le> norm x * KF" by fast |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
311 |
|
63558 | 312 |
from pos_bounded obtain K |
313 |
where K: "0 < K" and norm_prod: "\<And>a b. norm (a ** b) \<le> norm a * norm b * K" |
|
314 |
by fast |
|
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
|
315 |
let ?D = "\<lambda>f f' y. f y - f x - f' (y - x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
316 |
let ?N = "\<lambda>f f' y. norm (?D f f' y) / norm (y - x)" |
63040 | 317 |
define Ng where "Ng = ?N g g'" |
318 |
define Nf where "Nf = ?N f f'" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
319 |
|
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
|
320 |
let ?fun1 = "\<lambda>y. norm (f y ** g y - f x ** g x - (f x ** g' (y - x) + f' (y - x) ** g x)) / norm (y - x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
321 |
let ?fun2 = "\<lambda>y. norm (f x) * Ng y * K + Nf y * norm (g y) * K + KF * norm (g y - g x) * K" |
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
|
322 |
let ?F = "at x within s" |
21164 | 323 |
|
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
|
324 |
show ?thesis |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
325 |
proof (rule has_derivativeI_sandwich[of 1]) |
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
|
326 |
show "bounded_linear (\<lambda>h. f x ** g' h + f' h ** g x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
327 |
by (intro bounded_linear_add |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
328 |
bounded_linear_compose [OF bounded_linear_right] bounded_linear_compose [OF bounded_linear_left] |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
329 |
has_derivative_bounded_linear [OF g] has_derivative_bounded_linear [OF f]) |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
330 |
next |
61973 | 331 |
from g have "(g \<longlongrightarrow> g x) ?F" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
332 |
by (intro continuous_within[THEN iffD1] has_derivative_continuous) |
61973 | 333 |
moreover from f g have "(Nf \<longlongrightarrow> 0) ?F" "(Ng \<longlongrightarrow> 0) ?F" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
334 |
by (simp_all add: has_derivative_iff_norm Ng_def Nf_def) |
61973 | 335 |
ultimately have "(?fun2 \<longlongrightarrow> norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K) ?F" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
336 |
by (intro tendsto_intros) (simp_all add: LIM_zero_iff) |
61973 | 337 |
then show "(?fun2 \<longlongrightarrow> 0) ?F" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
338 |
by simp |
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
|
339 |
next |
63558 | 340 |
fix y :: 'd |
341 |
assume "y \<noteq> x" |
|
342 |
have "?fun1 y = |
|
343 |
norm (f x ** ?D g g' y + ?D f f' y ** g y + f' (y - x) ** (g y - g x)) / norm (y - x)" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
344 |
by (simp add: diff_left diff_right add_left add_right field_simps) |
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
|
345 |
also have "\<dots> \<le> (norm (f x) * norm (?D g g' y) * K + norm (?D f f' y) * norm (g y) * K + |
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
|
346 |
norm (y - x) * KF * norm (g y - g x) * K) / norm (y - x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
347 |
by (intro divide_right_mono mult_mono' |
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
|
348 |
order_trans [OF norm_triangle_ineq add_mono] |
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
|
349 |
order_trans [OF norm_prod mult_right_mono] |
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
|
350 |
mult_nonneg_nonneg order_refl norm_ge_zero norm_F |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
351 |
K [THEN order_less_imp_le]) |
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
|
352 |
also have "\<dots> = ?fun2 y" |
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
|
353 |
by (simp add: add_divide_distrib Ng_def Nf_def) |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
354 |
finally show "?fun1 y \<le> ?fun2 y" . |
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
|
355 |
qed simp |
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
|
356 |
qed |
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
|
357 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
358 |
lemmas has_derivative_mult[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult] |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
359 |
lemmas has_derivative_scaleR[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR] |
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
|
360 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
361 |
lemma has_derivative_setprod[simp, derivative_intros]: |
63558 | 362 |
fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_field" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
363 |
assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
364 |
shows "((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))) (at x within s)" |
63558 | 365 |
proof (cases "finite I") |
366 |
case True |
|
367 |
from this f show ?thesis |
|
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
|
368 |
proof induct |
63558 | 369 |
case empty |
370 |
then show ?case by simp |
|
371 |
next |
|
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
|
372 |
case (insert i I) |
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
|
373 |
let ?P = "\<lambda>y. f i x * (\<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x)) + (f' i y) * (\<Prod>i\<in>I. f i x)" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
374 |
have "((\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) has_derivative ?P) (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
375 |
using insert by (intro has_derivative_mult) 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
|
376 |
also have "?P = (\<lambda>y. \<Sum>i'\<in>insert i I. f' i' y * (\<Prod>j\<in>insert i I - {i'}. f j x))" |
63558 | 377 |
using insert(1,2) |
378 |
by (auto simp add: setsum_right_distrib insert_Diff_if intro!: ext setsum.cong) |
|
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
|
379 |
finally show ?case |
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
|
380 |
using insert by simp |
63558 | 381 |
qed |
382 |
next |
|
383 |
case False |
|
384 |
then show ?thesis by simp |
|
385 |
qed |
|
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
|
386 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
387 |
lemma has_derivative_power[simp, derivative_intros]: |
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
|
388 |
fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
389 |
assumes f: "(f has_derivative f') (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
390 |
shows "((\<lambda>x. f x^n) has_derivative (\<lambda>y. of_nat n * f' y * f x^(n - 1))) (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
391 |
using has_derivative_setprod[OF f, of "{..< n}"] by (simp add: setprod_constant ac_simps) |
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
|
392 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
393 |
lemma has_derivative_inverse': |
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
|
394 |
fixes x :: "'a::real_normed_div_algebra" |
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
|
395 |
assumes x: "x \<noteq> 0" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
396 |
shows "(inverse has_derivative (\<lambda>h. - (inverse x * h * inverse x))) (at x within s)" |
63558 | 397 |
(is "(?inv has_derivative ?f) _") |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
398 |
proof (rule has_derivativeI_sandwich) |
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
|
399 |
show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
400 |
apply (rule bounded_linear_minus) |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
401 |
apply (rule bounded_linear_mult_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
|
402 |
apply (rule bounded_linear_const_mult) |
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
|
403 |
apply (rule bounded_linear_ident) |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
404 |
done |
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
|
405 |
show "0 < norm x" using x by simp |
61973 | 406 |
show "((\<lambda>y. norm (?inv y - ?inv x) * norm (?inv x)) \<longlongrightarrow> 0) (at x within s)" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
407 |
apply (rule tendsto_mult_left_zero) |
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
|
408 |
apply (rule tendsto_norm_zero) |
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
|
409 |
apply (rule LIM_zero) |
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
|
410 |
apply (rule tendsto_inverse) |
63558 | 411 |
apply (rule tendsto_ident_at) |
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
|
412 |
apply (rule x) |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
413 |
done |
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
|
414 |
next |
63558 | 415 |
fix y :: 'a |
416 |
assume h: "y \<noteq> x" "dist y x < norm x" |
|
62397
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
61976
diff
changeset
|
417 |
then have "y \<noteq> 0" by auto |
63558 | 418 |
have "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) = |
419 |
norm ((?inv y - ?inv x) * (y - x) * ?inv x) / norm (y - x)" |
|
60758 | 420 |
apply (subst inverse_diff_inverse [OF \<open>y \<noteq> 0\<close> x]) |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
421 |
apply (subst minus_diff_minus) |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
422 |
apply (subst norm_minus_cancel) |
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
|
423 |
apply (simp add: left_diff_distrib) |
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
|
424 |
done |
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
|
425 |
also have "\<dots> \<le> norm (?inv y - ?inv x) * norm (y - x) * norm (?inv x) / norm (y - x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
426 |
apply (rule divide_right_mono [OF _ norm_ge_zero]) |
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
|
427 |
apply (rule order_trans [OF norm_mult_ineq]) |
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
|
428 |
apply (rule mult_right_mono [OF _ norm_ge_zero]) |
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
|
429 |
apply (rule norm_mult_ineq) |
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
|
430 |
done |
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
|
431 |
also have "\<dots> = norm (?inv y - ?inv x) * norm (?inv x)" |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
432 |
by simp |
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
|
433 |
finally show "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) \<le> |
63558 | 434 |
norm (?inv y - ?inv x) * norm (?inv x)" . |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
435 |
qed |
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
|
436 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
437 |
lemma has_derivative_inverse[simp, derivative_intros]: |
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
|
438 |
fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra" |
63558 | 439 |
assumes x: "f x \<noteq> 0" |
440 |
and f: "(f has_derivative f') (at x within s)" |
|
441 |
shows "((\<lambda>x. inverse (f x)) has_derivative (\<lambda>h. - (inverse (f x) * f' h * inverse (f x)))) |
|
442 |
(at x within s)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
443 |
using has_derivative_compose[OF f has_derivative_inverse', OF x] . |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
444 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
445 |
lemma has_derivative_divide[simp, derivative_intros]: |
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
|
446 |
fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra" |
63558 | 447 |
assumes f: "(f has_derivative f') (at x within s)" |
448 |
and g: "(g has_derivative g') (at x within s)" |
|
55967 | 449 |
assumes x: "g x \<noteq> 0" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
450 |
shows "((\<lambda>x. f x / g x) has_derivative |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
451 |
(\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)) (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
452 |
using has_derivative_mult[OF f has_derivative_inverse[OF x g]] |
56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset
|
453 |
by (simp add: field_simps) |
55967 | 454 |
|
63558 | 455 |
|
456 |
text \<open>Conventional form requires mult-AC laws. Types real and complex only.\<close> |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
457 |
|
63558 | 458 |
lemma has_derivative_divide'[derivative_intros]: |
55967 | 459 |
fixes f :: "_ \<Rightarrow> 'a::real_normed_field" |
63558 | 460 |
assumes f: "(f has_derivative f') (at x within s)" |
461 |
and g: "(g has_derivative g') (at x within s)" |
|
462 |
and x: "g x \<noteq> 0" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
463 |
shows "((\<lambda>x. f x / g x) has_derivative (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))) (at x within s)" |
55967 | 464 |
proof - |
63558 | 465 |
have "f' h / g x - f x * (inverse (g x) * g' h * inverse (g x)) = |
466 |
(f' h * g x - f x * g' h) / (g x * g x)" for h |
|
467 |
by (simp add: field_simps x) |
|
55967 | 468 |
then show ?thesis |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
469 |
using has_derivative_divide [OF f g] x |
55967 | 470 |
by simp |
471 |
qed |
|
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
|
472 |
|
63558 | 473 |
|
60758 | 474 |
subsection \<open>Uniqueness\<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
|
475 |
|
60758 | 476 |
text \<open> |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
477 |
This can not generally shown for @{const has_derivative}, as we need to approach the point from |
61799 | 478 |
all directions. There is a proof in \<open>Multivariate_Analysis\<close> for \<open>euclidean_space\<close>. |
60758 | 479 |
\<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
|
480 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
481 |
lemma has_derivative_zero_unique: |
63558 | 482 |
assumes "((\<lambda>x. 0) has_derivative F) (at x)" |
483 |
shows "F = (\<lambda>h. 0)" |
|
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
|
484 |
proof - |
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
|
485 |
interpret F: bounded_linear F |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
486 |
using assms by (rule has_derivative_bounded_linear) |
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
|
487 |
let ?r = "\<lambda>h. norm (F h) / norm h" |
61976 | 488 |
have *: "?r \<midarrow>0\<rightarrow> 0" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
489 |
using assms unfolding has_derivative_at by simp |
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
|
490 |
show "F = (\<lambda>h. 0)" |
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
|
491 |
proof |
63558 | 492 |
show "F h = 0" for h |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
493 |
proof (rule ccontr) |
63558 | 494 |
assume **: "\<not> ?thesis" |
495 |
then have h: "h \<noteq> 0" |
|
496 |
by (auto simp add: F.zero) |
|
497 |
with ** have "0 < ?r h" |
|
498 |
by simp |
|
499 |
from LIM_D [OF * this] obtain s |
|
500 |
where s: "0 < s" and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" |
|
501 |
by 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
|
502 |
from dense [OF s] obtain t where t: "0 < t \<and> t < s" .. |
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
503 |
let ?x = "scaleR (t / norm h) h" |
63558 | 504 |
have "?x \<noteq> 0" and "norm ?x < s" |
505 |
using t h by simp_all |
|
506 |
then have "?r ?x < ?r h" |
|
507 |
by (rule r) |
|
508 |
then show False |
|
509 |
using t h by (simp add: F.scaleR) |
|
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
|
510 |
qed |
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
|
511 |
qed |
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
|
512 |
qed |
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
|
513 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
514 |
lemma has_derivative_unique: |
63558 | 515 |
assumes "(f has_derivative F) (at x)" |
516 |
and "(f has_derivative F') (at x)" |
|
517 |
shows "F = F'" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
518 |
proof - |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
519 |
have "((\<lambda>x. 0) has_derivative (\<lambda>h. F h - F' h)) (at x)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
520 |
using has_derivative_diff [OF assms] by simp |
63558 | 521 |
then have "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
522 |
by (rule has_derivative_zero_unique) |
63558 | 523 |
then show "F = F'" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
524 |
unfolding fun_eq_iff right_minus_eq . |
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
|
525 |
qed |
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
|
526 |
|
63558 | 527 |
|
60758 | 528 |
subsection \<open>Differentiability predicate\<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
|
529 |
|
63558 | 530 |
definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" |
531 |
(infix "differentiable" 50) |
|
532 |
where "f differentiable F \<longleftrightarrow> (\<exists>D. (f has_derivative D) F)" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
533 |
|
63558 | 534 |
lemma differentiable_subset: |
535 |
"f differentiable (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f differentiable (at x within t)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
536 |
unfolding differentiable_def by (blast intro: has_derivative_subset) |
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
|
537 |
|
56261 | 538 |
lemmas differentiable_within_subset = differentiable_subset |
539 |
||
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
540 |
lemma differentiable_ident [simp, derivative_intros]: "(\<lambda>x. x) differentiable F" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
541 |
unfolding differentiable_def by (blast intro: has_derivative_ident) |
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
|
542 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
543 |
lemma differentiable_const [simp, derivative_intros]: "(\<lambda>z. a) differentiable F" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
544 |
unfolding differentiable_def by (blast intro: has_derivative_const) |
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
|
545 |
|
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
|
546 |
lemma differentiable_in_compose: |
63558 | 547 |
"f differentiable (at (g x) within (g`s)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> |
548 |
(\<lambda>x. f (g x)) differentiable (at x within s)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
549 |
unfolding differentiable_def by (blast intro: has_derivative_in_compose) |
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
|
550 |
|
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
|
551 |
lemma differentiable_compose: |
63558 | 552 |
"f differentiable (at (g x)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> |
553 |
(\<lambda>x. f (g x)) differentiable (at x within s)" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
554 |
by (blast intro: differentiable_in_compose differentiable_subset) |
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
|
555 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
556 |
lemma differentiable_sum [simp, derivative_intros]: |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
557 |
"f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
558 |
unfolding differentiable_def by (blast intro: has_derivative_add) |
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
|
559 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
560 |
lemma differentiable_minus [simp, derivative_intros]: |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
561 |
"f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
562 |
unfolding differentiable_def by (blast intro: has_derivative_minus) |
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
|
563 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
564 |
lemma differentiable_diff [simp, derivative_intros]: |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
565 |
"f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x - g x) differentiable F" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
566 |
unfolding differentiable_def by (blast intro: has_derivative_diff) |
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
|
567 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
568 |
lemma differentiable_mult [simp, derivative_intros]: |
63558 | 569 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
570 |
shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> |
|
571 |
(\<lambda>x. f x * g x) differentiable (at x within s)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
572 |
unfolding differentiable_def by (blast intro: has_derivative_mult) |
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
|
573 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
574 |
lemma differentiable_inverse [simp, derivative_intros]: |
63558 | 575 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_field" |
576 |
shows "f differentiable (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> |
|
577 |
(\<lambda>x. inverse (f x)) differentiable (at x within s)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
578 |
unfolding differentiable_def by (blast intro: has_derivative_inverse) |
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
|
579 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
580 |
lemma differentiable_divide [simp, derivative_intros]: |
63558 | 581 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_field" |
582 |
shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> |
|
583 |
g x \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / g x) differentiable (at x within s)" |
|
63092 | 584 |
unfolding divide_inverse by simp |
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
|
585 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
586 |
lemma differentiable_power [simp, derivative_intros]: |
63558 | 587 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_field" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
588 |
shows "f differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
589 |
unfolding differentiable_def by (blast intro: has_derivative_power) |
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
|
590 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
591 |
lemma differentiable_scaleR [simp, derivative_intros]: |
63558 | 592 |
"f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> |
593 |
(\<lambda>x. f x *\<^sub>R g x) differentiable (at x within s)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
594 |
unfolding differentiable_def by (blast intro: has_derivative_scaleR) |
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
|
595 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
596 |
lemma has_derivative_imp_has_field_derivative: |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
597 |
"(f has_derivative D) F \<Longrightarrow> (\<And>x. x * D' = D x) \<Longrightarrow> (f has_field_derivative D') F" |
63558 | 598 |
unfolding has_field_derivative_def |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
599 |
by (rule has_derivative_eq_rhs[of f D]) (simp_all add: fun_eq_iff mult.commute) |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
600 |
|
63558 | 601 |
lemma has_field_derivative_imp_has_derivative: |
602 |
"(f has_field_derivative D) F \<Longrightarrow> (f has_derivative op * D) F" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
603 |
by (simp add: has_field_derivative_def) |
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
|
604 |
|
63558 | 605 |
lemma DERIV_subset: |
606 |
"(f has_field_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> |
|
607 |
(f has_field_derivative f') (at x within t)" |
|
56261 | 608 |
by (simp add: has_field_derivative_def has_derivative_within_subset) |
609 |
||
59862 | 610 |
lemma has_field_derivative_at_within: |
63558 | 611 |
"(f has_field_derivative f') (at x) \<Longrightarrow> (f has_field_derivative f') (at x within s)" |
59862 | 612 |
using DERIV_subset by blast |
613 |
||
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
614 |
abbreviation (input) |
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
615 |
DERIV :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
63558 | 616 |
("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) |
617 |
where "DERIV f x :> D \<equiv> (f has_field_derivative D) (at x)" |
|
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
618 |
|
63558 | 619 |
abbreviation has_real_derivative :: "(real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> real filter \<Rightarrow> bool" |
620 |
(infix "(has'_real'_derivative)" 50) |
|
621 |
where "(f has_real_derivative D) F \<equiv> (f has_field_derivative D) F" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
622 |
|
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
623 |
lemma real_differentiable_def: |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
624 |
"f differentiable at x within s \<longleftrightarrow> (\<exists>D. (f has_real_derivative D) (at x within s))" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
625 |
proof safe |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
626 |
assume "f differentiable at x within s" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
627 |
then obtain f' where *: "(f has_derivative f') (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
628 |
unfolding differentiable_def by auto |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
629 |
then obtain c where "f' = (op * c)" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
630 |
by (metis real_bounded_linear has_derivative_bounded_linear mult.commute fun_eq_iff) |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
631 |
with * show "\<exists>D. (f has_real_derivative D) (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
632 |
unfolding has_field_derivative_def by auto |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
633 |
qed (auto simp: differentiable_def has_field_derivative_def) |
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
|
634 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
635 |
lemma real_differentiableE [elim?]: |
63558 | 636 |
assumes f: "f differentiable (at x within s)" |
637 |
obtains df where "(f has_real_derivative df) (at x within s)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
638 |
using assms by (auto simp: real_differentiable_def) |
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
|
639 |
|
63558 | 640 |
lemma differentiableD: |
641 |
"f differentiable (at x within s) \<Longrightarrow> \<exists>D. (f has_real_derivative D) (at x within s)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
642 |
by (auto elim: real_differentiableE) |
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
|
643 |
|
63558 | 644 |
lemma differentiableI: |
645 |
"(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
646 |
by (force simp add: real_differentiable_def) |
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
|
647 |
|
63079 | 648 |
lemma has_field_derivative_iff: |
649 |
"(f has_field_derivative D) (at x within S) \<longleftrightarrow> |
|
650 |
((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> D) (at x within S)" |
|
651 |
apply (simp add: has_field_derivative_def has_derivative_iff_norm bounded_linear_mult_right |
|
63558 | 652 |
LIM_zero_iff[symmetric, of _ D]) |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
653 |
apply (subst (2) tendsto_norm_zero_iff[symmetric]) |
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
|
654 |
apply (rule filterlim_cong) |
63558 | 655 |
apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide) |
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
|
656 |
done |
21164 | 657 |
|
63079 | 658 |
lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" |
659 |
unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff .. |
|
660 |
||
63558 | 661 |
lemma mult_commute_abs: "(\<lambda>x. x * c) = op * c" |
662 |
for c :: "'a::ab_semigroup_mult" |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
663 |
by (simp add: fun_eq_iff mult.commute) |
21164 | 664 |
|
63558 | 665 |
|
60758 | 666 |
subsection \<open>Vector derivative\<close> |
60177 | 667 |
|
668 |
lemma has_field_derivative_iff_has_vector_derivative: |
|
669 |
"(f has_field_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F" |
|
670 |
unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs .. |
|
671 |
||
672 |
lemma has_field_derivative_subset: |
|
63558 | 673 |
"(f has_field_derivative y) (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> |
674 |
(f has_field_derivative y) (at x within t)" |
|
60177 | 675 |
unfolding has_field_derivative_def by (rule has_derivative_subset) |
676 |
||
677 |
lemma has_vector_derivative_const[simp, derivative_intros]: "((\<lambda>x. c) has_vector_derivative 0) net" |
|
678 |
by (auto simp: has_vector_derivative_def) |
|
679 |
||
680 |
lemma has_vector_derivative_id[simp, derivative_intros]: "((\<lambda>x. x) has_vector_derivative 1) net" |
|
681 |
by (auto simp: has_vector_derivative_def) |
|
682 |
||
683 |
lemma has_vector_derivative_minus[derivative_intros]: |
|
684 |
"(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. - f x) has_vector_derivative (- f')) net" |
|
685 |
by (auto simp: has_vector_derivative_def) |
|
686 |
||
687 |
lemma has_vector_derivative_add[derivative_intros]: |
|
688 |
"(f has_vector_derivative f') net \<Longrightarrow> (g has_vector_derivative g') net \<Longrightarrow> |
|
689 |
((\<lambda>x. f x + g x) has_vector_derivative (f' + g')) net" |
|
690 |
by (auto simp: has_vector_derivative_def scaleR_right_distrib) |
|
691 |
||
692 |
lemma has_vector_derivative_setsum[derivative_intros]: |
|
693 |
"(\<And>i. i \<in> I \<Longrightarrow> (f i has_vector_derivative f' i) net) \<Longrightarrow> |
|
694 |
((\<lambda>x. \<Sum>i\<in>I. f i x) has_vector_derivative (\<Sum>i\<in>I. f' i)) net" |
|
695 |
by (auto simp: has_vector_derivative_def fun_eq_iff scaleR_setsum_right intro!: derivative_eq_intros) |
|
696 |
||
697 |
lemma has_vector_derivative_diff[derivative_intros]: |
|
698 |
"(f has_vector_derivative f') net \<Longrightarrow> (g has_vector_derivative g') net \<Longrightarrow> |
|
699 |
((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net" |
|
700 |
by (auto simp: has_vector_derivative_def scaleR_diff_right) |
|
701 |
||
61204 | 702 |
lemma has_vector_derivative_add_const: |
63558 | 703 |
"((\<lambda>t. g t + z) has_vector_derivative f') net = ((\<lambda>t. g t) has_vector_derivative f') net" |
704 |
apply (intro iffI) |
|
705 |
apply (drule has_vector_derivative_diff [where g = "\<lambda>t. z", OF _ has_vector_derivative_const]) |
|
706 |
apply simp |
|
707 |
apply (drule has_vector_derivative_add [OF _ has_vector_derivative_const]) |
|
708 |
apply simp |
|
709 |
done |
|
61204 | 710 |
|
711 |
lemma has_vector_derivative_diff_const: |
|
63558 | 712 |
"((\<lambda>t. g t - z) has_vector_derivative f') net = ((\<lambda>t. g t) has_vector_derivative f') net" |
713 |
using has_vector_derivative_add_const [where z = "-z"] |
|
714 |
by simp |
|
61204 | 715 |
|
60177 | 716 |
lemma (in bounded_linear) has_vector_derivative: |
717 |
assumes "(g has_vector_derivative g') F" |
|
718 |
shows "((\<lambda>x. f (g x)) has_vector_derivative f g') F" |
|
719 |
using has_derivative[OF assms[unfolded has_vector_derivative_def]] |
|
720 |
by (simp add: has_vector_derivative_def scaleR) |
|
721 |
||
722 |
lemma (in bounded_bilinear) has_vector_derivative: |
|
723 |
assumes "(f has_vector_derivative f') (at x within s)" |
|
724 |
and "(g has_vector_derivative g') (at x within s)" |
|
725 |
shows "((\<lambda>x. f x ** g x) has_vector_derivative (f x ** g' + f' ** g x)) (at x within s)" |
|
726 |
using FDERIV[OF assms(1-2)[unfolded has_vector_derivative_def]] |
|
727 |
by (simp add: has_vector_derivative_def scaleR_right scaleR_left scaleR_right_distrib) |
|
728 |
||
729 |
lemma has_vector_derivative_scaleR[derivative_intros]: |
|
730 |
"(f has_field_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow> |
|
731 |
((\<lambda>x. f x *\<^sub>R g x) has_vector_derivative (f x *\<^sub>R g' + f' *\<^sub>R g x)) (at x within s)" |
|
732 |
unfolding has_field_derivative_iff_has_vector_derivative |
|
733 |
by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_scaleR]) |
|
734 |
||
735 |
lemma has_vector_derivative_mult[derivative_intros]: |
|
736 |
"(f has_vector_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow> |
|
63558 | 737 |
((\<lambda>x. f x * g x) has_vector_derivative (f x * g' + f' * g x)) (at x within s)" |
738 |
for f g :: "real \<Rightarrow> 'a::real_normed_algebra" |
|
60177 | 739 |
by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult]) |
740 |
||
741 |
lemma has_vector_derivative_of_real[derivative_intros]: |
|
742 |
"(f has_field_derivative D) F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_vector_derivative (of_real D)) F" |
|
743 |
by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real]) |
|
63558 | 744 |
(simp add: has_field_derivative_iff_has_vector_derivative) |
60177 | 745 |
|
63558 | 746 |
lemma has_vector_derivative_continuous: |
747 |
"(f has_vector_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f" |
|
60177 | 748 |
by (auto intro: has_derivative_continuous simp: has_vector_derivative_def) |
749 |
||
750 |
lemma has_vector_derivative_mult_right[derivative_intros]: |
|
63558 | 751 |
fixes a :: "'a::real_normed_algebra" |
60177 | 752 |
shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. a * f x) has_vector_derivative (a * x)) F" |
753 |
by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_right]) |
|
754 |
||
755 |
lemma has_vector_derivative_mult_left[derivative_intros]: |
|
63558 | 756 |
fixes a :: "'a::real_normed_algebra" |
60177 | 757 |
shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x * a) has_vector_derivative (x * a)) F" |
758 |
by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_left]) |
|
759 |
||
760 |
||
60758 | 761 |
subsection \<open>Derivatives\<close> |
21164 | 762 |
|
61976 | 763 |
lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" |
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
764 |
by (simp add: DERIV_def) |
21164 | 765 |
|
63079 | 766 |
lemma has_field_derivativeD: |
767 |
"(f has_field_derivative D) (at x within S) \<Longrightarrow> |
|
768 |
((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> D) (at x within S)" |
|
769 |
by (simp add: has_field_derivative_iff) |
|
770 |
||
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
771 |
lemma DERIV_const [simp, derivative_intros]: "((\<lambda>x. k) has_field_derivative 0) F" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
772 |
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_const]) auto |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
773 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
774 |
lemma DERIV_ident [simp, derivative_intros]: "((\<lambda>x. x) has_field_derivative 1) F" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
775 |
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_ident]) auto |
21164 | 776 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
777 |
lemma field_differentiable_add[derivative_intros]: |
63558 | 778 |
"(f has_field_derivative f') F \<Longrightarrow> (g has_field_derivative g') F \<Longrightarrow> |
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
779 |
((\<lambda>z. f z + g z) has_field_derivative f' + g') F" |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
780 |
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_add]) |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
781 |
(auto simp: has_field_derivative_def field_simps mult_commute_abs) |
56261 | 782 |
|
783 |
corollary DERIV_add: |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
784 |
"(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow> |
63558 | 785 |
((\<lambda>x. f x + g x) has_field_derivative D + E) (at x within s)" |
56261 | 786 |
by (rule field_differentiable_add) |
787 |
||
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
788 |
lemma field_differentiable_minus[derivative_intros]: |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
789 |
"(f has_field_derivative f') F \<Longrightarrow> ((\<lambda>z. - (f z)) has_field_derivative -f') F" |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
790 |
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus]) |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
791 |
(auto simp: has_field_derivative_def field_simps mult_commute_abs) |
21164 | 792 |
|
63558 | 793 |
corollary DERIV_minus: |
794 |
"(f has_field_derivative D) (at x within s) \<Longrightarrow> |
|
795 |
((\<lambda>x. - f x) has_field_derivative -D) (at x within s)" |
|
56261 | 796 |
by (rule field_differentiable_minus) |
21164 | 797 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
798 |
lemma field_differentiable_diff[derivative_intros]: |
63558 | 799 |
"(f has_field_derivative f') F \<Longrightarrow> |
800 |
(g has_field_derivative g') F \<Longrightarrow> ((\<lambda>z. f z - g z) has_field_derivative f' - g') F" |
|
63092 | 801 |
by (simp only: diff_conv_add_uminus field_differentiable_add field_differentiable_minus) |
56261 | 802 |
|
803 |
corollary DERIV_diff: |
|
63558 | 804 |
"(f has_field_derivative D) (at x within s) \<Longrightarrow> |
805 |
(g has_field_derivative E) (at x within s) \<Longrightarrow> |
|
806 |
((\<lambda>x. f x - g x) has_field_derivative D - E) (at x within s)" |
|
56261 | 807 |
by (rule field_differentiable_diff) |
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
|
808 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
809 |
lemma DERIV_continuous: "(f has_field_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
810 |
by (drule has_derivative_continuous[OF has_field_derivative_imp_has_derivative]) simp |
21164 | 811 |
|
56261 | 812 |
corollary DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x" |
813 |
by (rule DERIV_continuous) |
|
814 |
||
815 |
lemma DERIV_continuous_on: |
|
63299 | 816 |
"(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative (D x)) (at x within s)) \<Longrightarrow> continuous_on s f" |
817 |
unfolding continuous_on_eq_continuous_within |
|
63558 | 818 |
by (intro continuous_at_imp_continuous_on ballI DERIV_continuous) |
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
|
819 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
820 |
lemma DERIV_mult': |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
821 |
"(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow> |
63558 | 822 |
((\<lambda>x. f x * g x) has_field_derivative f x * E + D * g x) (at x within s)" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
823 |
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult]) |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
824 |
(auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative) |
21164 | 825 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
826 |
lemma DERIV_mult[derivative_intros]: |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
827 |
"(f has_field_derivative Da) (at x within s) \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow> |
63558 | 828 |
((\<lambda>x. f x * g x) has_field_derivative Da * g x + Db * f x) (at x within s)" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
829 |
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult]) |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
830 |
(auto simp: field_simps dest: has_field_derivative_imp_has_derivative) |
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
|
831 |
|
60758 | 832 |
text \<open>Derivative of linear multiplication\<close> |
21164 | 833 |
|
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
|
834 |
lemma DERIV_cmult: |
63558 | 835 |
"(f has_field_derivative D) (at x within s) \<Longrightarrow> |
836 |
((\<lambda>x. c * f x) has_field_derivative c * D) (at x within s)" |
|
837 |
by (drule DERIV_mult' [OF DERIV_const]) simp |
|
21164 | 838 |
|
55967 | 839 |
lemma DERIV_cmult_right: |
63558 | 840 |
"(f has_field_derivative D) (at x within s) \<Longrightarrow> |
841 |
((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)" |
|
842 |
using DERIV_cmult by (auto simp add: ac_simps) |
|
55967 | 843 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
844 |
lemma DERIV_cmult_Id [simp]: "(op * c has_field_derivative c) (at x within s)" |
63558 | 845 |
using DERIV_ident [THEN DERIV_cmult, where c = c and x = x] by simp |
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
|
846 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
847 |
lemma DERIV_cdivide: |
63558 | 848 |
"(f has_field_derivative D) (at x within s) \<Longrightarrow> |
849 |
((\<lambda>x. f x / c) has_field_derivative D / c) (at x within s)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
850 |
using DERIV_cmult_right[of f D x s "1 / c"] by simp |
21164 | 851 |
|
63558 | 852 |
lemma DERIV_unique: "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E" |
853 |
unfolding DERIV_def by (rule LIM_unique) |
|
21164 | 854 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
855 |
lemma DERIV_setsum[derivative_intros]: |
63558 | 856 |
"(\<And> n. n \<in> S \<Longrightarrow> ((\<lambda>x. f x n) has_field_derivative (f' x n)) F) \<Longrightarrow> |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
857 |
((\<lambda>x. setsum (f x) S) has_field_derivative setsum (f' x) S) F" |
63558 | 858 |
by (rule has_derivative_imp_has_field_derivative [OF has_derivative_setsum]) |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
859 |
(auto simp: setsum_right_distrib mult_commute_abs dest: has_field_derivative_imp_has_derivative) |
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
|
860 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
861 |
lemma DERIV_inverse'[derivative_intros]: |
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset
|
862 |
assumes "(f has_field_derivative D) (at x within s)" |
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset
|
863 |
and "f x \<noteq> 0" |
63558 | 864 |
shows "((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) |
865 |
(at x within s)" |
|
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset
|
866 |
proof - |
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset
|
867 |
have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative op * D)" |
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset
|
868 |
by (rule arg_cong [of "\<lambda>x. x * D"]) (simp add: fun_eq_iff) |
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset
|
869 |
with assms have "(f has_derivative (\<lambda>x. x * D)) (at x within s)" |
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset
|
870 |
by (auto dest!: has_field_derivative_imp_has_derivative) |
60758 | 871 |
then show ?thesis using \<open>f x \<noteq> 0\<close> |
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset
|
872 |
by (auto intro: has_derivative_imp_has_field_derivative has_derivative_inverse) |
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59862
diff
changeset
|
873 |
qed |
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
|
874 |
|
61799 | 875 |
text \<open>Power of \<open>-1\<close>\<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
|
876 |
|
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
|
877 |
lemma DERIV_inverse: |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
878 |
"x \<noteq> 0 \<Longrightarrow> ((\<lambda>x. inverse(x)) has_field_derivative - (inverse x ^ Suc (Suc 0))) (at x within s)" |
51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset
|
879 |
by (drule DERIV_inverse' [OF DERIV_ident]) simp |
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
|
880 |
|
60758 | 881 |
text \<open>Derivative of inverse\<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
|
882 |
|
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
|
883 |
lemma DERIV_inverse_fun: |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
884 |
"(f has_field_derivative d) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> |
63558 | 885 |
((\<lambda>x. inverse (f x)) has_field_derivative (- (d * inverse(f x ^ Suc (Suc 0))))) (at x within s)" |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
886 |
by (drule (1) DERIV_inverse') (simp add: ac_simps nonzero_inverse_mult_distrib) |
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
|
887 |
|
60758 | 888 |
text \<open>Derivative of quotient\<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
|
889 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
890 |
lemma DERIV_divide[derivative_intros]: |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
891 |
"(f has_field_derivative D) (at x within s) \<Longrightarrow> |
63558 | 892 |
(g has_field_derivative E) (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> |
893 |
((\<lambda>x. f x / g x) has_field_derivative (D * g x - f x * E) / (g x * g x)) (at x within s)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
894 |
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_divide]) |
56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset
|
895 |
(auto dest: has_field_derivative_imp_has_derivative simp: field_simps) |
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
|
896 |
|
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
|
897 |
lemma DERIV_quotient: |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
898 |
"(f has_field_derivative d) (at x within s) \<Longrightarrow> |
63558 | 899 |
(g has_field_derivative e) (at x within s)\<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> |
900 |
((\<lambda>y. f y / g y) has_field_derivative (d * g x - (e * f x)) / (g x ^ Suc (Suc 0))) (at x within s)" |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
901 |
by (drule (2) DERIV_divide) (simp add: mult.commute) |
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
|
902 |
|
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
|
903 |
lemma DERIV_power_Suc: |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
904 |
"(f has_field_derivative D) (at x within s) \<Longrightarrow> |
63558 | 905 |
((\<lambda>x. f x ^ Suc n) has_field_derivative (1 + of_nat n) * (D * f x ^ n)) (at x within s)" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
906 |
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power]) |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
907 |
(auto simp: has_field_derivative_def) |
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
|
908 |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
909 |
lemma DERIV_power[derivative_intros]: |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
910 |
"(f has_field_derivative D) (at x within s) \<Longrightarrow> |
63558 | 911 |
((\<lambda>x. f x ^ n) has_field_derivative of_nat n * (D * f x ^ (n - Suc 0))) (at x within s)" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
912 |
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power]) |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
913 |
(auto simp: has_field_derivative_def) |
31880 | 914 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
915 |
lemma DERIV_pow: "((\<lambda>x. x ^ n) has_field_derivative real n * (x ^ (n - Suc 0))) (at x within s)" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset
|
916 |
using DERIV_power [OF DERIV_ident] by simp |
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
|
917 |
|
63558 | 918 |
lemma DERIV_chain': "(f has_field_derivative D) (at x within s) \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow> |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
919 |
((\<lambda>x. g (f x)) has_field_derivative E * D) (at x within s)" |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
920 |
using has_derivative_compose[of f "op * D" x s g "op * E"] |
63170 | 921 |
by (simp only: has_field_derivative_def mult_commute_abs ac_simps) |
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
|
922 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
923 |
corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow> |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
924 |
((\<lambda>x. f (g x)) has_field_derivative Da * Db) (at x within s)" |
55967 | 925 |
by (rule DERIV_chain') |
926 |
||
60758 | 927 |
text \<open>Standard version\<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
|
928 |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
929 |
lemma DERIV_chain: |
63558 | 930 |
"DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow> |
931 |
(f \<circ> g has_field_derivative Da * Db) (at x within s)" |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
932 |
by (drule (1) DERIV_chain', simp add: o_def mult.commute) |
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
|
933 |
|
63558 | 934 |
lemma DERIV_image_chain: |
935 |
"(f has_field_derivative Da) (at (g x) within (g ` s)) \<Longrightarrow> |
|
936 |
(g has_field_derivative Db) (at x within s) \<Longrightarrow> |
|
937 |
(f \<circ> g has_field_derivative Da * Db) (at x within s)" |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
938 |
using has_derivative_in_compose [of g "op * Db" x s f "op * Da "] |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
939 |
by (simp add: has_field_derivative_def o_def mult_commute_abs ac_simps) |
55967 | 940 |
|
941 |
(*These two are from HOL Light: HAS_COMPLEX_DERIVATIVE_CHAIN*) |
|
942 |
lemma DERIV_chain_s: |
|
943 |
assumes "(\<And>x. x \<in> s \<Longrightarrow> DERIV g x :> g'(x))" |
|
63558 | 944 |
and "DERIV f x :> f'" |
945 |
and "f x \<in> s" |
|
946 |
shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)" |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
947 |
by (metis (full_types) DERIV_chain' mult.commute assms) |
55967 | 948 |
|
949 |
lemma DERIV_chain3: (*HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV*) |
|
950 |
assumes "(\<And>x. DERIV g x :> g'(x))" |
|
63558 | 951 |
and "DERIV f x :> f'" |
952 |
shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)" |
|
55967 | 953 |
by (metis UNIV_I DERIV_chain_s [of UNIV] assms) |
954 |
||
63558 | 955 |
text \<open>Alternative definition for differentiability\<close> |
21164 | 956 |
|
957 |
lemma DERIV_LIM_iff: |
|
63558 | 958 |
fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a" |
959 |
shows "((\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0\<rightarrow> D) = ((\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D)" |
|
960 |
apply (rule iffI) |
|
961 |
apply (drule_tac k="- a" in LIM_offset) |
|
962 |
apply simp |
|
963 |
apply (drule_tac k="a" in LIM_offset) |
|
964 |
apply (simp add: add.commute) |
|
965 |
done |
|
21164 | 966 |
|
63079 | 967 |
lemmas DERIV_iff2 = has_field_derivative_iff |
968 |
||
969 |
lemma has_field_derivative_cong_ev: |
|
970 |
assumes "x = y" |
|
971 |
and *: "eventually (\<lambda>x. x \<in> s \<longrightarrow> f x = g x) (nhds x)" |
|
972 |
and "u = v" "s = t" "x \<in> s" |
|
63558 | 973 |
shows "(f has_field_derivative u) (at x within s) = (g has_field_derivative v) (at y within t)" |
63079 | 974 |
unfolding DERIV_iff2 |
975 |
proof (rule filterlim_cong) |
|
63558 | 976 |
from assms have "f y = g y" |
977 |
by (auto simp: eventually_nhds) |
|
63079 | 978 |
with * show "\<forall>\<^sub>F xa in at x within s. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)" |
979 |
unfolding eventually_at_filter |
|
980 |
by eventually_elim (auto simp: assms \<open>f y = g y\<close>) |
|
981 |
qed (simp_all add: assms) |
|
21164 | 982 |
|
63558 | 983 |
lemma DERIV_cong_ev: |
984 |
"x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow> |
|
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
|
985 |
DERIV f x :> u \<longleftrightarrow> DERIV g y :> v" |
63079 | 986 |
by (rule has_field_derivative_cong_ev) simp_all |
21164 | 987 |
|
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
|
988 |
lemma DERIV_shift: |
63079 | 989 |
"(f has_field_derivative y) (at (x + z)) = ((\<lambda>x. f (x + z)) has_field_derivative y) (at x)" |
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
990 |
by (simp add: DERIV_def field_simps) |
21164 | 991 |
|
63558 | 992 |
lemma DERIV_mirror: "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x)) x :> - y)" |
993 |
for f :: "real \<Rightarrow> real" and x y :: real |
|
56479
91958d4b30f7
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents:
56409
diff
changeset
|
994 |
by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right |
63558 | 995 |
tendsto_minus_cancel_left field_simps conj_commute) |
21164 | 996 |
|
63263
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
63170
diff
changeset
|
997 |
lemma floor_has_real_derivative: |
63558 | 998 |
fixes f :: "real \<Rightarrow> 'a::{floor_ceiling,order_topology}" |
63263
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
63170
diff
changeset
|
999 |
assumes "isCont f x" |
63558 | 1000 |
and "f x \<notin> \<int>" |
63263
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
63170
diff
changeset
|
1001 |
shows "((\<lambda>x. floor (f x)) has_real_derivative 0) (at x)" |
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
63170
diff
changeset
|
1002 |
proof (subst DERIV_cong_ev[OF refl _ refl]) |
63558 | 1003 |
show "((\<lambda>_. floor (f x)) has_real_derivative 0) (at x)" |
1004 |
by simp |
|
63263
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
63170
diff
changeset
|
1005 |
have "\<forall>\<^sub>F y in at x. \<lfloor>f y\<rfloor> = \<lfloor>f x\<rfloor>" |
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
63170
diff
changeset
|
1006 |
by (rule eventually_floor_eq[OF assms[unfolded continuous_at]]) |
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
63170
diff
changeset
|
1007 |
then show "\<forall>\<^sub>F y in nhds x. real_of_int \<lfloor>f y\<rfloor> = real_of_int \<lfloor>f x\<rfloor>" |
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
63170
diff
changeset
|
1008 |
unfolding eventually_at_filter |
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
63170
diff
changeset
|
1009 |
by eventually_elim auto |
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
63170
diff
changeset
|
1010 |
qed |
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
63170
diff
changeset
|
1011 |
|
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
63170
diff
changeset
|
1012 |
|
60758 | 1013 |
text \<open>Caratheodory formulation of derivative at a point\<close> |
21164 | 1014 |
|
55970
6d123f0ae358
Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents:
55967
diff
changeset
|
1015 |
lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*) |
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
|
1016 |
"(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)" |
63558 | 1017 |
(is "?lhs = ?rhs") |
21164 | 1018 |
proof |
63558 | 1019 |
assume ?lhs |
1020 |
show "\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l" |
|
21164 | 1021 |
proof (intro exI conjI) |
63558 | 1022 |
let ?g = "(\<lambda>z. if z = x then l else (f z - f x) / (z-x))" |
1023 |
show "\<forall>z. f z - f x = ?g z * (z - x)" |
|
1024 |
by simp |
|
1025 |
show "isCont ?g x" |
|
1026 |
using \<open>?lhs\<close> by (simp add: isCont_iff DERIV_def cong: LIM_equal [rule_format]) |
|
1027 |
show "?g x = l" |
|
1028 |
by simp |
|
21164 | 1029 |
qed |
1030 |
next |
|
63558 | 1031 |
assume ?rhs |
1032 |
then obtain g where "(\<forall>z. f z - f x = g z * (z - x))" and "isCont g x" and "g x = l" |
|
1033 |
by blast |
|
1034 |
then show ?lhs |
|
1035 |
by (auto simp add: isCont_iff DERIV_def cong: LIM_cong) |
|
21164 | 1036 |
qed |
1037 |
||
1038 |
||
60758 | 1039 |
subsection \<open>Local extrema\<close> |
29975 | 1040 |
|
63558 | 1041 |
text \<open>If @{term "0 < f' x"} then @{term x} is Locally Strictly Increasing At The Right.\<close> |
21164 | 1042 |
|
63079 | 1043 |
lemma has_real_derivative_pos_inc_right: |
63558 | 1044 |
fixes f :: "real \<Rightarrow> real" |
63079 | 1045 |
assumes der: "(f has_real_derivative l) (at x within S)" |
63558 | 1046 |
and l: "0 < l" |
63079 | 1047 |
shows "\<exists>d > 0. \<forall>h > 0. x + h \<in> S \<longrightarrow> h < d \<longrightarrow> f x < f (x + h)" |
1048 |
using assms |
|
1049 |
proof - |
|
1050 |
from der [THEN has_field_derivativeD, THEN tendstoD, OF l, unfolded eventually_at] |
|
63558 | 1051 |
obtain s where s: "0 < s" |
1052 |
and all: "\<And>xa. xa\<in>S \<Longrightarrow> xa \<noteq> x \<and> dist xa x < s \<longrightarrow> \<bar>(f xa - f x) / (xa - x) - l\<bar> < l" |
|
63079 | 1053 |
by (auto simp: dist_real_def) |
1054 |
then show ?thesis |
|
1055 |
proof (intro exI conjI strip) |
|
63558 | 1056 |
show "0 < s" by (rule s) |
1057 |
next |
|
1058 |
fix h :: real |
|
63079 | 1059 |
assume "0 < h" "h < s" "x + h \<in> S" |
1060 |
with all [of "x + h"] show "f x < f (x+h)" |
|
1061 |
proof (simp add: abs_if dist_real_def pos_less_divide_eq split: if_split_asm) |
|
63558 | 1062 |
assume "\<not> (f (x + h) - f x) / h < l" and h: "0 < h" |
1063 |
with l have "0 < (f (x + h) - f x) / h" |
|
1064 |
by arith |
|
1065 |
then show "f x < f (x + h)" |
|
63079 | 1066 |
by (simp add: pos_less_divide_eq h) |
1067 |
qed |
|
1068 |
qed |
|
1069 |
qed |
|
1070 |
||
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1071 |
lemma DERIV_pos_inc_right: |
63558 | 1072 |
fixes f :: "real \<Rightarrow> real" |
21164 | 1073 |
assumes der: "DERIV f x :> l" |
63558 | 1074 |
and l: "0 < l" |
1075 |
shows "\<exists>d > 0. \<forall>h > 0. h < d \<longrightarrow> f x < f (x + h)" |
|
63079 | 1076 |
using has_real_derivative_pos_inc_right[OF assms] |
1077 |
by auto |
|
1078 |
||
1079 |
lemma has_real_derivative_neg_dec_left: |
|
63558 | 1080 |
fixes f :: "real \<Rightarrow> real" |
63079 | 1081 |
assumes der: "(f has_real_derivative l) (at x within S)" |
63558 | 1082 |
and "l < 0" |
63079 | 1083 |
shows "\<exists>d > 0. \<forall>h > 0. x - h \<in> S \<longrightarrow> h < d \<longrightarrow> f x < f (x - h)" |
21164 | 1084 |
proof - |
63558 | 1085 |
from \<open>l < 0\<close> have l: "- l > 0" |
1086 |
by simp |
|
63079 | 1087 |
from der [THEN has_field_derivativeD, THEN tendstoD, OF l, unfolded eventually_at] |
63558 | 1088 |
obtain s where s: "0 < s" |
1089 |
and all: "\<And>xa. xa\<in>S \<Longrightarrow> xa \<noteq> x \<and> dist xa x < s \<longrightarrow> \<bar>(f xa - f x) / (xa - x) - l\<bar> < - l" |
|
63079 | 1090 |
by (auto simp: dist_real_def) |
63558 | 1091 |
then show ?thesis |
21164 | 1092 |
proof (intro exI conjI strip) |
63558 | 1093 |
show "0 < s" by (rule s) |
1094 |
next |
|
1095 |
fix h :: real |
|
63079 | 1096 |
assume "0 < h" "h < s" "x - h \<in> S" |
1097 |
with all [of "x - h"] show "f x < f (x-h)" |
|
1098 |
proof (simp add: abs_if pos_less_divide_eq dist_real_def split add: if_split_asm) |
|
63558 | 1099 |
assume "- ((f (x-h) - f x) / h) < l" and h: "0 < h" |
1100 |
with l have "0 < (f (x-h) - f x) / h" |
|
1101 |
by arith |
|
1102 |
then show "f x < f (x - h)" |
|
63079 | 1103 |
by (simp add: pos_less_divide_eq h) |
21164 | 1104 |
qed |
1105 |
qed |
|
1106 |
qed |
|
1107 |
||
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1108 |
lemma DERIV_neg_dec_left: |
63558 | 1109 |
fixes f :: "real \<Rightarrow> real" |
21164 | 1110 |
assumes der: "DERIV f x :> l" |
63558 | 1111 |
and l: "l < 0" |
1112 |
shows "\<exists>d > 0. \<forall>h > 0. h < d \<longrightarrow> f x < f (x - h)" |
|
63079 | 1113 |
using has_real_derivative_neg_dec_left[OF assms] |
1114 |
by auto |
|
1115 |
||
1116 |
lemma has_real_derivative_pos_inc_left: |
|
63558 | 1117 |
fixes f :: "real \<Rightarrow> real" |
1118 |
shows "(f has_real_derivative l) (at x within S) \<Longrightarrow> 0 < l \<Longrightarrow> |
|
1119 |
\<exists>d>0. \<forall>h>0. x - h \<in> S \<longrightarrow> h < d \<longrightarrow> f (x - h) < f x" |
|
1120 |
by (rule has_real_derivative_neg_dec_left [of "\<lambda>x. - f x" "-l" x S, simplified]) |
|
63079 | 1121 |
(auto simp add: DERIV_minus) |
21164 | 1122 |
|
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1123 |
lemma DERIV_pos_inc_left: |
63558 | 1124 |
fixes f :: "real \<Rightarrow> real" |
1125 |
shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d \<longrightarrow> f (x - h) < f x" |
|
63079 | 1126 |
using has_real_derivative_pos_inc_left |
1127 |
by blast |
|
1128 |
||
1129 |
lemma has_real_derivative_neg_dec_right: |
|
63558 | 1130 |
fixes f :: "real \<Rightarrow> real" |
1131 |
shows "(f has_real_derivative l) (at x within S) \<Longrightarrow> l < 0 \<Longrightarrow> |
|
1132 |
\<exists>d > 0. \<forall>h > 0. x + h \<in> S \<longrightarrow> h < d \<longrightarrow> f x > f (x + h)" |
|
1133 |
by (rule has_real_derivative_pos_inc_right [of "\<lambda>x. - f x" "-l" x S, simplified]) |
|
63079 | 1134 |
(auto simp add: DERIV_minus) |
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1135 |
|
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1136 |
lemma DERIV_neg_dec_right: |
63558 | 1137 |
fixes f :: "real \<Rightarrow> real" |
1138 |
shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d \<longrightarrow> f x > f (x + h)" |
|
63079 | 1139 |
using has_real_derivative_neg_dec_right by blast |
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1140 |
|
21164 | 1141 |
lemma DERIV_local_max: |
63558 | 1142 |
fixes f :: "real \<Rightarrow> real" |
21164 | 1143 |
assumes der: "DERIV f x :> l" |
63558 | 1144 |
and d: "0 < d" |
1145 |
and le: "\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> f y \<le> f x" |
|
21164 | 1146 |
shows "l = 0" |
1147 |
proof (cases rule: linorder_cases [of l 0]) |
|
63558 | 1148 |
case equal |
1149 |
then show ?thesis . |
|
21164 | 1150 |
next |
1151 |
case less |
|
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1152 |
from DERIV_neg_dec_left [OF der less] |
63558 | 1153 |
obtain d' where d': "0 < d'" and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x - h)" |
1154 |
by blast |
|
1155 |
obtain e where "0 < e \<and> e < d \<and> e < d'" |
|
1156 |
using real_lbound_gt_zero [OF d d'] .. |
|
1157 |
with lt le [THEN spec [where x="x - e"]] show ?thesis |
|
1158 |
by (auto simp add: abs_if) |
|
21164 | 1159 |
next |
1160 |
case greater |
|
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1161 |
from DERIV_pos_inc_right [OF der greater] |
63558 | 1162 |
obtain d' where d': "0 < d'" and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x + h)" |
1163 |
by blast |
|
1164 |
obtain e where "0 < e \<and> e < d \<and> e < d'" |
|
1165 |
using real_lbound_gt_zero [OF d d'] .. |
|
1166 |
with lt le [THEN spec [where x="x + e"]] show ?thesis |
|
1167 |
by (auto simp add: abs_if) |
|
21164 | 1168 |
qed |
1169 |
||
63558 | 1170 |
text \<open>Similar theorem for a local minimum\<close> |
21164 | 1171 |
lemma DERIV_local_min: |
63558 | 1172 |
fixes f :: "real \<Rightarrow> real" |
1173 |
shows "DERIV f x :> l \<Longrightarrow> 0 < d \<Longrightarrow> \<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> f x \<le> f y \<Longrightarrow> l = 0" |
|
1174 |
by (drule DERIV_minus [THEN DERIV_local_max]) auto |
|
21164 | 1175 |
|
1176 |
||
60758 | 1177 |
text\<open>In particular, if a function is locally flat\<close> |
21164 | 1178 |
lemma DERIV_local_const: |
63558 | 1179 |
fixes f :: "real \<Rightarrow> real" |
1180 |
shows "DERIV f x :> l \<Longrightarrow> 0 < d \<Longrightarrow> \<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> f x = f y \<Longrightarrow> l = 0" |
|
1181 |
by (auto dest!: DERIV_local_max) |
|
21164 | 1182 |
|
29975 | 1183 |
|
60758 | 1184 |
subsection \<open>Rolle's Theorem\<close> |
29975 | 1185 |
|
63558 | 1186 |
text \<open>Lemma about introducing open ball in open interval\<close> |
1187 |
lemma lemma_interval_lt: "a < x \<Longrightarrow> x < b \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> a < y \<and> y < b)" |
|
1188 |
for a b x :: real |
|
1189 |
apply (simp add: abs_less_iff) |
|
1190 |
apply (insert linorder_linear [of "x - a" "b - x"]) |
|
1191 |
apply safe |
|
1192 |
apply (rule_tac x = "x - a" in exI) |
|
1193 |
apply (rule_tac [2] x = "b - x" in exI) |
|
1194 |
apply auto |
|
1195 |
done |
|
27668 | 1196 |
|
63558 | 1197 |
lemma lemma_interval: "a < x \<Longrightarrow> x < b \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b)" |
1198 |
for a b x :: real |
|
1199 |
apply (drule lemma_interval_lt) |
|
1200 |
apply auto |
|
1201 |
apply force |
|
1202 |
done |
|
21164 | 1203 |
|
63558 | 1204 |
text \<open>Rolle's Theorem. |
21164 | 1205 |
If @{term f} is defined and continuous on the closed interval |
61799 | 1206 |
\<open>[a,b]\<close> and differentiable on the open interval \<open>(a,b)\<close>, |
63558 | 1207 |
and @{term "f a = f b"}, |
1208 |
then there exists \<open>x0 \<in> (a,b)\<close> such that @{term "f' x0 = 0"}\<close> |
|
21164 | 1209 |
theorem Rolle: |
63558 | 1210 |
fixes a b :: real |
21164 | 1211 |
assumes lt: "a < b" |
63558 | 1212 |
and eq: "f a = f b" |
1213 |
and con: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x" |
|
1214 |
and dif [rule_format]: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable (at x)" |
|
1215 |
shows "\<exists>z. a < z \<and> z < b \<and> DERIV f z :> 0" |
|
21164 | 1216 |
proof - |
63558 | 1217 |
have le: "a \<le> b" |
1218 |
using lt by simp |
|
21164 | 1219 |
from isCont_eq_Ub [OF le con] |
63558 | 1220 |
obtain x where x_max: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f z \<le> f x" and "a \<le> x" "x \<le> b" |
21164 | 1221 |
by blast |
1222 |
from isCont_eq_Lb [OF le con] |
|
63558 | 1223 |
obtain x' where x'_min: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f x' \<le> f z" and "a \<le> x'" "x' \<le> b" |
21164 | 1224 |
by blast |
63558 | 1225 |
consider "a < x" "x < b" | "x = a \<or> x = b" |
1226 |
using \<open>a \<le> x\<close> \<open>x \<le> b\<close> by arith |
|
1227 |
then show ?thesis |
|
21164 | 1228 |
proof cases |
63558 | 1229 |
case 1 |
1230 |
\<comment>\<open>@{term f} attains its maximum within the interval\<close> |
|
1231 |
obtain d where d: "0 < d" and bound: "\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b" |
|
1232 |
using lemma_interval [OF 1] by blast |
|
1233 |
then have bound': "\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> f y \<le> f x" |
|
1234 |
using x_max by blast |
|
1235 |
obtain l where der: "DERIV f x :> l" |
|
1236 |
using differentiableD [OF dif [OF conjI [OF 1]]] .. |
|
1237 |
\<comment>\<open>the derivative at a local maximum is zero\<close> |
|
1238 |
have "l = 0" |
|
1239 |
by (rule DERIV_local_max [OF der d bound']) |
|
1240 |
with 1 der show ?thesis by auto |
|
21164 | 1241 |
next |
63558 | 1242 |
case 2 |
1243 |
then have fx: "f b = f x" by (auto simp add: eq) |
|
1244 |
consider "a < x'" "x' < b" | "x' = a \<or> x' = b" |
|
1245 |
using \<open>a \<le> x'\<close> \<open>x' \<le> b\<close> by arith |
|
1246 |
then show ?thesis |
|
21164 | 1247 |
proof cases |
63558 | 1248 |
case 1 |
1249 |
\<comment> \<open>@{term f} attains its minimum within the interval\<close> |
|
1250 |
from lemma_interval [OF 1] |
|
21164 | 1251 |
obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b" |
63558 | 1252 |
by blast |
1253 |
then have bound': "\<forall>y. \<bar>x' - y\<bar> < d \<longrightarrow> f x' \<le> f y" |
|
1254 |
using x'_min by blast |
|
1255 |
from differentiableD [OF dif [OF conjI [OF 1]]] |
|
21164 | 1256 |
obtain l where der: "DERIV f x' :> l" .. |
63558 | 1257 |
have "l = 0" by (rule DERIV_local_min [OF der d bound']) |
1258 |
\<comment> \<open>the derivative at a local minimum is zero\<close> |
|
1259 |
then show ?thesis using 1 der by auto |
|
21164 | 1260 |
next |
63558 | 1261 |
case 2 |
1262 |
\<comment> \<open>@{term f} is constant throughout the interval\<close> |
|
1263 |
then have fx': "f b = f x'" by (auto simp: eq) |
|
1264 |
from dense [OF lt] obtain r where r: "a < r" "r < b" by blast |
|
1265 |
obtain d where d: "0 < d" and bound: "\<forall>y. \<bar>r - y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b" |
|
1266 |
using lemma_interval [OF r] by blast |
|
1267 |
have eq_fb: "f z = f b" if "a \<le> z" and "z \<le> b" for z |
|
1268 |
proof (rule order_antisym) |
|
1269 |
show "f z \<le> f b" by (simp add: fx x_max that) |
|
1270 |
show "f b \<le> f z" by (simp add: fx' x'_min that) |
|
21164 | 1271 |
qed |
63558 | 1272 |
have bound': "\<forall>y. \<bar>r - y\<bar> < d \<longrightarrow> f r = f y" |
21164 | 1273 |
proof (intro strip) |
63558 | 1274 |
fix y :: real |
1275 |
assume lt: "\<bar>r - y\<bar> < d" |
|
1276 |
then have "f y = f b" by (simp add: eq_fb bound) |
|
1277 |
then show "f r = f y" by (simp add: eq_fb r order_less_imp_le) |
|
21164 | 1278 |
qed |
63558 | 1279 |
obtain l where der: "DERIV f r :> l" |
1280 |
using differentiableD [OF dif [OF conjI [OF r]]] .. |
|
1281 |
have "l = 0" |
|
1282 |
by (rule DERIV_local_const [OF der d bound']) |
|
1283 |
\<comment> \<open>the derivative of a constant function is zero\<close> |
|
1284 |
with r der show ?thesis by auto |
|
21164 | 1285 |
qed |
1286 |
qed |
|
1287 |
qed |
|
1288 |
||
1289 |
||
63558 | 1290 |
subsection \<open>Mean Value Theorem\<close> |
21164 | 1291 |
|
63558 | 1292 |
lemma lemma_MVT: "f a - (f b - f a) / (b - a) * a = f b - (f b - f a) / (b - a) * b" |
1293 |
for a b :: real |
|
51481
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset
|
1294 |
by (cases "a = b") (simp_all add: field_simps) |
21164 | 1295 |
|
1296 |
theorem MVT: |
|
63558 | 1297 |
fixes a b :: real |
1298 |
assumes lt: "a < b" |
|
1299 |
and con: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x" |
|
1300 |
and dif [rule_format]: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable (at x)" |
|
1301 |
shows "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l" |
|
21164 | 1302 |
proof - |
63558 | 1303 |
let ?F = "\<lambda>x. f x - ((f b - f a) / (b - a)) * x" |
1304 |
have cont_f: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x" |
|
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56369
diff
changeset
|
1305 |
using con by (fast intro: continuous_intros) |
63558 | 1306 |
have dif_f: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable (at x)" |
1307 |
proof clarify |
|
1308 |
fix x :: real |
|
1309 |
assume x: "a < x" "x < b" |
|
1310 |
obtain l where der: "DERIV f x :> l" |
|
1311 |
using differentiableD [OF dif [OF conjI [OF x]]] .. |
|
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
1312 |
show "?F differentiable (at x)" |
63558 | 1313 |
by (rule differentiableI [where D = "l - (f b - f a) / (b - a)"], |
21164 | 1314 |
blast intro: DERIV_diff DERIV_cmult_Id der) |
1315 |
qed |
|
63558 | 1316 |
from Rolle [where f = ?F, OF lt lemma_MVT cont_f dif_f] |
1317 |
obtain z where z: "a < z" "z < b" and der: "DERIV ?F z :> 0" |
|
21164 | 1318 |
by blast |
63558 | 1319 |
have "DERIV (\<lambda>x. ((f b - f a) / (b - a)) * x) z :> (f b - f a) / (b - a)" |
21164 | 1320 |
by (rule DERIV_cmult_Id) |
63558 | 1321 |
then have der_f: "DERIV (\<lambda>x. ?F x + (f b - f a) / (b - a) * x) z :> 0 + (f b - f a) / (b - a)" |
21164 | 1322 |
by (rule DERIV_add [OF der]) |
1323 |
show ?thesis |
|
1324 |
proof (intro exI conjI) |
|
63558 | 1325 |
show "a < z" and "z < b" using z . |
1326 |
show "f b - f a = (b - a) * ((f b - f a) / (b - a))" by simp |
|
1327 |
show "DERIV f z :> ((f b - f a) / (b - a))" using der_f by simp |
|
21164 | 1328 |
qed |
1329 |
qed |
|
1330 |
||
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1331 |
lemma MVT2: |
63558 | 1332 |
"a < b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> DERIV f x :> f' x \<Longrightarrow> |
1333 |
\<exists>z::real. a < z \<and> z < b \<and> (f b - f a = (b - a) * f' z)" |
|
1334 |
apply (drule MVT) |
|
1335 |
apply (blast intro: DERIV_isCont) |
|
1336 |
apply (force dest: order_less_imp_le simp add: real_differentiable_def) |
|
1337 |
apply (blast dest: DERIV_unique order_less_imp_le) |
|
1338 |
done |
|
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1339 |
|
21164 | 1340 |
|
63558 | 1341 |
text \<open>A function is constant if its derivative is 0 over an interval.\<close> |
21164 | 1342 |
|
1343 |
lemma DERIV_isconst_end: |
|
63558 | 1344 |
fixes f :: "real \<Rightarrow> real" |
1345 |
shows "a < b \<Longrightarrow> |
|
1346 |
\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow> |
|
1347 |
\<forall>x. a < x \<and> x < b \<longrightarrow> DERIV f x :> 0 \<Longrightarrow> f b = f a" |
|
1348 |
apply (drule (1) MVT) |
|
1349 |
apply (blast intro: differentiableI) |
|
1350 |
apply (auto dest!: DERIV_unique simp add: diff_eq_eq) |
|
1351 |
done |
|
21164 | 1352 |
|
1353 |
lemma DERIV_isconst1: |
|
63558 | 1354 |
fixes f :: "real \<Rightarrow> real" |
1355 |
shows "a < b \<Longrightarrow> |
|
1356 |
\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow> |
|
1357 |
\<forall>x. a < x \<and> x < b \<longrightarrow> DERIV f x :> 0 \<Longrightarrow> |
|
1358 |
\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x = f a" |
|
1359 |
apply safe |
|
1360 |
apply (drule_tac x = a in order_le_imp_less_or_eq) |
|
1361 |
apply safe |
|
1362 |
apply (drule_tac b = x in DERIV_isconst_end) |
|
1363 |
apply auto |
|
1364 |
done |
|
21164 | 1365 |
|
1366 |
lemma DERIV_isconst2: |
|
63558 | 1367 |
fixes f :: "real \<Rightarrow> real" |
1368 |
shows "a < b \<Longrightarrow> |
|
1369 |
\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow> |
|
1370 |
\<forall>x. a < x \<and> x < b \<longrightarrow> DERIV f x :> 0 \<Longrightarrow> |
|
1371 |
a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> f x = f a" |
|
1372 |
by (blast dest: DERIV_isconst1) |
|
21164 | 1373 |
|
63558 | 1374 |
lemma DERIV_isconst3: |
1375 |
fixes a b x y :: real |
|
1376 |
assumes "a < b" |
|
1377 |
and "x \<in> {a <..< b}" |
|
1378 |
and "y \<in> {a <..< b}" |
|
1379 |
and derivable: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> DERIV f x :> 0" |
|
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1380 |
shows "f x = f y" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1381 |
proof (cases "x = y") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1382 |
case False |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1383 |
let ?a = "min x y" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1384 |
let ?b = "max x y" |
63558 | 1385 |
|
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1386 |
have "\<forall>z. ?a \<le> z \<and> z \<le> ?b \<longrightarrow> DERIV f z :> 0" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1387 |
proof (rule allI, rule impI) |
63558 | 1388 |
fix z :: real |
1389 |
assume "?a \<le> z \<and> z \<le> ?b" |
|
1390 |
then have "a < z" and "z < b" |
|
1391 |
using \<open>x \<in> {a <..< b}\<close> and \<open>y \<in> {a <..< b}\<close> by auto |
|
1392 |
then have "z \<in> {a<..<b}" by auto |
|
1393 |
then show "DERIV f z :> 0" by (rule derivable) |
|
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1394 |
qed |
63558 | 1395 |
then have isCont: "\<forall>z. ?a \<le> z \<and> z \<le> ?b \<longrightarrow> isCont f z" |
1396 |
and DERIV: "\<forall>z. ?a < z \<and> z < ?b \<longrightarrow> DERIV f z :> 0" |
|
1397 |
using DERIV_isCont by auto |
|
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1398 |
|
60758 | 1399 |
have "?a < ?b" using \<open>x \<noteq> y\<close> by auto |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1400 |
from DERIV_isconst2[OF this isCont DERIV, of x] and DERIV_isconst2[OF this isCont DERIV, of y] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1401 |
show ?thesis by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1402 |
qed auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
1403 |
|
21164 | 1404 |
lemma DERIV_isconst_all: |
63558 | 1405 |
fixes f :: "real \<Rightarrow> real" |
1406 |
shows "\<forall>x. DERIV f x :> 0 \<Longrightarrow> f x = f y" |
|
1407 |
apply (rule linorder_cases [of x y]) |
|
1408 |
apply (blast intro: sym DERIV_isCont DERIV_isconst_end)+ |
|
1409 |
done |
|
21164 | 1410 |
|
1411 |
lemma DERIV_const_ratio_const: |
|
63558 | 1412 |
fixes f :: "real \<Rightarrow> real" |
1413 |
shows "a \<noteq> b \<Longrightarrow> \<forall>x. DERIV f x :> k \<Longrightarrow> f b - f a = (b - a) * k" |
|
1414 |
apply (rule linorder_cases [of a b]) |
|
1415 |
apply auto |
|
1416 |
apply (drule_tac [!] f = f in MVT) |
|
1417 |
apply (auto dest: DERIV_isCont DERIV_unique simp: real_differentiable_def) |
|
1418 |
apply (auto dest: DERIV_unique simp: ring_distribs) |
|
1419 |
done |
|
21164 | 1420 |
|
1421 |
lemma DERIV_const_ratio_const2: |
|
63558 | 1422 |
fixes f :: "real \<Rightarrow> real" |
1423 |
shows "a \<noteq> b \<Longrightarrow> \<forall>x. DERIV f x :> k \<Longrightarrow> (f b - f a) / (b - a) = k" |
|
1424 |
apply (rule_tac c1 = "b-a" in mult_right_cancel [THEN iffD1]) |
|
1425 |
apply (auto dest!: DERIV_const_ratio_const simp add: mult.assoc) |
|
1426 |
done |
|
21164 | 1427 |
|
63558 | 1428 |
lemma real_average_minus_first [simp]: "(a + b) / 2 - a = (b - a) / 2" |
1429 |
for a b :: real |
|
1430 |
by simp |
|
21164 | 1431 |
|
63558 | 1432 |
lemma real_average_minus_second [simp]: "(b + a) / 2 - a = (b - a) / 2" |
1433 |
for a b :: real |
|
1434 |
by simp |
|
21164 | 1435 |
|
63558 | 1436 |
text \<open>Gallileo's "trick": average velocity = av. of end velocities.\<close> |
21164 | 1437 |
|
1438 |
lemma DERIV_const_average: |
|
63558 | 1439 |
fixes v :: "real \<Rightarrow> real" |
1440 |
and a b :: real |
|
1441 |
assumes neq: "a \<noteq> b" |
|
1442 |
and der: "\<forall>x. DERIV v x :> k" |
|
1443 |
shows "v ((a + b) / 2) = (v a + v b) / 2" |
|
21164 | 1444 |
proof (cases rule: linorder_cases [of a b]) |
63558 | 1445 |
case equal |
1446 |
with neq show ?thesis by simp |
|
21164 | 1447 |
next |
1448 |
case less |
|
1449 |
have "(v b - v a) / (b - a) = k" |
|
1450 |
by (rule DERIV_const_ratio_const2 [OF neq der]) |
|
63558 | 1451 |
then have "(b - a) * ((v b - v a) / (b - a)) = (b - a) * k" |
1452 |
by simp |
|
21164 | 1453 |
moreover have "(v ((a + b) / 2) - v a) / ((a + b) / 2 - a) = k" |
63558 | 1454 |
by (rule DERIV_const_ratio_const2 [OF _ der]) (simp add: neq) |
1455 |
ultimately show ?thesis |
|
1456 |
using neq by force |
|
21164 | 1457 |
next |
1458 |
case greater |
|
1459 |
have "(v b - v a) / (b - a) = k" |
|
1460 |
by (rule DERIV_const_ratio_const2 [OF neq der]) |
|
63558 | 1461 |
then have "(b - a) * ((v b - v a) / (b - a)) = (b - a) * k" |
1462 |
by simp |
|
21164 | 1463 |
moreover have " (v ((b + a) / 2) - v a) / ((b + a) / 2 - a) = k" |
63558 | 1464 |
by (rule DERIV_const_ratio_const2 [OF _ der]) (simp add: neq) |
1465 |
ultimately show ?thesis |
|
1466 |
using neq by (force simp add: add.commute) |
|
21164 | 1467 |
qed |
1468 |
||
63558 | 1469 |
text \<open> |
1470 |
A function with positive derivative is increasing. |
|
1471 |
A simple proof using the MVT, by Jeremy Avigad. And variants. |
|
1472 |
\<close> |
|
56261 | 1473 |
lemma DERIV_pos_imp_increasing_open: |
63558 | 1474 |
fixes a b :: real |
1475 |
and f :: "real \<Rightarrow> real" |
|
1476 |
assumes "a < b" |
|
1477 |
and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<exists>y. DERIV f x :> y \<and> y > 0)" |
|
1478 |
and con: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x" |
|
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1479 |
shows "f a < f b" |
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1480 |
proof (rule ccontr) |
63558 | 1481 |
assume f: "\<not> ?thesis" |
1482 |
have "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l" |
|
1483 |
by (rule MVT) (use assms Deriv.differentiableI in \<open>force+\<close>) |
|
1484 |
then obtain l z where z: "a < z" "z < b" "DERIV f z :> l" and "f b - f a = (b - a) * l" |
|
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1485 |
by auto |
63558 | 1486 |
with assms f have "\<not> l > 0" |
36777
be5461582d0f
avoid using real-specific versions of generic lemmas
huffman
parents:
35216
diff
changeset
|
1487 |
by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le) |
41550 | 1488 |
with assms z show False |
56261 | 1489 |
by (metis DERIV_unique) |
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1490 |
qed |
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1491 |
|
56261 | 1492 |
lemma DERIV_pos_imp_increasing: |
63558 | 1493 |
fixes a b :: real |
1494 |
and f :: "real \<Rightarrow> real" |
|
1495 |
assumes "a < b" |
|
1496 |
and "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> (\<exists>y. DERIV f x :> y \<and> y > 0)" |
|
56261 | 1497 |
shows "f a < f b" |
63558 | 1498 |
by (metis DERIV_pos_imp_increasing_open [of a b f] assms DERIV_continuous less_imp_le) |
56261 | 1499 |
|
45791 | 1500 |
lemma DERIV_nonneg_imp_nondecreasing: |
63558 | 1501 |
fixes a b :: real |
1502 |
and f :: "real \<Rightarrow> real" |
|
1503 |
assumes "a \<le> b" |
|
1504 |
and "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> (\<exists>y. DERIV f x :> y \<and> y \<ge> 0)" |
|
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1505 |
shows "f a \<le> f b" |
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1506 |
proof (rule ccontr, cases "a = b") |
63558 | 1507 |
assume "\<not> ?thesis" and "a = b" |
41550 | 1508 |
then show False by auto |
37891 | 1509 |
next |
63558 | 1510 |
assume *: "\<not> ?thesis" |
1511 |
assume "a \<noteq> b" |
|
1512 |
with assms have "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l" |
|
33690 | 1513 |
apply - |
1514 |
apply (rule MVT) |
|
1515 |
apply auto |
|
63558 | 1516 |
apply (metis DERIV_isCont) |
1517 |
apply (metis differentiableI less_le) |
|
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1518 |
done |
63558 | 1519 |
then obtain l z where lz: "a < z" "z < b" "DERIV f z :> l" and **: "f b - f a = (b - a) * l" |
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1520 |
by auto |
63558 | 1521 |
with * have "a < b" "f b < f a" by auto |
1522 |
with ** have "\<not> l \<ge> 0" by (auto simp add: not_le algebra_simps) |
|
1523 |
(metis * add_le_cancel_right assms(1) less_eq_real_def mult_right_mono add_left_mono linear order_refl) |
|
1524 |
with assms lz show False |
|
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1525 |
by (metis DERIV_unique order_less_imp_le) |
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1526 |
qed |
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1527 |
|
56261 | 1528 |
lemma DERIV_neg_imp_decreasing_open: |
63558 | 1529 |
fixes a b :: real |
1530 |
and f :: "real \<Rightarrow> real" |
|
1531 |
assumes "a < b" |
|
1532 |
and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<exists>y. DERIV f x :> y \<and> y < 0)" |
|
1533 |
and con: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x" |
|
56261 | 1534 |
shows "f a > f b" |
1535 |
proof - |
|
63558 | 1536 |
have "(\<lambda>x. -f x) a < (\<lambda>x. -f x) b" |
1537 |
apply (rule DERIV_pos_imp_increasing_open [of a b "\<lambda>x. -f x"]) |
|
56261 | 1538 |
using assms |
63558 | 1539 |
apply auto |
56261 | 1540 |
apply (metis field_differentiable_minus neg_0_less_iff_less) |
1541 |
done |
|
63558 | 1542 |
then show ?thesis |
56261 | 1543 |
by simp |
1544 |
qed |
|
1545 |
||
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1546 |
lemma DERIV_neg_imp_decreasing: |
63558 | 1547 |
fixes a b :: real |
1548 |
and f :: "real \<Rightarrow> real" |
|
1549 |
assumes "a < b" |
|
1550 |
and "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> (\<exists>y. DERIV f x :> y \<and> y < 0)" |
|
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1551 |
shows "f a > f b" |
63558 | 1552 |
by (metis DERIV_neg_imp_decreasing_open [of a b f] assms DERIV_continuous less_imp_le) |
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1553 |
|
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1554 |
lemma DERIV_nonpos_imp_nonincreasing: |
63558 | 1555 |
fixes a b :: real |
1556 |
and f :: "real \<Rightarrow> real" |
|
1557 |
assumes "a \<le> b" |
|
1558 |
and "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> (\<exists>y. DERIV f x :> y \<and> y \<le> 0)" |
|
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1559 |
shows "f a \<ge> f b" |
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1560 |
proof - |
63558 | 1561 |
have "(\<lambda>x. -f x) a \<le> (\<lambda>x. -f x) b" |
1562 |
apply (rule DERIV_nonneg_imp_nondecreasing [of a b "\<lambda>x. -f x"]) |
|
33690 | 1563 |
using assms |
63558 | 1564 |
apply auto |
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1565 |
apply (metis DERIV_minus neg_0_le_iff_le) |
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1566 |
done |
63558 | 1567 |
then show ?thesis |
33654
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1568 |
by simp |
abf780db30ea
A number of theorems contributed by Jeremy Avigad
paulson
parents:
31902
diff
changeset
|
1569 |
qed |
21164 | 1570 |
|
56289 | 1571 |
lemma DERIV_pos_imp_increasing_at_bot: |
63558 | 1572 |
fixes f :: "real \<Rightarrow> real" |
1573 |
assumes "\<And>x. x \<le> b \<Longrightarrow> (\<exists>y. DERIV f x :> y \<and> y > 0)" |
|
1574 |
and lim: "(f \<longlongrightarrow> flim) at_bot" |
|
56289 | 1575 |
shows "flim < f b" |
1576 |
proof - |
|
1577 |
have "flim \<le> f (b - 1)" |
|
1578 |
apply (rule tendsto_ge_const [OF _ lim]) |
|
63558 | 1579 |
apply (auto simp: trivial_limit_at_bot_linorder eventually_at_bot_linorder) |
56289 | 1580 |
apply (rule_tac x="b - 2" in exI) |
1581 |
apply (force intro: order.strict_implies_order DERIV_pos_imp_increasing [where f=f] assms) |
|
1582 |
done |
|
63558 | 1583 |
also have "\<dots> < f b" |
56289 | 1584 |
by (force intro: DERIV_pos_imp_increasing [where f=f] assms) |
1585 |
finally show ?thesis . |
|
1586 |
qed |
|
1587 |
||
1588 |
lemma DERIV_neg_imp_decreasing_at_top: |
|
63558 | 1589 |
fixes f :: "real \<Rightarrow> real" |
1590 |
assumes der: "\<And>x. x \<ge> b \<Longrightarrow> (\<exists>y. DERIV f x :> y \<and> y < 0)" |
|
1591 |
and lim: "(f \<longlongrightarrow> flim) at_top" |
|
56289 | 1592 |
shows "flim < f b" |
1593 |
apply (rule DERIV_pos_imp_increasing_at_bot [where f = "\<lambda>i. f (-i)" and b = "-b", simplified]) |
|
63558 | 1594 |
apply (metis DERIV_mirror der le_minus_iff neg_0_less_iff_less) |
56289 | 1595 |
apply (metis filterlim_at_top_mirror lim) |
1596 |
done |
|
1597 |
||
60758 | 1598 |
text \<open>Derivative of inverse function\<close> |
23041 | 1599 |
|
1600 |
lemma DERIV_inverse_function: |
|
1601 |
fixes f g :: "real \<Rightarrow> real" |
|
1602 |
assumes der: "DERIV f (g x) :> D" |
|
63558 | 1603 |
and neq: "D \<noteq> 0" |
1604 |
and x: "a < x" "x < b" |
|
1605 |
and inj: "\<forall>y. a < y \<and> y < b \<longrightarrow> f (g y) = y" |
|
1606 |
and cont: "isCont g x" |
|
23041 | 1607 |
shows "DERIV g x :> inverse D" |
1608 |
unfolding DERIV_iff2 |
|
23044 | 1609 |
proof (rule LIM_equal2) |
1610 |
show "0 < min (x - a) (b - x)" |
|
63558 | 1611 |
using x by arith |
23044 | 1612 |
next |
23041 | 1613 |
fix y |
23044 | 1614 |
assume "norm (y - x) < min (x - a) (b - x)" |
63558 | 1615 |
then have "a < y" and "y < b" |
23044 | 1616 |
by (simp_all add: abs_less_iff) |
63558 | 1617 |
then show "(g y - g x) / (y - x) = inverse ((f (g y) - x) / (g y - g x))" |
23041 | 1618 |
by (simp add: inj) |
1619 |
next |
|
61976 | 1620 |
have "(\<lambda>z. (f z - f (g x)) / (z - g x)) \<midarrow>g x\<rightarrow> D" |
23041 | 1621 |
by (rule der [unfolded DERIV_iff2]) |
63558 | 1622 |
then have 1: "(\<lambda>z. (f z - x) / (z - g x)) \<midarrow>g x\<rightarrow> D" |
1623 |
using inj x by simp |
|
23041 | 1624 |
have 2: "\<exists>d>0. \<forall>y. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow> g y \<noteq> g x" |
56219 | 1625 |
proof (rule exI, safe) |
23044 | 1626 |
show "0 < min (x - a) (b - x)" |
63558 | 1627 |
using x by simp |
23041 | 1628 |
next |
1629 |
fix y |
|
23044 | 1630 |
assume "norm (y - x) < min (x - a) (b - x)" |
63558 | 1631 |
then have y: "a < y" "y < b" |
23044 | 1632 |
by (simp_all add: abs_less_iff) |
23041 | 1633 |
assume "g y = g x" |
63558 | 1634 |
then have "f (g y) = f (g x)" by simp |
1635 |
then have "y = x" using inj y x by simp |
|
23041 | 1636 |
also assume "y \<noteq> x" |
1637 |
finally show False by simp |
|
1638 |
qed |
|
61976 | 1639 |
have "(\<lambda>y. (f (g y) - x) / (g y - g x)) \<midarrow>x\<rightarrow> D" |
23041 | 1640 |
using cont 1 2 by (rule isCont_LIM_compose2) |
63558 | 1641 |
then show "(\<lambda>y. inverse ((f (g y) - x) / (g y - g x))) \<midarrow>x\<rightarrow> inverse D" |
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44317
diff
changeset
|
1642 |
using neq by (rule tendsto_inverse) |
23041 | 1643 |
qed |
1644 |
||
60758 | 1645 |
subsection \<open>Generalized Mean Value Theorem\<close> |
29975 | 1646 |
|
21164 | 1647 |
theorem GMVT: |
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset
|
1648 |
fixes a b :: real |
21164 | 1649 |
assumes alb: "a < b" |
41550 | 1650 |
and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
1651 |
and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable (at x)" |
41550 | 1652 |
and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
1653 |
and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable (at x)" |
53381 | 1654 |
shows "\<exists>g'c f'c c. |
63558 | 1655 |
DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> (f b - f a) * g'c = (g b - g a) * f'c" |
21164 | 1656 |
proof - |
63558 | 1657 |
let ?h = "\<lambda>x. (f b - f a) * g x - (g b - g a) * f x" |
1658 |
have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" |
|
1659 |
proof (rule MVT) |
|
1660 |
from assms show "a < b" by simp |
|
1661 |
show "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x" |
|
1662 |
using fc gc by simp |
|
1663 |
show "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable (at x)" |
|
1664 |
using fd gd by simp |
|
1665 |
qed |
|
1666 |
then obtain l where l: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" .. |
|
1667 |
then obtain c where c: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" .. |
|
21164 | 1668 |
|
63558 | 1669 |
from c have cint: "a < c \<and> c < b" by auto |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
1670 |
with gd have "g differentiable (at c)" by simp |
63558 | 1671 |
then have "\<exists>D. DERIV g c :> D" by (rule differentiableD) |
1672 |
then obtain g'c where g'c: "DERIV g c :> g'c" .. |
|
21164 | 1673 |
|
63558 | 1674 |
from c have "a < c \<and> c < b" by auto |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
1675 |
with fd have "f differentiable (at c)" by simp |
63558 | 1676 |
then have "\<exists>D. DERIV f c :> D" by (rule differentiableD) |
1677 |
then obtain f'c where f'c: "DERIV f c :> f'c" .. |
|
21164 | 1678 |
|
63558 | 1679 |
from c have "DERIV ?h c :> l" by auto |
41368 | 1680 |
moreover have "DERIV ?h c :> g'c * (f b - f a) - f'c * (g b - g a)" |
63558 | 1681 |
using g'c f'c by (auto intro!: derivative_eq_intros) |
21164 | 1682 |
ultimately have leq: "l = g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique) |
1683 |
||
63558 | 1684 |
have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" |
1685 |
proof - |
|
1686 |
from c have "?h b - ?h a = (b - a) * l" by auto |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51642
diff
changeset
|
1687 |
also from leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp |
63558 | 1688 |
finally show ?thesis by simp |
1689 |
qed |
|
1690 |
moreover have "?h b - ?h a = 0" |
|
1691 |
proof - |
|
21164 | 1692 |
have "?h b - ?h a = |
63558 | 1693 |
((f b)*(g b) - (f a)*(g b) - (g b)*(f b) + (g a)*(f b)) - |
1694 |
((f b)*(g a) - (f a)*(g a) - (g b)*(f a) + (g a)*(f a))" |
|
29667 | 1695 |
by (simp add: algebra_simps) |
63558 | 1696 |
then show ?thesis by auto |
1697 |
qed |
|
21164 | 1698 |
ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto |
1699 |
with alb have "g'c * (f b - f a) - f'c * (g b - g a) = 0" by simp |
|
63558 | 1700 |
then have "g'c * (f b - f a) = f'c * (g b - g a)" by simp |
1701 |
then have "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: ac_simps) |
|
1702 |
with g'c f'c cint show ?thesis by auto |
|
21164 | 1703 |
qed |
1704 |
||
50327 | 1705 |
lemma GMVT': |
1706 |
fixes f g :: "real \<Rightarrow> real" |
|
1707 |
assumes "a < b" |
|
63558 | 1708 |
and isCont_f: "\<And>z. a \<le> z \<Longrightarrow> z \<le> b \<Longrightarrow> isCont f z" |
1709 |
and isCont_g: "\<And>z. a \<le> z \<Longrightarrow> z \<le> b \<Longrightarrow> isCont g z" |
|
1710 |
and DERIV_g: "\<And>z. a < z \<Longrightarrow> z < b \<Longrightarrow> DERIV g z :> (g' z)" |
|
1711 |
and DERIV_f: "\<And>z. a < z \<Longrightarrow> z < b \<Longrightarrow> DERIV f z :> (f' z)" |
|
50327 | 1712 |
shows "\<exists>c. a < c \<and> c < b \<and> (f b - f a) * g' c = (g b - g a) * f' c" |
1713 |
proof - |
|
1714 |
have "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> |
|
63558 | 1715 |
a < c \<and> c < b \<and> (f b - f a) * g'c = (g b - g a) * f'c" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
55970
diff
changeset
|
1716 |
using assms by (intro GMVT) (force simp: real_differentiable_def)+ |
50327 | 1717 |
then obtain c where "a < c" "c < b" "(f b - f a) * g' c = (g b - g a) * f' c" |
1718 |
using DERIV_f DERIV_g by (force dest: DERIV_unique) |
|
1719 |
then show ?thesis |
|
1720 |
by auto |
|
1721 |
qed |
|
1722 |
||
51529
2d2f59e6055a
move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
hoelzl
parents:
51526
diff
changeset
|
1723 |
|
60758 | 1724 |
subsection \<open>L'Hopitals rule\<close> |
51529
2d2f59e6055a
move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
hoelzl
parents:
51526
diff
changeset
|
1725 |
|
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1726 |
lemma isCont_If_ge: |
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1727 |
fixes a :: "'a :: linorder_topology" |
63558 | 1728 |
shows "continuous (at_left a) g \<Longrightarrow> (f \<longlongrightarrow> g a) (at_right a) \<Longrightarrow> |
1729 |
isCont (\<lambda>x. if x \<le> a then g x else f x) a" |
|
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1730 |
unfolding isCont_def continuous_within |
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1731 |
apply (intro filterlim_split_at) |
63558 | 1732 |
apply (subst filterlim_cong[OF refl refl, where g=g]) |
1733 |
apply (simp_all add: eventually_at_filter less_le) |
|
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1734 |
apply (subst filterlim_cong[OF refl refl, where g=f]) |
63558 | 1735 |
apply (simp_all add: eventually_at_filter less_le) |
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1736 |
done |
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1737 |
|
50327 | 1738 |
lemma lhopital_right_0: |
50329 | 1739 |
fixes f0 g0 :: "real \<Rightarrow> real" |
61973 | 1740 |
assumes f_0: "(f0 \<longlongrightarrow> 0) (at_right 0)" |
63558 | 1741 |
and g_0: "(g0 \<longlongrightarrow> 0) (at_right 0)" |
1742 |
and ev: |
|
1743 |
"eventually (\<lambda>x. g0 x \<noteq> 0) (at_right 0)" |
|
1744 |
"eventually (\<lambda>x. g' x \<noteq> 0) (at_right 0)" |
|
1745 |
"eventually (\<lambda>x. DERIV f0 x :> f' x) (at_right 0)" |
|
1746 |
"eventually (\<lambda>x. DERIV g0 x :> g' x) (at_right 0)" |
|
1747 |
and lim: "((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> x) (at_right 0)" |
|
61973 | 1748 |
shows "((\<lambda> x. f0 x / g0 x) \<longlongrightarrow> x) (at_right 0)" |
50327 | 1749 |
proof - |
63040 | 1750 |
define f where [abs_def]: "f x = (if x \<le> 0 then 0 else f0 x)" for x |
50329 | 1751 |
then have "f 0 = 0" by simp |
1752 |
||
63040 | 1753 |
define g where [abs_def]: "g x = (if x \<le> 0 then 0 else g0 x)" for x |
50329 | 1754 |
then have "g 0 = 0" by simp |
1755 |
||
1756 |
have "eventually (\<lambda>x. g0 x \<noteq> 0 \<and> g' x \<noteq> 0 \<and> |
|
1757 |
DERIV f0 x :> (f' x) \<and> DERIV g0 x :> (g' x)) (at_right 0)" |
|
1758 |
using ev by eventually_elim auto |
|
1759 |
then obtain a where [arith]: "0 < a" |
|
1760 |
and g0_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g0 x \<noteq> 0" |
|
50327 | 1761 |
and g'_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g' x \<noteq> 0" |
50329 | 1762 |
and f0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV f0 x :> (f' x)" |
1763 |
and g0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV g0 x :> (g' x)" |
|
56219 | 1764 |
unfolding eventually_at by (auto simp: dist_real_def) |
50327 | 1765 |
|
50329 | 1766 |
have g_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g x \<noteq> 0" |
1767 |
using g0_neq_0 by (simp add: g_def) |
|
1768 |
||
63558 | 1769 |
have f: "DERIV f x :> (f' x)" if x: "0 < x" "x < a" for x |
1770 |
using that |
|
1771 |
by (intro DERIV_cong_ev[THEN iffD1, OF _ _ _ f0[OF x]]) |
|
1772 |
(auto simp: f_def eventually_nhds_metric dist_real_def intro!: exI[of _ x]) |
|
50329 | 1773 |
|
63558 | 1774 |
have g: "DERIV g x :> (g' x)" if x: "0 < x" "x < a" for x |
1775 |
using that |
|
1776 |
by (intro DERIV_cong_ev[THEN iffD1, OF _ _ _ g0[OF x]]) |
|
1777 |
(auto simp: g_def eventually_nhds_metric dist_real_def intro!: exI[of _ x]) |
|
50329 | 1778 |
|
1779 |
have "isCont f 0" |
|
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1780 |
unfolding f_def by (intro isCont_If_ge f_0 continuous_const) |
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1781 |
|
50329 | 1782 |
have "isCont g 0" |
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1783 |
unfolding g_def by (intro isCont_If_ge g_0 continuous_const) |
50329 | 1784 |
|
50327 | 1785 |
have "\<exists>\<zeta>. \<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)" |
63558 | 1786 |
proof (rule bchoice, rule ballI) |
1787 |
fix x |
|
1788 |
assume "x \<in> {0 <..< a}" |
|
50327 | 1789 |
then have x[arith]: "0 < x" "x < a" by auto |
60758 | 1790 |
with g'_neq_0 g_neq_0 \<open>g 0 = 0\<close> have g': "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> 0 \<noteq> g' x" "g 0 \<noteq> g x" |
50327 | 1791 |
by auto |
50328 | 1792 |
have "\<And>x. 0 \<le> x \<Longrightarrow> x < a \<Longrightarrow> isCont f x" |
60758 | 1793 |
using \<open>isCont f 0\<close> f by (auto intro: DERIV_isCont simp: le_less) |
50328 | 1794 |
moreover have "\<And>x. 0 \<le> x \<Longrightarrow> x < a \<Longrightarrow> isCont g x" |
60758 | 1795 |
using \<open>isCont g 0\<close> g by (auto intro: DERIV_isCont simp: le_less) |
50328 | 1796 |
ultimately have "\<exists>c. 0 < c \<and> c < x \<and> (f x - f 0) * g' c = (g x - g 0) * f' c" |
60758 | 1797 |
using f g \<open>x < a\<close> by (intro GMVT') auto |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51642
diff
changeset
|
1798 |
then obtain c where *: "0 < c" "c < x" "(f x - f 0) * g' c = (g x - g 0) * f' c" |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51642
diff
changeset
|
1799 |
by blast |
50327 | 1800 |
moreover |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51642
diff
changeset
|
1801 |
from * g'(1)[of c] g'(2) have "(f x - f 0) / (g x - g 0) = f' c / g' c" |
50327 | 1802 |
by (simp add: field_simps) |
1803 |
ultimately show "\<exists>y. 0 < y \<and> y < x \<and> f x / g x = f' y / g' y" |
|
60758 | 1804 |
using \<open>f 0 = 0\<close> \<open>g 0 = 0\<close> by (auto intro!: exI[of _ c]) |
50327 | 1805 |
qed |
53381 | 1806 |
then obtain \<zeta> where "\<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)" .. |
50327 | 1807 |
then have \<zeta>: "eventually (\<lambda>x. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)) (at_right 0)" |
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1808 |
unfolding eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def) |
50327 | 1809 |
moreover |
1810 |
from \<zeta> have "eventually (\<lambda>x. norm (\<zeta> x) \<le> x) (at_right 0)" |
|
1811 |
by eventually_elim auto |
|
61973 | 1812 |
then have "((\<lambda>x. norm (\<zeta> x)) \<longlongrightarrow> 0) (at_right 0)" |
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57953
diff
changeset
|
1813 |
by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"]) auto |
61973 | 1814 |
then have "(\<zeta> \<longlongrightarrow> 0) (at_right 0)" |
50327 | 1815 |
by (rule tendsto_norm_zero_cancel) |
1816 |
with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)" |
|
61810 | 1817 |
by (auto elim!: eventually_mono simp: filterlim_at) |
61973 | 1818 |
from this lim have "((\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) \<longlongrightarrow> x) (at_right 0)" |
50327 | 1819 |
by (rule_tac filterlim_compose[of _ _ _ \<zeta>]) |
61973 | 1820 |
ultimately have "((\<lambda>t. f t / g t) \<longlongrightarrow> x) (at_right 0)" (is ?P) |
50328 | 1821 |
by (rule_tac filterlim_cong[THEN iffD1, OF refl refl]) |
61810 | 1822 |
(auto elim: eventually_mono) |
50329 | 1823 |
also have "?P \<longleftrightarrow> ?thesis" |
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1824 |
by (rule filterlim_cong) (auto simp: f_def g_def eventually_at_filter) |
50329 | 1825 |
finally show ?thesis . |
50327 | 1826 |
qed |
1827 |
||
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1828 |
lemma lhopital_right: |
63558 | 1829 |
"(f \<longlongrightarrow> 0) (at_right x) \<Longrightarrow> (g \<longlongrightarrow> 0) (at_right x) \<Longrightarrow> |
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1830 |
eventually (\<lambda>x. g x \<noteq> 0) (at_right x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1831 |
eventually (\<lambda>x. g' x \<noteq> 0) (at_right x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1832 |
eventually (\<lambda>x. DERIV f x :> f' x) (at_right x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1833 |
eventually (\<lambda>x. DERIV g x :> g' x) (at_right x) \<Longrightarrow> |
61973 | 1834 |
((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at_right x) \<Longrightarrow> |
1835 |
((\<lambda> x. f x / g x) \<longlongrightarrow> y) (at_right x)" |
|
63558 | 1836 |
for x :: real |
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1837 |
unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1838 |
by (rule lhopital_right_0) |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1839 |
|
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1840 |
lemma lhopital_left: |
63558 | 1841 |
"(f \<longlongrightarrow> 0) (at_left x) \<Longrightarrow> (g \<longlongrightarrow> 0) (at_left x) \<Longrightarrow> |
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1842 |
eventually (\<lambda>x. g x \<noteq> 0) (at_left x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1843 |
eventually (\<lambda>x. g' x \<noteq> 0) (at_left x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1844 |
eventually (\<lambda>x. DERIV f x :> f' x) (at_left x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1845 |
eventually (\<lambda>x. DERIV g x :> g' x) (at_left x) \<Longrightarrow> |
61973 | 1846 |
((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at_left x) \<Longrightarrow> |
1847 |
((\<lambda> x. f x / g x) \<longlongrightarrow> y) (at_left x)" |
|
63558 | 1848 |
for x :: real |
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1849 |
unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror |
56479
91958d4b30f7
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents:
56409
diff
changeset
|
1850 |
by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror) |
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1851 |
|
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1852 |
lemma lhopital: |
63558 | 1853 |
"(f \<longlongrightarrow> 0) (at x) \<Longrightarrow> (g \<longlongrightarrow> 0) (at x) \<Longrightarrow> |
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1854 |
eventually (\<lambda>x. g x \<noteq> 0) (at x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1855 |
eventually (\<lambda>x. g' x \<noteq> 0) (at x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1856 |
eventually (\<lambda>x. DERIV f x :> f' x) (at x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1857 |
eventually (\<lambda>x. DERIV g x :> g' x) (at x) \<Longrightarrow> |
61973 | 1858 |
((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at x) \<Longrightarrow> |
1859 |
((\<lambda> x. f x / g x) \<longlongrightarrow> y) (at x)" |
|
63558 | 1860 |
for x :: real |
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1861 |
unfolding eventually_at_split filterlim_at_split |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1862 |
by (auto intro!: lhopital_right[of f x g g' f'] lhopital_left[of f x g g' f']) |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1863 |
|
50327 | 1864 |
lemma lhopital_right_0_at_top: |
1865 |
fixes f g :: "real \<Rightarrow> real" |
|
1866 |
assumes g_0: "LIM x at_right 0. g x :> at_top" |
|
63558 | 1867 |
and ev: |
1868 |
"eventually (\<lambda>x. g' x \<noteq> 0) (at_right 0)" |
|
1869 |
"eventually (\<lambda>x. DERIV f x :> f' x) (at_right 0)" |
|
1870 |
"eventually (\<lambda>x. DERIV g x :> g' x) (at_right 0)" |
|
1871 |
and lim: "((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> x) (at_right 0)" |
|
61973 | 1872 |
shows "((\<lambda> x. f x / g x) \<longlongrightarrow> x) (at_right 0)" |
50327 | 1873 |
unfolding tendsto_iff |
1874 |
proof safe |
|
63558 | 1875 |
fix e :: real |
1876 |
assume "0 < e" |
|
50327 | 1877 |
with lim[unfolded tendsto_iff, rule_format, of "e / 4"] |
63558 | 1878 |
have "eventually (\<lambda>t. dist (f' t / g' t) x < e / 4) (at_right 0)" |
1879 |
by simp |
|
50327 | 1880 |
from eventually_conj[OF eventually_conj[OF ev(1) ev(2)] eventually_conj[OF ev(3) this]] |
1881 |
obtain a where [arith]: "0 < a" |
|
1882 |
and g'_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g' x \<noteq> 0" |
|
1883 |
and f0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV f x :> (f' x)" |
|
1884 |
and g0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV g x :> (g' x)" |
|
1885 |
and Df: "\<And>t. 0 < t \<Longrightarrow> t < a \<Longrightarrow> dist (f' t / g' t) x < e / 4" |
|
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1886 |
unfolding eventually_at_le by (auto simp: dist_real_def) |
50327 | 1887 |
|
63558 | 1888 |
from Df have "eventually (\<lambda>t. t < a) (at_right 0)" "eventually (\<lambda>t::real. 0 < t) (at_right 0)" |
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51529
diff
changeset
|
1889 |
unfolding eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def) |
50327 | 1890 |
|
1891 |
moreover |
|
50328 | 1892 |
have "eventually (\<lambda>t. 0 < g t) (at_right 0)" "eventually (\<lambda>t. g a < g t) (at_right 0)" |
61810 | 1893 |
using g_0 by (auto elim: eventually_mono simp: filterlim_at_top_dense) |
50327 | 1894 |
|
1895 |
moreover |
|
61973 | 1896 |
have inv_g: "((\<lambda>x. inverse (g x)) \<longlongrightarrow> 0) (at_right 0)" |
50327 | 1897 |
using tendsto_inverse_0 filterlim_mono[OF g_0 at_top_le_at_infinity order_refl] |
1898 |
by (rule filterlim_compose) |
|
61973 | 1899 |
then have "((\<lambda>x. norm (1 - g a * inverse (g x))) \<longlongrightarrow> norm (1 - g a * 0)) (at_right 0)" |
50327 | 1900 |
by (intro tendsto_intros) |
61973 | 1901 |
then have "((\<lambda>x. norm (1 - g a / g x)) \<longlongrightarrow> 1) (at_right 0)" |
50327 | 1902 |
by (simp add: inverse_eq_divide) |
1903 |
from this[unfolded tendsto_iff, rule_format, of 1] |
|
1904 |
have "eventually (\<lambda>x. norm (1 - g a / g x) < 2) (at_right 0)" |
|
61810 | 1905 |
by (auto elim!: eventually_mono simp: dist_real_def) |
50327 | 1906 |
|
1907 |
moreover |
|
63558 | 1908 |
from inv_g have "((\<lambda>t. norm ((f a - x * g a) * inverse (g t))) \<longlongrightarrow> norm ((f a - x * g a) * 0)) |
1909 |
(at_right 0)" |
|
50327 | 1910 |
by (intro tendsto_intros) |
61973 | 1911 |
then have "((\<lambda>t. norm (f a - x * g a) / norm (g t)) \<longlongrightarrow> 0) (at_right 0)" |
50327 | 1912 |
by (simp add: inverse_eq_divide) |
60758 | 1913 |
from this[unfolded tendsto_iff, rule_format, of "e / 2"] \<open>0 < e\<close> |
50327 | 1914 |
have "eventually (\<lambda>t. norm (f a - x * g a) / norm (g t) < e / 2) (at_right 0)" |
1915 |
by (auto simp: dist_real_def) |
|
1916 |
||
1917 |
ultimately show "eventually (\<lambda>t. dist (f t / g t) x < e) (at_right 0)" |
|
1918 |
proof eventually_elim |
|
1919 |
fix t assume t[arith]: "0 < t" "t < a" "g a < g t" "0 < g t" |
|
1920 |
assume ineq: "norm (1 - g a / g t) < 2" "norm (f a - x * g a) / norm (g t) < e / 2" |
|
1921 |
||
1922 |
have "\<exists>y. t < y \<and> y < a \<and> (g a - g t) * f' y = (f a - f t) * g' y" |
|
1923 |
using f0 g0 t(1,2) by (intro GMVT') (force intro!: DERIV_isCont)+ |
|
53381 | 1924 |
then obtain y where [arith]: "t < y" "y < a" |
1925 |
and D_eq0: "(g a - g t) * f' y = (f a - f t) * g' y" |
|
1926 |
by blast |
|
1927 |
from D_eq0 have D_eq: "(f t - f a) / (g t - g a) = f' y / g' y" |
|
60758 | 1928 |
using \<open>g a < g t\<close> g'_neq_0[of y] by (auto simp add: field_simps) |
50327 | 1929 |
|
1930 |
have *: "f t / g t - x = ((f t - f a) / (g t - g a) - x) * (1 - g a / g t) + (f a - x * g a) / g t" |
|
1931 |
by (simp add: field_simps) |
|
1932 |
have "norm (f t / g t - x) \<le> |
|
1933 |
norm (((f t - f a) / (g t - g a) - x) * (1 - g a / g t)) + norm ((f a - x * g a) / g t)" |
|
1934 |
unfolding * by (rule norm_triangle_ineq) |
|
1935 |
also have "\<dots> = dist (f' y / g' y) x * norm (1 - g a / g t) + norm (f a - x * g a) / norm (g t)" |
|
1936 |
by (simp add: abs_mult D_eq dist_real_def) |
|
1937 |
also have "\<dots> < (e / 4) * 2 + e / 2" |
|
60758 | 1938 |
using ineq Df[of y] \<open>0 < e\<close> by (intro add_le_less_mono mult_mono) auto |
50327 | 1939 |
finally show "dist (f t / g t) x < e" |
1940 |
by (simp add: dist_real_def) |
|
1941 |
qed |
|
1942 |
qed |
|
1943 |
||
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1944 |
lemma lhopital_right_at_top: |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1945 |
"LIM x at_right x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1946 |
eventually (\<lambda>x. g' x \<noteq> 0) (at_right x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1947 |
eventually (\<lambda>x. DERIV f x :> f' x) (at_right x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1948 |
eventually (\<lambda>x. DERIV g x :> g' x) (at_right x) \<Longrightarrow> |
61973 | 1949 |
((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at_right x) \<Longrightarrow> |
1950 |
((\<lambda> x. f x / g x) \<longlongrightarrow> y) (at_right x)" |
|
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1951 |
unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1952 |
by (rule lhopital_right_0_at_top) |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1953 |
|
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1954 |
lemma lhopital_left_at_top: |
63558 | 1955 |
"LIM x at_left x. g x :> at_top \<Longrightarrow> |
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1956 |
eventually (\<lambda>x. g' x \<noteq> 0) (at_left x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1957 |
eventually (\<lambda>x. DERIV f x :> f' x) (at_left x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1958 |
eventually (\<lambda>x. DERIV g x :> g' x) (at_left x) \<Longrightarrow> |
61973 | 1959 |
((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at_left x) \<Longrightarrow> |
1960 |
((\<lambda> x. f x / g x) \<longlongrightarrow> y) (at_left x)" |
|
63558 | 1961 |
for x :: real |
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1962 |
unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror |
56479
91958d4b30f7
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents:
56409
diff
changeset
|
1963 |
by (rule lhopital_right_at_top[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror) |
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1964 |
|
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1965 |
lemma lhopital_at_top: |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1966 |
"LIM x at x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1967 |
eventually (\<lambda>x. g' x \<noteq> 0) (at x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1968 |
eventually (\<lambda>x. DERIV f x :> f' x) (at x) \<Longrightarrow> |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1969 |
eventually (\<lambda>x. DERIV g x :> g' x) (at x) \<Longrightarrow> |
61973 | 1970 |
((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at x) \<Longrightarrow> |
1971 |
((\<lambda> x. f x / g x) \<longlongrightarrow> y) (at x)" |
|
50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1972 |
unfolding eventually_at_split filterlim_at_split |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1973 |
by (auto intro!: lhopital_right_at_top[of g x g' f f'] lhopital_left_at_top[of g x g' f f']) |
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50329
diff
changeset
|
1974 |
|
50347 | 1975 |
lemma lhospital_at_top_at_top: |
1976 |
fixes f g :: "real \<Rightarrow> real" |
|
1977 |
assumes g_0: "LIM x at_top. g x :> at_top" |
|
63558 | 1978 |
and g': "eventually (\<lambda>x. g' x \<noteq> 0) at_top" |
1979 |
and Df: "eventually (\<lambda>x. DERIV f x :> f' x) at_top" |
|
1980 |
and Dg: "eventually (\<lambda>x. DERIV g x :> g' x) at_top" |
|
1981 |
and lim: "((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> x) at_top" |
|
61973 | 1982 |
shows "((\<lambda> x. f x / g x) \<longlongrightarrow> x) at_top" |
50347 | 1983 |
unfolding filterlim_at_top_to_right |
1984 |
proof (rule lhopital_right_0_at_top) |
|
1985 |
let ?F = "\<lambda>x. f (inverse x)" |
|
1986 |
let ?G = "\<lambda>x. g (inverse x)" |
|
1987 |
let ?R = "at_right (0::real)" |
|
1988 |
let ?D = "\<lambda>f' x. f' (inverse x) * - (inverse x ^ Suc (Suc 0))" |
|
1989 |
show "LIM x ?R. ?G x :> at_top" |
|
1990 |
using g_0 unfolding filterlim_at_top_to_right . |
|
1991 |
show "eventually (\<lambda>x. DERIV ?G x :> ?D g' x) ?R" |
|
1992 |
unfolding eventually_at_right_to_top |
|
63558 | 1993 |
using Dg eventually_ge_at_top[where c=1] |
50347 | 1994 |
apply eventually_elim |
1995 |
apply (rule DERIV_cong) |
|
63558 | 1996 |
apply (rule DERIV_chain'[where f=inverse]) |
1997 |
apply (auto intro!: DERIV_inverse) |
|
50347 | 1998 |
done |
1999 |
show "eventually (\<lambda>x. DERIV ?F x :> ?D f' x) ?R" |
|
2000 |
unfolding eventually_at_right_to_top |
|
63558 | 2001 |
using Df eventually_ge_at_top[where c=1] |
50347 | 2002 |
apply eventually_elim |
2003 |
apply (rule DERIV_cong) |
|
63558 | 2004 |
apply (rule DERIV_chain'[where f=inverse]) |
2005 |
apply (auto intro!: DERIV_inverse) |
|
50347 | 2006 |
done |
2007 |
show "eventually (\<lambda>x. ?D g' x \<noteq> 0) ?R" |
|
2008 |
unfolding eventually_at_right_to_top |
|
63558 | 2009 |
using g' eventually_ge_at_top[where c=1] |
50347 | 2010 |
by eventually_elim auto |
61973 | 2011 |
show "((\<lambda>x. ?D f' x / ?D g' x) \<longlongrightarrow> x) ?R" |
50347 | 2012 |
unfolding filterlim_at_right_to_top |
2013 |
apply (intro filterlim_cong[THEN iffD2, OF refl refl _ lim]) |
|
63558 | 2014 |
using eventually_ge_at_top[where c=1] |
56479
91958d4b30f7
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents:
56409
diff
changeset
|
2015 |
by eventually_elim simp |
50347 | 2016 |
qed |
2017 |
||
21164 | 2018 |
end |