tagged some theories
authorimmler
Wed Aug 29 07:50:28 2018 +0100 (13 months ago)
changeset 688385e013478bced
parent 68837 99f0aee4adbd
child 68839 d8251a61cce8
tagged some theories
src/HOL/Analysis/Bounded_Continuous_Function.thy
src/HOL/Analysis/Bounded_Linear_Function.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Lipschitz.thy
src/HOL/Analysis/Uniform_Limit.thy
     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.55    by (simp add: dist_norm)
    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.59    by (metis bounded_linear_add)
    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.269    by (simp add: exp_times_scaleR_commute)
   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>
   5.113    Global_Theory.add_thms_dynamic (@{binding uniform_limit_eq_intros},