src/HOL/Analysis/Derivative.thy
author paulson <lp15@cam.ac.uk>
Sun, 20 May 2018 22:10:21 +0100
changeset 68241 39a311f50344
parent 68239 0764ee22a4d1
child 68527 2f4e2aab190a
permissions -rw-r--r--
correcting the statements of the MVTs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63627
6ddb43c6b711 rename HOL-Multivariate_Analysis to HOL-Analysis.
hoelzl
parents: 63469
diff changeset
     1
(*  Title:      HOL/Analysis/Derivative.thy
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
     2
    Author:     John Harrison
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
     3
    Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light); tidied by LCP
36350
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
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
     6
section \<open>Multivariate calculus in Euclidean space\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from 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
62207
45eee631ea4f added lemma
immler
parents: 62101
diff changeset
     9
imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from 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
63938
f6ce08859d4c More mainly topological results
paulson <lp15@cam.ac.uk>
parents: 63918
diff changeset
    12
declare bounded_linear_inner_left [intro]
61915
e9812a95d108 theory for type of bounded linear functions; differentiation under the integral sign
immler
parents: 61907
diff changeset
    13
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
    14
declare has_derivative_bounded_linear[dest]
44137
ac5cb4c86448 simplify some proofs
huffman
parents: 44125
diff changeset
    15
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
    16
subsection \<open>Derivatives\<close>
51642
400ec5ae7f8f move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents: 51641
diff changeset
    17
400ec5ae7f8f move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents: 51641
diff changeset
    18
lemma has_derivative_add_const:
400ec5ae7f8f move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents: 51641
diff changeset
    19
  "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
    20
  by (intro derivative_eq_intros) auto
51642
400ec5ae7f8f move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents: 51641
diff changeset
    21
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    22
67968
a5ad4c015d1c removed dots at the end of (sub)titles
nipkow
parents: 67685
diff changeset
    23
subsection \<open>Derivative with composed bilinear function\<close>
51642
400ec5ae7f8f move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents: 51641
diff changeset
    24
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
    25
text \<open>More explicit epsilon-delta forms.\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    26
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    27
lemma has_derivative_within':
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    28
  "(f has_derivative f')(at x within s) \<longleftrightarrow>
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    29
    bounded_linear f' \<and>
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    30
    (\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    31
      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
    32
  unfolding has_derivative_within Lim_within dist_norm
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    33
  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
    34
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    35
lemma has_derivative_at':
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
    36
  "(f has_derivative f') (at x) 
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
    37
   \<longleftrightarrow> bounded_linear f' \<and>
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
    38
       (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
    39
        norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
    40
  using has_derivative_within' [of f f' x UNIV] by simp
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    41
67979
53323937ee25 new material about vec, real^1, etc.
paulson <lp15@cam.ac.uk>
parents: 67968
diff changeset
    42
lemma has_derivative_at_withinI:
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    43
  "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    44
  unfolding has_derivative_within' has_derivative_at'
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    45
  by blast
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    46
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    47
lemma has_derivative_within_open:
68095
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
    48
  "a \<in> S \<Longrightarrow> open S \<Longrightarrow>
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
    49
    (f has_derivative f') (at a within S) \<longleftrightarrow> (f has_derivative f') (at a)"
37730
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
    50
  by (simp only: at_within_interior interior_open)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    51
43338
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    52
lemma has_derivative_right:
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    53
  fixes f :: "real \<Rightarrow> real"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    54
    and y :: "real"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66394
diff changeset
    55
  shows "(f has_derivative (( * ) y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
    56
         ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
43338
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    57
proof -
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
    58
  have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
    59
    ((\<lambda>t. (f t - f x) / (t - x) - y) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I))"
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
    60
    by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib)
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
    61
  also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) \<longlongrightarrow> y) (at x within ({x<..} \<inter> I))"
43338
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    62
    by (simp add: Lim_null[symmetric])
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
    63
  also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x<..} \<inter> I))"
44140
2c10c35dd4be remove several redundant and unused theorems about derivatives
huffman
parents: 44137
diff changeset
    64
    by (intro Lim_cong_within) (simp_all add: field_simps)
43338
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    65
  finally show ?thesis
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44140
diff changeset
    66
    by (simp add: bounded_linear_mult_right has_derivative_within)
43338
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    67
qed
a150d16bf77c lemmas about right derivative and limits
hoelzl
parents: 41970
diff changeset
    68
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
    69
subsubsection \<open>Caratheodory characterization\<close>
55970
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    70
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    71
lemma DERIV_caratheodory_within:
68095
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
    72
  "(f has_field_derivative l) (at x within S) \<longleftrightarrow>
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
    73
   (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within S) g \<and> g x = l)"
55970
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    74
      (is "?lhs = ?rhs")
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    75
proof
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 56151
diff changeset
    76
  assume ?lhs
55970
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    77
  show ?rhs
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    78
  proof (intro exI conjI)
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    79
    let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    80
    show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
68095
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
    81
    show "continuous (at x within S) ?g" using \<open>?lhs\<close>
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
    82
      by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within)
55970
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    83
    show "?g x = l" by simp
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    84
  qed
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    85
next
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    86
  assume ?rhs
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    87
  then obtain g where
68095
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
    88
    "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within S) g" and "g x = l" by blast
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 56151
diff changeset
    89
  thus ?lhs
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
    90
    by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within)
55970
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    91
qed
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
    92
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
    93
subsection \<open>Differentiability\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    94
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    95
definition
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    96
  differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool"
56182
528fae0816ea update syntax of has_*derivative to infix 50; fixed proofs
hoelzl
parents: 56181
diff changeset
    97
    (infix "differentiable'_on" 50)
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
    98
  where "f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable (at x within s))"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
    99
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   100
lemma differentiableI: "(f has_derivative f') net \<Longrightarrow> f differentiable net"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   101
  unfolding differentiable_def
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   102
  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
   103
62533
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   104
lemma differentiable_onD: "\<lbrakk>f differentiable_on S; x \<in> S\<rbrakk> \<Longrightarrow> f differentiable (at x within S)"
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   105
  using differentiable_on_def by blast
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   106
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   107
lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   108
  unfolding differentiable_def
67979
53323937ee25 new material about vec, real^1, etc.
paulson <lp15@cam.ac.uk>
parents: 67968
diff changeset
   109
  using has_derivative_at_withinI
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   110
  by blast
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   111
61104
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   112
lemma differentiable_at_imp_differentiable_on:
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   113
  "(\<And>x. x \<in> s \<Longrightarrow> f differentiable at x) \<Longrightarrow> f differentiable_on s"
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   114
  by (metis differentiable_at_withinI differentiable_on_def)
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   115
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   116
corollary differentiable_iff_scaleR:
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   117
  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   118
  shows "f differentiable F \<longleftrightarrow> (\<exists>d. (f has_derivative (\<lambda>x. x *\<^sub>R d)) F)"
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   119
  by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR)
3c2d4636cebc new lemmas about vector_derivative, complex numbers, paths, etc.
paulson
parents: 61076
diff changeset
   120
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   121
lemma differentiable_on_eq_differentiable_at:
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   122
  "open s \<Longrightarrow> f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   123
  unfolding differentiable_on_def
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51478
diff changeset
   124
  by (metis at_within_interior interior_open)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   125
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   126
lemma differentiable_transform_within:
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61975
diff changeset
   127
  assumes "f differentiable (at x within s)"
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61975
diff changeset
   128
    and "0 < d"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   129
    and "x \<in> s"
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61975
diff changeset
   130
    and "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   131
  shows "g differentiable (at x within s)"
62087
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61975
diff changeset
   132
   using assms has_derivative_transform_within unfolding differentiable_def
44841d07ef1d revisions to limits and derivatives, plus new lemmas
paulson
parents: 61975
diff changeset
   133
   by blast
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   134
63469
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   135
lemma differentiable_on_ident [simp, derivative_intros]: "(\<lambda>x. x) differentiable_on S"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   136
  by (simp add: differentiable_at_imp_differentiable_on)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   137
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   138
lemma differentiable_on_id [simp, derivative_intros]: "id differentiable_on S"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   139
  by (simp add: id_def)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   140
63955
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63952
diff changeset
   141
lemma differentiable_on_const [simp, derivative_intros]: "(\<lambda>z. c) differentiable_on S"
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63952
diff changeset
   142
  by (simp add: differentiable_on_def)
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63952
diff changeset
   143
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63952
diff changeset
   144
lemma differentiable_on_mult [simp, derivative_intros]:
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63952
diff changeset
   145
  fixes f :: "'M::real_normed_vector \<Rightarrow> 'a::real_normed_algebra"
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63952
diff changeset
   146
  shows "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) differentiable_on S"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   147
  unfolding differentiable_on_def differentiable_def
63955
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63952
diff changeset
   148
  using differentiable_def differentiable_mult by blast
51a3d38d2281 more new material
paulson <lp15@cam.ac.uk>
parents: 63952
diff changeset
   149
63469
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   150
lemma differentiable_on_compose:
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   151
   "\<lbrakk>g differentiable_on S; f differentiable_on (g ` S)\<rbrakk> \<Longrightarrow> (\<lambda>x. f (g x)) differentiable_on S"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   152
by (simp add: differentiable_in_compose differentiable_on_def)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   153
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   154
lemma bounded_linear_imp_differentiable_on: "bounded_linear f \<Longrightarrow> f differentiable_on S"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   155
  by (simp add: differentiable_on_def bounded_linear_imp_differentiable)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   156
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   157
lemma linear_imp_differentiable_on:
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   158
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   159
  shows "linear f \<Longrightarrow> f differentiable_on S"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   160
by (simp add: differentiable_on_def linear_imp_differentiable)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   161
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   162
lemma differentiable_on_minus [simp, derivative_intros]:
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   163
   "f differentiable_on S \<Longrightarrow> (\<lambda>z. -(f z)) differentiable_on S"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   164
by (simp add: differentiable_on_def)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   165
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   166
lemma differentiable_on_add [simp, derivative_intros]:
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   167
   "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z + g z) differentiable_on S"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   168
by (simp add: differentiable_on_def)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   169
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   170
lemma differentiable_on_diff [simp, derivative_intros]:
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   171
   "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z - g z) differentiable_on S"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   172
by (simp add: differentiable_on_def)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   173
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   174
lemma differentiable_on_inverse [simp, derivative_intros]:
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   175
  fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   176
  shows "f differentiable_on S \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> f x \<noteq> 0) \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable_on S"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   177
by (simp add: differentiable_on_def)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   178
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   179
lemma differentiable_on_scaleR [derivative_intros, simp]:
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   180
   "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) differentiable_on S"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   181
  unfolding differentiable_on_def
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   182
  by (blast intro: differentiable_scaleR)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   183
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   184
lemma has_derivative_sqnorm_at [derivative_intros, simp]:
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   185
  "((\<lambda>x. (norm x)\<^sup>2) has_derivative (\<lambda>x. 2 *\<^sub>R (a \<bullet> x))) (at a)"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   186
  using bounded_bilinear.FDERIV  [of "(\<bullet>)" id id a _ id id]
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   187
  by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner)
63469
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   188
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   189
lemma differentiable_sqnorm_at [derivative_intros, simp]:
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   190
  fixes a :: "'a :: {real_normed_vector,real_inner}"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   191
  shows "(\<lambda>x. (norm x)\<^sup>2) differentiable (at a)"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   192
by (force simp add: differentiable_def intro: has_derivative_sqnorm_at)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   193
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   194
lemma differentiable_on_sqnorm [derivative_intros, simp]:
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   195
  fixes S :: "'a :: {real_normed_vector,real_inner} set"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   196
  shows "(\<lambda>x. (norm x)\<^sup>2) differentiable_on S"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   197
by (simp add: differentiable_at_imp_differentiable_on)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   198
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   199
lemma differentiable_norm_at [derivative_intros, simp]:
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   200
  fixes a :: "'a :: {real_normed_vector,real_inner}"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   201
  shows "a \<noteq> 0 \<Longrightarrow> norm differentiable (at a)"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   202
using differentiableI has_derivative_norm by blast
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   203
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   204
lemma differentiable_on_norm [derivative_intros, simp]:
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   205
  fixes S :: "'a :: {real_normed_vector,real_inner} set"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   206
  shows "0 \<notin> S \<Longrightarrow> norm differentiable_on S"
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   207
by (metis differentiable_at_imp_differentiable_on differentiable_norm_at)
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
   208
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   209
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   210
subsection \<open>Frechet derivative and Jacobian matrix\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   211
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   212
definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)"
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   213
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   214
lemma frechet_derivative_works:
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   215
  "f differentiable net \<longleftrightarrow> (f has_derivative (frechet_derivative f net)) net"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   216
  unfolding frechet_derivative_def differentiable_def
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   217
  unfolding some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] ..
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   218
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 56151
diff changeset
   219
lemma linear_frechet_derivative: "f differentiable net \<Longrightarrow> linear (frechet_derivative f net)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   220
  unfolding frechet_derivative_works has_derivative_def
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
   221
  by (auto intro: bounded_linear.linear)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   222
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   223
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   224
subsection \<open>Differentiability implies continuity\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   225
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   226
lemma differentiable_imp_continuous_within:
51642
400ec5ae7f8f move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents: 51641
diff changeset
   227
  "f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 56151
diff changeset
   228
  by (auto simp: differentiable_def intro: has_derivative_continuous)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   229
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   230
lemma differentiable_imp_continuous_on:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   231
  "f differentiable_on s \<Longrightarrow> continuous_on s f"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   232
  unfolding differentiable_on_def continuous_on_eq_continuous_within
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   233
  using differentiable_imp_continuous_within by blast
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   234
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   235
lemma differentiable_on_subset:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   236
  "f differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable_on s"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   237
  unfolding differentiable_on_def
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   238
  using differentiable_within_subset
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   239
  by blast
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   240
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   241
lemma differentiable_on_empty: "f differentiable_on {}"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   242
  unfolding differentiable_on_def
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   243
  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
   244
67685
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
   245
lemma has_derivative_continuous_on:
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
   246
  "(\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x within s)) \<Longrightarrow> continuous_on s f"
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
   247
  by (auto intro!: differentiable_imp_continuous_on differentiableI simp: differentiable_on_def)
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
   248
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   249
text \<open>Results about neighborhoods filter.\<close>
56151
41f9d22a9fa4 add lemmas about nhds filter; tuned proof
huffman
parents: 56150
diff changeset
   250
41f9d22a9fa4 add lemmas about nhds filter; tuned proof
huffman
parents: 56150
diff changeset
   251
lemma eventually_nhds_metric_le:
41f9d22a9fa4 add lemmas about nhds filter; tuned proof
huffman
parents: 56150
diff changeset
   252
  "eventually P (nhds a) = (\<exists>d>0. \<forall>x. dist x a \<le> d \<longrightarrow> P x)"
41f9d22a9fa4 add lemmas about nhds filter; tuned proof
huffman
parents: 56150
diff changeset
   253
  unfolding eventually_nhds_metric by (safe, rule_tac x="d / 2" in exI, auto)
41f9d22a9fa4 add lemmas about nhds filter; tuned proof
huffman
parents: 56150
diff changeset
   254
41f9d22a9fa4 add lemmas about nhds filter; tuned proof
huffman
parents: 56150
diff changeset
   255
lemma le_nhds: "F \<le> nhds a \<longleftrightarrow> (\<forall>S. open S \<and> a \<in> S \<longrightarrow> eventually (\<lambda>x. x \<in> S) F)"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61808
diff changeset
   256
  unfolding le_filter_def eventually_nhds by (fast elim: eventually_mono)
56151
41f9d22a9fa4 add lemmas about nhds filter; tuned proof
huffman
parents: 56150
diff changeset
   257
41f9d22a9fa4 add lemmas about nhds filter; tuned proof
huffman
parents: 56150
diff changeset
   258
lemma le_nhds_metric: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a < e) F)"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61808
diff changeset
   259
  unfolding le_filter_def eventually_nhds_metric by (fast elim: eventually_mono)
56151
41f9d22a9fa4 add lemmas about nhds filter; tuned proof
huffman
parents: 56150
diff changeset
   260
41f9d22a9fa4 add lemmas about nhds filter; tuned proof
huffman
parents: 56150
diff changeset
   261
lemma le_nhds_metric_le: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a \<le> e) F)"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61808
diff changeset
   262
  unfolding le_filter_def eventually_nhds_metric_le by (fast elim: eventually_mono)
56151
41f9d22a9fa4 add lemmas about nhds filter; tuned proof
huffman
parents: 56150
diff changeset
   263
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   264
text \<open>Several results are easier using a "multiplied-out" variant.
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   265
(I got this idea from Dieudonne's proof of the chain rule).\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   266
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   267
lemma has_derivative_within_alt:
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   268
  "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   269
    (\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm(y - x) < d \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> e * norm (y - x))"
56151
41f9d22a9fa4 add lemmas about nhds filter; tuned proof
huffman
parents: 56150
diff changeset
   270
  unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59558
diff changeset
   271
    eventually_at dist_norm diff_diff_eq
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
   272
  by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   273
56320
e84c12d4a886 tuned proofs
huffman
parents: 56271
diff changeset
   274
lemma has_derivative_within_alt2:
e84c12d4a886 tuned proofs
huffman
parents: 56271
diff changeset
   275
  "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
e84c12d4a886 tuned proofs
huffman
parents: 56271
diff changeset
   276
    (\<forall>e>0. eventually (\<lambda>y. norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)) (at x within s))"
e84c12d4a886 tuned proofs
huffman
parents: 56271
diff changeset
   277
  unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
59815
cce82e360c2f explicit commutative additive inverse operation;
haftmann
parents: 59558
diff changeset
   278
    eventually_at dist_norm diff_diff_eq
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
   279
  by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
56320
e84c12d4a886 tuned proofs
huffman
parents: 56271
diff changeset
   280
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   281
lemma has_derivative_at_alt:
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   282
  "(f has_derivative f') (at x) \<longleftrightarrow>
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   283
    bounded_linear f' \<and>
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   284
    (\<forall>e>0. \<exists>d>0. \<forall>y. norm(y - x) < d \<longrightarrow> norm (f y - f x - f'(y - x)) \<le> e * norm (y - x))"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   285
  using has_derivative_within_alt[where s=UNIV]
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   286
  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
   287
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   288
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   289
subsection \<open>The chain rule\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   290
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   291
lemma diff_chain_within[derivative_intros]:
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   292
  assumes "(f has_derivative f') (at x within s)"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   293
    and "(g has_derivative g') (at (f x) within (f ` s))"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   294
  shows "((g \<circ> f) has_derivative (g' \<circ> f'))(at x within s)"
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 56151
diff changeset
   295
  using has_derivative_in_compose[OF assms]
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   296
  by (simp add: comp_def)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   297
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   298
lemma diff_chain_at[derivative_intros]:
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   299
  "(f has_derivative f') (at x) \<Longrightarrow>
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   300
    (g has_derivative g') (at (f x)) \<Longrightarrow> ((g \<circ> f) has_derivative (g' \<circ> f')) (at x)"
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 56151
diff changeset
   301
  using has_derivative_compose[of f f' x UNIV g g']
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   302
  by (simp add: comp_def)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   303
68095
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   304
lemma has_vector_derivative_within_open:
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   305
  "a \<in> S \<Longrightarrow> open S \<Longrightarrow>
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   306
    (f has_vector_derivative f') (at a within S) \<longleftrightarrow> (f has_vector_derivative f') (at a)"
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   307
  by (simp only: at_within_interior interior_open)
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   308
64394
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64287
diff changeset
   309
lemma field_vector_diff_chain_within:
68095
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   310
 assumes Df: "(f has_vector_derivative f') (at x within S)"
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   311
     and Dg: "(g has_field_derivative g') (at (f x) within f ` S)"
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   312
 shows "((g \<circ> f) has_vector_derivative (f' * g')) (at x within S)"
64394
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64287
diff changeset
   313
using diff_chain_within[OF Df[unfolded has_vector_derivative_def]
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64287
diff changeset
   314
                       Dg [unfolded has_field_derivative_def]]
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64287
diff changeset
   315
 by (auto simp: o_def mult.commute has_vector_derivative_def)
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64287
diff changeset
   316
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64287
diff changeset
   317
lemma vector_derivative_diff_chain_within:
68095
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   318
  assumes Df: "(f has_vector_derivative f') (at x within S)"
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   319
     and Dg: "(g has_derivative g') (at (f x) within f`S)"
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   320
  shows "((g \<circ> f) has_vector_derivative (g' f')) (at x within S)"
64394
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64287
diff changeset
   321
using diff_chain_within[OF Df[unfolded has_vector_derivative_def] Dg]
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64287
diff changeset
   322
  linear.scaleR[OF has_derivative_linear[OF Dg]]
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64287
diff changeset
   323
  unfolding has_vector_derivative_def o_def
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64287
diff changeset
   324
  by (auto simp: o_def mult.commute has_vector_derivative_def)
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64287
diff changeset
   325
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   326
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   327
subsection \<open>Composition rules stated just for differentiability\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   328
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   329
lemma differentiable_chain_at:
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   330
  "f differentiable (at x) \<Longrightarrow>
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   331
    g differentiable (at (f x)) \<Longrightarrow> (g \<circ> f) differentiable (at x)"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   332
  unfolding differentiable_def
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   333
  by (meson diff_chain_at)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   334
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   335
lemma differentiable_chain_within:
68095
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   336
  "f differentiable (at x within S) \<Longrightarrow>
4fa3e63ecc7e starting to tidy up Interval_Integral.thy
paulson <lp15@cam.ac.uk>
parents: 68073
diff changeset
   337
    g differentiable (at(f x) within (f ` S)) \<Longrightarrow> (g \<circ> f) differentiable (at x within S)"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   338
  unfolding differentiable_def
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   339
  by (meson diff_chain_within)
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   340
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   341
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   342
subsection \<open>Uniqueness of derivative\<close>
37730
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   343
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
   344
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   345
text \<open>
37730
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   346
 The general result is a bit messy because we need approachability of the
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   347
 limit point from any direction. But OK for nontrivial intervals etc.
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   348
\<close>
51363
d4d00c804645 changed has_derivative_intros into a named theorems collection
hoelzl
parents: 50939
diff changeset
   349
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   350
lemma frechet_derivative_unique_within:
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   351
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   352
  assumes 1: "(f has_derivative f') (at x within S)"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   353
    and 2: "(f has_derivative f'') (at x within S)"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   354
    and S: "\<And>i e. \<lbrakk>i\<in>Basis; e>0\<rbrakk> \<Longrightarrow> \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> S"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   355
  shows "f' = f''"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   356
proof -
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   357
  note as = assms(1,2)[unfolded has_derivative_def]
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   358
  then interpret f': bounded_linear f' by auto
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   359
  from as interpret f'': bounded_linear f'' by auto
68058
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   360
  have "x islimpt S" unfolding islimpt_approachable
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   361
  proof (intro allI impI)
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   362
    fix e :: real
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   363
    assume "e > 0"
68058
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   364
    obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> S"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   365
      using assms(3) SOME_Basis \<open>e>0\<close> by blast
68058
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   366
    then show "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   367
      by (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI) (auto simp: dist_norm SOME_Basis nonzero_Basis)  qed
68058
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   368
  then have *: "netlimit (at x within S) = x"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   369
    by (simp add: Lim_ident_at trivial_limit_within)
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   370
  show ?thesis
68058
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   371
  proof (rule linear_eq_stdbasis)
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   372
    show "linear f'" "linear f''"
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   373
      unfolding linear_conv_bounded_linear using as by auto
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   374
  next
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   375
    fix i :: 'a
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   376
    assume i: "i \<in> Basis"
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62949
diff changeset
   377
    define e where "e = norm (f' i - f'' i)"
68058
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   378
    show "f' i = f'' i"
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   379
    proof (rule ccontr)
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   380
      assume "f' i \<noteq> f'' i"
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   381
      then have "e > 0"
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   382
        unfolding e_def by auto
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   383
      obtain d where d:
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   384
        "0 < d"
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   385
        "(\<And>y. y\<in>S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow>
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   386
          dist ((f y - f x - f' (y - x)) /\<^sub>R norm (y - x) -
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   387
              (f y - f x - f'' (y - x)) /\<^sub>R norm (y - x)) (0 - 0) < e)"
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   388
        using tendsto_diff [OF as(1,2)[THEN conjunct2]]
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   389
        unfolding * Lim_within
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   390
        using \<open>e>0\<close> by blast
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   391
      obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> S"
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   392
        using assms(3) i d(1) by blast
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   393
      have *: "norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) =
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61915
diff changeset
   394
        norm ((1 / \<bar>c\<bar>) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))"
68058
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   395
        unfolding scaleR_right_distrib by auto
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   396
      also have "\<dots> = norm ((1 / \<bar>c\<bar>) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   397
        unfolding f'.scaleR f''.scaleR
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   398
        unfolding scaleR_right_distrib scaleR_minus_right
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   399
        by auto
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   400
      also have "\<dots> = e"
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   401
        unfolding e_def
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   402
        using c(1)
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   403
        using norm_minus_cancel[of "f' i - f'' i"]
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   404
        by auto
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   405
      finally show False
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   406
        using c
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   407
        using d(2)[of "x + c *\<^sub>R i"]
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   408
        unfolding dist_norm
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   409
        unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   410
          scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   411
        using i
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   412
        by (auto simp: inverse_eq_divide)
69715dfdc286 more general tidying up
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   413
    qed
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   414
  qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   415
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   416
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   417
lemma frechet_derivative_unique_within_closed_interval:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   418
  fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   419
  assumes ab: "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   420
    and x: "x \<in> cbox a b"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   421
    and "(f has_derivative f' ) (at x within cbox a b)"
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   422
    and "(f has_derivative f'') (at x within cbox a b)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   423
  shows "f' = f''"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   424
proof (rule frechet_derivative_unique_within)
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   425
  fix e :: real
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   426
  fix i :: 'a
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   427
  assume "e > 0" and i: "i \<in> Basis"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   428
  then show "\<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> cbox a b"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   429
  proof (cases "x\<bullet>i = a\<bullet>i")
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   430
    case True
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   431
    with ab[of i] \<open>e>0\<close> x i show ?thesis
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   432
      by (rule_tac x="(min (b\<bullet>i - a\<bullet>i) e) / 2" in exI)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   433
         (auto simp add: mem_box field_simps inner_simps inner_Basis)
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   434
  next
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   435
    case False
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   436
    moreover have "a \<bullet> i < x \<bullet> i"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   437
      using False i mem_box(2) x by force
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   438
    moreover {
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50418
diff changeset
   439
      have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> a\<bullet>i *2 + x\<bullet>i - a\<bullet>i"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   440
        by auto
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   441
      also have "\<dots> = a\<bullet>i + x\<bullet>i"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   442
        by auto
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   443
      also have "\<dots> \<le> 2 * (x\<bullet>i)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   444
        using \<open>a \<bullet> i < x \<bullet> i\<close> by auto
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   445
      finally have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> x \<bullet> i * 2"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   446
        by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   447
    }
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   448
    moreover have "min (x \<bullet> i - a \<bullet> i) e \<ge> 0"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   449
      by (simp add: \<open>0 < e\<close> \<open>a \<bullet> i < x \<bullet> i\<close> less_eq_real_def)
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   450
    then have "x \<bullet> i * 2 \<le> b \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   451
      using i mem_box(2) x by force
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   452
    ultimately show ?thesis
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   453
    using ab[of i] \<open>e>0\<close> x i 
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   454
      by (rule_tac x="- (min (x\<bullet>i - a\<bullet>i) e) / 2" in exI)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   455
         (auto simp add: mem_box field_simps inner_simps inner_Basis)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   456
  qed
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   457
qed (use assms in auto)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   458
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   459
lemma frechet_derivative_unique_within_open_interval:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   460
  fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   461
  assumes x: "x \<in> box a b"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   462
    and f: "(f has_derivative f' ) (at x within box a b)" "(f has_derivative f'') (at x within box a b)"
37650
181a70d7b525 generalize some lemmas about derivatives
huffman
parents: 37648
diff changeset
   463
  shows "f' = f''"
181a70d7b525 generalize some lemmas about derivatives
huffman
parents: 37648
diff changeset
   464
proof -
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   465
  have "at x within box a b = at x"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   466
    by (metis x at_within_interior interior_open open_box)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   467
  with f show "f' = f''"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   468
    by (simp add: has_derivative_unique)
37650
181a70d7b525 generalize some lemmas about derivatives
huffman
parents: 37648
diff changeset
   469
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   470
37730
1a24950dae33 generalize some lemmas about derivatives
huffman
parents: 37650
diff changeset
   471
lemma frechet_derivative_at:
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   472
  "(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   473
  using differentiable_def frechet_derivative_works has_derivative_unique by blast
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   474
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   475
lemma frechet_derivative_within_cbox:
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   476
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   477
  assumes "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   478
    and "x \<in> cbox a b"
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   479
    and "(f has_derivative f') (at x within cbox a b)"
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   480
  shows "frechet_derivative f (at x within cbox a b) = f'"
55970
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
   481
  using assms
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
   482
  by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   483
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   484
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   485
subsection \<open>The traditional Rolle theorem in one dimension\<close>
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   486
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   487
text \<open>Derivatives of local minima and maxima are zero.\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   488
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   489
lemma has_derivative_local_min:
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   490
  fixes f :: "'a::real_normed_vector \<Rightarrow> real"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   491
  assumes deriv: "(f has_derivative f') (at x)"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   492
  assumes min: "eventually (\<lambda>y. f x \<le> f y) (at x)"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   493
  shows "f' = (\<lambda>h. 0)"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   494
proof
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   495
  fix h :: 'a
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   496
  interpret f': bounded_linear f'
56182
528fae0816ea update syntax of has_*derivative to infix 50; fixed proofs
hoelzl
parents: 56181
diff changeset
   497
    using deriv by (rule has_derivative_bounded_linear)
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   498
  show "f' h = 0"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   499
  proof (cases "h = 0")
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   500
    case False
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   501
    from min obtain d where d1: "0 < d" and d2: "\<forall>y\<in>ball x d. f x \<le> f y"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   502
      unfolding eventually_at by (force simp: dist_commute)
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   503
    have "FDERIV (\<lambda>r. x + r *\<^sub>R h) 0 :> (\<lambda>r. r *\<^sub>R h)"
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   504
      by (intro derivative_eq_intros) auto
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   505
    then have "FDERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> (\<lambda>k. f' (k *\<^sub>R h))"
56182
528fae0816ea update syntax of has_*derivative to infix 50; fixed proofs
hoelzl
parents: 56181
diff changeset
   506
      by (rule has_derivative_compose, simp add: deriv)
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   507
    then have "DERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> f' h"
56182
528fae0816ea update syntax of has_*derivative to infix 50; fixed proofs
hoelzl
parents: 56181
diff changeset
   508
      unfolding has_field_derivative_def by (simp add: f'.scaleR mult_commute_abs)
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   509
    moreover have "0 < d / norm h" using d1 and \<open>h \<noteq> 0\<close> by simp
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   510
    moreover have "\<forall>y. \<bar>0 - y\<bar> < d / norm h \<longrightarrow> f (x + 0 *\<^sub>R h) \<le> f (x + y *\<^sub>R h)"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   511
      using \<open>h \<noteq> 0\<close> by (auto simp add: d2 dist_norm pos_less_divide_eq)
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   512
    ultimately show "f' h = 0"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   513
      by (rule DERIV_local_min)
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   514
  qed simp
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   515
qed
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   516
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   517
lemma has_derivative_local_max:
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   518
  fixes f :: "'a::real_normed_vector \<Rightarrow> real"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   519
  assumes "(f has_derivative f') (at x)"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   520
  assumes "eventually (\<lambda>y. f y \<le> f x) (at x)"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   521
  shows "f' = (\<lambda>h. 0)"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   522
  using has_derivative_local_min [of "\<lambda>x. - f x" "\<lambda>h. - f' h" "x"]
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   523
  using assms unfolding fun_eq_iff by simp
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   524
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   525
lemma differential_zero_maxmin:
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   526
  fixes f::"'a::real_normed_vector \<Rightarrow> real"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   527
  assumes "x \<in> S"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   528
    and "open S"
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   529
    and deriv: "(f has_derivative f') (at x)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   530
    and mono: "(\<forall>y\<in>S. f y \<le> f x) \<or> (\<forall>y\<in>S. f x \<le> f y)"
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   531
  shows "f' = (\<lambda>v. 0)"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   532
  using mono
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   533
proof
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   534
  assume "\<forall>y\<in>S. f y \<le> f x"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   535
  with \<open>x \<in> S\<close> and \<open>open S\<close> have "eventually (\<lambda>y. f y \<le> f x) (at x)"
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   536
    unfolding eventually_at_topological by auto
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   537
  with deriv show ?thesis
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   538
    by (rule has_derivative_local_max)
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   539
next
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   540
  assume "\<forall>y\<in>S. f x \<le> f y"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   541
  with \<open>x \<in> S\<close> and \<open>open S\<close> have "eventually (\<lambda>y. f x \<le> f y) (at x)"
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   542
    unfolding eventually_at_topological by auto
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   543
  with deriv show ?thesis
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   544
    by (rule has_derivative_local_min)
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   545
qed
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   546
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   547
lemma differential_zero_maxmin_component: (* TODO: delete? *)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   548
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50418
diff changeset
   549
  assumes k: "k \<in> Basis"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   550
    and ball: "0 < e" "(\<forall>y \<in> ball x e. (f y)\<bullet>k \<le> (f x)\<bullet>k) \<or> (\<forall>y\<in>ball x e. (f x)\<bullet>k \<le> (f y)\<bullet>k)"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   551
    and diff: "f differentiable (at x)"
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50418
diff changeset
   552
  shows "(\<Sum>j\<in>Basis. (frechet_derivative f (at x) j \<bullet> k) *\<^sub>R j) = (0::'a)" (is "?D k = 0")
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   553
proof -
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   554
  let ?f' = "frechet_derivative f (at x)"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   555
  have "x \<in> ball x e" using \<open>0 < e\<close> by simp
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   556
  moreover have "open (ball x e)" by simp
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   557
  moreover have "((\<lambda>x. f x \<bullet> k) has_derivative (\<lambda>h. ?f' h \<bullet> k)) (at x)"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   558
    using bounded_linear_inner_left diff[unfolded frechet_derivative_works]
56182
528fae0816ea update syntax of has_*derivative to infix 50; fixed proofs
hoelzl
parents: 56181
diff changeset
   559
    by (rule bounded_linear.has_derivative)
56133
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   560
  ultimately have "(\<lambda>h. frechet_derivative f (at x) h \<bullet> k) = (\<lambda>v. 0)"
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   561
    using ball(2) by (rule differential_zero_maxmin)
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   562
  then show ?thesis
304e37faf1ac generalization of differential_zero_maxmin to class real_normed_vector
huffman
parents: 56117
diff changeset
   563
    unfolding fun_eq_iff by simp
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36844
diff changeset
   564
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   565
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   566
theorem Rolle:
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   567
  fixes f :: "real \<Rightarrow> real"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   568
  assumes "a < b"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   569
    and fab: "f a = f b"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   570
    and contf: "continuous_on {a..b} f"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   571
    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   572
  shows "\<exists>x\<in>{a <..< b}. f' x = (\<lambda>v. 0)"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   573
proof -
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   574
  have "\<exists>x\<in>box a b. (\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   575
  proof -
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   576
    have "(a + b) / 2 \<in> {a..b}"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   577
      using assms(1) by auto
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   578
    then have *: "{a..b} \<noteq> {}"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   579
      by auto
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   580
    obtain d where d: "d \<in>cbox a b" "\<forall>y\<in>cbox a b. f y \<le> f d"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   581
      using continuous_attains_sup[OF compact_Icc * contf] by auto
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   582
    obtain c where c: "c \<in> cbox a b" "\<forall>y\<in>cbox a b. f c \<le> f y"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   583
      using continuous_attains_inf[OF compact_Icc * contf] by auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   584
    show ?thesis
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   585
    proof (cases "d \<in> box a b \<or> c \<in> box a b")
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   586
      case True
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   587
      then show ?thesis
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   588
        by (metis c(2) d(2) box_subset_cbox subset_iff)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   589
    next
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62949
diff changeset
   590
      define e where "e = (a + b) /2"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   591
      case False
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   592
      then have "f d = f c"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   593
        using d c fab by auto
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   594
      with c d have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
55970
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
   595
        by force
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   596
      then show ?thesis
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   597
        by (rule_tac x=e in bexI) (auto simp: e_def \<open>a < b\<close>)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   598
    qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   599
  qed
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   600
  then obtain x where x: "x \<in> {a <..< b}" "(\<forall>y\<in>{a <..< b}. f x \<le> f y) \<or> (\<forall>y\<in>{a <..< b}. f y \<le> f x)"
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   601
    by auto
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   602
  then have "f' x = (\<lambda>v. 0)"
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 54230
diff changeset
   603
    apply (rule_tac differential_zero_maxmin[of x "box a b" f "f' x"])
55970
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
   604
    using assms
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   605
    apply auto
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   606
    done
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   607
  then show ?thesis
55970
6d123f0ae358 Some new proofs. Tidying up, esp to remove "apply rule".
paulson <lp15@cam.ac.uk>
parents: 55665
diff changeset
   608
    by (metis x(1))
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   609
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   610
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   611
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   612
subsection \<open>One-dimensional mean value theorem\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   613
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   614
lemma mvt:
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   615
  fixes f :: "real \<Rightarrow> real"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   616
  assumes "a < b"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   617
    and contf: "continuous_on {a..b} f"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   618
    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   619
  shows "\<exists>x\<in>{a<..<b}. f b - f a = (f' x) (b - a)"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   620
proof -
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   621
  have "\<exists>x\<in>{a <..< b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   622
  proof (intro Rolle[OF \<open>a < b\<close>, of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   623
    fix x
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   624
    assume x: "a < x" "x < b"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   625
    show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   626
        (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   627
      by (intro derivative_intros derf[OF x])
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   628
  qed (use assms in \<open>auto intro!: continuous_intros simp: field_simps\<close>)
55665
4381a2b622ea tuned proofs;
wenzelm
parents: 54775
diff changeset
   629
  then obtain x where
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   630
    "x \<in> {a <..< b}"
55665
4381a2b622ea tuned proofs;
wenzelm
parents: 54775
diff changeset
   631
    "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   632
  then show ?thesis
61762
d50b993b4fb9 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents: 61649
diff changeset
   633
    by (metis (hide_lams) assms(1) diff_gt_0_iff_gt eq_iff_diff_eq_0
64240
eabf80376aab more standardized names
haftmann
parents: 64008
diff changeset
   634
      zero_less_mult_iff nonzero_mult_div_cancel_right not_real_square_gt_zero
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   635
      times_divide_eq_left)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   636
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   637
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   638
lemma mvt_simple:
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   639
  fixes f :: "real \<Rightarrow> real"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   640
  assumes "a < b"
68241
39a311f50344 correcting the statements of the MVTs
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   641
    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x within {a..b})"
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   642
  shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)"
56264
2a091015a896 tuned proofs
huffman
parents: 56261
diff changeset
   643
proof (rule mvt)
2a091015a896 tuned proofs
huffman
parents: 56261
diff changeset
   644
  have "f differentiable_on {a..b}"
68241
39a311f50344 correcting the statements of the MVTs
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   645
    using derf unfolding differentiable_on_def differentiable_def by force
56264
2a091015a896 tuned proofs
huffman
parents: 56261
diff changeset
   646
  then show "continuous_on {a..b} f"
2a091015a896 tuned proofs
huffman
parents: 56261
diff changeset
   647
    by (rule differentiable_imp_continuous_on)
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   648
  show "(f has_derivative f' x) (at x)" if "a < x" "x < b" for x
68241
39a311f50344 correcting the statements of the MVTs
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   649
    by (metis at_within_Icc_at derf leI order.asym that)
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   650
qed (rule assms)
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   651
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   652
lemma mvt_very_simple:
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   653
  fixes f :: "real \<Rightarrow> real"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   654
  assumes "a \<le> b"
68241
39a311f50344 correcting the statements of the MVTs
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   655
    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x within {a..b})"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   656
  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
   657
proof (cases "a = b")
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   658
  interpret bounded_linear "f' b"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   659
    using assms(2) assms(1) by auto
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   660
  case True
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   661
  then show ?thesis
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   662
    by force
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   663
next
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   664
  case False
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   665
  then show ?thesis
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   666
    using mvt_simple[OF _ derf]
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   667
    by (metis \<open>a \<le> b\<close> atLeastAtMost_iff dual_order.order_iff_strict greaterThanLessThan_iff)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   668
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   669
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   670
text \<open>A nice generalization (see Havin's proof of 5.19 from Rudin's book).\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   671
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   672
lemma mvt_general:
56223
7696903b9e61 generalize theory of operator norms to work with class real_normed_vector
huffman
parents: 56217
diff changeset
   673
  fixes f :: "real \<Rightarrow> 'a::real_inner"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   674
  assumes "a < b"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   675
    and contf: "continuous_on {a..b} f"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   676
    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   677
  shows "\<exists>x\<in>{a<..<b}. norm (f b - f a) \<le> norm (f' x (b - a))"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   678
proof -
56264
2a091015a896 tuned proofs
huffman
parents: 56261
diff changeset
   679
  have "\<exists>x\<in>{a<..<b}. (f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   680
    apply (rule mvt [OF \<open>a < b\<close>])
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   681
    apply (intro continuous_intros contf)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   682
    using derf apply (blast intro: has_derivative_inner_right)
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   683
    done
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   684
  then obtain x where x: "x \<in> {a<..<b}"
56264
2a091015a896 tuned proofs
huffman
parents: 56261
diff changeset
   685
    "(f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)" ..
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   686
  show ?thesis
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   687
  proof (cases "f a = f b")
36844
5f9385ecc1a7 Removed usage of normalizating locales.
hoelzl
parents: 36725
diff changeset
   688
    case False
53077
a1b3784f8129 more symbols;
wenzelm
parents: 51733
diff changeset
   689
    have "norm (f b - f a) * norm (f b - f a) = (norm (f b - f a))\<^sup>2"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   690
      by (simp add: power2_eq_square)
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   691
    also have "\<dots> = (f b - f a) \<bullet> (f b - f a)"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   692
      unfolding power2_norm_eq_inner ..
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   693
    also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)"
56264
2a091015a896 tuned proofs
huffman
parents: 56261
diff changeset
   694
      using x(2) by (simp only: inner_diff_right)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   695
    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
   696
      by (rule norm_cauchy_schwarz)
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   697
    finally show ?thesis
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   698
      using False x(1)
56217
dc429a5b13c4 Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents: 56196
diff changeset
   699
      by (auto simp add: mult_left_cancel)
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   700
  next
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   701
    case True
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   702
    then show ?thesis
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   703
      using \<open>a < b\<close> by (rule_tac x="(a + b) /2" in bexI) auto
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   704
  qed
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   705
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   706
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   707
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   708
subsection \<open>More general bound theorems\<close>
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   709
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   710
proposition differentiable_bound_general:
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   711
  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   712
  assumes "a < b"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   713
    and f_cont: "continuous_on {a..b} f"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   714
    and phi_cont: "continuous_on {a..b} \<phi>"
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   715
    and f': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   716
    and phi': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<phi> has_vector_derivative \<phi>' x) (at x)"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   717
    and bnd: "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> norm (f' x) \<le> \<phi>' x"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   718
  shows "norm (f b - f a) \<le> \<phi> b - \<phi> a"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   719
proof -
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   720
  {
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   721
    fix x assume x: "a < x" "x < b"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   722
    have "0 \<le> norm (f' x)" by simp
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   723
    also have "\<dots> \<le> \<phi>' x" using x by (auto intro!: bnd)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   724
    finally have "0 \<le> \<phi>' x" .
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   725
  } note phi'_nonneg = this
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   726
  note f_tendsto = assms(2)[simplified continuous_on_def, rule_format]
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   727
  note phi_tendsto = assms(3)[simplified continuous_on_def, rule_format]
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   728
  {
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   729
    fix e::real assume "e > 0"
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62949
diff changeset
   730
    define e2 where "e2 = e / 2"
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62949
diff changeset
   731
    with \<open>e > 0\<close> have "e2 > 0" by simp
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   732
    let ?le = "\<lambda>x1. norm (f x1 - f a) \<le> \<phi> x1 - \<phi> a + e * (x1 - a) + e"
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62949
diff changeset
   733
    define A where "A = {x2. a \<le> x2 \<and> x2 \<le> b \<and> (\<forall>x1\<in>{a ..< x2}. ?le x1)}"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   734
    have A_subset: "A \<subseteq> {a..b}" by (auto simp: A_def)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   735
    {
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   736
      fix x2
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   737
      assume a: "a \<le> x2" "x2 \<le> b" and le: "\<forall>x1\<in>{a..<x2}. ?le x1"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   738
      have "?le x2" using \<open>e > 0\<close>
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   739
      proof cases
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   740
        assume "x2 \<noteq> a" with a have "a < x2" by simp
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   741
        have "at x2 within {a <..<x2}\<noteq> bot"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   742
          using \<open>a < x2\<close>
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   743
          by (auto simp: trivial_limit_within islimpt_in_closure)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   744
        moreover
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   745
        have "((\<lambda>x1. (\<phi> x1 - \<phi> a) + e * (x1 - a) + e) \<longlongrightarrow> (\<phi> x2 - \<phi> a) + e * (x2 - a) + e) (at x2 within {a <..<x2})"
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   746
          "((\<lambda>x1. norm (f x1 - f a)) \<longlongrightarrow> norm (f x2 - f a)) (at x2 within {a <..<x2})"
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   747
          using a
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   748
          by (auto intro!: tendsto_eq_intros f_tendsto phi_tendsto
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   749
            intro: tendsto_within_subset[where S="{a..b}"])
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   750
        moreover
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   751
        have "eventually (\<lambda>x. x > a) (at x2 within {a <..<x2})"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   752
          by (auto simp: eventually_at_filter)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   753
        hence "eventually ?le (at x2 within {a <..<x2})"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   754
          unfolding eventually_at_filter
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   755
          by eventually_elim (insert le, auto)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   756
        ultimately
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   757
        show ?thesis
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   758
          by (rule tendsto_le)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   759
      qed simp
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   760
    } note le_cont = this
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   761
    have "a \<in> A"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   762
      using assms by (auto simp: A_def)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   763
    hence [simp]: "A \<noteq> {}" by auto
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   764
    have A_ivl: "\<And>x1 x2. x2 \<in> A \<Longrightarrow> x1 \<in> {a ..x2} \<Longrightarrow> x1 \<in> A"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   765
      by (simp add: A_def)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   766
    have [simp]: "bdd_above A" by (auto simp: A_def)
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62949
diff changeset
   767
    define y where "y = Sup A"
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   768
    have "y \<le> b"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   769
      unfolding y_def
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   770
      by (simp add: cSup_le_iff) (simp add: A_def)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   771
     have leI: "\<And>x x1. a \<le> x1 \<Longrightarrow> x \<in> A \<Longrightarrow> x1 < x \<Longrightarrow> ?le x1"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   772
       by (auto simp: A_def intro!: le_cont)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   773
    have y_all_le: "\<forall>x1\<in>{a..<y}. ?le x1"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   774
      by (auto simp: y_def less_cSup_iff leI)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   775
    have "a \<le> y"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   776
      by (metis \<open>a \<in> A\<close> \<open>bdd_above A\<close> cSup_upper y_def)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   777
    have "y \<in> A"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   778
      using y_all_le \<open>a \<le> y\<close> \<open>y \<le> b\<close>
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   779
      by (auto simp: A_def)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   780
    hence "A = {a .. y}"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   781
      using A_subset by (auto simp: subset_iff y_def cSup_upper intro: A_ivl)
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   782
    from le_cont[OF \<open>a \<le> y\<close> \<open>y \<le> b\<close> y_all_le] have le_y: "?le y" .
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   783
    have "y = b"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   784
    proof (cases "a = y")
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   785
      case True
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   786
      with \<open>a < b\<close> have "y < b" by simp
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   787
      with \<open>a = y\<close> f_cont phi_cont \<open>e2 > 0\<close>
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   788
      have 1: "\<forall>\<^sub>F x in at y within {y..b}. dist (f x) (f y) < e2"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   789
       and 2: "\<forall>\<^sub>F x in at y within {y..b}. dist (\<phi> x) (\<phi> y) < e2"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   790
        by (auto simp: continuous_on_def tendsto_iff)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   791
      have 3: "eventually (\<lambda>x. y < x) (at y within {y..b})"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   792
        by (auto simp: eventually_at_filter)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   793
      have 4: "eventually (\<lambda>x::real. x < b) (at y within {y..b})"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   794
        using _ \<open>y < b\<close>
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   795
        by (rule order_tendstoD) (auto intro!: tendsto_eq_intros)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   796
      from 1 2 3 4
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   797
      have eventually_le: "eventually (\<lambda>x. ?le x) (at y within {y .. b})"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   798
      proof eventually_elim
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   799
        case (elim x1)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   800
        have "norm (f x1 - f a) = norm (f x1 - f y)"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   801
          by (simp add: \<open>a = y\<close>)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   802
        also have "norm (f x1 - f y) \<le> e2"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   803
          using elim \<open>a = y\<close> by (auto simp : dist_norm intro!:  less_imp_le)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   804
        also have "\<dots> \<le> e2 + (\<phi> x1 - \<phi> a + e2 + e * (x1 - a))"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   805
          using \<open>0 < e\<close> elim
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   806
          by (intro add_increasing2[OF add_nonneg_nonneg order.refl])
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   807
            (auto simp: \<open>a = y\<close> dist_norm intro!: mult_nonneg_nonneg)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   808
        also have "\<dots> = \<phi> x1 - \<phi> a + e * (x1 - a) + e"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   809
          by (simp add: e2_def)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   810
        finally show "?le x1" .
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   811
      qed
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   812
      from this[unfolded eventually_at_topological] \<open>?le y\<close>
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   813
      obtain S where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   814
        by metis
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   815
      from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 62087
diff changeset
   816
        by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62949
diff changeset
   817
      define d' where "d' = min b (y + (d/2))"
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   818
      have "d' \<in> A"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   819
        unfolding A_def
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   820
      proof safe
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   821
        show "a \<le> d'" using \<open>a = y\<close> \<open>0 < d\<close> \<open>y < b\<close> by (simp add: d'_def)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   822
        show "d' \<le> b" by (simp add: d'_def)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   823
        fix x1
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   824
        assume "x1 \<in> {a..<d'}"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   825
        hence "x1 \<in> S" "x1 \<in> {y..b}"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   826
          by (auto simp: \<open>a = y\<close> d'_def dist_real_def intro!: d )
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   827
        thus "?le x1"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   828
          by (rule S)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   829
      qed
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   830
      hence "d' \<le> y"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   831
        unfolding y_def
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   832
        by (rule cSup_upper) simp
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   833
      then show "y = b" using \<open>d > 0\<close> \<open>y < b\<close>
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   834
        by (simp add: d'_def)
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   835
    next
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   836
      case False
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   837
      with \<open>a \<le> y\<close> have "a < y" by simp
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   838
      show "y = b"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   839
      proof (rule ccontr)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   840
        assume "y \<noteq> b"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   841
        hence "y < b" using \<open>y \<le> b\<close> by simp
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   842
        let ?F = "at y within {y..<b}"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   843
        from f' phi'
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   844
        have "(f has_vector_derivative f' y) ?F"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   845
          and "(\<phi> has_vector_derivative \<phi>' y) ?F"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   846
          using \<open>a < y\<close> \<open>y < b\<close>
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   847
          by (auto simp add: at_within_open[of _ "{a<..<b}"] has_vector_derivative_def
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   848
            intro!: has_derivative_subset[where s="{a<..<b}" and t="{y..<b}"])
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   849
        hence "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \<le> e2 * \<bar>x1 - y\<bar>"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   850
            "\<forall>\<^sub>F x1 in ?F. norm (\<phi> x1 - \<phi> y - (x1 - y) *\<^sub>R \<phi>' y) \<le> e2 * \<bar>x1 - y\<bar>"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   851
          using \<open>e2 > 0\<close>
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   852
          by (auto simp: has_derivative_within_alt2 has_vector_derivative_def)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   853
        moreover
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   854
        have "\<forall>\<^sub>F x1 in ?F. y \<le> x1" "\<forall>\<^sub>F x1 in ?F. x1 < b"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   855
          by (auto simp: eventually_at_filter)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   856
        ultimately
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   857
        have "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y) \<le> (\<phi> x1 - \<phi> y) + e * \<bar>x1 - y\<bar>"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   858
          (is "\<forall>\<^sub>F x1 in ?F. ?le' x1")
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   859
        proof eventually_elim
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   860
          case (elim x1)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   861
          from norm_triangle_ineq2[THEN order_trans, OF elim(1)]
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   862
          have "norm (f x1 - f y) \<le> norm (f' y) * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   863
            by (simp add: ac_simps)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   864
          also have "norm (f' y) \<le> \<phi>' y" using bnd \<open>a < y\<close> \<open>y < b\<close> by simp
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   865
          also have "\<phi>' y * \<bar>x1 - y\<bar> \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar>"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   866
            using elim by (simp add: ac_simps)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   867
          finally
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   868
          have "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   869
            by (auto simp: mult_right_mono)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   870
          thus ?case by (simp add: e2_def)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   871
        qed
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   872
        moreover have "?le' y" by simp
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   873
        ultimately obtain S
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   874
        where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..<b} \<Longrightarrow> ?le' x"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   875
          unfolding eventually_at_topological
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   876
          by metis
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   877
        from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   878
          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   879
        define d' where "d' = min ((y + b)/2) (y + (d/2))"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   880
        have "d' \<in> A"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   881
          unfolding A_def
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   882
        proof safe
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   883
          show "a \<le> d'" using \<open>a < y\<close> \<open>0 < d\<close> \<open>y < b\<close> by (simp add: d'_def)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   884
          show "d' \<le> b" using \<open>y < b\<close> by (simp add: d'_def min_def)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   885
          fix x1
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   886
          assume x1: "x1 \<in> {a..<d'}"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   887
          show "?le x1"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   888
          proof (cases "x1 < y")
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   889
            case True
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   890
            then show ?thesis
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   891
              using \<open>y \<in> A\<close> local.leI x1 by auto
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   892
          next
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   893
            case False
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   894
            hence x1': "x1 \<in> S" "x1 \<in> {y..<b}" using x1
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   895
              by (auto simp: d'_def dist_real_def intro!: d)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   896
            have "norm (f x1 - f a) \<le> norm (f x1 - f y) + norm (f y - f a)"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   897
              by (rule order_trans[OF _ norm_triangle_ineq]) simp
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   898
            also note S(3)[OF x1']
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   899
            also note le_y
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   900
            finally show "?le x1"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   901
              using False by (auto simp: algebra_simps)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   902
          qed
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   903
        qed
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   904
        hence "d' \<le> y"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   905
          unfolding y_def by (rule cSup_upper) simp
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   906
        thus False using \<open>d > 0\<close> \<open>y < b\<close>
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   907
          by (simp add: d'_def min_def split: if_split_asm)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   908
      qed
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   909
    qed
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   910
    with le_y have "norm (f b - f a) \<le> \<phi> b - \<phi> a + e * (b - a + 1)"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   911
      by (simp add: algebra_simps)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   912
  } note * = this
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   913
  show ?thesis
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   914
  proof (rule field_le_epsilon)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   915
    fix e::real assume "e > 0"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   916
    then show "norm (f b - f a) \<le> \<phi> b - \<phi> a + e"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   917
      using *[of "e / (b - a + 1)"] \<open>a < b\<close> by simp
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   918
  qed
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   919
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   920
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
   921
lemma differentiable_bound:
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   922
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   923
  assumes "convex S"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   924
    and derf: "\<And>x. x\<in>S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   925
    and B: "\<And>x. x \<in> S \<Longrightarrow> onorm (f' x) \<le> B"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   926
    and x: "x \<in> S"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   927
    and y: "y \<in> S"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   928
  shows "norm (f x - f y) \<le> B * norm (x - y)"
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   929
proof -
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   930
  let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   931
  let ?\<phi> = "\<lambda>h. h * B * norm (x - y)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   932
  have *: "x + u *\<^sub>R (y - x) \<in> S" if "u \<in> {0..1}" for u
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   933
  proof -
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   934
    have "u *\<^sub>R y = u *\<^sub>R (y - x) + u *\<^sub>R x"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   935
      by (simp add: scale_right_diff_distrib)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   936
    then show "x + u *\<^sub>R (y - x) \<in> S"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   937
      using that \<open>convex S\<close> unfolding convex_alt by (metis (no_types) atLeastAtMost_iff linordered_field_class.sign_simps(2) pth_c(3) scaleR_collapse x y)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   938
  qed
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   939
  have "\<And>z. z \<in> (\<lambda>u. x + u *\<^sub>R (y - x)) ` {0..1} \<Longrightarrow>
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   940
          (f has_derivative f' z) (at z within (\<lambda>u. x + u *\<^sub>R (y - x)) ` {0..1})"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   941
    by (auto intro: * has_derivative_within_subset [OF derf])
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   942
  then have "continuous_on (?p ` {0..1}) f"
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   943
    unfolding continuous_on_eq_continuous_within
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   944
    by (meson has_derivative_continuous)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   945
  with * have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   946
    by (intro continuous_intros)+
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   947
  {
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   948
    fix u::real assume u: "u \<in>{0 <..< 1}"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   949
    let ?u = "?p u"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   950
    interpret linear "(f' ?u)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   951
      using u by (auto intro!: has_derivative_linear derf *)
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56183
diff changeset
   952
    have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   953
      by (intro derivative_intros has_derivative_within_subset [OF derf]) (use u * in auto)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   954
    hence "((f \<circ> ?p) has_vector_derivative f' ?u (y - x)) (at u)"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   955
      by (simp add: has_derivative_within_open[OF u open_greaterThanLessThan]
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   956
        scaleR has_vector_derivative_def o_def)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   957
  } note 2 = this
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   958
  have 3: "continuous_on {0..1} ?\<phi>"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   959
    by (rule continuous_intros)+
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   960
  have 4: "(?\<phi> has_vector_derivative B * norm (x - y)) (at u)" for u
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   961
    by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   962
  {
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   963
    fix u::real assume u: "u \<in>{0 <..< 1}"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   964
    let ?u = "?p u"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   965
    interpret bounded_linear "(f' ?u)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   966
      using u by (auto intro!: has_derivative_bounded_linear derf *)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   967
    have "norm (f' ?u (y - x)) \<le> onorm (f' ?u) * norm (y - x)"
67682
00c436488398 tuned proofs -- prefer explicit names for facts from 'interpret';
wenzelm
parents: 67399
diff changeset
   968
      by (rule onorm) (rule bounded_linear)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   969
    also have "onorm (f' ?u) \<le> B"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   970
      using u by (auto intro!: assms(3)[rule_format] *)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   971
    finally have "norm ((f' ?u) (y - x)) \<le> B * norm (x - y)"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   972
      by (simp add: mult_right_mono norm_minus_commute)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   973
  } note 5 = this
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
   974
  have "norm (f x - f y) = norm ((f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 1 - (f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 0)"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
   975
    by (auto simp add: norm_minus_commute)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   976
  also
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   977
  from differentiable_bound_general[OF zero_less_one 1, OF 3 2 4 5]
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   978
  have "norm ((f \<circ> ?p) 1 - (f \<circ> ?p) 0) \<le> B * norm (x - y)"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   979
    by simp
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   980
  finally show ?thesis .
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   981
qed
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   982
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   983
lemma
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   984
  differentiable_bound_segment:
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   985
  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   986
  assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R a \<in> G"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   987
  assumes f': "\<And>x. x \<in> G \<Longrightarrow> (f has_derivative f' x) (at x within G)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
   988
  assumes B: "\<And>x. x \<in> {0..1} \<Longrightarrow> onorm (f' (x0 + x *\<^sub>R a)) \<le> B"
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   989
  shows "norm (f (x0 + a) - f x0) \<le> norm a * B"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   990
proof -
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   991
  let ?G = "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66394
diff changeset
   992
  have "?G = (+) x0 ` (\<lambda>x. x *\<^sub>R a) ` {0..1}" by auto
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   993
  also have "convex \<dots>"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   994
    by (intro convex_translation convex_scaled convex_real_interval)
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   995
  finally have "convex ?G" .
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   996
  moreover have "?G \<subseteq> G" "x0 \<in> ?G" "x0 + a \<in> ?G" using assms by (auto intro: image_eqI[where x=1])
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   997
  ultimately show ?thesis
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
   998
    using has_derivative_subset[OF f' \<open>?G \<subseteq> G\<close>] B
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
   999
      differentiable_bound[of "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}" f f' B "x0 + a" x0]
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
  1000
    by (force simp: ac_simps)
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1001
qed
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1002
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1003
lemma differentiable_bound_linearization:
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1004
  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
  1005
  assumes S: "\<And>t. t \<in> {0..1} \<Longrightarrow> a + t *\<^sub>R (b - a) \<in> S"
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1006
  assumes f'[derivative_intros]: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
  1007
  assumes B: "\<And>x. x \<in> S \<Longrightarrow> onorm (f' x - f' x0) \<le> B"
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1008
  assumes "x0 \<in> S"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1009
  shows "norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1010
proof -
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62949
diff changeset
  1011
  define g where [abs_def]: "g x = f x - f' x0 x" for x
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1012
  have g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative (\<lambda>i. f' x i - f' x0 i)) (at x within S)"
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1013
    unfolding g_def using assms
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1014
    by (auto intro!: derivative_eq_intros
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1015
      bounded_linear.has_derivative[OF has_derivative_bounded_linear, OF f'])
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
  1016
  from B have "\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
  1017
    using assms by (auto simp: fun_diff_def)
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
  1018
  with differentiable_bound_segment[OF S g] \<open>x0 \<in> S\<close>
60178
f620c70f9e9b generalized differentiable_bound; some further variations of differentiable_bound
immler
parents: 60177
diff changeset
  1019
  show ?thesis
63469
b6900858dcb9 lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents: 63170
diff changeset
  1020
    by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1021
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1022
67685
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1023
lemma vector_differentiable_bound_linearization:
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1024
  fixes f::"real \<Rightarrow> 'b::real_normed_vector"
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1025
  assumes f': "\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)"
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1026
  assumes "closed_segment a b \<subseteq> S"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68095
diff changeset
  1027
  assumes B: "\<And>x. x \<in> S \<Longrightarrow> norm (f' x - f' x0) \<le> B"
67685
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1028
  assumes "x0 \<in> S"
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1029
  shows "norm (f b - f a - (b - a) *\<^sub>R f' x0) \<le> norm (b - a) * B"
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1030
  using assms
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1031
  by (intro differentiable_bound_linearization[of a b S f "\<lambda>x h. h *\<^sub>R f' x" x0 B])
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1032
    (force simp: closed_segment_real_eq has_vector_derivative_def
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1033
      scaleR_diff_right[symmetric] mult.commute[of B]
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1034
      intro!: onorm_le mult_left_mono)+
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1035
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1036
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
  1037
text \<open>In particular.\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1038
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1039
lemma has_derivative_zero_constant:
60179
d87c8c2d4938 generalized class constraints
immler
parents: 60178
diff changeset
  1040
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
  1041
  assumes "convex s"
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1042
    and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1043
  shows "\<exists>c. \<forall>x\<in>s. f x = c"
56332
289dd9166d04 tuned proofs
hoelzl
parents: 56320
diff changeset
  1044
proof -
289dd9166d04 tuned proofs
hoelzl
parents: 56320
diff changeset
  1045
  { fix x y assume "x \<in> s" "y \<in> s"
289dd9166d04 tuned proofs
hoelzl
parents: 56320
diff changeset
  1046
    then have "norm (f x - f y) \<le> 0 * norm (x - y)"
289dd9166d04 tuned proofs
hoelzl
parents: 56320
diff changeset
  1047
      using assms by (intro differentiable_bound[of s]) (auto simp: onorm_zero)
289dd9166d04 tuned proofs
hoelzl
parents: 56320
diff changeset
  1048
    then have "f x = f y"
289dd9166d04 tuned proofs
hoelzl
parents: 56320
diff changeset
  1049
      by simp }
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
  1050
  then show ?thesis
56332
289dd9166d04 tuned proofs
hoelzl
parents: 56320
diff changeset
  1051
    by metis
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
  1052
qed
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1053
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61520
diff changeset
  1054
lemma has_field_derivative_zero_constant:
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61520
diff changeset
  1055
  assumes "convex s" "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative 0) (at x within s)"
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61520
diff changeset
  1056
  shows   "\<exists>c. \<forall>x\<in>s. f (x) = (c :: 'a :: real_normed_field)"
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61520
diff changeset
  1057
proof (rule has_derivative_zero_constant)
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66394
diff changeset
  1058
  have A: "( * ) 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61520
diff changeset
  1059
  fix x assume "x \<in> s" thus "(f has_derivative (\<lambda>h. 0)) (at x within s)"
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61520
diff changeset
  1060
    using assms(2)[of x] by (simp add: has_field_derivative_def A)
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61520
diff changeset
  1061
qed fact
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61520
diff changeset
  1062
67685
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1063
lemma
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1064
  has_vector_derivative_zero_constant:
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1065
  assumes "convex s"
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1066
  assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_vector_derivative 0) (at x within s)"
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1067
  obtains c where "\<And>x. x \<in> s \<Longrightarrow> f x = c"
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1068
  using has_derivative_zero_constant[of s f] assms
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1069
  by (auto simp: has_vector_derivative_def)
bdff8bf0a75b moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents: 67682
diff changeset
  1070
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
  1071
lemma has_derivative_zero_unique:
60179
d87c8c2d4938 generalized class constraints
immler
parents: 60178
diff changeset
  1072
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
  1073
  assumes "convex s"
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1074
    and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1075
    and "x \<in> s" "y \<in> s"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1076
  shows "f x = f y"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1077
  using has_derivative_zero_constant[OF assms(1,2)] assms(3-) by force
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1078
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1079
lemma has_derivative_zero_unique_connected:
60179
d87c8c2d4938 generalized class constraints
immler
parents: 60178
diff changeset
  1080
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1081
  assumes "open s" "connected s"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1082
  assumes f: "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>x. 0)) (at x)"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1083
  assumes "x \<in> s" "y \<in> s"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1084
  shows "f x = f y"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
  1085
proof (rule connected_local_const[where f=f, OF \<open>connected s\<close> \<open>x\<in>s\<close> \<open>y\<in>s\<close>])
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1086
  show "\<forall>a\<in>s. eventually (\<lambda>b. f a = f b) (at a within s)"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1087
  proof
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1088
    fix a assume "a \<in> s"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
  1089
    with \<open>open s\<close> obtain e where "0 < e" "ball a e \<subseteq> s"
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1090
      by (rule openE)
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1091
    then have "\<exists>c. \<forall>x\<in>ball a e. f x = c"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1092
      by (intro has_derivative_zero_constant)
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1093
         (auto simp: at_within_open[OF _ open_ball] f convex_ball)
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
  1094
    with \<open>0<e\<close> have "\<forall>x\<in>ball a e. f a = f x"
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1095
      by auto
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1096
    then show "eventually (\<lambda>b. f a = f b) (at a within s)"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
  1097
      using \<open>0<e\<close> unfolding eventually_at_topological
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1098
      by (intro exI[of _ "ball a e"]) auto
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1099
  qed
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1100
qed
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1101
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60179
diff changeset
  1102
subsection \<open>Differentiability of inverse function (most basic form)\<close>
33741
4c414d0835ab Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
hoelzl
parents:
diff changeset
  1103
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1104
lemma has_derivative_inverse_basic:
56226
29fd6bd9228e generalize some theorems
huffman
parents: 56223
diff changeset
  1105
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
68055
2cab37094fc4 more defer/prefer
paulson <lp15@cam.ac.uk>
parents: 67979
diff changeset
  1106
  assumes derf: "(f has_derivative f') (at (g y))"
2cab37094fc4 more defer/prefer
paulson <lp15@cam.ac.uk>
parents: 67979
diff changeset
  1107
    and ling': "bounded_linear g'"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
  1108
    and "g' \<circ> f' = id"
68055
2cab37094fc4 more defer/prefer
paulson <lp15@cam.ac.uk>
parents: 67979
diff changeset
  1109
    and contg: "continuous (at y) g"
2cab37094fc4 more defer/prefer
paulson <lp15@cam.ac.uk>
parents: 67979
diff changeset
  1110
    and "open T"
2cab37094fc4 more defer/prefer
paulson <lp15@cam.ac.uk>
parents: 67979
diff changeset
  1111
    and "y \<in> T"
2cab37094fc4 more defer/prefer
paulson <lp15@cam.ac.uk>
parents: 67979
diff changeset
  1112
    and fg: "\<And>z. z \<in> T \<Longrightarrow> f (g z) = z"
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1113
  shows "(g has_derivative g') (at y)"
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
  1114
proof -
44123
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1115
  interpret f': bounded_linear f'
2362a970e348 Derivative.thy: clean up formatting
huffman
parents: 44081
diff changeset
  1116
    using assms unfolding has_derivative_def by auto
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
  1117
  interpret g': bounded_linear g'
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
  1118
    using assms by auto
55665
4381a2b622ea tuned proofs;
wenzelm
parents: 54775
diff changeset
  1119
  obtain C where C: "0 < C" "\<And>x. norm (g' x) \<le> norm x * C"
4381a2b622ea tuned proofs;
wenzelm
parents: 54775
diff changeset
  1120
    using bounded_linear.pos_bounded[OF assms(2)] by blast
53781
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
  1121
  have lem1: "\<forall>e>0. \<exists>d>0. \<forall>z.
1e86d0b66866 tuned proofs;
wenzelm
parents: 53600
diff changeset
  1122
    norm (z - y) < d \<longrightarrow> norm (g z - g y - g'(z - y)) \<le> e * norm (g z - g y)"
68055
2cab37094fc4 more defer/prefer
paulson <lp15@cam.ac.uk>
parents: 67979
diff changeset
  1123
  proof (intro allI impI)
61165
8020249565fb tuned proofs;
wenzelm
parents: 61104
diff changeset
  1124
    fix e :: real
8020249565fb tuned proofs;
wenzelm
parents: 61104
diff changeset
  1125
    assume "e > 0"
8020249565fb tuned proofs;
wenzelm
parents: 61104
diff changeset
  1126
    with C(1) have *: "e / C > 0" by auto
68055
2cab37094fc4 more defer/prefer
paulson <lp15@cam.ac.uk>
parents: 67979
diff changeset
  1127
    obtain d0 where  "0 < d0" and d0:
2cab37094fc4 more defer/prefer
paulson <lp15@cam.ac.uk>
parents: 67979
d