--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy Tue Aug 28 21:08:42 2018 +0200
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy Wed Aug 29 07:50:28 2018 +0100
@@ -7,7 +7,7 @@
subsection \<open>Definition\<close>
-definition "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
+definition%important "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
typedef (overloaded) ('a, 'b) bcontfun ("(_ \<Rightarrow>\<^sub>C /_)" [22, 21] 21) =
"bcontfun::('a::topological_space \<Rightarrow> 'b::metric_space) set"
@@ -41,7 +41,7 @@
instantiation bcontfun :: (topological_space, metric_space) metric_space
begin
-lift_definition dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real"
+lift_definition%important dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real"
is "\<lambda>f g. (SUP x. dist (f x) (g x))" .
definition uniformity_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b \<times> 'a \<Rightarrow>\<^sub>C 'b) filter"
@@ -175,8 +175,8 @@
subsection \<open>Complete Space\<close>
-instance bcontfun :: (metric_space, complete_space) complete_space
-proof
+instance%important bcontfun :: (metric_space, complete_space) complete_space
+proof%unimportant
fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun"
assume "Cauchy f" \<comment> \<open>Cauchy equals uniform convergence\<close>
then obtain g where "uniform_limit UNIV f g sequentially"
@@ -191,9 +191,9 @@
qed
-subsection \<open>Supremum norm for a normed vector space\<close>
+subsection%unimportant \<open>Supremum norm for a normed vector space\<close>
-instantiation bcontfun :: (topological_space, real_normed_vector) real_vector
+instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_vector
begin
lemma uminus_cont: "f \<in> bcontfun \<Longrightarrow> (\<lambda>x. - f x) \<in> bcontfun" for f::"'a \<Rightarrow> 'b"
@@ -247,7 +247,7 @@
"bounded (range f) \<Longrightarrow> norm (f x) \<le> (SUP x. norm (f x))"
by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp)
-instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector
+instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_normed_vector
begin
definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real"
@@ -290,7 +290,7 @@
using dist_bound[of f 0 b] assms
by (simp add: dist_norm)
-subsection \<open>(bounded) continuous extenstion\<close>
+subsection%unimportant \<open>(bounded) continuous extenstion\<close>
lemma integral_clamp:
"integral {t0::real..clamp t0 t1 x} f =
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Tue Aug 28 21:08:42 2018 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Wed Aug 29 07:50:28 2018 +0100
@@ -37,7 +37,7 @@
lemmas onorm_componentwise_le = order_trans[OF onorm_componentwise]
-subsection \<open>Intro rules for @{term bounded_linear}\<close>
+subsection%unimportant \<open>Intro rules for @{term bounded_linear}\<close>
named_theorems bounded_linear_intros
@@ -79,7 +79,7 @@
bounded_linear_inner_right_comp
-subsection \<open>declaration of derivative/continuous/tendsto introduction rules for bounded linear functions\<close>
+subsection%unimportant \<open>declaration of derivative/continuous/tendsto introduction rules for bounded linear functions\<close>
attribute_setup bounded_linear =
\<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
@@ -112,9 +112,9 @@
]))\<close>
-subsection \<open>type of bounded linear functions\<close>
+subsection \<open>Type of bounded linear functions\<close>
-typedef (overloaded) ('a, 'b) blinfun ("(_ \<Rightarrow>\<^sub>L /_)" [22, 21] 21) =
+typedef%important (overloaded) ('a, 'b) blinfun ("(_ \<Rightarrow>\<^sub>L /_)" [22, 21] 21) =
"{f::'a::real_normed_vector\<Rightarrow>'b::real_normed_vector. bounded_linear f}"
morphisms blinfun_apply Blinfun
by (blast intro: bounded_linear_intros)
@@ -135,12 +135,12 @@
by (auto simp: Blinfun_inverse)
-subsection \<open>type class instantiations\<close>
+subsection \<open>Type class instantiations\<close>
instantiation blinfun :: (real_normed_vector, real_normed_vector) real_normed_vector
begin
-lift_definition norm_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real" is onorm .
+lift_definition%important norm_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real" is onorm .
lift_definition minus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
is "\<lambda>f g x. f x - g x"
@@ -158,14 +158,14 @@
lift_definition uminus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>f x. - f x"
by (rule bounded_linear_minus)
-lift_definition zero_blinfun :: "'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>x. 0"
+lift_definition%important zero_blinfun :: "'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>x. 0"
by (rule bounded_linear_zero)
-lift_definition plus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
+lift_definition%important plus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
is "\<lambda>f g x. f x + g x"
by (metis bounded_linear_add)
-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"
+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"
by (metis bounded_linear_compose bounded_linear_scaleR_right)
definition sgn_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
@@ -365,7 +365,7 @@
by (rule convergentI)
qed
-subsection \<open>On Euclidean Space\<close>
+subsection%unimportant \<open>On Euclidean Space\<close>
lemma Zfun_sum:
assumes "finite s"
@@ -586,7 +586,7 @@
qed
-subsection \<open>concrete bounded linear functions\<close>
+subsection%unimportant \<open>concrete bounded linear functions\<close>
lemma transfer_bounded_bilinear_bounded_linearI:
assumes "g = (\<lambda>i x. (blinfun_apply (f i) x))"
--- a/src/HOL/Analysis/Derivative.thy Tue Aug 28 21:08:42 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy Wed Aug 29 07:50:28 2018 +0100
@@ -3,7 +3,7 @@
Author: Robert Himmelmann, TU Muenchen (translation from HOL Light); tidied by LCP
*)
-section \<open>Multivariate calculus in Euclidean space\<close>
+section \<open>Derivative\<close>
theory Derivative
imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function
@@ -20,11 +20,11 @@
by (intro derivative_eq_intros) auto
-subsection \<open>Derivative with composed bilinear function\<close>
+subsection%unimportant \<open>Derivative with composed bilinear function\<close>
text \<open>More explicit epsilon-delta forms.\<close>
-lemma has_derivative_within':
+proposition has_derivative_within':
"(f has_derivative f')(at x within s) \<longleftrightarrow>
bounded_linear f' \<and>
(\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
@@ -92,7 +92,7 @@
subsection \<open>Differentiability\<close>
-definition
+definition%important
differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool"
(infix "differentiable'_on" 50)
where "f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable (at x within s))"
@@ -113,7 +113,7 @@
"(\<And>x. x \<in> s \<Longrightarrow> f differentiable at x) \<Longrightarrow> f differentiable_on s"
by (metis differentiable_at_withinI differentiable_on_def)
-corollary differentiable_iff_scaleR:
+corollary%unimportant differentiable_iff_scaleR:
fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
shows "f differentiable F \<longleftrightarrow> (\<exists>d. (f has_derivative (\<lambda>x. x *\<^sub>R d)) F)"
by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR)
@@ -211,7 +211,7 @@
definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)"
-lemma frechet_derivative_works:
+proposition frechet_derivative_works:
"f differentiable net \<longleftrightarrow> (f has_derivative (frechet_derivative f net)) net"
unfolding frechet_derivative_def differentiable_def
unfolding some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] ..
@@ -223,7 +223,7 @@
subsection \<open>Differentiability implies continuity\<close>
-lemma differentiable_imp_continuous_within:
+proposition differentiable_imp_continuous_within:
"f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
by (auto simp: differentiable_def intro: has_derivative_continuous)
@@ -288,7 +288,7 @@
subsection \<open>The chain rule\<close>
-lemma diff_chain_within[derivative_intros]:
+proposition diff_chain_within[derivative_intros]:
assumes "(f has_derivative f') (at x within s)"
and "(g has_derivative g') (at (f x) within (f ` s))"
shows "((g \<circ> f) has_derivative (g' \<circ> f'))(at x within s)"
@@ -324,7 +324,7 @@
by (auto simp: o_def mult.commute has_vector_derivative_def)
-subsection \<open>Composition rules stated just for differentiability\<close>
+subsection%unimportant \<open>Composition rules stated just for differentiability\<close>
lemma differentiable_chain_at:
"f differentiable (at x) \<Longrightarrow>
@@ -342,12 +342,12 @@
subsection \<open>Uniqueness of derivative\<close>
-text \<open>
+text%important \<open>
The general result is a bit messy because we need approachability of the
limit point from any direction. But OK for nontrivial intervals etc.
\<close>
-lemma frechet_derivative_unique_within:
+proposition frechet_derivative_unique_within:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes 1: "(f has_derivative f') (at x within S)"
and 2: "(f has_derivative f'') (at x within S)"
@@ -414,7 +414,7 @@
qed
qed
-lemma frechet_derivative_unique_within_closed_interval:
+proposition frechet_derivative_unique_within_closed_interval:
fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes ab: "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
and x: "x \<in> cbox a b"
@@ -611,7 +611,7 @@
subsection \<open>One-dimensional mean value theorem\<close>
-lemma mvt:
+theorem mvt:
fixes f :: "real \<Rightarrow> real"
assumes "a < b"
and contf: "continuous_on {a..b} f"
@@ -1242,7 +1242,7 @@
text \<open>Here's the simplest way of not assuming much about g.\<close>
-lemma has_derivative_inverse:
+proposition has_derivative_inverse:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "compact S"
and "x \<in> S"
@@ -1265,7 +1265,9 @@
qed
-subsection \<open>Proving surjectivity via Brouwer fixpoint theorem\<close>
+subsection \<open>Inverse function theorem\<close>
+
+text \<open>Proving surjectivity via Brouwer fixpoint theorem\<close>
lemma brouwer_surjective:
fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
@@ -1493,7 +1495,7 @@
text \<open>On a region.\<close>
-lemma has_derivative_inverse_on:
+theorem has_derivative_inverse_on:
fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
assumes "open S"
and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
@@ -1650,7 +1652,7 @@
done
qed
-lemma has_derivative_sequence:
+proposition has_derivative_sequence:
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
assumes "convex S"
and derf: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
@@ -1896,7 +1898,7 @@
subsection \<open>Differentiation of a series\<close>
-lemma has_derivative_series:
+proposition has_derivative_series:
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
assumes "convex S"
and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
@@ -1999,6 +2001,8 @@
shows "(\<lambda>x. \<Sum>n. f n x) differentiable (at x0)"
using differentiable_series[OF assms, of x0] \<open>x0 \<in> S\<close> by blast+
+subsection \<open>Derivative as a vector\<close>
+
text \<open>Considering derivative @{typ "real \<Rightarrow> 'b::real_normed_vector"} as a vector.\<close>
definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
@@ -2032,7 +2036,7 @@
lemma differentiableI_vector: "(f has_vector_derivative y) F \<Longrightarrow> f differentiable F"
by (auto simp: differentiable_def has_vector_derivative_def)
-lemma vector_derivative_works:
+proposition vector_derivative_works:
"f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net"
(is "?l = ?r")
proof
@@ -2086,55 +2090,6 @@
apply (auto simp: netlimit_within eventually_at_filter elim: eventually_mono)
done
-definition deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
- "deriv f x \<equiv> SOME D. DERIV f x :> D"
-
-lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
- unfolding deriv_def by (metis some_equality DERIV_unique)
-
-lemma DERIV_deriv_iff_has_field_derivative:
- "DERIV f x :> deriv f x \<longleftrightarrow> (\<exists>f'. (f has_field_derivative f') (at x))"
- by (auto simp: has_field_derivative_def DERIV_imp_deriv)
-
-lemma DERIV_deriv_iff_real_differentiable:
- fixes x :: real
- shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
- unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff)
-
-lemma deriv_cong_ev:
- assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
- shows "deriv f x = deriv g y"
-proof -
- have "(\<lambda>D. (f has_field_derivative D) (at x)) = (\<lambda>D. (g has_field_derivative D) (at y))"
- by (intro ext DERIV_cong_ev refl assms)
- thus ?thesis by (simp add: deriv_def assms)
-qed
-
-lemma higher_deriv_cong_ev:
- assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
- shows "(deriv ^^ n) f x = (deriv ^^ n) g y"
-proof -
- from assms(1) have "eventually (\<lambda>x. (deriv ^^ n) f x = (deriv ^^ n) g x) (nhds x)"
- proof (induction n arbitrary: f g)
- case (Suc n)
- from Suc.prems have "eventually (\<lambda>y. eventually (\<lambda>z. f z = g z) (nhds y)) (nhds x)"
- by (simp add: eventually_eventually)
- hence "eventually (\<lambda>x. deriv f x = deriv g x) (nhds x)"
- by eventually_elim (rule deriv_cong_ev, simp_all)
- thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps)
- qed auto
- from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp
-qed
-
-lemma real_derivative_chain:
- fixes x :: real
- shows "f differentiable at x \<Longrightarrow> g differentiable at (f x)
- \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
- by (metis DERIV_deriv_iff_real_differentiable DERIV_chain DERIV_imp_deriv)
-lemma field_derivative_eq_vector_derivative:
- "(deriv f x) = vector_derivative f (at x)"
-by (simp add: mult.commute deriv_def vector_derivative_def has_vector_derivative_def has_field_derivative_def)
-
lemma islimpt_closure_open:
fixes s :: "'a::perfect_space set"
assumes "open s" and t: "t = closure s" "x \<in> t"
@@ -2312,7 +2267,7 @@
subsection\<open>The notion of being field differentiable\<close>
-definition field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
+definition%important field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
(infixr "(field'_differentiable)" 50)
where "f field_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
@@ -2321,10 +2276,6 @@
unfolding field_differentiable_def differentiable_def
using has_field_derivative_imp_has_derivative by auto
-lemma field_differentiable_derivI:
- "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
-by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
-
lemma field_differentiable_imp_continuous_at:
"f field_differentiable (at x within S) \<Longrightarrow> continuous (at x within S) f"
by (metis DERIV_continuous field_differentiable_def)
@@ -2434,12 +2385,6 @@
unfolding field_differentiable_def
by (metis at_within_open)
-lemma vector_derivative_chain_at_general:
- assumes "f differentiable at x" "g field_differentiable at (f x)"
- shows "vector_derivative (g \<circ> f) (at x) = vector_derivative f (at x) * deriv g (f x)"
- apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
- using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
-
lemma exp_scaleR_has_vector_derivative_right:
"((\<lambda>t. exp (t *\<^sub>R A)) has_vector_derivative exp (t *\<^sub>R A) * A) (at t within T)"
unfolding has_vector_derivative_def
@@ -2515,11 +2460,72 @@
using exp_scaleR_has_vector_derivative_right[of A t]
by (simp add: exp_times_scaleR_commute)
+subsection \<open>Field derivative\<close>
+
+definition%important deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
+ "deriv f x \<equiv> SOME D. DERIV f x :> D"
+
+lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
+ unfolding deriv_def by (metis some_equality DERIV_unique)
+
+lemma DERIV_deriv_iff_has_field_derivative:
+ "DERIV f x :> deriv f x \<longleftrightarrow> (\<exists>f'. (f has_field_derivative f') (at x))"
+ by (auto simp: has_field_derivative_def DERIV_imp_deriv)
+
+lemma DERIV_deriv_iff_real_differentiable:
+ fixes x :: real
+ shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
+ unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff)
+
+lemma deriv_cong_ev:
+ assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
+ shows "deriv f x = deriv g y"
+proof -
+ have "(\<lambda>D. (f has_field_derivative D) (at x)) = (\<lambda>D. (g has_field_derivative D) (at y))"
+ by (intro ext DERIV_cong_ev refl assms)
+ thus ?thesis by (simp add: deriv_def assms)
+qed
+
+lemma higher_deriv_cong_ev:
+ assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
+ shows "(deriv ^^ n) f x = (deriv ^^ n) g y"
+proof -
+ from assms(1) have "eventually (\<lambda>x. (deriv ^^ n) f x = (deriv ^^ n) g x) (nhds x)"
+ proof (induction n arbitrary: f g)
+ case (Suc n)
+ from Suc.prems have "eventually (\<lambda>y. eventually (\<lambda>z. f z = g z) (nhds y)) (nhds x)"
+ by (simp add: eventually_eventually)
+ hence "eventually (\<lambda>x. deriv f x = deriv g x) (nhds x)"
+ by eventually_elim (rule deriv_cong_ev, simp_all)
+ thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps)
+ qed auto
+ from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp
+qed
+
+lemma real_derivative_chain:
+ fixes x :: real
+ shows "f differentiable at x \<Longrightarrow> g differentiable at (f x)
+ \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
+ by (metis DERIV_deriv_iff_real_differentiable DERIV_chain DERIV_imp_deriv)
+lemma field_derivative_eq_vector_derivative:
+ "(deriv f x) = vector_derivative f (at x)"
+by (simp add: mult.commute deriv_def vector_derivative_def has_vector_derivative_def has_field_derivative_def)
+
+proposition field_differentiable_derivI:
+ "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
+by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
+
+lemma vector_derivative_chain_at_general:
+ assumes "f differentiable at x" "g field_differentiable at (f x)"
+ shows "vector_derivative (g \<circ> f) (at x) = vector_derivative f (at x) * deriv g (f x)"
+ apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
+ using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
+
subsection \<open>Relation between convexity and derivative\<close>
(* TODO: Generalise to real vector spaces? *)
-lemma convex_on_imp_above_tangent:
+proposition convex_on_imp_above_tangent:
assumes convex: "convex_on A f" and connected: "connected A"
assumes c: "c \<in> interior A" and x : "x \<in> A"
assumes deriv: "(f has_field_derivative f') (at c within A)"
@@ -2602,7 +2608,7 @@
by (auto intro!: exI[where x="UNIV \<times> S"] S open_Times)
qed
-lemma has_derivative_partialsI:
+proposition has_derivative_partialsI:
fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
assumes fx: "((\<lambda>x. f x y) has_derivative fx) (at x within X)"
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)"
@@ -2767,7 +2773,7 @@
qed
-subsection \<open>Differentiable case distinction\<close>
+subsection%unimportant \<open>Differentiable case distinction\<close>
lemma has_derivative_within_If_eq:
"((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within S) =
--- a/src/HOL/Analysis/Lipschitz.thy Tue Aug 28 21:08:42 2018 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy Wed Aug 29 07:50:28 2018 +0100
@@ -7,11 +7,11 @@
imports Borel_Space
begin
-definition lipschitz_on
+definition%important lipschitz_on
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))"
bundle lipschitz_syntax begin
-notation lipschitz_on ("_-lipschitz'_on" [1000])
+notation%important lipschitz_on ("_-lipschitz'_on" [1000])
end
bundle no_lipschitz_syntax begin
no_notation lipschitz_on ("_-lipschitz'_on" [1000])
@@ -103,7 +103,7 @@
qed
qed (rule lipschitz_on_nonneg[OF f])
-proposition lipschitz_on_concat_max:
+lemma lipschitz_on_concat_max:
fixes a b c::real
assumes f: "L-lipschitz_on {a .. b} f"
assumes g: "M-lipschitz_on {b .. c} g"
@@ -118,7 +118,7 @@
subsubsection \<open>Continuity\<close>
-lemma lipschitz_on_uniformly_continuous:
+proposition lipschitz_on_uniformly_continuous:
assumes "L-lipschitz_on X f"
shows "uniformly_continuous_on X f"
unfolding uniformly_continuous_on_def
@@ -132,7 +132,7 @@
by (force intro!: exI[where x="e/(L + 1)"] simp: field_simps)
qed
-lemma lipschitz_on_continuous_on:
+proposition lipschitz_on_continuous_on:
"continuous_on X f" if "L-lipschitz_on X f"
by (rule uniformly_continuous_imp_continuous[OF lipschitz_on_uniformly_continuous[OF that]])
@@ -143,7 +143,7 @@
subsubsection \<open>Differentiable functions\<close>
-lemma bounded_derivative_imp_lipschitz:
+proposition bounded_derivative_imp_lipschitz:
assumes "\<And>x. x \<in> X \<Longrightarrow> (f has_derivative f' x) (at x within X)"
assumes convex: "convex X"
assumes "\<And>x. x \<in> X \<Longrightarrow> onorm (f' x) \<le> C" "0 \<le> C"
@@ -154,7 +154,7 @@
qed fact
-subsubsection \<open>Structural introduction rules\<close>
+subsubsection%unimportant \<open>Structural introduction rules\<close>
named_theorems lipschitz_intros "structural introduction rules for Lipschitz controls"
@@ -480,7 +480,7 @@
subsection \<open>Local Lipschitz continuity (uniform for a family of functions)\<close>
-definition local_lipschitz::
+definition%important local_lipschitz::
"'a::metric_space set \<Rightarrow> 'b::metric_space set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c::metric_space) \<Rightarrow> bool"
where
"local_lipschitz T X f \<equiv> \<forall>x \<in> X. \<forall>t \<in> T.
@@ -785,7 +785,7 @@
by (auto intro: exI[where x=1])
qed
-lemma c1_implies_local_lipschitz:
+proposition c1_implies_local_lipschitz:
fixes T::"real set" and X::"'a::{banach,heine_borel} set"
and f::"real \<Rightarrow> 'a \<Rightarrow> 'a"
assumes f': "\<And>t x. t \<in> T \<Longrightarrow> x \<in> X \<Longrightarrow> (f t has_derivative blinfun_apply (f' (t, x))) (at x)"
--- a/src/HOL/Analysis/Uniform_Limit.thy Tue Aug 28 21:08:42 2018 +0200
+++ b/src/HOL/Analysis/Uniform_Limit.thy Wed Aug 29 07:50:28 2018 +0100
@@ -9,10 +9,13 @@
imports Connected Summation_Tests
begin
-definition uniformly_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> ('a \<Rightarrow> 'b) filter"
+
+subsection \<open>Definition\<close>
+
+definition%important uniformly_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> ('a \<Rightarrow> 'b) filter"
where "uniformly_on S l = (INF e:{0 <..}. principal {f. \<forall>x\<in>S. dist (f x) (l x) < e})"
-abbreviation
+abbreviation%important
"uniform_limit S f l \<equiv> filterlim f (uniformly_on S l)"
definition uniformly_convergent_on where
@@ -21,7 +24,7 @@
definition uniformly_Cauchy_on where
"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)"
-lemma uniform_limit_iff:
+proposition uniform_limit_iff:
"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)"
unfolding filterlim_iff uniformly_on_def
by (subst eventually_INF_base)
@@ -64,7 +67,10 @@
by eventually_elim force
qed
-lemma swap_uniform_limit:
+
+subsection \<open>Exchange limits\<close>
+
+proposition swap_uniform_limit:
assumes f: "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) (at x within S)"
assumes g: "(g \<longlongrightarrow> l) F"
assumes uc: "uniform_limit S f h F"
@@ -108,6 +114,9 @@
using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
qed
+
+subsection \<open>Uniform limit theorem\<close>
+
lemma tendsto_uniform_limitI:
assumes "uniform_limit S f l F"
assumes "x \<in> S"
@@ -115,7 +124,7 @@
using assms
by (auto intro!: tendstoI simp: eventually_mono dest!: uniform_limitD)
-lemma uniform_limit_theorem:
+theorem uniform_limit_theorem:
assumes c: "\<forall>\<^sub>F n in F. continuous_on A (f n)"
assumes ul: "uniform_limit A f l F"
assumes "\<not> trivial_limit F"
@@ -307,7 +316,10 @@
unfolding uniformly_convergent_on_def convergent_def
by (auto dest: tendsto_uniform_limitI)
-lemma weierstrass_m_test_ev:
+
+subsection \<open>Weierstrass M-Test\<close>
+
+proposition weierstrass_m_test_ev:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially"
assumes "summable M"
@@ -354,7 +366,7 @@
qed
text\<open>Alternative version, formulated as in HOL Light\<close>
-corollary series_comparison_uniform:
+corollary%unimportant series_comparison_uniform:
fixes f :: "_ \<Rightarrow> nat \<Rightarrow> _ :: banach"
assumes g: "summable g" and le: "\<And>n x. N \<le> n \<and> x \<in> A \<Longrightarrow> norm(f x n) \<le> g n"
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)"
@@ -367,20 +379,20 @@
done
qed
-corollary weierstrass_m_test:
+corollary%unimportant weierstrass_m_test:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
assumes "summable M"
shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
using assms by (intro weierstrass_m_test_ev always_eventually) auto
-corollary weierstrass_m_test'_ev:
+corollary%unimportant weierstrass_m_test'_ev:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially" "summable M"
shows "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test_ev[OF assms])
-corollary weierstrass_m_test':
+corollary%unimportant weierstrass_m_test':
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n" "summable M"
shows "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
@@ -389,6 +401,9 @@
lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
by simp
+
+subsection%unimportant \<open>Structural introduction rules\<close>
+
named_theorems uniform_limit_intros "introduction rules for uniform_limit"
setup \<open>
Global_Theory.add_thms_dynamic (@{binding uniform_limit_eq_intros},