author immler Wed Aug 29 07:50:28 2018 +0100 (13 months ago) changeset 68838 5e013478bced parent 68837 99f0aee4adbd child 68839 d8251a61cce8
tagged some theories
```     1.1 --- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Tue Aug 28 21:08:42 2018 +0200
1.2 +++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Wed Aug 29 07:50:28 2018 +0100
1.3 @@ -7,7 +7,7 @@
1.4
1.5  subsection \<open>Definition\<close>
1.6
1.7 -definition "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
1.8 +definition%important "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
1.9
1.10  typedef (overloaded) ('a, 'b) bcontfun ("(_ \<Rightarrow>\<^sub>C /_)" [22, 21] 21) =
1.11    "bcontfun::('a::topological_space \<Rightarrow> 'b::metric_space) set"
1.12 @@ -41,7 +41,7 @@
1.13  instantiation bcontfun :: (topological_space, metric_space) metric_space
1.14  begin
1.15
1.16 -lift_definition dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real"
1.17 +lift_definition%important dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real"
1.18    is "\<lambda>f g. (SUP x. dist (f x) (g x))" .
1.19
1.20  definition uniformity_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b \<times> 'a \<Rightarrow>\<^sub>C 'b) filter"
1.21 @@ -175,8 +175,8 @@
1.22
1.23  subsection \<open>Complete Space\<close>
1.24
1.25 -instance bcontfun :: (metric_space, complete_space) complete_space
1.26 -proof
1.27 +instance%important bcontfun :: (metric_space, complete_space) complete_space
1.28 +proof%unimportant
1.29    fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun"
1.30    assume "Cauchy f"  \<comment> \<open>Cauchy equals uniform convergence\<close>
1.31    then obtain g where "uniform_limit UNIV f g sequentially"
1.32 @@ -191,9 +191,9 @@
1.33  qed
1.34
1.35
1.36 -subsection \<open>Supremum norm for a normed vector space\<close>
1.37 +subsection%unimportant \<open>Supremum norm for a normed vector space\<close>
1.38
1.39 -instantiation bcontfun :: (topological_space, real_normed_vector) real_vector
1.40 +instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_vector
1.41  begin
1.42
1.43  lemma uminus_cont: "f \<in> bcontfun \<Longrightarrow> (\<lambda>x. - f x) \<in> bcontfun" for f::"'a \<Rightarrow> 'b"
1.44 @@ -247,7 +247,7 @@
1.45    "bounded (range f) \<Longrightarrow> norm (f x) \<le> (SUP x. norm (f x))"
1.46    by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp)
1.47
1.48 -instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector
1.49 +instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_normed_vector
1.50  begin
1.51
1.52  definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real"
1.53 @@ -290,7 +290,7 @@
1.54    using dist_bound[of f 0 b] assms
1.56
1.57 -subsection \<open>(bounded) continuous extenstion\<close>
1.58 +subsection%unimportant \<open>(bounded) continuous extenstion\<close>
1.59
1.60  lemma integral_clamp:
1.61    "integral {t0::real..clamp t0 t1 x} f =
```
```     2.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Tue Aug 28 21:08:42 2018 +0200
2.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Wed Aug 29 07:50:28 2018 +0100
2.3 @@ -37,7 +37,7 @@
2.4
2.5  lemmas onorm_componentwise_le = order_trans[OF onorm_componentwise]
2.6
2.7 -subsection \<open>Intro rules for @{term bounded_linear}\<close>
2.8 +subsection%unimportant \<open>Intro rules for @{term bounded_linear}\<close>
2.9
2.10  named_theorems bounded_linear_intros
2.11
2.12 @@ -79,7 +79,7 @@
2.13    bounded_linear_inner_right_comp
2.14
2.15
2.16 -subsection \<open>declaration of derivative/continuous/tendsto introduction rules for bounded linear functions\<close>
2.17 +subsection%unimportant \<open>declaration of derivative/continuous/tendsto introduction rules for bounded linear functions\<close>
2.18
2.19  attribute_setup bounded_linear =
2.20    \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
2.21 @@ -112,9 +112,9 @@
2.22        ]))\<close>
2.23
2.24
2.25 -subsection \<open>type of bounded linear functions\<close>
2.26 +subsection \<open>Type of bounded linear functions\<close>
2.27
2.28 -typedef (overloaded) ('a, 'b) blinfun ("(_ \<Rightarrow>\<^sub>L /_)" [22, 21] 21) =
2.29 +typedef%important (overloaded) ('a, 'b) blinfun ("(_ \<Rightarrow>\<^sub>L /_)" [22, 21] 21) =
2.30    "{f::'a::real_normed_vector\<Rightarrow>'b::real_normed_vector. bounded_linear f}"
2.31    morphisms blinfun_apply Blinfun
2.32    by (blast intro: bounded_linear_intros)
2.33 @@ -135,12 +135,12 @@
2.34    by (auto simp: Blinfun_inverse)
2.35
2.36
2.37 -subsection \<open>type class instantiations\<close>
2.38 +subsection \<open>Type class instantiations\<close>
2.39
2.40  instantiation blinfun :: (real_normed_vector, real_normed_vector) real_normed_vector
2.41  begin
2.42
2.43 -lift_definition norm_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real" is onorm .
2.44 +lift_definition%important norm_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real" is onorm .
2.45
2.46  lift_definition minus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
2.47    is "\<lambda>f g x. f x - g x"
2.48 @@ -158,14 +158,14 @@
2.49  lift_definition uminus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>f x. - f x"
2.50    by (rule bounded_linear_minus)
2.51
2.52 -lift_definition zero_blinfun :: "'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>x. 0"
2.53 +lift_definition%important zero_blinfun :: "'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>x. 0"
2.54    by (rule bounded_linear_zero)
2.55
2.56 -lift_definition plus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
2.57 +lift_definition%important plus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
2.58    is "\<lambda>f g x. f x + g x"
2.60
2.61 -lift_definition scaleR_blinfun::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>r f x. r *\<^sub>R f x"
2.62 +lift_definition%important scaleR_blinfun::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>r f x. r *\<^sub>R f x"
2.63    by (metis bounded_linear_compose bounded_linear_scaleR_right)
2.64
2.65  definition sgn_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
2.66 @@ -365,7 +365,7 @@
2.67      by (rule convergentI)
2.68  qed
2.69
2.70 -subsection \<open>On Euclidean Space\<close>
2.71 +subsection%unimportant \<open>On Euclidean Space\<close>
2.72
2.73  lemma Zfun_sum:
2.74    assumes "finite s"
2.75 @@ -586,7 +586,7 @@
2.76  qed
2.77
2.78
2.79 -subsection \<open>concrete bounded linear functions\<close>
2.80 +subsection%unimportant \<open>concrete bounded linear functions\<close>
2.81
2.82  lemma transfer_bounded_bilinear_bounded_linearI:
2.83    assumes "g = (\<lambda>i x. (blinfun_apply (f i) x))"
```
```     3.1 --- a/src/HOL/Analysis/Derivative.thy	Tue Aug 28 21:08:42 2018 +0200
3.2 +++ b/src/HOL/Analysis/Derivative.thy	Wed Aug 29 07:50:28 2018 +0100
3.3 @@ -3,7 +3,7 @@
3.4      Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light); tidied by LCP
3.5  *)
3.6
3.7 -section \<open>Multivariate calculus in Euclidean space\<close>
3.8 +section \<open>Derivative\<close>
3.9
3.10  theory Derivative
3.11  imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function
3.12 @@ -20,11 +20,11 @@
3.13    by (intro derivative_eq_intros) auto
3.14
3.15
3.16 -subsection \<open>Derivative with composed bilinear function\<close>
3.17 +subsection%unimportant \<open>Derivative with composed bilinear function\<close>
3.18
3.19  text \<open>More explicit epsilon-delta forms.\<close>
3.20
3.21 -lemma has_derivative_within':
3.22 +proposition has_derivative_within':
3.23    "(f has_derivative f')(at x within s) \<longleftrightarrow>
3.24      bounded_linear f' \<and>
3.25      (\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
3.26 @@ -92,7 +92,7 @@
3.27
3.28  subsection \<open>Differentiability\<close>
3.29
3.30 -definition
3.31 +definition%important
3.32    differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool"
3.33      (infix "differentiable'_on" 50)
3.34    where "f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable (at x within s))"
3.35 @@ -113,7 +113,7 @@
3.36    "(\<And>x. x \<in> s \<Longrightarrow> f differentiable at x) \<Longrightarrow> f differentiable_on s"
3.37    by (metis differentiable_at_withinI differentiable_on_def)
3.38
3.39 -corollary differentiable_iff_scaleR:
3.40 +corollary%unimportant differentiable_iff_scaleR:
3.41    fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
3.42    shows "f differentiable F \<longleftrightarrow> (\<exists>d. (f has_derivative (\<lambda>x. x *\<^sub>R d)) F)"
3.43    by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR)
3.44 @@ -211,7 +211,7 @@
3.45
3.46  definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)"
3.47
3.48 -lemma frechet_derivative_works:
3.49 +proposition frechet_derivative_works:
3.50    "f differentiable net \<longleftrightarrow> (f has_derivative (frechet_derivative f net)) net"
3.51    unfolding frechet_derivative_def differentiable_def
3.52    unfolding some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] ..
3.53 @@ -223,7 +223,7 @@
3.54
3.55  subsection \<open>Differentiability implies continuity\<close>
3.56
3.57 -lemma differentiable_imp_continuous_within:
3.58 +proposition differentiable_imp_continuous_within:
3.59    "f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
3.60    by (auto simp: differentiable_def intro: has_derivative_continuous)
3.61
3.62 @@ -288,7 +288,7 @@
3.63
3.64  subsection \<open>The chain rule\<close>
3.65
3.66 -lemma diff_chain_within[derivative_intros]:
3.67 +proposition diff_chain_within[derivative_intros]:
3.68    assumes "(f has_derivative f') (at x within s)"
3.69      and "(g has_derivative g') (at (f x) within (f ` s))"
3.70    shows "((g \<circ> f) has_derivative (g' \<circ> f'))(at x within s)"
3.71 @@ -324,7 +324,7 @@
3.72    by (auto simp: o_def mult.commute has_vector_derivative_def)
3.73
3.74
3.75 -subsection \<open>Composition rules stated just for differentiability\<close>
3.76 +subsection%unimportant \<open>Composition rules stated just for differentiability\<close>
3.77
3.78  lemma differentiable_chain_at:
3.79    "f differentiable (at x) \<Longrightarrow>
3.80 @@ -342,12 +342,12 @@
3.81  subsection \<open>Uniqueness of derivative\<close>
3.82
3.83
3.84 -text \<open>
3.85 +text%important \<open>
3.86   The general result is a bit messy because we need approachability of the
3.87   limit point from any direction. But OK for nontrivial intervals etc.
3.88  \<close>
3.89
3.90 -lemma frechet_derivative_unique_within:
3.91 +proposition frechet_derivative_unique_within:
3.92    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
3.93    assumes 1: "(f has_derivative f') (at x within S)"
3.94      and 2: "(f has_derivative f'') (at x within S)"
3.95 @@ -414,7 +414,7 @@
3.96    qed
3.97  qed
3.98
3.99 -lemma frechet_derivative_unique_within_closed_interval:
3.100 +proposition frechet_derivative_unique_within_closed_interval:
3.101    fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
3.102    assumes ab: "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
3.103      and x: "x \<in> cbox a b"
3.104 @@ -611,7 +611,7 @@
3.105
3.106  subsection \<open>One-dimensional mean value theorem\<close>
3.107
3.108 -lemma mvt:
3.109 +theorem mvt:
3.110    fixes f :: "real \<Rightarrow> real"
3.111    assumes "a < b"
3.112      and contf: "continuous_on {a..b} f"
3.113 @@ -1242,7 +1242,7 @@
3.114
3.115  text \<open>Here's the simplest way of not assuming much about g.\<close>
3.116
3.117 -lemma has_derivative_inverse:
3.118 +proposition has_derivative_inverse:
3.119    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
3.120    assumes "compact S"
3.121      and "x \<in> S"
3.122 @@ -1265,7 +1265,9 @@
3.123  qed
3.124
3.125
3.126 -subsection \<open>Proving surjectivity via Brouwer fixpoint theorem\<close>
3.127 +subsection \<open>Inverse function theorem\<close>
3.128 +
3.129 +text \<open>Proving surjectivity via Brouwer fixpoint theorem\<close>
3.130
3.131  lemma brouwer_surjective:
3.132    fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
3.133 @@ -1493,7 +1495,7 @@
3.134
3.135  text \<open>On a region.\<close>
3.136
3.137 -lemma has_derivative_inverse_on:
3.138 +theorem has_derivative_inverse_on:
3.139    fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
3.140    assumes "open S"
3.141      and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
3.142 @@ -1650,7 +1652,7 @@
3.143      done
3.144  qed
3.145
3.146 -lemma has_derivative_sequence:
3.147 +proposition has_derivative_sequence:
3.148    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
3.149    assumes "convex S"
3.150      and derf: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
3.151 @@ -1896,7 +1898,7 @@
3.152
3.153  subsection \<open>Differentiation of a series\<close>
3.154
3.155 -lemma has_derivative_series:
3.156 +proposition has_derivative_series:
3.157    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
3.158    assumes "convex S"
3.159      and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
3.160 @@ -1999,6 +2001,8 @@
3.161    shows   "(\<lambda>x. \<Sum>n. f n x) differentiable (at x0)"
3.162    using differentiable_series[OF assms, of x0] \<open>x0 \<in> S\<close> by blast+
3.163
3.164 +subsection \<open>Derivative as a vector\<close>
3.165 +
3.166  text \<open>Considering derivative @{typ "real \<Rightarrow> 'b::real_normed_vector"} as a vector.\<close>
3.167
3.168  definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
3.169 @@ -2032,7 +2036,7 @@
3.170  lemma differentiableI_vector: "(f has_vector_derivative y) F \<Longrightarrow> f differentiable F"
3.171    by (auto simp: differentiable_def has_vector_derivative_def)
3.172
3.173 -lemma vector_derivative_works:
3.174 +proposition vector_derivative_works:
3.175    "f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net"
3.176      (is "?l = ?r")
3.177  proof
3.178 @@ -2086,55 +2090,6 @@
3.179    apply (auto simp: netlimit_within eventually_at_filter elim: eventually_mono)
3.180    done
3.181
3.182 -definition deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
3.183 -  "deriv f x \<equiv> SOME D. DERIV f x :> D"
3.184 -
3.185 -lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
3.186 -  unfolding deriv_def by (metis some_equality DERIV_unique)
3.187 -
3.188 -lemma DERIV_deriv_iff_has_field_derivative:
3.189 -  "DERIV f x :> deriv f x \<longleftrightarrow> (\<exists>f'. (f has_field_derivative f') (at x))"
3.190 -  by (auto simp: has_field_derivative_def DERIV_imp_deriv)
3.191 -
3.192 -lemma DERIV_deriv_iff_real_differentiable:
3.193 -  fixes x :: real
3.194 -  shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
3.195 -  unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff)
3.196 -
3.197 -lemma deriv_cong_ev:
3.198 -  assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
3.199 -  shows   "deriv f x = deriv g y"
3.200 -proof -
3.201 -  have "(\<lambda>D. (f has_field_derivative D) (at x)) = (\<lambda>D. (g has_field_derivative D) (at y))"
3.202 -    by (intro ext DERIV_cong_ev refl assms)
3.203 -  thus ?thesis by (simp add: deriv_def assms)
3.204 -qed
3.205 -
3.206 -lemma higher_deriv_cong_ev:
3.207 -  assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
3.208 -  shows   "(deriv ^^ n) f x = (deriv ^^ n) g y"
3.209 -proof -
3.210 -  from assms(1) have "eventually (\<lambda>x. (deriv ^^ n) f x = (deriv ^^ n) g x) (nhds x)"
3.211 -  proof (induction n arbitrary: f g)
3.212 -    case (Suc n)
3.213 -    from Suc.prems have "eventually (\<lambda>y. eventually (\<lambda>z. f z = g z) (nhds y)) (nhds x)"
3.214 -      by (simp add: eventually_eventually)
3.215 -    hence "eventually (\<lambda>x. deriv f x = deriv g x) (nhds x)"
3.216 -      by eventually_elim (rule deriv_cong_ev, simp_all)
3.217 -    thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps)
3.218 -  qed auto
3.219 -  from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp
3.220 -qed
3.221 -
3.222 -lemma real_derivative_chain:
3.223 -  fixes x :: real
3.224 -  shows "f differentiable at x \<Longrightarrow> g differentiable at (f x)
3.225 -    \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
3.226 -  by (metis DERIV_deriv_iff_real_differentiable DERIV_chain DERIV_imp_deriv)
3.227 -lemma field_derivative_eq_vector_derivative:
3.228 -   "(deriv f x) = vector_derivative f (at x)"
3.229 -by (simp add: mult.commute deriv_def vector_derivative_def has_vector_derivative_def has_field_derivative_def)
3.230 -
3.231  lemma islimpt_closure_open:
3.232    fixes s :: "'a::perfect_space set"
3.233    assumes "open s" and t: "t = closure s" "x \<in> t"
3.234 @@ -2312,7 +2267,7 @@
3.235
3.236  subsection\<open>The notion of being field differentiable\<close>
3.237
3.238 -definition field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
3.239 +definition%important field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
3.240             (infixr "(field'_differentiable)" 50)
3.241    where "f field_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
3.242
3.243 @@ -2321,10 +2276,6 @@
3.244    unfolding field_differentiable_def differentiable_def
3.245    using has_field_derivative_imp_has_derivative by auto
3.246
3.247 -lemma field_differentiable_derivI:
3.248 -    "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
3.249 -by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
3.250 -
3.251  lemma field_differentiable_imp_continuous_at:
3.252      "f field_differentiable (at x within S) \<Longrightarrow> continuous (at x within S) f"
3.253    by (metis DERIV_continuous field_differentiable_def)
3.254 @@ -2434,12 +2385,6 @@
3.255    unfolding field_differentiable_def
3.256    by (metis at_within_open)
3.257
3.258 -lemma vector_derivative_chain_at_general:
3.259 -  assumes "f differentiable at x" "g field_differentiable at (f x)"
3.260 -  shows "vector_derivative (g \<circ> f) (at x) = vector_derivative f (at x) * deriv g (f x)"
3.261 -  apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
3.262 -  using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
3.263 -
3.264  lemma exp_scaleR_has_vector_derivative_right:
3.265    "((\<lambda>t. exp (t *\<^sub>R A)) has_vector_derivative exp (t *\<^sub>R A) * A) (at t within T)"
3.266    unfolding has_vector_derivative_def
3.267 @@ -2515,11 +2460,72 @@
3.268    using exp_scaleR_has_vector_derivative_right[of A t]
3.270
3.271 +subsection \<open>Field derivative\<close>
3.272 +
3.273 +definition%important deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
3.274 +  "deriv f x \<equiv> SOME D. DERIV f x :> D"
3.275 +
3.276 +lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
3.277 +  unfolding deriv_def by (metis some_equality DERIV_unique)
3.278 +
3.279 +lemma DERIV_deriv_iff_has_field_derivative:
3.280 +  "DERIV f x :> deriv f x \<longleftrightarrow> (\<exists>f'. (f has_field_derivative f') (at x))"
3.281 +  by (auto simp: has_field_derivative_def DERIV_imp_deriv)
3.282 +
3.283 +lemma DERIV_deriv_iff_real_differentiable:
3.284 +  fixes x :: real
3.285 +  shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
3.286 +  unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff)
3.287 +
3.288 +lemma deriv_cong_ev:
3.289 +  assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
3.290 +  shows   "deriv f x = deriv g y"
3.291 +proof -
3.292 +  have "(\<lambda>D. (f has_field_derivative D) (at x)) = (\<lambda>D. (g has_field_derivative D) (at y))"
3.293 +    by (intro ext DERIV_cong_ev refl assms)
3.294 +  thus ?thesis by (simp add: deriv_def assms)
3.295 +qed
3.296 +
3.297 +lemma higher_deriv_cong_ev:
3.298 +  assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
3.299 +  shows   "(deriv ^^ n) f x = (deriv ^^ n) g y"
3.300 +proof -
3.301 +  from assms(1) have "eventually (\<lambda>x. (deriv ^^ n) f x = (deriv ^^ n) g x) (nhds x)"
3.302 +  proof (induction n arbitrary: f g)
3.303 +    case (Suc n)
3.304 +    from Suc.prems have "eventually (\<lambda>y. eventually (\<lambda>z. f z = g z) (nhds y)) (nhds x)"
3.305 +      by (simp add: eventually_eventually)
3.306 +    hence "eventually (\<lambda>x. deriv f x = deriv g x) (nhds x)"
3.307 +      by eventually_elim (rule deriv_cong_ev, simp_all)
3.308 +    thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps)
3.309 +  qed auto
3.310 +  from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp
3.311 +qed
3.312 +
3.313 +lemma real_derivative_chain:
3.314 +  fixes x :: real
3.315 +  shows "f differentiable at x \<Longrightarrow> g differentiable at (f x)
3.316 +    \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
3.317 +  by (metis DERIV_deriv_iff_real_differentiable DERIV_chain DERIV_imp_deriv)
3.318 +lemma field_derivative_eq_vector_derivative:
3.319 +   "(deriv f x) = vector_derivative f (at x)"
3.320 +by (simp add: mult.commute deriv_def vector_derivative_def has_vector_derivative_def has_field_derivative_def)
3.321 +
3.322 +proposition field_differentiable_derivI:
3.323 +    "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
3.324 +by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
3.325 +
3.326 +lemma vector_derivative_chain_at_general:
3.327 +  assumes "f differentiable at x" "g field_differentiable at (f x)"
3.328 +  shows "vector_derivative (g \<circ> f) (at x) = vector_derivative f (at x) * deriv g (f x)"
3.329 +  apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
3.330 +  using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
3.331 +
3.332
3.333  subsection \<open>Relation between convexity and derivative\<close>
3.334
3.335  (* TODO: Generalise to real vector spaces? *)
3.336 -lemma convex_on_imp_above_tangent:
3.337 +proposition convex_on_imp_above_tangent:
3.338    assumes convex: "convex_on A f" and connected: "connected A"
3.339    assumes c: "c \<in> interior A" and x : "x \<in> A"
3.340    assumes deriv: "(f has_field_derivative f') (at c within A)"
3.341 @@ -2602,7 +2608,7 @@
3.342      by (auto intro!: exI[where x="UNIV \<times> S"] S open_Times)
3.343  qed
3.344
3.345 -lemma has_derivative_partialsI:
3.346 +proposition has_derivative_partialsI:
3.347    fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
3.348    assumes fx: "((\<lambda>x. f x y) has_derivative fx) (at x within X)"
3.349    assumes fy: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>y. f x y) has_derivative blinfun_apply (fy x y)) (at y within Y)"
3.350 @@ -2767,7 +2773,7 @@
3.351  qed
3.352
3.353
3.354 -subsection \<open>Differentiable case distinction\<close>
3.355 +subsection%unimportant \<open>Differentiable case distinction\<close>
3.356
3.357  lemma has_derivative_within_If_eq:
3.358    "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within S) =
```
```     4.1 --- a/src/HOL/Analysis/Lipschitz.thy	Tue Aug 28 21:08:42 2018 +0200
4.2 +++ b/src/HOL/Analysis/Lipschitz.thy	Wed Aug 29 07:50:28 2018 +0100
4.3 @@ -7,11 +7,11 @@
4.4    imports Borel_Space
4.5  begin
4.6
4.7 -definition lipschitz_on
4.8 +definition%important lipschitz_on
4.9    where "lipschitz_on C U f \<longleftrightarrow> (0 \<le> C \<and> (\<forall>x \<in> U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y))"
4.10
4.11  bundle lipschitz_syntax begin
4.12 -notation lipschitz_on ("_-lipschitz'_on" [1000])
4.13 +notation%important lipschitz_on ("_-lipschitz'_on" [1000])
4.14  end
4.15  bundle no_lipschitz_syntax begin
4.16  no_notation lipschitz_on ("_-lipschitz'_on" [1000])
4.17 @@ -103,7 +103,7 @@
4.18    qed
4.19  qed (rule lipschitz_on_nonneg[OF f])
4.20
4.21 -proposition lipschitz_on_concat_max:
4.22 +lemma lipschitz_on_concat_max:
4.23    fixes a b c::real
4.24    assumes f: "L-lipschitz_on {a .. b} f"
4.25    assumes g: "M-lipschitz_on {b .. c} g"
4.26 @@ -118,7 +118,7 @@
4.27
4.28  subsubsection \<open>Continuity\<close>
4.29
4.30 -lemma lipschitz_on_uniformly_continuous:
4.31 +proposition lipschitz_on_uniformly_continuous:
4.32    assumes "L-lipschitz_on X f"
4.33    shows "uniformly_continuous_on X f"
4.34    unfolding uniformly_continuous_on_def
4.35 @@ -132,7 +132,7 @@
4.36      by (force intro!: exI[where x="e/(L + 1)"] simp: field_simps)
4.37  qed
4.38
4.39 -lemma lipschitz_on_continuous_on:
4.40 +proposition lipschitz_on_continuous_on:
4.41    "continuous_on X f" if "L-lipschitz_on X f"
4.42    by (rule uniformly_continuous_imp_continuous[OF lipschitz_on_uniformly_continuous[OF that]])
4.43
4.44 @@ -143,7 +143,7 @@
4.45
4.46  subsubsection \<open>Differentiable functions\<close>
4.47
4.48 -lemma bounded_derivative_imp_lipschitz:
4.49 +proposition bounded_derivative_imp_lipschitz:
4.50    assumes "\<And>x. x \<in> X \<Longrightarrow> (f has_derivative f' x) (at x within X)"
4.51    assumes convex: "convex X"
4.52    assumes "\<And>x. x \<in> X \<Longrightarrow> onorm (f' x) \<le> C" "0 \<le> C"
4.53 @@ -154,7 +154,7 @@
4.54  qed fact
4.55
4.56
4.57 -subsubsection \<open>Structural introduction rules\<close>
4.58 +subsubsection%unimportant \<open>Structural introduction rules\<close>
4.59
4.60  named_theorems lipschitz_intros "structural introduction rules for Lipschitz controls"
4.61
4.62 @@ -480,7 +480,7 @@
4.63
4.64  subsection \<open>Local Lipschitz continuity (uniform for a family of functions)\<close>
4.65
4.66 -definition local_lipschitz::
4.67 +definition%important local_lipschitz::
4.68    "'a::metric_space set \<Rightarrow> 'b::metric_space set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c::metric_space) \<Rightarrow> bool"
4.69    where
4.70    "local_lipschitz T X f \<equiv> \<forall>x \<in> X. \<forall>t \<in> T.
4.71 @@ -785,7 +785,7 @@
4.72      by (auto intro: exI[where x=1])
4.73  qed
4.74
4.75 -lemma c1_implies_local_lipschitz:
4.76 +proposition c1_implies_local_lipschitz:
4.77    fixes T::"real set" and X::"'a::{banach,heine_borel} set"
4.78      and f::"real \<Rightarrow> 'a \<Rightarrow> 'a"
4.79    assumes f': "\<And>t x. t \<in> T \<Longrightarrow> x \<in> X \<Longrightarrow> (f t has_derivative blinfun_apply (f' (t, x))) (at x)"
```
```     5.1 --- a/src/HOL/Analysis/Uniform_Limit.thy	Tue Aug 28 21:08:42 2018 +0200
5.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Wed Aug 29 07:50:28 2018 +0100
5.3 @@ -9,10 +9,13 @@
5.4  imports Connected Summation_Tests
5.5  begin
5.6
5.7 -definition uniformly_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> ('a \<Rightarrow> 'b) filter"
5.8 +
5.9 +subsection \<open>Definition\<close>
5.10 +
5.11 +definition%important uniformly_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> ('a \<Rightarrow> 'b) filter"
5.12    where "uniformly_on S l = (INF e:{0 <..}. principal {f. \<forall>x\<in>S. dist (f x) (l x) < e})"
5.13
5.14 -abbreviation
5.15 +abbreviation%important
5.16    "uniform_limit S f l \<equiv> filterlim f (uniformly_on S l)"
5.17
5.18  definition uniformly_convergent_on where
5.19 @@ -21,7 +24,7 @@
5.20  definition uniformly_Cauchy_on where
5.21    "uniformly_Cauchy_on X f \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>x\<in>X. \<forall>(m::nat)\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e)"
5.22
5.23 -lemma uniform_limit_iff:
5.24 +proposition uniform_limit_iff:
5.25    "uniform_limit S f l F \<longleftrightarrow> (\<forall>e>0. \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e)"
5.26    unfolding filterlim_iff uniformly_on_def
5.27    by (subst eventually_INF_base)
5.28 @@ -64,7 +67,10 @@
5.29      by eventually_elim force
5.30  qed
5.31
5.32 -lemma swap_uniform_limit:
5.33 +
5.34 +subsection \<open>Exchange limits\<close>
5.35 +
5.36 +proposition swap_uniform_limit:
5.37    assumes f: "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) (at x within S)"
5.38    assumes g: "(g \<longlongrightarrow> l) F"
5.39    assumes uc: "uniform_limit S f h F"
5.40 @@ -108,6 +114,9 @@
5.41      using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
5.42  qed
5.43
5.44 +
5.45 +subsection \<open>Uniform limit theorem\<close>
5.46 +
5.47  lemma tendsto_uniform_limitI:
5.48    assumes "uniform_limit S f l F"
5.49    assumes "x \<in> S"
5.50 @@ -115,7 +124,7 @@
5.51    using assms
5.52    by (auto intro!: tendstoI simp: eventually_mono dest!: uniform_limitD)
5.53
5.54 -lemma uniform_limit_theorem:
5.55 +theorem uniform_limit_theorem:
5.56    assumes c: "\<forall>\<^sub>F n in F. continuous_on A (f n)"
5.57    assumes ul: "uniform_limit A f l F"
5.58    assumes "\<not> trivial_limit F"
5.59 @@ -307,7 +316,10 @@
5.60    unfolding uniformly_convergent_on_def convergent_def
5.61    by (auto dest: tendsto_uniform_limitI)
5.62
5.63 -lemma weierstrass_m_test_ev:
5.64 +
5.65 +subsection \<open>Weierstrass M-Test\<close>
5.66 +
5.67 +proposition weierstrass_m_test_ev:
5.68  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
5.69  assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially"
5.70  assumes "summable M"
5.71 @@ -354,7 +366,7 @@
5.72  qed
5.73
5.74  text\<open>Alternative version, formulated as in HOL Light\<close>
5.75 -corollary series_comparison_uniform:
5.76 +corollary%unimportant series_comparison_uniform:
5.77    fixes f :: "_ \<Rightarrow> nat \<Rightarrow> _ :: banach"
5.78    assumes g: "summable g" and le: "\<And>n x. N \<le> n \<and> x \<in> A \<Longrightarrow> norm(f x n) \<le> g n"
5.79      shows "\<exists>l. \<forall>e. 0 < e \<longrightarrow> (\<exists>N. \<forall>n x. N \<le> n \<and> x \<in> A \<longrightarrow> dist(sum (f x) {..<n}) (l x) < e)"
5.80 @@ -367,20 +379,20 @@
5.81      done
5.82  qed
5.83
5.84 -corollary weierstrass_m_test:
5.85 +corollary%unimportant weierstrass_m_test:
5.86    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
5.87    assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
5.88    assumes "summable M"
5.89    shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
5.90    using assms by (intro weierstrass_m_test_ev always_eventually) auto
5.91
5.92 -corollary weierstrass_m_test'_ev:
5.93 +corollary%unimportant weierstrass_m_test'_ev:
5.94    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
5.95    assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially" "summable M"
5.96    shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
5.97    unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test_ev[OF assms])
5.98
5.99 -corollary weierstrass_m_test':
5.100 +corollary%unimportant weierstrass_m_test':
5.101    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
5.102    assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n" "summable M"
5.103    shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
5.104 @@ -389,6 +401,9 @@
5.105  lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
5.106    by simp
5.107
5.108 +
5.109 +subsection%unimportant \<open>Structural introduction rules\<close>
5.110 +
5.111  named_theorems uniform_limit_intros "introduction rules for uniform_limit"
5.112  setup \<open>