src/HOL/Multivariate_Analysis/Derivative.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46898 1570b30ee040
child 50418 bd68cf816dd3
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36334
diff changeset
     1
(*  Title:                       HOL/Multivariate_Analysis/Derivative.thy
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36334
diff changeset
     2
    Author:                      John Harrison
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36334
diff changeset
     3
    Translation from HOL Light:  Robert Himmelmann, TU Muenchen
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36334
diff changeset
     4
*)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
     5
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
     6
header {* Multivariate calculus in Euclidean space. *}
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
     7
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
     8
theory Derivative
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
     9
imports Brouwer_Fixpoint Operator_Norm
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    10
begin
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    11
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    12
(* Because I do not want to type this all the time *)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    13
lemmas linear_linear = linear_conv_bounded_linear[THEN sym]
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    14
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    15
subsection {* Derivatives *}
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    16
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    17
text {* The definition is slightly tricky since we make it work over
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    18
  nets of a particular form. This lets us prove theorems generally and use 
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    19
  "at a" or "at a within s" for restriction to a set (1-sided on R etc.) *}
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    20
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 43338
diff changeset
    21
definition has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a filter \<Rightarrow> bool)"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    22
(infixl "(has'_derivative)" 12) where
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    23
 "(f has_derivative f') net \<equiv> bounded_linear f' \<and> ((\<lambda>y. (1 / (norm (y - netlimit net))) *\<^sub>R
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    24
   (f y - (f (netlimit net) + f'(y - netlimit net)))) ---> 0) net"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    25
44137
ac5cb4c86448 simplify some proofs
huffman
parents: 44125
diff changeset
    26
lemma derivative_linear[dest]:
ac5cb4c86448 simplify some proofs
huffman
parents: 44125
diff changeset
    27
  "(f has_derivative f') net \<Longrightarrow> bounded_linear f'"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    28
  unfolding has_derivative_def by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    29
37730
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    30
lemma netlimit_at_vector:
44137
ac5cb4c86448 simplify some proofs
huffman
parents: 44125
diff changeset
    31
  (* TODO: move *)
37730
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    32
  fixes a :: "'a::real_normed_vector"
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    33
  shows "netlimit (at a) = a"
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    34
proof (cases "\<exists>x. x \<noteq> a")
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    35
  case True then obtain x where x: "x \<noteq> a" ..
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    36
  have "\<not> trivial_limit (at a)"
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    37
    unfolding trivial_limit_def eventually_at dist_norm
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    38
    apply clarsimp
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    39
    apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI)
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    40
    apply (simp add: norm_sgn sgn_zero_iff x)
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    41
    done
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    42
  thus ?thesis
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    43
    by (rule netlimit_within [of a UNIV, unfolded within_UNIV])
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    44
qed simp
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    45
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    46
lemma FDERIV_conv_has_derivative:
44137
ac5cb4c86448 simplify some proofs
huffman
parents: 44125
diff changeset
    47
  shows "FDERIV f x :> f' = (f has_derivative f') (at x)"
ac5cb4c86448 simplify some proofs
huffman
parents: 44125
diff changeset
    48
  unfolding fderiv_def has_derivative_def netlimit_at_vector
ac5cb4c86448 simplify some proofs
huffman
parents: 44125
diff changeset
    49
  by (simp add: diff_diff_eq Lim_at_zero [where a=x]
44568
e6f291cb5810 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents: 44531
diff changeset
    50
    tendsto_norm_zero_iff [where 'b='b, symmetric])
44137
ac5cb4c86448 simplify some proofs
huffman
parents: 44125
diff changeset
    51
ac5cb4c86448 simplify some proofs
huffman
parents: 44125
diff changeset
    52
lemma DERIV_conv_has_derivative:
ac5cb4c86448 simplify some proofs
huffman
parents: 44125
diff changeset
    53
  "(DERIV f x :> f') = (f has_derivative op * f') (at x)"
ac5cb4c86448 simplify some proofs
huffman
parents: 44125
diff changeset
    54
  unfolding deriv_fderiv FDERIV_conv_has_derivative
ac5cb4c86448 simplify some proofs
huffman
parents: 44125
diff changeset
    55
  by (subst mult_commute, rule refl)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    56
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
    57
text {* These are the only cases we'll care about, probably. *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    58
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    59
lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    60
         bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    61
  unfolding has_derivative_def and Lim by(auto simp add:netlimit_within)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    62
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    63
lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    64
         bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
45031
9583f2b56f85 add lemmas within_empty and tendsto_bot;
huffman
parents: 44907
diff changeset
    65
  using has_derivative_within [of f f' x UNIV] by simp
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    66
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
    67
text {* More explicit epsilon-delta forms. *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    68
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    69
lemma has_derivative_within':
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    70
  "(f has_derivative f')(at x within s) \<longleftrightarrow> bounded_linear f' \<and>
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    71
        (\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm(x' - x) \<and> norm(x' - x) < d
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    72
        \<longrightarrow> norm(f x' - f x - f'(x' - x)) / norm(x' - x) < e)"
36587
534418d8d494 remove redundant lemma vector_dist_norm
huffman
parents: 36581
diff changeset
    73
  unfolding has_derivative_within Lim_within dist_norm
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
    74
  unfolding diff_0_right by (simp add: diff_diff_eq)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    75
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    76
lemma has_derivative_at':
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    77
 "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    78
   (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm(x' - x) \<and> norm(x' - x) < d
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    79
        \<longrightarrow> norm(f x' - f x - f'(x' - x)) / norm(x' - x) < e)"
45031
9583f2b56f85 add lemmas within_empty and tendsto_bot;
huffman
parents: 44907
diff changeset
    80
  using has_derivative_within' [of f f' x UNIV] by simp
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    81
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    82
lemma has_derivative_at_within: "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    83
  unfolding has_derivative_within' has_derivative_at' by meson
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    84
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    85
lemma has_derivative_within_open:
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    86
  "a \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a))"
37730
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    87
  by (simp only: at_within_interior interior_open)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    88
43338
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    89
lemma has_derivative_right:
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    90
  fixes f :: "real \<Rightarrow> real" and y :: "real"
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    91
  shows "(f has_derivative (op * y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    92
    ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x <..} \<inter> I))"
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    93
proof -
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    94
  have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) ---> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    95
    ((\<lambda>t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \<inter> I))"
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
    96
    by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib)
43338
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    97
  also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))"
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    98
    by (simp add: Lim_null[symmetric])
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    99
  also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))"
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   100
    by (intro Lim_cong_within) (simp_all add: field_simps)
43338
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
   101
  finally show ?thesis
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   102
    by (simp add: bounded_linear_mult_right has_derivative_within)
43338
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
   103
qed
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
   104
37648
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   105
lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   106
proof -
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   107
  assume "bounded_linear f"
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   108
  then interpret f: bounded_linear f .
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   109
  show "linear f"
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   110
    by (simp add: f.add f.scaleR linear_def)
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   111
qed
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   112
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   113
lemma derivative_is_linear:
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   114
  "(f has_derivative f') net \<Longrightarrow> linear f'"
37648
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   115
  by (rule derivative_linear [THEN bounded_linear_imp_linear])
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   116
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
   117
subsubsection {* Combining theorems. *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   118
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   119
lemma has_derivative_id: "((\<lambda>x. x) has_derivative (\<lambda>h. h)) net"
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   120
  unfolding has_derivative_def
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   121
  by (simp add: bounded_linear_ident tendsto_const)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   122
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   123
lemma has_derivative_const: "((\<lambda>x. c) has_derivative (\<lambda>h. 0)) net"
44125
230a8665c919 mark some redundant theorems as legacy
huffman
parents: 44124
diff changeset
   124
  unfolding has_derivative_def
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   125
  by (simp add: bounded_linear_zero tendsto_const)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   126
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   127
lemma (in bounded_linear) has_derivative': "(f has_derivative f) net"
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   128
  unfolding has_derivative_def apply(rule,rule bounded_linear_axioms)
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   129
  unfolding diff by (simp add: tendsto_const)
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   130
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   131
lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   132
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   133
lemma (in bounded_linear) has_derivative:
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   134
  assumes "((\<lambda>x. g x) has_derivative (\<lambda>h. g' h)) net"
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   135
  shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>h. f (g' h))) net"
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   136
  using assms unfolding has_derivative_def
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   137
  apply safe
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   138
  apply (erule bounded_linear_compose [OF local.bounded_linear])
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   139
  apply (drule local.tendsto)
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   140
  apply (simp add: local.scaleR local.diff local.add local.zero)
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   141
  done
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   142
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   143
lemmas scaleR_right_has_derivative =
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 45031
diff changeset
   144
  bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   145
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   146
lemmas scaleR_left_has_derivative =
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 45031
diff changeset
   147
  bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   148
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   149
lemmas inner_right_has_derivative =
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 45031
diff changeset
   150
  bounded_linear.has_derivative [OF bounded_linear_inner_right]
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   151
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   152
lemmas inner_left_has_derivative =
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 45031
diff changeset
   153
  bounded_linear.has_derivative [OF bounded_linear_inner_left]
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   154
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   155
lemmas mult_right_has_derivative =
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 45031
diff changeset
   156
  bounded_linear.has_derivative [OF bounded_linear_mult_right]
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   157
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   158
lemmas mult_left_has_derivative =
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 45031
diff changeset
   159
  bounded_linear.has_derivative [OF bounded_linear_mult_left]
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   160
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   161
lemmas euclidean_component_has_derivative =
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   162
  bounded_linear.has_derivative [OF bounded_linear_euclidean_component]
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   163
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   164
lemma has_derivative_neg:
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   165
  assumes "(f has_derivative f') net"
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   166
  shows "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   167
  using scaleR_right_has_derivative [where r="-1", OF assms] by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   168
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   169
lemma has_derivative_add:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   170
  assumes "(f has_derivative f') net" and "(g has_derivative g') net"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   171
  shows "((\<lambda>x. f(x) + g(x)) has_derivative (\<lambda>h. f'(h) + g'(h))) net"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   172
proof-
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   173
  note as = assms[unfolded has_derivative_def]
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   174
  show ?thesis unfolding has_derivative_def apply(rule,rule bounded_linear_add)
44125
230a8665c919 mark some redundant theorems as legacy
huffman
parents: 44124
diff changeset
   175
    using tendsto_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   176
    by (auto simp add: algebra_simps)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   177
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   178
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   179
lemma has_derivative_add_const:
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   180
  "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   181
  by (drule has_derivative_add, rule has_derivative_const, auto)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   182
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   183
lemma has_derivative_sub:
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   184
  assumes "(f has_derivative f') net" and "(g has_derivative g') net"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   185
  shows "((\<lambda>x. f(x) - g(x)) has_derivative (\<lambda>h. f'(h) - g'(h))) net"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   186
  unfolding diff_minus by (intro has_derivative_add has_derivative_neg assms)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   187
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   188
lemma has_derivative_setsum:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   189
  assumes "finite s" and "\<forall>a\<in>s. ((f a) has_derivative (f' a)) net"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   190
  shows "((\<lambda>x. setsum (\<lambda>a. f a x) s) has_derivative (\<lambda>h. setsum (\<lambda>a. f' a h) s)) net"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   191
  using assms by (induct, simp_all add: has_derivative_const has_derivative_add)
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
   192
text {* Somewhat different results for derivative of scalar multiplier. *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   193
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   194
(** move **)
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   195
lemma linear_vmul_component: (* TODO: delete *)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   196
  assumes lf: "linear f"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   197
  shows "linear (\<lambda>x. f x $$ k *\<^sub>R v)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   198
  using lf
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   199
  by (auto simp add: linear_def algebra_simps)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   200
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   201
lemmas has_derivative_intros =
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   202
  has_derivative_id has_derivative_const
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   203
  has_derivative_add has_derivative_sub has_derivative_neg
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   204
  has_derivative_add_const
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   205
  scaleR_left_has_derivative scaleR_right_has_derivative
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   206
  inner_left_has_derivative inner_right_has_derivative
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   207
  euclidean_component_has_derivative
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   208
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
   209
subsubsection {* Limit transformation for derivatives *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   210
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   211
lemma has_derivative_transform_within:
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   212
  assumes "0 < d" "x \<in> s" "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'" "(f has_derivative f') (at x within s)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   213
  shows "(g has_derivative f') (at x within s)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   214
  using assms(4) unfolding has_derivative_within apply- apply(erule conjE,rule,assumption)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   215
  apply(rule Lim_transform_within[OF assms(1)]) defer apply assumption
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   216
  apply(rule,rule) apply(drule assms(3)[rule_format]) using assms(3)[rule_format, OF assms(2)] by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   217
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   218
lemma has_derivative_transform_at:
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   219
  assumes "0 < d" "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'" "(f has_derivative f') (at x)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   220
  shows "(g has_derivative f') (at x)"
45031
9583f2b56f85 add lemmas within_empty and tendsto_bot;
huffman
parents: 44907
diff changeset
   221
  using has_derivative_transform_within [of d x UNIV f g f'] assms by simp
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   222
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   223
lemma has_derivative_transform_within_open:
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   224
  assumes "open s" "x \<in> s" "\<forall>y\<in>s. f y = g y" "(f has_derivative f') (at x)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   225
  shows "(g has_derivative f') (at x)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   226
  using assms(4) unfolding has_derivative_at apply- apply(erule conjE,rule,assumption)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   227
  apply(rule Lim_transform_within_open[OF assms(1,2)]) defer apply assumption
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   228
  apply(rule,rule) apply(drule assms(3)[rule_format]) using assms(3)[rule_format, OF assms(2)] by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   229
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
   230
subsection {* Differentiability *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   231
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36334
diff changeset
   232
no_notation Deriv.differentiable (infixl "differentiable" 60)
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36334
diff changeset
   233
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 43338
diff changeset
   234
definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" (infixr "differentiable" 30) where
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   235
  "f differentiable net \<equiv> (\<exists>f'. (f has_derivative f') net)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   236
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   237
definition differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "differentiable'_on" 30) where
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   238
  "f differentiable_on s \<equiv> (\<forall>x\<in>s. f differentiable (at x within s))"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   239
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   240
lemma differentiableI: "(f has_derivative f') net \<Longrightarrow> f differentiable net"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   241
  unfolding differentiable_def by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   242
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   243
lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   244
  unfolding differentiable_def using has_derivative_at_within by blast
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   245
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   246
lemma differentiable_within_open: (* TODO: delete *)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   247
  assumes "a \<in> s" and "open s"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   248
  shows "f differentiable (at a within s) \<longleftrightarrow> (f differentiable (at a))"
37730
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   249
  using assms by (simp only: at_within_interior interior_open)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   250
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   251
lemma differentiable_on_eq_differentiable_at:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   252
  "open s \<Longrightarrow> (f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x))"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   253
  unfolding differentiable_on_def
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   254
  by (auto simp add: at_within_interior interior_open)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   255
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   256
lemma differentiable_transform_within:
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   257
  assumes "0 < d" and "x \<in> s" and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   258
  assumes "f differentiable (at x within s)"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   259
  shows "g differentiable (at x within s)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   260
  using assms(4) unfolding differentiable_def
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   261
  by (auto intro!: has_derivative_transform_within[OF assms(1-3)])
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   262
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   263
lemma differentiable_transform_at:
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   264
  assumes "0 < d" "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'" "f differentiable at x"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   265
  shows "g differentiable at x"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   266
  using assms(3) unfolding differentiable_def
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   267
  using has_derivative_transform_at[OF assms(1-2)] by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   268
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   269
subsection {* Frechet derivative and Jacobian matrix. *}
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   270
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   271
definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   272
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   273
lemma frechet_derivative_works:
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   274
 "f differentiable net \<longleftrightarrow> (f has_derivative (frechet_derivative f net)) net"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   275
  unfolding frechet_derivative_def differentiable_def and some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] ..
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   276
37648
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   277
lemma linear_frechet_derivative:
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   278
  shows "f differentiable net \<Longrightarrow> linear(frechet_derivative f net)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   279
  unfolding frechet_derivative_works has_derivative_def
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   280
  by (auto intro: bounded_linear_imp_linear)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   281
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
   282
subsection {* Differentiability implies continuity *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   283
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   284
lemma Lim_mul_norm_within:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   285
  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   286
  shows "(f ---> 0) (at a within s) \<Longrightarrow> ((\<lambda>x. norm(x - a) *\<^sub>R f(x)) ---> 0) (at a within s)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   287
  unfolding Lim_within apply(rule,rule)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   288
  apply(erule_tac x=e in allE,erule impE,assumption,erule exE,erule conjE)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   289
  apply(rule_tac x="min d 1" in exI) apply rule defer
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   290
  apply(rule,erule_tac x=x in ballE) unfolding dist_norm diff_0_right
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   291
  by(auto intro!: mult_strict_mono[of _ "1::real", unfolded mult_1_left])
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   292
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   293
lemma differentiable_imp_continuous_within:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   294
  assumes "f differentiable (at x within s)" 
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   295
  shows "continuous (at x within s) f"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   296
proof-
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   297
  from assms guess f' unfolding differentiable_def has_derivative_within ..
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   298
  note f'=this
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   299
  then interpret bounded_linear f' by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   300
  have *:"\<And>xa. x\<noteq>xa \<Longrightarrow> (f' \<circ> (\<lambda>y. y - x)) xa + norm (xa - x) *\<^sub>R ((1 / norm (xa - x)) *\<^sub>R (f xa - (f x + f' (xa - x)))) - ((f' \<circ> (\<lambda>y. y - x)) x + 0) = f xa - f x"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   301
    using zero by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   302
  have **:"continuous (at x within s) (f' \<circ> (\<lambda>y. y - x))"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   303
    apply(rule continuous_within_compose) apply(rule continuous_intros)+
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   304
    by(rule linear_continuous_within[OF f'[THEN conjunct1]])
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   305
  show ?thesis unfolding continuous_within
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   306
    using f'[THEN conjunct2, THEN Lim_mul_norm_within]
44125
230a8665c919 mark some redundant theorems as legacy
huffman
parents: 44124
diff changeset
   307
    apply- apply(drule tendsto_add)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   308
    apply(rule **[unfolded continuous_within])
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   309
    unfolding Lim_within and dist_norm
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   310
    apply (rule, rule)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   311
    apply (erule_tac x=e in allE)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   312
    apply (erule impE | assumption)+
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   313
    apply (erule exE, rule_tac x=d in exI)
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   314
    by (auto simp add: zero *)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   315
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   316
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   317
lemma differentiable_imp_continuous_at:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   318
  "f differentiable at x \<Longrightarrow> continuous (at x) f"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   319
 by(rule differentiable_imp_continuous_within[of _ x UNIV, unfolded within_UNIV])
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   320
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   321
lemma differentiable_imp_continuous_on:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   322
  "f differentiable_on s \<Longrightarrow> continuous_on s f"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   323
  unfolding differentiable_on_def continuous_on_eq_continuous_within
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   324
  using differentiable_imp_continuous_within by blast
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   325
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   326
lemma has_derivative_within_subset:
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   327
 "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   328
  unfolding has_derivative_within using Lim_within_subset by blast
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   329
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   330
lemma differentiable_within_subset:
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   331
  "f differentiable (at x within t) \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable (at x within s)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   332
  unfolding differentiable_def using has_derivative_within_subset by blast
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   333
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   334
lemma differentiable_on_subset:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   335
  "f differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable_on s"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   336
  unfolding differentiable_on_def using differentiable_within_subset by blast
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   337
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   338
lemma differentiable_on_empty: "f differentiable_on {}"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   339
  unfolding differentiable_on_def by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   340
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
   341
text {* Several results are easier using a "multiplied-out" variant.
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
   342
(I got this idea from Dieudonne's proof of the chain rule). *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   343
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   344
lemma has_derivative_within_alt:
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   345
 "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   346
  (\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm(y - x) < d \<longrightarrow> norm(f(y) - f(x) - f'(y - x)) \<le> e * norm(y - x))" (is "?lhs \<longleftrightarrow> ?rhs")
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   347
proof
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   348
  assume ?lhs thus ?rhs
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   349
    unfolding has_derivative_within apply-apply(erule conjE,rule,assumption)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   350
    unfolding Lim_within
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   351
    apply(rule,erule_tac x=e in allE,rule,erule impE,assumption)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   352
    apply(erule exE,rule_tac x=d in exI)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   353
    apply(erule conjE,rule,assumption,rule,rule)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   354
  proof-
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   355
    fix x y e d assume as:"0 < e" "0 < d" "norm (y - x) < d" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   356
      dist ((1 / norm (xa - x)) *\<^sub>R (f xa - (f x + f' (xa - x)))) 0 < e" "y \<in> s" "bounded_linear f'"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   357
    then interpret bounded_linear f' by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   358
    show "norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)" proof(cases "y=x")
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   359
      case True thus ?thesis using `bounded_linear f'` by(auto simp add: zero)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   360
    next
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   361
      case False hence "norm (f y - (f x + f' (y - x))) < e * norm (y - x)" using as(4)[rule_format, OF `y\<in>s`]
41958
5abc60a017e0 eliminated hard tabs;
wenzelm
parents: 41829
diff changeset
   362
        unfolding dist_norm diff_0_right using as(3)
5abc60a017e0 eliminated hard tabs;
wenzelm
parents: 41829
diff changeset
   363
        using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded dist_norm]
5abc60a017e0 eliminated hard tabs;
wenzelm
parents: 41829
diff changeset
   364
        by (auto simp add: linear_0 linear_sub)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   365
      thus ?thesis by(auto simp add:algebra_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   366
    qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   367
  qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   368
next
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   369
  assume ?rhs thus ?lhs unfolding has_derivative_within Lim_within
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   370
    apply-apply(erule conjE,rule,assumption)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   371
    apply(rule,erule_tac x="e/2" in allE,rule,erule impE) defer
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   372
    apply(erule exE,rule_tac x=d in exI)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   373
    apply(erule conjE,rule,assumption,rule,rule)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   374
    unfolding dist_norm diff_0_right norm_scaleR
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   375
    apply(erule_tac x=xa in ballE,erule impE)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   376
  proof-
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   377
    fix e d y assume "bounded_linear f'" "0 < e" "0 < d" "y \<in> s" "0 < norm (y - x) \<and> norm (y - x) < d"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   378
        "norm (f y - f x - f' (y - x)) \<le> e / 2 * norm (y - x)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   379
    thus "\<bar>1 / norm (y - x)\<bar> * norm (f y - (f x + f' (y - x))) < e"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   380
      apply(rule_tac le_less_trans[of _ "e/2"])
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   381
      by(auto intro!:mult_imp_div_pos_le simp add:algebra_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   382
  qed auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   383
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   384
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   385
lemma has_derivative_at_alt:
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35028
diff changeset
   386
  "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   387
  (\<forall>e>0. \<exists>d>0. \<forall>y. norm(y - x) < d \<longrightarrow> norm(f y - f x - f'(y - x)) \<le> e * norm(y - x))"
45031
9583f2b56f85 add lemmas within_empty and tendsto_bot;
huffman
parents: 44907
diff changeset
   388
  using has_derivative_within_alt[where s=UNIV] by simp
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   389
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   390
subsection {* The chain rule. *}
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   391
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   392
lemma diff_chain_within:
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   393
  assumes "(f has_derivative f') (at x within s)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   394
  assumes "(g has_derivative g') (at (f x) within (f ` s))"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   395
  shows "((g o f) has_derivative (g' o f'))(at x within s)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   396
  unfolding has_derivative_within_alt
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   397
  apply(rule,rule bounded_linear_compose[unfolded o_def[THEN sym]])
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   398
  apply(rule assms(2)[unfolded has_derivative_def,THEN conjE],assumption)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   399
  apply(rule assms(1)[unfolded has_derivative_def,THEN conjE],assumption)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   400
proof(rule,rule)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   401
  note assms = assms[unfolded has_derivative_within_alt]
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   402
  fix e::real assume "0<e"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   403
  guess B1 using bounded_linear.pos_bounded[OF assms(1)[THEN conjunct1, rule_format]] .. note B1 = this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   404
  guess B2 using bounded_linear.pos_bounded[OF assms(2)[THEN conjunct1, rule_format]] .. note B2 = this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   405
  have *:"e / 2 / B2 > 0" using `e>0` B2 apply-apply(rule divide_pos_pos) by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   406
  guess d1 using assms(1)[THEN conjunct2, rule_format, OF *] .. note d1 = this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   407
  have *:"e / 2 / (1 + B1) > 0" using `e>0` B1 apply-apply(rule divide_pos_pos) by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   408
  guess de using assms(2)[THEN conjunct2, rule_format, OF *] .. note de = this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   409
  guess d2 using assms(1)[THEN conjunct2, rule_format, OF zero_less_one] .. note d2 = this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   410
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   411
  def d0 \<equiv> "(min d1 d2)/2" have d0:"d0>0" "d0 < d1" "d0 < d2" unfolding d0_def using d1 d2 by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   412
  def d \<equiv> "(min d0 (de / (B1 + 1))) / 2" have "de * 2 / (B1 + 1) > de / (B1 + 1)" apply(rule divide_strict_right_mono) using B1 de by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   413
  hence d:"d>0" "d < d1" "d < d2" "d < (de / (B1 + 1))" unfolding d_def using d0 d1 d2 de B1 by(auto intro!: divide_pos_pos simp add:min_less_iff_disj not_less)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   414
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   415
  show "\<exists>d>0. \<forall>y\<in>s. norm (y - x) < d \<longrightarrow> norm ((g \<circ> f) y - (g \<circ> f) x - (g' \<circ> f') (y - x)) \<le> e * norm (y - x)" apply(rule_tac x=d in exI)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   416
    proof(rule,rule `d>0`,rule,rule) 
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   417
    fix y assume as:"y \<in> s" "norm (y - x) < d"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   418
    hence 1:"norm (f y - f x - f' (y - x)) \<le> min (norm (y - x)) (e / 2 / B2 * norm (y - x))" using d1 d2 d by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   419
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   420
    have "norm (f y - f x) \<le> norm (f y - f x - f' (y - x)) + norm (f' (y - x))"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   421
      using norm_triangle_sub[of "f y - f x" "f' (y - x)"]
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   422
      by(auto simp add:algebra_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   423
    also have "\<dots> \<le> norm (f y - f x - f' (y - x)) + B1 * norm (y - x)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   424
      apply(rule add_left_mono) using B1 by(auto simp add:algebra_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   425
    also have "\<dots> \<le> min (norm (y - x)) (e / 2 / B2 * norm (y - x)) + B1 * norm (y - x)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   426
      apply(rule add_right_mono) using d1 d2 d as by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   427
    also have "\<dots> \<le> norm (y - x) + B1 * norm (y - x)" by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   428
    also have "\<dots> = norm (y - x) * (1 + B1)" by(auto simp add:field_simps)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   429
    finally have 3:"norm (f y - f x) \<le> norm (y - x) * (1 + B1)" by auto 
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   430
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   431
    hence "norm (f y - f x) \<le> d * (1 + B1)" apply-
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   432
      apply(rule order_trans,assumption,rule mult_right_mono)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   433
      using as B1 by auto 
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   434
    also have "\<dots> < de" using d B1 by(auto simp add:field_simps) 
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   435
    finally have "norm (g (f y) - g (f x) - g' (f y - f x)) \<le> e / 2 / (1 + B1) * norm (f y - f x)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   436
      apply-apply(rule de[THEN conjunct2,rule_format])
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   437
      using `y\<in>s` using d as by auto 
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   438
    also have "\<dots> = (e / 2) * (1 / (1 + B1) * norm (f y - f x))" by auto 
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   439
    also have "\<dots> \<le> e / 2 * norm (y - x)" apply(rule mult_left_mono)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   440
      using `e>0` and 3 using B1 and `e>0` by(auto simp add:divide_le_eq)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   441
    finally have 4:"norm (g (f y) - g (f x) - g' (f y - f x)) \<le> e / 2 * norm (y - x)" by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   442
    
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   443
    interpret g': bounded_linear g' using assms(2) by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   444
    interpret f': bounded_linear f' using assms(1) by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   445
    have "norm (- g' (f' (y - x)) + g' (f y - f x)) = norm (g' (f y - f x - f' (y - x)))"
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36334
diff changeset
   446
      by(auto simp add:algebra_simps f'.diff g'.diff g'.add)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   447
    also have "\<dots> \<le> B2 * norm (f y - f x - f' (y - x))" using B2
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   448
      by (auto simp add: algebra_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   449
    also have "\<dots> \<le> B2 * (e / 2 / B2 * norm (y - x))"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   450
      apply (rule mult_left_mono) using as d1 d2 d B2 by auto 
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   451
    also have "\<dots> \<le> e / 2 * norm (y - x)" using B2 by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   452
    finally have 5:"norm (- g' (f' (y - x)) + g' (f y - f x)) \<le> e / 2 * norm (y - x)" by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   453
    
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   454
    have "norm (g (f y) - g (f x) - g' (f y - f x)) + norm (g (f y) - g (f x) - g' (f' (y - x)) - (g (f y) - g (f x) - g' (f y - f x))) \<le> e * norm (y - x)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   455
      using 5 4 by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   456
    thus "norm ((g \<circ> f) y - (g \<circ> f) x - (g' \<circ> f') (y - x)) \<le> e * norm (y - x)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   457
      unfolding o_def apply- apply(rule order_trans, rule norm_triangle_sub)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   458
      by assumption
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   459
  qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   460
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   461
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   462
lemma diff_chain_at:
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   463
  "(f has_derivative f') (at x) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> ((g o f) has_derivative (g' o f')) (at x)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   464
  using diff_chain_within[of f f' x UNIV g g']
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   465
  using has_derivative_within_subset[of g g' "f x" UNIV "range f"]
45031
9583f2b56f85 add lemmas within_empty and tendsto_bot;
huffman
parents: 44907
diff changeset
   466
  by simp
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   467
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   468
subsection {* Composition rules stated just for differentiability. *}
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   469
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   470
lemma differentiable_const [intro]:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   471
  "(\<lambda>z. c) differentiable (net::'a::real_normed_vector filter)"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   472
  unfolding differentiable_def using has_derivative_const by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   473
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   474
lemma differentiable_id [intro]:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   475
  "(\<lambda>z. z) differentiable (net::'a::real_normed_vector filter)"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   476
    unfolding differentiable_def using has_derivative_id by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   477
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   478
lemma differentiable_cmul [intro]:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   479
  "f differentiable net \<Longrightarrow>
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   480
  (\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   481
  unfolding differentiable_def
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   482
  apply(erule exE, drule scaleR_right_has_derivative) by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   483
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   484
lemma differentiable_neg [intro]:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   485
  "f differentiable net \<Longrightarrow>
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   486
  (\<lambda>z. -(f z)) differentiable (net::'a::real_normed_vector filter)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   487
  unfolding differentiable_def
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   488
  apply(erule exE, drule has_derivative_neg) by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   489
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   490
lemma differentiable_add: "f differentiable net \<Longrightarrow> g differentiable net
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 43338
diff changeset
   491
   \<Longrightarrow> (\<lambda>z. f z + g z) differentiable (net::'a::real_normed_vector filter)"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   492
    unfolding differentiable_def apply(erule exE)+ apply(rule_tac x="\<lambda>z. f' z + f'a z" in exI)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   493
    apply(rule has_derivative_add) by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   494
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   495
lemma differentiable_sub: "f differentiable net \<Longrightarrow> g differentiable net
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 43338
diff changeset
   496
  \<Longrightarrow> (\<lambda>z. f z - g z) differentiable (net::'a::real_normed_vector filter)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   497
  unfolding differentiable_def apply(erule exE)+
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   498
  apply(rule_tac x="\<lambda>z. f' z - f'a z" in exI)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   499
  apply(rule has_derivative_sub) by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   500
37648
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   501
lemma differentiable_setsum:
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   502
  assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   503
  shows "(\<lambda>x. setsum (\<lambda>a. f a x) s) differentiable net"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   504
proof-
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   505
  guess f' using bchoice[OF assms(2)[unfolded differentiable_def]] ..
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   506
  thus ?thesis unfolding differentiable_def apply-
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   507
    apply(rule,rule has_derivative_setsum[where f'=f'],rule assms(1)) by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   508
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   509
37648
41b7dfdc4941 generalize more euclidean_space lemmas
huffman
parents: 37606
diff changeset
   510
lemma differentiable_setsum_numseg:
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   511
  shows "\<forall>i. m \<le> i \<and> i \<le> n \<longrightarrow> (f i) differentiable net \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) {m::nat..n}) differentiable net"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   512
  apply(rule differentiable_setsum) using finite_atLeastAtMost[of n m] by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   513
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   514
lemma differentiable_chain_at:
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   515
  "f differentiable (at x) \<Longrightarrow> g differentiable (at(f x)) \<Longrightarrow> (g o f) differentiable (at x)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   516
  unfolding differentiable_def by(meson diff_chain_at)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   517
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   518
lemma differentiable_chain_within:
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   519
  "f differentiable (at x within s) \<Longrightarrow> g differentiable (at(f x) within (f ` s))
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   520
   \<Longrightarrow> (g o f) differentiable (at x within s)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   521
  unfolding differentiable_def by(meson diff_chain_within)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   522
37730
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   523
subsection {* Uniqueness of derivative *}
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   524
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   525
text {*
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   526
 The general result is a bit messy because we need approachability of the
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   527
 limit point from any direction. But OK for nontrivial intervals etc.
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   528
*}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   529
    
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   530
lemma frechet_derivative_unique_within:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   531
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   532
  assumes "(f has_derivative f') (at x within s)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   533
  assumes "(f has_derivative f'') (at x within s)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   534
  assumes "(\<forall>i<DIM('a). \<forall>e>0. \<exists>d. 0 < abs(d) \<and> abs(d) < e \<and> (x + d *\<^sub>R basis i) \<in> s)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   535
  shows "f' = f''"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   536
proof-
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   537
  note as = assms(1,2)[unfolded has_derivative_def]
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   538
  then interpret f': bounded_linear f' by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   539
  from as interpret f'': bounded_linear f'' by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   540
  have "x islimpt s" unfolding islimpt_approachable
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   541
  proof(rule,rule)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   542
    fix e::real assume "0<e" guess d
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   543
      using assms(3)[rule_format,OF DIM_positive `e>0`] ..
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   544
    thus "\<exists>x'\<in>s. x' \<noteq> x \<and> dist x' x < e"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   545
      apply(rule_tac x="x + d *\<^sub>R basis 0" in bexI)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   546
      unfolding dist_norm by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   547
  qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   548
  hence *:"netlimit (at x within s) = x" apply-apply(rule netlimit_within)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   549
    unfolding trivial_limit_within by simp
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   550
  show ?thesis  apply(rule linear_eq_stdbasis)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   551
    unfolding linear_conv_bounded_linear
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   552
    apply(rule as(1,2)[THEN conjunct1])+
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   553
  proof(rule,rule,rule ccontr)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   554
    fix i assume i:"i<DIM('a)" def e \<equiv> "norm (f' (basis i) - f'' (basis i))"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   555
    assume "f' (basis i) \<noteq> f'' (basis i)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   556
    hence "e>0" unfolding e_def by auto
44125
230a8665c919 mark some redundant theorems as legacy
huffman
parents: 44124
diff changeset
   557
    guess d using tendsto_diff [OF as(1,2)[THEN conjunct2], unfolded * Lim_within,rule_format,OF `e>0`] .. note d=this
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   558
    guess c using assms(3)[rule_format,OF i d[THEN conjunct1]] .. note c=this
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   559
    have *:"norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R basis i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R basis i)) = norm ((1 / abs c) *\<^sub>R (- (f' (c *\<^sub>R basis i)) + f'' (c *\<^sub>R basis i)))"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   560
      unfolding scaleR_right_distrib by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   561
    also have "\<dots> = norm ((1 / abs c) *\<^sub>R (c *\<^sub>R (- (f' (basis i)) + f'' (basis i))))"  
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   562
      unfolding f'.scaleR f''.scaleR
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   563
      unfolding scaleR_right_distrib scaleR_minus_right by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   564
    also have "\<dots> = e" unfolding e_def using c[THEN conjunct1]
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   565
      using norm_minus_cancel[of "f' (basis i) - f'' (basis i)"]
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   566
      by (auto simp add: add.commute ab_diff_minus)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   567
    finally show False using c
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   568
      using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R basis i"]
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   569
      unfolding dist_norm
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   570
      unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   571
        scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   572
      using i by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   573
  qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   574
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   575
37730
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   576
lemma frechet_derivative_unique_at:
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   577
  shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
37730
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   578
  unfolding FDERIV_conv_has_derivative [symmetric]
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   579
  by (rule FDERIV_unique)
41829
455cbcbba8c2 add name continuous_isCont to unnamed lemma
hoelzl
parents: 40702
diff changeset
   580
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   581
lemma continuous_isCont: "isCont f x = continuous (at x) f"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   582
  unfolding isCont_def LIM_def
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   583
  unfolding continuous_at Lim_at unfolding dist_nz by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   584
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   585
lemma frechet_derivative_unique_within_closed_interval:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   586
  fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   587
  assumes "\<forall>i<DIM('a). a$$i < b$$i" "x \<in> {a..b}" (is "x\<in>?I")
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   588
  assumes "(f has_derivative f' ) (at x within {a..b})"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   589
  assumes "(f has_derivative f'') (at x within {a..b})"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   590
  shows "f' = f''"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   591
  apply(rule frechet_derivative_unique_within)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   592
  apply(rule assms(3,4))+
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   593
proof(rule,rule,rule,rule)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   594
  fix e::real and i assume "e>0" and i:"i<DIM('a)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   595
  thus "\<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R basis i \<in> {a..b}"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   596
  proof(cases "x$$i=a$$i")
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   597
    case True thus ?thesis
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   598
      apply(rule_tac x="(min (b$$i - a$$i)  e) / 2" in exI)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   599
      using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2)
44457
d366fa5551ef declare euclidean_simps [simp] at the point they are proved;
huffman
parents: 44282
diff changeset
   600
      unfolding mem_interval euclidean_simps
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   601
      using i by (auto simp add: field_simps)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   602
  next note * = assms(2)[unfolded mem_interval,THEN spec[where x=i]]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   603
    case False moreover have "a $$ i < x $$ i" using False * by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   604
    moreover {
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   605
      have "a $$ i * 2 + min (x $$ i - a $$ i) e \<le> a$$i *2 + x$$i - a$$i"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   606
        by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   607
      also have "\<dots> = a$$i + x$$i" by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   608
      also have "\<dots> \<le> 2 * x$$i" using * by auto 
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   609
      finally have "a $$ i * 2 + min (x $$ i - a $$ i) e \<le> x $$ i * 2" by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   610
    }
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   611
    moreover have "min (x $$ i - a $$ i) e \<ge> 0" using * and `e>0` by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   612
    hence "x $$ i * 2 \<le> b $$ i * 2 + min (x $$ i - a $$ i) e" using * by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   613
    ultimately show ?thesis
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   614
      apply(rule_tac x="- (min (x$$i - a$$i) e) / 2" in exI)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   615
      using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2)
44457
d366fa5551ef declare euclidean_simps [simp] at the point they are proved;
huffman
parents: 44282
diff changeset
   616
      unfolding mem_interval euclidean_simps
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   617
      using i by (auto simp add: field_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   618
  qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   619
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   620
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   621
lemma frechet_derivative_unique_within_open_interval:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   622
  fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   623
  assumes "x \<in> {a<..<b}"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   624
  assumes "(f has_derivative f' ) (at x within {a<..<b})"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   625
  assumes "(f has_derivative f'') (at x within {a<..<b})"
37650
181a70d7b525 generalize some lemmas about derivatives
huffman
parents: 37648
diff changeset
   626
  shows "f' = f''"
181a70d7b525 generalize some lemmas about derivatives
huffman
parents: 37648
diff changeset
   627
proof -
181a70d7b525 generalize some lemmas about derivatives
huffman
parents: 37648
diff changeset
   628
  from assms(1) have *: "at x within {a<..<b} = at x"
181a70d7b525 generalize some lemmas about derivatives
huffman
parents: 37648
diff changeset
   629
    by (simp add: at_within_interior interior_open open_interval)
181a70d7b525 generalize some lemmas about derivatives
huffman
parents: 37648
diff changeset
   630
  from assms(2,3) [unfolded *] show "f' = f''"
181a70d7b525 generalize some lemmas about derivatives
huffman
parents: 37648
diff changeset
   631
    by (rule frechet_derivative_unique_at)
181a70d7b525 generalize some lemmas about derivatives
huffman
parents: 37648
diff changeset
   632
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   633
37730
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   634
lemma frechet_derivative_at:
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   635
  shows "(f has_derivative f') (at x) \<Longrightarrow> (f' = frechet_derivative f (at x))"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   636
  apply(rule frechet_derivative_unique_at[of f],assumption)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   637
  unfolding frechet_derivative_works[THEN sym] using differentiable_def by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   638
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   639
lemma frechet_derivative_within_closed_interval:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   640
  fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   641
  assumes "\<forall>i<DIM('a). a$$i < b$$i" and "x \<in> {a..b}"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   642
  assumes "(f has_derivative f') (at x within {a.. b})"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   643
  shows "frechet_derivative f (at x within {a.. b}) = f'"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   644
  apply(rule frechet_derivative_unique_within_closed_interval[where f=f]) 
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   645
  apply(rule assms(1,2))+ unfolding frechet_derivative_works[THEN sym]
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   646
  unfolding differentiable_def using assms(3) by auto 
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   647
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   648
subsection {* The traditional Rolle theorem in one dimension. *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   649
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   650
lemma linear_componentwise:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   651
  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   652
  assumes lf: "linear f"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   653
  shows "(f x) $$ j = (\<Sum>i<DIM('a). (x$$i) * (f (basis i)$$j))" (is "?lhs = ?rhs")
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   654
proof -
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   655
  have fA: "finite {..<DIM('a)}" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   656
  have "?rhs = (\<Sum>i<DIM('a). x$$i *\<^sub>R f (basis i))$$j"
44457
d366fa5551ef declare euclidean_simps [simp] at the point they are proved;
huffman
parents: 44282
diff changeset
   657
    by simp
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   658
  then show ?thesis
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   659
    unfolding linear_setsum_mul[OF lf fA, symmetric]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   660
    unfolding euclidean_representation[symmetric] ..
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   661
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   662
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   663
text {* We do not introduce @{text jacobian}, which is defined on matrices, instead we use
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   664
  the unfolding of it. *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   665
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   666
lemma jacobian_works:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   667
  "(f::('a::euclidean_space) \<Rightarrow> ('b::euclidean_space)) differentiable net \<longleftrightarrow>
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   668
   (f has_derivative (\<lambda>h. \<chi>\<chi> i.
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   669
      \<Sum>j<DIM('a). frechet_derivative f net (basis j) $$ i * h $$ j)) net"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   670
  (is "?differentiable \<longleftrightarrow> (f has_derivative (\<lambda>h. \<chi>\<chi> i. ?SUM h i)) net")
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   671
proof
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   672
  assume *: ?differentiable
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   673
  { fix h i
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   674
    have "?SUM h i = frechet_derivative f net h $$ i" using *
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   675
      by (auto intro!: setsum_cong
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   676
               simp: linear_componentwise[of _ h i] linear_frechet_derivative) }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   677
  thus "(f has_derivative (\<lambda>h. \<chi>\<chi> i. ?SUM h i)) net"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   678
    using * by (simp add: frechet_derivative_works)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   679
qed (auto intro!: differentiableI)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   680
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   681
lemma differential_zero_maxmin_component:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   682
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   683
  assumes k: "k < DIM('b)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   684
    and ball: "0 < e" "((\<forall>y \<in> ball x e. (f y)$$k \<le> (f x)$$k) \<or> (\<forall>y\<in>ball x e. (f x)$$k \<le> (f y)$$k))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   685
    and diff: "f differentiable (at x)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   686
  shows "(\<chi>\<chi> j. frechet_derivative f (at x) (basis j) $$ k) = (0::'a)" (is "?D k = 0")
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   687
proof (rule ccontr)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   688
  assume "?D k \<noteq> 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   689
  then obtain j where j: "?D k $$ j \<noteq> 0" "j < DIM('a)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   690
    unfolding euclidean_lambda_beta euclidean_eq[of _ "0::'a"] by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   691
  hence *: "\<bar>?D k $$ j\<bar> / 2 > 0" by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   692
  note as = diff[unfolded jacobian_works has_derivative_at_alt]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   693
  guess e' using as[THEN conjunct2, rule_format, OF *] .. note e' = this
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   694
  guess d using real_lbound_gt_zero[OF ball(1) e'[THEN conjunct1]] .. note d = this
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   695
  { fix c assume "abs c \<le> d"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   696
    hence *:"norm (x + c *\<^sub>R basis j - x) < e'" using norm_basis[of j] d by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   697
    let ?v = "(\<chi>\<chi> i. \<Sum>l<DIM('a). ?D i $$ l * (c *\<^sub>R basis j :: 'a) $$ l)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   698
    have if_dist: "\<And> P a b c. a * (if P then b else c) = (if P then a * b else a * c)" by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   699
    have "\<bar>(f (x + c *\<^sub>R basis j) - f x - ?v) $$ k\<bar> \<le>
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   700
        norm (f (x + c *\<^sub>R basis j) - f x - ?v)" by (rule component_le_norm)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   701
    also have "\<dots> \<le> \<bar>?D k $$ j\<bar> / 2 * \<bar>c\<bar>"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44647
diff changeset
   702
      using e'[THEN conjunct2, rule_format, OF *] and norm_basis[of j] by fastforce
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   703
    finally have "\<bar>(f (x + c *\<^sub>R basis j) - f x - ?v) $$ k\<bar> \<le> \<bar>?D k $$ j\<bar> / 2 * \<bar>c\<bar>" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   704
    hence "\<bar>f (x + c *\<^sub>R basis j) $$ k - f x $$ k - c * ?D k $$ j\<bar> \<le> \<bar>?D k $$ j\<bar> / 2 * \<bar>c\<bar>"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   705
      unfolding euclidean_simps euclidean_lambda_beta using j k
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   706
      by (simp add: if_dist setsum_cases field_simps) } note * = this
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   707
  have "x + d *\<^sub>R basis j \<in> ball x e" "x - d *\<^sub>R basis j \<in> ball x e"
36587
534418d8d494 remove redundant lemma vector_dist_norm
huffman
parents: 36581
diff changeset
   708
    unfolding mem_ball dist_norm using norm_basis[of j] d by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   709
  hence **:"((f (x - d *\<^sub>R basis j))$$k \<le> (f x)$$k \<and> (f (x + d *\<^sub>R basis j))$$k \<le> (f x)$$k) \<or>
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   710
         ((f (x - d *\<^sub>R basis j))$$k \<ge> (f x)$$k \<and> (f (x + d *\<^sub>R basis j))$$k \<ge> (f x)$$k)" using ball by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   711
  have ***: "\<And>y y1 y2 d dx::real.
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   712
    (y1\<le>y\<and>y2\<le>y) \<or> (y\<le>y1\<and>y\<le>y2) \<Longrightarrow> d < abs dx \<Longrightarrow> abs(y1 - y - - dx) \<le> d \<Longrightarrow> (abs (y2 - y - dx) \<le> d) \<Longrightarrow> False" by arith
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   713
  show False apply(rule ***[OF **, where dx="d * ?D k $$ j" and d="\<bar>?D k $$ j\<bar> / 2 * \<bar>d\<bar>"])
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   714
    using *[of "-d"] and *[of d] and d[THEN conjunct1] and j
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   715
    unfolding mult_minus_left
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   716
    unfolding abs_mult diff_minus_eq_add scaleR_minus_left
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   717
    unfolding algebra_simps by (auto intro: mult_pos_pos)
34906
bb9dad7de515 spurious proof failure
haftmann
parents: 34291
diff changeset
   718
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   719
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
   720
text {* In particular if we have a mapping into @{typ "real"}. *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   721
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   722
lemma differential_zero_maxmin:
37650
181a70d7b525 generalize some lemmas about derivatives
huffman
parents: 37648
diff changeset
   723
  fixes f::"'a\<Colon>euclidean_space \<Rightarrow> real"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   724
  assumes "x \<in> s" "open s"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   725
  and deriv: "(f has_derivative f') (at x)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   726
  and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   727
  shows "f' = (\<lambda>v. 0)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   728
proof -
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   729
  obtain e where e:"e>0" "ball x e \<subseteq> s"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   730
    using `open s`[unfolded open_contains_ball] and `x \<in> s` by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   731
  with differential_zero_maxmin_component[where 'b=real, of 0 e x f, simplified]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   732
  have "(\<chi>\<chi> j. frechet_derivative f (at x) (basis j)) = (0::'a)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   733
    unfolding differentiable_def using mono deriv by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   734
  with frechet_derivative_at[OF deriv, symmetric]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   735
  have "\<forall>i<DIM('a). f' (basis i) = 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   736
    by (simp add: euclidean_eq[of _ "0::'a"])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   737
  with derivative_is_linear[OF deriv, THEN linear_componentwise, of _ 0]
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   738
  show ?thesis by (simp add: fun_eq_iff)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   739
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   740
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   741
lemma rolle: fixes f::"real\<Rightarrow>real"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   742
  assumes "a < b" and "f a = f b" and "continuous_on {a..b} f"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   743
  assumes "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   744
  shows "\<exists>x\<in>{a<..<b}. f' x = (\<lambda>v. 0)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   745
proof-
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   746
  have "\<exists>x\<in>{a<..<b}. ((\<forall>y\<in>{a<..<b}. f x \<le> f y) \<or> (\<forall>y\<in>{a<..<b}. f y \<le> f x))"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   747
  proof-
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   748
    have "(a + b) / 2 \<in> {a .. b}" using assms(1) by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   749
    hence *:"{a .. b}\<noteq>{}" by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   750
    guess d using continuous_attains_sup[OF compact_interval * assms(3)] .. note d=this
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   751
    guess c using continuous_attains_inf[OF compact_interval * assms(3)] .. note c=this
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   752
    show ?thesis
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   753
    proof(cases "d\<in>{a<..<b} \<or> c\<in>{a<..<b}")
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   754
      case True thus ?thesis
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   755
        apply(erule_tac disjE) apply(rule_tac x=d in bexI)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   756
        apply(rule_tac[3] x=c in bexI)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   757
        using d c by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   758
    next
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   759
      def e \<equiv> "(a + b) /2"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   760
      case False hence "f d = f c" using d c assms(2) by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   761
      hence "\<And>x. x\<in>{a..b} \<Longrightarrow> f x = f d"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   762
        using c d apply- apply(erule_tac x=x in ballE)+ by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   763
      thus ?thesis
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   764
        apply(rule_tac x=e in bexI) unfolding e_def using assms(1) by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   765
    qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   766
  qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   767
  then guess x .. note x=this
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   768
  hence "f' x = (\<lambda>v. 0)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   769
    apply(rule_tac differential_zero_maxmin[of x "{a<..<b}" f "f' x"])
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   770
    defer apply(rule open_interval)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   771
    apply(rule assms(4)[unfolded has_derivative_at[THEN sym],THEN bspec[where x=x]],assumption)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   772
    unfolding o_def apply(erule disjE,rule disjI2) by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   773
  thus ?thesis apply(rule_tac x=x in bexI) unfolding o_def apply rule
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   774
    apply(drule_tac x=v in fun_cong) using x(1) by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   775
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   776
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   777
subsection {* One-dimensional mean value theorem. *}
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   778
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   779
lemma mvt: fixes f::"real \<Rightarrow> real"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   780
  assumes "a < b" and "continuous_on {a .. b} f"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   781
  assumes "\<forall>x\<in>{a<..<b}. (f has_derivative (f' x)) (at x)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   782
  shows "\<exists>x\<in>{a<..<b}. (f b - f a = (f' x) (b - a))"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   783
proof-
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   784
  have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   785
    apply(rule rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"])
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   786
    defer
44531
1d477a2b1572 replace some continuous_on lemmas with more general versions
huffman
parents: 44457
diff changeset
   787
    apply(rule continuous_on_intros assms(2))+
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   788
  proof
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   789
    fix x assume x:"x \<in> {a<..<b}"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   790
    show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   791
      by (intro has_derivative_intros assms(3)[rule_format,OF x]
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
   792
        mult_right_has_derivative)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   793
  qed(insert assms(1), auto simp add:field_simps)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   794
  then guess x ..
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   795
  thus ?thesis apply(rule_tac x=x in bexI)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   796
    apply(drule fun_cong[of _ _ "b - a"]) by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   797
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   798
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   799
lemma mvt_simple:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   800
  fixes f::"real \<Rightarrow> real"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   801
  assumes "a<b" and "\<forall>x\<in>{a..b}. (f has_derivative f' x) (at x within {a..b})"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   802
  shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   803
  apply(rule mvt)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   804
  apply(rule assms(1), rule differentiable_imp_continuous_on)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   805
  unfolding differentiable_on_def differentiable_def defer
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   806
proof
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   807
  fix x assume x:"x \<in> {a<..<b}" show "(f has_derivative f' x) (at x)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   808
    unfolding has_derivative_within_open[OF x open_interval,THEN sym] 
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   809
    apply(rule has_derivative_within_subset)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   810
    apply(rule assms(2)[rule_format])
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   811
    using x by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   812
qed(insert assms(2), auto)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   813
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   814
lemma mvt_very_simple:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   815
  fixes f::"real \<Rightarrow> real"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   816
  assumes "a \<le> b" and "\<forall>x\<in>{a..b}. (f has_derivative f'(x)) (at x within {a..b})"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   817
  shows "\<exists>x\<in>{a..b}. f b - f a = f' x (b - a)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   818
proof (cases "a = b")
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   819
  interpret bounded_linear "f' b" using assms(2) assms(1) by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   820
  case True thus ?thesis apply(rule_tac x=a in bexI)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   821
    using assms(2)[THEN bspec[where x=a]] unfolding has_derivative_def
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   822
    unfolding True using zero by auto next
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   823
  case False thus ?thesis using mvt_simple[OF _ assms(2)] using assms(1) by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   824
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   825
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
   826
text {* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   827
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   828
lemma mvt_general:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   829
  fixes f::"real\<Rightarrow>'a::euclidean_space"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   830
  assumes "a<b" and "continuous_on {a..b} f"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   831
  assumes "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   832
  shows "\<exists>x\<in>{a<..<b}. norm(f b - f a) \<le> norm(f'(x) (b - a))"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   833
proof-
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   834
  have "\<exists>x\<in>{a<..<b}. (op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   835
    apply(rule mvt) apply(rule assms(1))
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   836
    apply(rule continuous_on_inner continuous_on_intros assms(2))+
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
   837
    unfolding o_def apply(rule,rule has_derivative_intros)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   838
    using assms(3) by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   839
  then guess x .. note x=this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   840
  show ?thesis proof(cases "f a = f b")
36844
5f9385ecc1a7 Removed usage of normalizating locales.
hoelzl
parents: 36725
diff changeset
   841
    case False
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   842
    have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   843
      by (simp add: power2_eq_square)
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35290
diff changeset
   844
    also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   845
    also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   846
      using x unfolding inner_simps by (auto simp add: inner_diff_left)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   847
    also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   848
      by (rule norm_cauchy_schwarz)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   849
    finally show ?thesis using False x(1)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   850
      by (auto simp add: real_mult_left_cancel)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   851
  next
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   852
    case True thus ?thesis using assms(1)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   853
      apply (rule_tac x="(a + b) /2" in bexI) by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   854
  qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   855
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   856
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
   857
text {* Still more general bound theorem. *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   858
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   859
lemma differentiable_bound:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   860
  fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   861
  assumes "convex s" and "\<forall>x\<in>s. (f has_derivative f'(x)) (at x within s)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   862
  assumes "\<forall>x\<in>s. onorm(f' x) \<le> B" and x:"x\<in>s" and y:"y\<in>s"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   863
  shows "norm(f x - f y) \<le> B * norm(x - y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   864
proof-
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   865
  let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   866
  have *:"\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   867
    using assms(1)[unfolded convex_alt,rule_format,OF x y]
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   868
    unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   869
    by (auto simp add: algebra_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   870
  hence 1:"continuous_on {0..1} (f \<circ> ?p)" apply-
44531
1d477a2b1572 replace some continuous_on lemmas with more general versions
huffman
parents: 44457
diff changeset
   871
    apply(rule continuous_on_intros)+
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   872
    unfolding continuous_on_eq_continuous_within
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   873
    apply(rule,rule differentiable_imp_continuous_within)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   874
    unfolding differentiable_def apply(rule_tac x="f' xa" in exI)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   875
    apply(rule has_derivative_within_subset)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   876
    apply(rule assms(2)[rule_format]) by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   877
  have 2:"\<forall>u\<in>{0<..<1}. ((f \<circ> ?p) has_derivative f' (x + u *\<^sub>R (y - x)) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   878
  proof rule
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   879
    case goal1
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   880
    let ?u = "x + u *\<^sub>R (y - x)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   881
    have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within {0<..<1})" 
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   882
      apply(rule diff_chain_within) apply(rule has_derivative_intros)+ 
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   883
      apply(rule has_derivative_within_subset)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   884
      apply(rule assms(2)[rule_format]) using goal1 * by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   885
    thus ?case
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   886
      unfolding has_derivative_within_open[OF goal1 open_interval] by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   887
  qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   888
  guess u using mvt_general[OF zero_less_one 1 2] .. note u = this
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   889
  have **:"\<And>x y. x\<in>s \<Longrightarrow> norm (f' x y) \<le> B * norm y"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   890
  proof-
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   891
    case goal1
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   892
    have "norm (f' x y) \<le> onorm (f' x) * norm y"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   893
      using onorm(1)[OF derivative_is_linear[OF assms(2)[rule_format,OF goal1]]] by assumption
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   894
    also have "\<dots> \<le> B * norm y"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   895
      apply(rule mult_right_mono)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   896
      using assms(3)[rule_format,OF goal1]
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   897
      by(auto simp add:field_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   898
    finally show ?case by simp
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   899
  qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   900
  have "norm (f x - f y) = norm ((f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 1 - (f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 0)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   901
    by(auto simp add:norm_minus_commute) 
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   902
  also have "\<dots> \<le> norm (f' (x + u *\<^sub>R (y - x)) (y - x))" using u by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   903
  also have "\<dots> \<le> B * norm(y - x)" apply(rule **) using * and u by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   904
  finally show ?thesis by(auto simp add:norm_minus_commute)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   905
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   906
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   907
lemma differentiable_bound_real:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   908
  fixes f::"real \<Rightarrow> real"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   909
  assumes "convex s" and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   910
  assumes "\<forall>x\<in>s. onorm(f' x) \<le> B" and x:"x\<in>s" and y:"y\<in>s"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   911
  shows "norm(f x - f y) \<le> B * norm(x - y)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   912
  using differentiable_bound[of s f f' B x y]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   913
  unfolding Ball_def image_iff o_def using assms by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   914
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
   915
text {* In particular. *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   916
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   917
lemma has_derivative_zero_constant:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   918
  fixes f::"real\<Rightarrow>real"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   919
  assumes "convex s" "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   920
  shows "\<exists>c. \<forall>x\<in>s. f x = c"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   921
proof(cases "s={}")
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   922
  case False then obtain x where "x\<in>s" by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   923
  have "\<And>y. y\<in>s \<Longrightarrow> f x = f y" proof- case goal1
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   924
    thus ?case
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   925
      using differentiable_bound_real[OF assms(1-2), of 0 x y] and `x\<in>s`
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   926
      unfolding onorm_const by auto qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   927
  thus ?thesis apply(rule_tac x="f x" in exI) by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   928
qed auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   929
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   930
lemma has_derivative_zero_unique: fixes f::"real\<Rightarrow>real"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   931
  assumes "convex s" and "a \<in> s" and "f a = c"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   932
  assumes "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)" and "x\<in>s"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   933
  shows "f x = c"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   934
  using has_derivative_zero_constant[OF assms(1,4)] using assms(2-3,5) by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   935
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   936
subsection {* Differentiability of inverse function (most basic form). *}
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   937
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   938
lemma has_derivative_inverse_basic:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   939
  fixes f::"'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   940
  assumes "(f has_derivative f') (at (g y))"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   941
  assumes "bounded_linear g'" and "g' \<circ> f' = id" and "continuous (at y) g"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   942
  assumes "open t" and "y \<in> t" and "\<forall>z\<in>t. f(g z) = z"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   943
  shows "(g has_derivative g') (at y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   944
proof-
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   945
  interpret f': bounded_linear f'
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   946
    using assms unfolding has_derivative_def by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   947
  interpret g': bounded_linear g' using assms by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   948
  guess C using bounded_linear.pos_bounded[OF assms(2)] .. note C = this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   949
(*  have fgid:"\<And>x. g' (f' x) = x" using assms(3) unfolding o_def id_def apply()*)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   950
  have lem1:"\<forall>e>0. \<exists>d>0. \<forall>z. norm(z - y) < d \<longrightarrow> norm(g z - g y - g'(z - y)) \<le> e * norm(g z - g y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   951
  proof(rule,rule)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   952
    case goal1
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   953
    have *:"e / C > 0" apply(rule divide_pos_pos) using `e>0` C by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   954
    guess d0 using assms(1)[unfolded has_derivative_at_alt,THEN conjunct2,rule_format,OF *] .. note d0=this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   955
    guess d1 using assms(4)[unfolded continuous_at Lim_at,rule_format,OF d0[THEN conjunct1]] .. note d1=this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   956
    guess d2 using assms(5)[unfolded open_dist,rule_format,OF assms(6)] .. note d2=this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   957
    guess d using real_lbound_gt_zero[OF d1[THEN conjunct1] d2[THEN conjunct1]] .. note d=this
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   958
    thus ?case apply(rule_tac x=d in exI) apply rule defer
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   959
    proof(rule,rule)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   960
      fix z assume as:"norm (z - y) < d" hence "z\<in>t"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   961
        using d2 d unfolding dist_norm by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   962
      have "norm (g z - g y - g' (z - y)) \<le> norm (g' (f (g z) - y - f' (g z - g y)))"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   963
        unfolding g'.diff f'.diff
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   964
        unfolding assms(3)[unfolded o_def id_def, THEN fun_cong] 
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   965
        unfolding assms(7)[rule_format,OF `z\<in>t`]
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   966
        apply(subst norm_minus_cancel[THEN sym]) by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   967
      also have "\<dots> \<le> norm(f (g z) - y - f' (g z - g y)) * C"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   968
        by (rule C [THEN conjunct2, rule_format])
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   969
      also have "\<dots> \<le> (e / C) * norm (g z - g y) * C"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   970
        apply(rule mult_right_mono)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   971
        apply(rule d0[THEN conjunct2,rule_format,unfolded assms(7)[rule_format,OF `y\<in>t`]])
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   972
        apply(cases "z=y") defer
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   973
        apply(rule d1[THEN conjunct2, unfolded dist_norm,rule_format])
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   974
        using as d C d0 by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   975
      also have "\<dots> \<le> e * norm (g z - g y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   976
        using C by (auto simp add: field_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   977
      finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   978
        by simp
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   979
    qed auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   980
  qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   981
  have *:"(0::real) < 1 / 2" by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   982
  guess d using lem1[rule_format,OF *] .. note d=this
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   983
  def B\<equiv>"C*2"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   984
  have "B>0" unfolding B_def using C by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   985
  have lem2:"\<forall>z. norm(z - y) < d \<longrightarrow> norm(g z - g y) \<le> B * norm(z - y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   986
  proof(rule,rule) case goal1
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   987
    have "norm (g z - g y) \<le> norm(g' (z - y)) + norm ((g z - g y) - g'(z - y))"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   988
      by(rule norm_triangle_sub)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   989
    also have "\<dots> \<le> norm(g' (z - y)) + 1 / 2 * norm (g z - g y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   990
      apply(rule add_left_mono) using d and goal1 by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   991
    also have "\<dots> \<le> norm (z - y) * C + 1 / 2 * norm (g z - g y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   992
      apply(rule add_right_mono) using C by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   993
    finally show ?case unfolding B_def by(auto simp add:field_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   994
  qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   995
  show ?thesis unfolding has_derivative_at_alt
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   996
  proof(rule,rule assms,rule,rule) case goal1
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   997
    hence *:"e/B >0" apply-apply(rule divide_pos_pos) using `B>0` by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   998
    guess d' using lem1[rule_format,OF *] .. note d'=this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   999
    guess k using real_lbound_gt_zero[OF d[THEN conjunct1] d'[THEN conjunct1]] .. note k=this
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1000
    show ?case
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1001
      apply(rule_tac x=k in exI,rule) defer
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1002
    proof(rule,rule)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1003
      fix z assume as:"norm(z - y) < k"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1004
      hence "norm (g z - g y - g' (z - y)) \<le> e / B * norm(g z - g y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1005
        using d' k by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1006
      also have "\<dots> \<le> e * norm(z - y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1007
        unfolding times_divide_eq_left pos_divide_le_eq[OF `B>0`]
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1008
        using lem2[THEN spec[where x=z]] using k as using `e>0`
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1009
        by (auto simp add: field_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1010
      finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (z - y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1011
        by simp qed(insert k, auto)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1012
  qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1013
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1014
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
  1015
text {* Simply rewrite that based on the domain point x. *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1016
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1017
lemma has_derivative_inverse_basic_x:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1018
  fixes f::"'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1019
  assumes "(f has_derivative f') (at x)" "bounded_linear g'" "g' o f' = id"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1020
  "continuous (at (f x)) g" "g(f x) = x" "open t" "f x \<in> t" "\<forall>y\<in>t. f(g y) = y"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1021
  shows "(g has_derivative g') (at (f(x)))"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1022
  apply(rule has_derivative_inverse_basic) using assms by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1023
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
  1024
text {* This is the version in Dieudonne', assuming continuity of f and g. *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1025
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1026
lemma has_derivative_inverse_dieudonne:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1027
  fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1028
  assumes "open s" "open (f ` s)" "continuous_on s f" "continuous_on (f ` s) g" "\<forall>x\<in>s. g(f x) = x"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1029
  (**) "x\<in>s" "(f has_derivative f') (at x)"  "bounded_linear g'" "g' o f' = id"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1030
  shows "(g has_derivative g') (at (f x))"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1031
  apply(rule has_derivative_inverse_basic_x[OF assms(7-9) _ _ assms(2)])
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1032
  using assms(3-6) unfolding continuous_on_eq_continuous_at[OF assms(1)]
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1033
    continuous_on_eq_continuous_at[OF assms(2)] by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1034
44124
4c2a61a897d8 Derivative.thy: more sensible subsection headings
huffman
parents: 44123
diff changeset
  1035
text {* Here's the simplest way of not assuming much about g. *}
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1036
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1037
lemma has_derivative_inverse:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1038
  fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1039
  assumes "compact s" "x \<in> s" "f x \<in> interior(f ` s)" "continuous_on s f"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1040
  "\<forall>y\<in>s. g(f y) = y" "(f has_derivative f') (at x)" "bounded_linear g'" "g' \<circ> f' = id"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1041
  shows "(g has_derivative g') (at (f x))"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1042
proof-
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1043
  { fix y assume "y\<in>interior (f ` s)" 
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1044
    then obtain x where "x\<in>s" and *:"y = f x"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1045
      unfolding image_iff using interior_subset by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1046
    have "f (g y) = y" unfolding * and assms(5)[rule_format,OF `x\<in>s`] ..
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1047
  } note * = this
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1048
  show ?thesis
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1049
    apply(rule has_derivative_inverse_basic_x[OF assms(6-8)])
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1050
    apply(rule continuous_on_interior[OF _ assms(3)])
44647
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44568
diff changeset
  1051
    apply(rule continuous_on_inv[OF assms(4,1)])
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1052
    apply(rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1053
    by(rule, rule *, assumption)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1054
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1055
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1056
subsection {* Proving surjectivity via Brouwer fixpoint theorem. *}
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1057
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1058
lemma brouwer_surjective:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1059
  fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'n"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1060
  assumes "compact t" "convex t"  "t \<noteq> {}" "continuous_on t f"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1061
  "\<forall>x\<in>s. \<forall>y\<in>t. x + (y - f y) \<in> t" "x\<in>s"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1062
  shows "\<exists>y\<in>t. f y = x"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1063
proof-
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1064
  have *:"\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1065
    by(auto simp add:algebra_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1066
  show ?thesis
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1067
    unfolding *
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1068
    apply(rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1069
    apply(rule continuous_on_intros assms)+ using assms(4-6) by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1070
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1071
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1072
lemma brouwer_surjective_cball:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1073
  fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'n"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1074
  assumes "0 < e" "continuous_on (cball a e) f"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1075
  "\<forall>x\<in>s. \<forall>y\<in>cball a e. x + (y - f y) \<in> cball a e" "x\<in>s"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1076
  shows "\<exists>y\<in>cball a e. f y = x"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1077
  apply(rule brouwer_surjective)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1078
  apply(rule compact_cball convex_cball)+
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1079
  unfolding cball_eq_empty using assms by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1080
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1081
text {* See Sussmann: "Multidifferential calculus", Theorem 2.1.1 *}
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1082
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1083
lemma sussmann_open_mapping:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1084
  fixes f::"'a::euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1085
  assumes "open s" "continuous_on s f" "x \<in> s" 
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1086
  "(f has_derivative f') (at x)" "bounded_linear g'" "f' \<circ> g' = id"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
  1087
  "t \<subseteq> s" "x \<in> interior t"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1088
  shows "f x \<in> interior (f ` t)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1089
proof- 
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1090
  interpret f':bounded_linear f'
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1091
    using assms unfolding has_derivative_def by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1092
  interpret g':bounded_linear g' using assms by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1093
  guess B using bounded_linear.pos_bounded[OF assms(5)] .. note B=this
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1094
  hence *:"1/(2*B)>0" by (auto intro!: divide_pos_pos)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1095
  guess e0 using assms(4)[unfolded has_derivative_at_alt,THEN conjunct2,rule_format,OF *] .. note e0=this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1096
  guess e1 using assms(8)[unfolded mem_interior_cball] .. note e1=this
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1097
  have *:"0<e0/B" "0<e1/B"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1098
    apply(rule_tac[!] divide_pos_pos) using e0 e1 B by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1099
  guess e using real_lbound_gt_zero[OF *] .. note e=this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1100
  have "\<forall>z\<in>cball (f x) (e/2). \<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1101
    apply(rule,rule brouwer_surjective_cball[where s="cball (f x) (e/2)"])
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1102
    prefer 3 apply(rule,rule)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1103
  proof-
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1104
    show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1105
      unfolding g'.diff
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1106
      apply(rule continuous_on_compose[of _ _ f, unfolded o_def])
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1107
      apply(rule continuous_on_intros linear_continuous_on[OF assms(5)])+
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1108
      apply(rule continuous_on_subset[OF assms(2)])
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1109
      apply(rule,unfold image_iff,erule bexE)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1110
    proof-
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1111
      fix y z assume as:"y \<in>cball (f x) e"  "z = x + (g' y - g' (f x))"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1112
      have "dist x z = norm (g' (f x) - g' y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1113
        unfolding as(2) and dist_norm by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1114
      also have "\<dots> \<le> norm (f x - y) * B"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1115
        unfolding g'.diff[THEN sym] using B by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1116
      also have "\<dots> \<le> e * B"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1117
        using as(1)[unfolded mem_cball dist_norm] using B by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1118
      also have "\<dots> \<le> e1" using e unfolding less_divide_eq using B by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1119
      finally have "z\<in>cball x e1" unfolding mem_cball by force
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1120
      thus "z \<in> s" using e1 assms(7) by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1121
    qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1122
  next
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1123
    fix y z assume as:"y \<in> cball (f x) (e / 2)" "z \<in> cball (f x) e"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1124
    have "norm (g' (z - f x)) \<le> norm (z - f x) * B" using B by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1125
    also have "\<dots> \<le> e * B" apply(rule mult_right_mono)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1126
      using as(2)[unfolded mem_cball dist_norm] and B
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1127
      unfolding norm_minus_commute by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1128
    also have "\<dots> < e0" using e and B unfolding less_divide_eq by auto
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1129
    finally have *:"norm (x + g' (z - f x) - x) < e0" by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1130
    have **:"f x + f' (x + g' (z - f x) - x) = z"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1131
      using assms(6)[unfolded o_def id_def,THEN cong] by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1132
    have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le> norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1133
      using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1134
      by (auto simp add: algebra_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1135
    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1136
      using e0[THEN conjunct2,rule_format,OF *]
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1137
      unfolding algebra_simps ** by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1138
    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1139
      using as(1)[unfolded mem_cball dist_norm] by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1140
    also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1141
      using * and B by (auto simp add: field_simps)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1142
    also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2" by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1143
    also have "\<dots> \<le> e/2 + e/2" apply(rule add_right_mono)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1144
      using as(2)[unfolded mem_cball dist_norm]
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1145
      unfolding norm_minus_commute by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1146
    finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1147
      unfolding mem_cball dist_norm by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1148
  qed(insert e, auto) note lem = this
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1149
  show ?thesis unfolding mem_interior apply(rule_tac x="e/2" in exI)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1150
    apply(rule,rule divide_pos_pos) prefer 3
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1151
  proof
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1152
    fix y assume "y \<in> ball (f x) (e/2)"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1153
    hence *:"y\<in>cball (f x) (e/2)" by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1154
    guess z using lem[rule_format,OF *] .. note z=this
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1155
    hence "norm (g' (z - f x)) \<le> norm (z - f x) * B"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1156
      using B by (auto simp add: field_simps)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1157
    also have "\<dots> \<le> e * B"
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1158
      apply (rule mult_right_mono) using z(1)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1159
      unfolding mem_cball dist_norm norm_minus_commute using B by auto
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1160
    also have "\<dots> \<le> e1"  using e B unfolding less_divide_eq by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1161
    finally have "x + g'(z - f x) \<in> t" apply-
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1162
      apply(rule e1[THEN conjunct2,unfolded subset_eq,rule_format])
36587
534418d8d494 remove redundant lemma vector_dist_norm
huffman
parents: 36581
diff changeset
  1163
      unfolding mem_cball dist_norm by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1164
    thus "y \<in> f ` t" using z by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1165
  qed(insert e, auto)
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1166
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1167
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1168
text {* Hence the following eccentric variant of the inverse function theorem.    *)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1169
(* This has no continuity assumptions, but we do need the inverse function.  *)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1170
(* We could put f' o g = I but this happens to fit with the minimal linear   *)
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1171
(* algebra theory I've set up so far. *}
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1172
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
  1173
(* move  before left_inverse_linear in Euclidean_Space*)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
  1174
44123