equal
deleted
inserted
replaced
6 section \<open>Multivariate calculus in Euclidean space\<close> |
6 section \<open>Multivariate calculus in Euclidean space\<close> |
7 |
7 |
8 theory Derivative |
8 theory Derivative |
9 imports Brouwer_Fixpoint Operator_Norm Uniform_Limit |
9 imports Brouwer_Fixpoint Operator_Norm Uniform_Limit |
10 begin |
10 begin |
11 |
|
12 lemma netlimit_at_vector: (* TODO: move *) |
|
13 fixes a :: "'a::real_normed_vector" |
|
14 shows "netlimit (at a) = a" |
|
15 proof (cases "\<exists>x. x \<noteq> a") |
|
16 case True then obtain x where x: "x \<noteq> a" .. |
|
17 have "\<not> trivial_limit (at a)" |
|
18 unfolding trivial_limit_def eventually_at dist_norm |
|
19 apply clarsimp |
|
20 apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI) |
|
21 apply (simp add: norm_sgn sgn_zero_iff x) |
|
22 done |
|
23 then show ?thesis |
|
24 by (rule netlimit_within [of a UNIV]) |
|
25 qed simp |
|
26 |
11 |
27 declare has_derivative_bounded_linear[dest] |
12 declare has_derivative_bounded_linear[dest] |
28 |
13 |
29 subsection \<open>Derivatives\<close> |
14 subsection \<open>Derivatives\<close> |
30 |
15 |