--- a/src/HOL/Finite_Set.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Finite_Set.thy Mon Oct 26 23:41:27 2015 +0000
@@ -1545,6 +1545,10 @@
apply(auto simp add: intro:ccontr)
done
+lemma card_1_singletonE:
+ assumes "card A = 1" obtains x where "A = {x}"
+ using assms by (auto simp: card_Suc_eq)
+
lemma card_le_Suc_iff: "finite A \<Longrightarrow>
Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
--- a/src/HOL/Library/Convex.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Library/Convex.thy Mon Oct 26 23:41:27 2015 +0000
@@ -96,7 +96,7 @@
lemma convex_halfspace_gt: "convex {x. inner a x > b}"
using convex_halfspace_lt[of "-a" "-b"] by auto
-lemma convex_real_interval:
+lemma convex_real_interval [iff]:
fixes a b :: "real"
shows "convex {a..}" and "convex {..b}"
and "convex {a<..}" and "convex {..<b}"
--- a/src/HOL/Library/Inner_Product.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Library/Inner_Product.thy Mon Oct 26 23:41:27 2015 +0000
@@ -81,6 +81,20 @@
lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"
by (simp add: norm_eq_sqrt_inner)
+text \<open>Identities involving real multiplication and division.\<close>
+
+lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)"
+ by (metis real_inner_class.inner_scaleR_left scaleR_conv_of_real)
+
+lemma inner_mult_right: "inner a (of_real m * b) = m * (inner a b)"
+ by (metis real_inner_class.inner_scaleR_right scaleR_conv_of_real)
+
+lemma inner_mult_left': "inner (a * of_real m) b = m * (inner a b)"
+ by (simp add: of_real_def)
+
+lemma inner_mult_right': "inner a (b * of_real m) = (inner a b) * m"
+ by (simp add: of_real_def real_inner_class.inner_scaleR_right)
+
lemma Cauchy_Schwarz_ineq:
"(inner x y)\<^sup>2 \<le> inner x x * inner y y"
proof (cases)
@@ -141,6 +155,16 @@
end
+lemma inner_divide_left:
+ fixes a :: "'a :: {real_inner,real_div_algebra}"
+ shows "inner (a / of_real m) b = (inner a b) / m"
+ by (metis (no_types) divide_inverse inner_commute inner_scaleR_right mult.left_neutral mult.right_neutral mult_scaleR_right of_real_inverse scaleR_conv_of_real times_divide_eq_left)
+
+lemma inner_divide_right:
+ fixes a :: "'a :: {real_inner,real_div_algebra}"
+ shows "inner a (b / of_real m) = (inner a b) / m"
+ by (metis inner_commute inner_divide_left)
+
text \<open>
Re-enable constraints for @{term "open"},
@{term dist}, and @{term norm}.
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Oct 26 23:41:27 2015 +0000
@@ -2484,7 +2484,7 @@
shows "convex hull {a,b,c} \<subseteq> s"
using s
apply (clarsimp simp add: convex_hull_insert [of "{b,c}" a] segment_convex_hull)
- apply (meson subs convexD convex_segment ends_in_segment(1) ends_in_segment(2) subsetCE)
+ apply (meson subs convexD convex_closed_segment ends_in_segment(1) ends_in_segment(2) subsetCE)
done
lemma triangle_path_integrals_starlike_primitive:
@@ -3096,7 +3096,6 @@
using path_integral_nearby [OF assms, where Ends=False]
by simp_all
- thm has_vector_derivative_polynomial_function
corollary differentiable_polynomial_function:
fixes p :: "real \<Rightarrow> 'a::euclidean_space"
shows "polynomial_function p \<Longrightarrow> p differentiable_on s"
@@ -3112,6 +3111,11 @@
shows "polynomial_function p \<Longrightarrow> valid_path p"
by (force simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_polymonial_function C1_differentiable_polynomial_function)
+lemma valid_path_subpath_trivial [simp]:
+ fixes g :: "real \<Rightarrow> 'a::euclidean_space"
+ shows "z \<noteq> g x \<Longrightarrow> valid_path (subpath x x g)"
+ by (simp add: subpath_def valid_path_polynomial_function)
+
lemma path_integral_bound_exists:
assumes s: "open s"
and g: "valid_path g"
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Oct 26 23:41:27 2015 +0000
@@ -1083,7 +1083,7 @@
also have "... \<le> B * cmod (z - w) ^ n / (fact n) * cmod (w - z)"
apply (rule complex_differentiable_bound
[where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
- and s = "closed_segment w z", OF convex_segment])
+ and s = "closed_segment w z", OF convex_closed_segment])
apply (auto simp: ends_in_segment real_of_nat_def DERIV_subset [OF sum_deriv wzs]
norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
done
@@ -1096,7 +1096,7 @@
lemma complex_mvt_line:
assumes "\<And>u. u \<in> closed_segment w z \<Longrightarrow> (f has_field_derivative f'(u)) (at u)"
- shows "\<exists>u. u \<in> open_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
+ shows "\<exists>u. u \<in> closed_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
proof -
have twz: "\<And>t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)"
by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
@@ -1107,11 +1107,10 @@
"\<lambda>u. Re o (\<lambda>h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\<lambda>t. t *\<^sub>R (z - w))"])
apply auto
apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
- apply (auto simp add: open_segment_def twz) []
- apply (intro derivative_eq_intros has_derivative_at_within)
- apply simp_all
+ apply (auto simp: closed_segment_def twz) []
+ apply (intro derivative_eq_intros has_derivative_at_within, simp_all)
apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
- apply (force simp add: twz closed_segment_def)
+ apply (force simp: twz closed_segment_def)
done
qed
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Oct 26 23:41:27 2015 +0000
@@ -464,7 +464,7 @@
"norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
show "convex (closed_segment 0 z)"
- by (rule convex_segment [of 0 z])
+ by (rule convex_closed_segment [of 0 z])
next
fix k x
assume "x \<in> closed_segment 0 z" "k \<le> n"
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Oct 26 23:41:27 2015 +0000
@@ -17,10 +17,10 @@
(* To be moved elsewhere *)
(* ------------------------------------------------------------------------- *)
-lemma linear_scaleR: "linear (\<lambda>x. scaleR c x)"
+lemma linear_scaleR [simp]: "linear (\<lambda>x. scaleR c x)"
by (simp add: linear_iff scaleR_add_right)
-lemma linear_scaleR_left: "linear (\<lambda>r. scaleR r x)"
+lemma linear_scaleR_left [simp]: "linear (\<lambda>r. scaleR r x)"
by (simp add: linear_iff scaleR_add_left)
lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x::'a::real_vector. scaleR c x)"
@@ -259,33 +259,62 @@
by blast
qed
-lemma closure_bounded_linear_image:
+lemma closure_bounded_linear_image_subset:
assumes f: "bounded_linear f"
shows "f ` closure S \<subseteq> closure (f ` S)"
using linear_continuous_on [OF f] closed_closure closure_subset
by (rule image_closure_subset)
-lemma closure_linear_image:
+lemma closure_linear_image_subset:
fixes f :: "'m::euclidean_space \<Rightarrow> 'n::real_normed_vector"
assumes "linear f"
- shows "f ` (closure S) \<le> closure (f ` S)"
+ shows "f ` (closure S) \<subseteq> closure (f ` S)"
using assms unfolding linear_conv_bounded_linear
- by (rule closure_bounded_linear_image)
+ by (rule closure_bounded_linear_image_subset)
+
+lemma closed_injective_linear_image:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes S: "closed S" and f: "linear f" "inj f"
+ shows "closed (f ` S)"
+proof -
+ obtain g where g: "linear g" "g \<circ> f = id"
+ using linear_injective_left_inverse [OF f] by blast
+ then have confg: "continuous_on (range f) g"
+ using linear_continuous_on linear_conv_bounded_linear by blast
+ have [simp]: "g ` f ` S = S"
+ using g by (simp add: image_comp)
+ have cgf: "closed (g ` f ` S)"
+ by (simp add: `g \<circ> f = id` S image_comp)
+ have [simp]: "{x \<in> range f. g x \<in> S} = f ` S"
+ using g by (simp add: o_def id_def image_def) metis
+ show ?thesis
+ apply (rule closedin_closed_trans [of "range f"])
+ apply (rule continuous_closedin_preimage [OF confg cgf, simplified])
+ apply (rule closed_injective_image_subspace)
+ using f
+ apply (auto simp: linear_linear linear_injective_0)
+ done
+qed
+
+lemma closed_injective_linear_image_eq:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes f: "linear f" "inj f"
+ shows "(closed(image f s) \<longleftrightarrow> closed s)"
+ by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff)
lemma closure_injective_linear_image:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'n::euclidean_space"
- assumes "linear f" "inj f"
- shows "f ` (closure S) = closure (f ` S)"
-proof -
- obtain f' where f': "linear f' \<and> f \<circ> f' = id \<and> f' \<circ> f = id"
- using assms linear_injective_isomorphism[of f] isomorphism_expand by auto
- then have "f' ` closure (f ` S) \<le> closure (S)"
- using closure_linear_image[of f' "f ` S"] image_comp[of f' f] by auto
- then have "f ` f' ` closure (f ` S) \<le> f ` closure S" by auto
- then have "closure (f ` S) \<le> f ` closure S"
- using image_comp[of f f' "closure (f ` S)"] f' by auto
- then show ?thesis using closure_linear_image[of f S] assms by auto
-qed
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
+ apply (rule subset_antisym)
+ apply (simp add: closure_linear_image_subset)
+ by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono)
+
+lemma closure_bounded_linear_image:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "\<lbrakk>linear f; bounded S\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
+ apply (rule subset_antisym, simp add: closure_linear_image_subset)
+ apply (rule closure_minimal, simp add: closure_subset image_mono)
+ by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear)
lemma closure_scaleR:
fixes S :: "'a::real_normed_vector set"
@@ -293,7 +322,7 @@
proof
show "(op *\<^sub>R c) ` (closure S) \<subseteq> closure ((op *\<^sub>R c) ` S)"
using bounded_linear_scaleR_right
- by (rule closure_bounded_linear_image)
+ by (rule closure_bounded_linear_image_subset)
show "closure ((op *\<^sub>R c) ` S) \<subseteq> (op *\<^sub>R c) ` (closure S)"
by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
qed
@@ -1422,12 +1451,12 @@
then show ?thesis by (auto simp add: convex_def Ball_def)
qed
-lemma connected_ball:
+lemma connected_ball [iff]:
fixes x :: "'a::real_normed_vector"
shows "connected (ball x e)"
using convex_connected convex_ball by auto
-lemma connected_cball:
+lemma connected_cball [iff]:
fixes x :: "'a::real_normed_vector"
shows "connected (cball x e)"
using convex_connected convex_cball by auto
@@ -2212,140 +2241,6 @@
qed
-subsection \<open>Caratheodory's theorem.\<close>
-
-lemma convex_hull_caratheodory:
- fixes p :: "('a::euclidean_space) set"
- shows "convex hull p =
- {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and>
- (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
- unfolding convex_hull_explicit set_eq_iff mem_Collect_eq
-proof (rule, rule)
- fix y
- let ?P = "\<lambda>n. \<exists>s u. finite s \<and> card s = n \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and>
- setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
- assume "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
- then obtain N where "?P N" by auto
- then have "\<exists>n\<le>N. (\<forall>k<n. \<not> ?P k) \<and> ?P n"
- apply (rule_tac ex_least_nat_le)
- apply auto
- done
- then obtain n where "?P n" and smallest: "\<forall>k<n. \<not> ?P k"
- by blast
- then obtain s u where obt: "finite s" "card s = n" "s\<subseteq>p" "\<forall>x\<in>s. 0 \<le> u x"
- "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
-
- have "card s \<le> DIM('a) + 1"
- proof (rule ccontr, simp only: not_le)
- assume "DIM('a) + 1 < card s"
- then have "affine_dependent s"
- using affine_dependent_biggerset[OF obt(1)] by auto
- then obtain w v where wv: "setsum w s = 0" "v\<in>s" "w v \<noteq> 0" "(\<Sum>v\<in>s. w v *\<^sub>R v) = 0"
- using affine_dependent_explicit_finite[OF obt(1)] by auto
- def i \<equiv> "(\<lambda>v. (u v) / (- w v)) ` {v\<in>s. w v < 0}"
- def t \<equiv> "Min i"
- have "\<exists>x\<in>s. w x < 0"
- proof (rule ccontr, simp add: not_less)
- assume as:"\<forall>x\<in>s. 0 \<le> w x"
- then have "setsum w (s - {v}) \<ge> 0"
- apply (rule_tac setsum_nonneg)
- apply auto
- done
- then have "setsum w s > 0"
- unfolding setsum.remove[OF obt(1) \<open>v\<in>s\<close>]
- using as[THEN bspec[where x=v]] and \<open>v\<in>s\<close>
- using \<open>w v \<noteq> 0\<close>
- by auto
- then show False using wv(1) by auto
- qed
- then have "i \<noteq> {}" unfolding i_def by auto
-
- then have "t \<ge> 0"
- using Min_ge_iff[of i 0 ] and obt(1)
- unfolding t_def i_def
- using obt(4)[unfolded le_less]
- by (auto simp: divide_le_0_iff)
- have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
- proof
- fix v
- assume "v \<in> s"
- then have v: "0 \<le> u v"
- using obt(4)[THEN bspec[where x=v]] by auto
- show "0 \<le> u v + t * w v"
- proof (cases "w v < 0")
- case False
- thus ?thesis using v \<open>t\<ge>0\<close> by auto
- next
- case True
- then have "t \<le> u v / (- w v)"
- using \<open>v\<in>s\<close>
- unfolding t_def i_def
- apply (rule_tac Min_le)
- using obt(1)
- apply auto
- done
- then show ?thesis
- unfolding real_0_le_add_iff
- using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[symmetric]]]
- by auto
- qed
- qed
-
- obtain a where "a \<in> s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
- using Min_in[OF _ \<open>i\<noteq>{}\<close>] and obt(1) unfolding i_def t_def by auto
- then have a: "a \<in> s" "u a + t * w a = 0" by auto
- have *: "\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
- unfolding setsum.remove[OF obt(1) \<open>a\<in>s\<close>] by auto
- have "(\<Sum>v\<in>s. u v + t * w v) = 1"
- unfolding setsum.distrib wv(1) setsum_right_distrib[symmetric] obt(5) by auto
- moreover have "(\<Sum>v\<in>s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y"
- unfolding setsum.distrib obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4)
- using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp
- ultimately have "?P (n - 1)"
- apply (rule_tac x="(s - {a})" in exI)
- apply (rule_tac x="\<lambda>v. u v + t * w v" in exI)
- using obt(1-3) and t and a
- apply (auto simp add: * scaleR_left_distrib)
- done
- then show False
- using smallest[THEN spec[where x="n - 1"]] by auto
- qed
- then show "\<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and>
- (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
- using obt by auto
-qed auto
-
-lemma caratheodory:
- "convex hull p =
- {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
- card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
- unfolding set_eq_iff
- apply rule
- apply rule
- unfolding mem_Collect_eq
-proof -
- fix x
- assume "x \<in> convex hull p"
- then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
- "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
- unfolding convex_hull_caratheodory by auto
- then show "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
- apply (rule_tac x=s in exI)
- using hull_subset[of s convex]
- using convex_convex_hull[unfolded convex_explicit, of s,
- THEN spec[where x=s], THEN spec[where x=u]]
- apply auto
- done
-next
- fix x
- assume "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
- then obtain s where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1" "x \<in> convex hull s"
- by auto
- then show "x \<in> convex hull p"
- using hull_mono[OF \<open>s\<subseteq>p\<close>] by auto
-qed
-
-
subsection \<open>Some Properties of Affine Dependent Sets\<close>
lemma affine_independent_empty: "\<not> affine_dependent {}"
@@ -2572,7 +2467,8 @@
subsection \<open>Affine Dimension of a Set\<close>
-definition "aff_dim V =
+definition aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
+ where "aff_dim V =
(SOME d :: int.
\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)"
@@ -2782,6 +2678,9 @@
using aff_independent_finite[of B] card_gt_0_iff[of B] by auto
qed
+lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1"
+ by (simp add: aff_dim_empty [symmetric])
+
lemma aff_dim_affine_hull: "aff_dim (affine hull S) = aff_dim S"
unfolding aff_dim_def using hull_hull[of _ S] by auto
@@ -2829,6 +2728,13 @@
shows "of_nat (card B) = aff_dim B + 1"
using aff_dim_unique[of B B] assms by auto
+lemma affine_independent_iff_card:
+ fixes s :: "'a::euclidean_space set"
+ shows "~ affine_dependent s \<longleftrightarrow> finite s \<and> aff_dim s = int(card s) - 1"
+ apply (rule iffI)
+ apply (simp add: aff_dim_affine_independent aff_independent_finite)
+ by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff)
+
lemma aff_dim_sing:
fixes a :: "'n::euclidean_space"
shows "aff_dim {a} = 0"
@@ -3136,6 +3042,165 @@
shows "dim S < DIM ('n) \<Longrightarrow> interior S = {}"
by (metis low_dim_interior affine_hull_univ dim_affine_hull less_not_refl dim_UNIV)
+subsection \<open>Caratheodory's theorem.\<close>
+
+lemma convex_hull_caratheodory_aff_dim:
+ fixes p :: "('a::euclidean_space) set"
+ shows "convex hull p =
+ {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> aff_dim p + 1 \<and>
+ (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
+ unfolding convex_hull_explicit set_eq_iff mem_Collect_eq
+proof (intro allI iffI)
+ fix y
+ let ?P = "\<lambda>n. \<exists>s u. finite s \<and> card s = n \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and>
+ setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
+ assume "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
+ then obtain N where "?P N" by auto
+ then have "\<exists>n\<le>N. (\<forall>k<n. \<not> ?P k) \<and> ?P n"
+ apply (rule_tac ex_least_nat_le)
+ apply auto
+ done
+ then obtain n where "?P n" and smallest: "\<forall>k<n. \<not> ?P k"
+ by blast
+ then obtain s u where obt: "finite s" "card s = n" "s\<subseteq>p" "\<forall>x\<in>s. 0 \<le> u x"
+ "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
+
+ have "card s \<le> aff_dim p + 1"
+ proof (rule ccontr, simp only: not_le)
+ assume "aff_dim p + 1 < card s"
+ then have "affine_dependent s"
+ using affine_dependent_biggerset[OF obt(1)] independent_card_le_aff_dim not_less obt(3)
+ by blast
+ then obtain w v where wv: "setsum w s = 0" "v\<in>s" "w v \<noteq> 0" "(\<Sum>v\<in>s. w v *\<^sub>R v) = 0"
+ using affine_dependent_explicit_finite[OF obt(1)] by auto
+ def i \<equiv> "(\<lambda>v. (u v) / (- w v)) ` {v\<in>s. w v < 0}"
+ def t \<equiv> "Min i"
+ have "\<exists>x\<in>s. w x < 0"
+ proof (rule ccontr, simp add: not_less)
+ assume as:"\<forall>x\<in>s. 0 \<le> w x"
+ then have "setsum w (s - {v}) \<ge> 0"
+ apply (rule_tac setsum_nonneg)
+ apply auto
+ done
+ then have "setsum w s > 0"
+ unfolding setsum.remove[OF obt(1) \<open>v\<in>s\<close>]
+ using as[THEN bspec[where x=v]] \<open>v\<in>s\<close> \<open>w v \<noteq> 0\<close> by auto
+ then show False using wv(1) by auto
+ qed
+ then have "i \<noteq> {}" unfolding i_def by auto
+ then have "t \<ge> 0"
+ using Min_ge_iff[of i 0 ] and obt(1)
+ unfolding t_def i_def
+ using obt(4)[unfolded le_less]
+ by (auto simp: divide_le_0_iff)
+ have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
+ proof
+ fix v
+ assume "v \<in> s"
+ then have v: "0 \<le> u v"
+ using obt(4)[THEN bspec[where x=v]] by auto
+ show "0 \<le> u v + t * w v"
+ proof (cases "w v < 0")
+ case False
+ thus ?thesis using v \<open>t\<ge>0\<close> by auto
+ next
+ case True
+ then have "t \<le> u v / (- w v)"
+ using \<open>v\<in>s\<close> unfolding t_def i_def
+ apply (rule_tac Min_le)
+ using obt(1) apply auto
+ done
+ then show ?thesis
+ unfolding real_0_le_add_iff
+ using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[symmetric]]]
+ by auto
+ qed
+ qed
+ obtain a where "a \<in> s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
+ using Min_in[OF _ \<open>i\<noteq>{}\<close>] and obt(1) unfolding i_def t_def by auto
+ then have a: "a \<in> s" "u a + t * w a = 0" by auto
+ have *: "\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
+ unfolding setsum.remove[OF obt(1) \<open>a\<in>s\<close>] by auto
+ have "(\<Sum>v\<in>s. u v + t * w v) = 1"
+ unfolding setsum.distrib wv(1) setsum_right_distrib[symmetric] obt(5) by auto
+ moreover have "(\<Sum>v\<in>s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y"
+ unfolding setsum.distrib obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4)
+ using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp
+ ultimately have "?P (n - 1)"
+ apply (rule_tac x="(s - {a})" in exI)
+ apply (rule_tac x="\<lambda>v. u v + t * w v" in exI)
+ using obt(1-3) and t and a
+ apply (auto simp add: * scaleR_left_distrib)
+ done
+ then show False
+ using smallest[THEN spec[where x="n - 1"]] by auto
+ qed
+ then show "\<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> aff_dim p + 1 \<and>
+ (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
+ using obt by auto
+qed auto
+
+lemma caratheodory_aff_dim:
+ fixes p :: "('a::euclidean_space) set"
+ shows "convex hull p = {x. \<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> aff_dim p + 1 \<and> x \<in> convex hull s}"
+ (is "?lhs = ?rhs")
+proof
+ show "?lhs \<subseteq> ?rhs"
+ apply (subst convex_hull_caratheodory_aff_dim)
+ apply clarify
+ apply (rule_tac x="s" in exI)
+ apply (simp add: hull_subset convex_explicit [THEN iffD1, OF convex_convex_hull])
+ done
+next
+ show "?rhs \<subseteq> ?lhs"
+ using hull_mono by blast
+qed
+
+lemma convex_hull_caratheodory:
+ fixes p :: "('a::euclidean_space) set"
+ shows "convex hull p =
+ {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and>
+ (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
+ (is "?lhs = ?rhs")
+proof (intro set_eqI iffI)
+ fix x
+ assume "x \<in> ?lhs" then show "x \<in> ?rhs"
+ apply (simp only: convex_hull_caratheodory_aff_dim Set.mem_Collect_eq)
+ apply (erule ex_forward)+
+ using aff_dim_subset_univ [of p]
+ apply simp
+ done
+next
+ fix x
+ assume "x \<in> ?rhs" then show "x \<in> ?lhs"
+ by (auto simp add: convex_hull_explicit)
+qed
+
+theorem caratheodory:
+ "convex hull p =
+ {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
+ card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
+proof safe
+ fix x
+ assume "x \<in> convex hull p"
+ then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
+ "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
+ unfolding convex_hull_caratheodory by auto
+ then show "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
+ apply (rule_tac x=s in exI)
+ using hull_subset[of s convex]
+ using convex_convex_hull[unfolded convex_explicit, of s,
+ THEN spec[where x=s], THEN spec[where x=u]]
+ apply auto
+ done
+next
+ fix x s
+ assume "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1" "x \<in> convex hull s"
+ then show "x \<in> convex hull p"
+ using hull_mono[OF \<open>s\<subseteq>p\<close>] by auto
+qed
+
+
subsection \<open>Relative interior of a set\<close>
definition "rel_interior S =
@@ -5708,20 +5773,33 @@
shows "is_interval s \<longleftrightarrow> convex s"
by (metis is_interval_convex convex_connected is_interval_connected_1)
-lemma convex_connected_1:
+lemma connected_convex_1:
fixes s :: "real set"
shows "connected s \<longleftrightarrow> convex s"
by (metis is_interval_convex convex_connected is_interval_connected_1)
+lemma connected_convex_1_gen:
+ fixes s :: "'a :: euclidean_space set"
+ assumes "DIM('a) = 1"
+ shows "connected s \<longleftrightarrow> convex s"
+proof -
+ obtain f:: "'a \<Rightarrow> real" where linf: "linear f" and "inj f"
+ using subspace_isomorphism [where 'a = 'a and 'b = real]
+ by (metis DIM_real dim_UNIV subspace_UNIV assms)
+ then have "f -` (f ` s) = s"
+ by (simp add: inj_vimage_image_eq)
+ then show ?thesis
+ by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image)
+qed
subsection \<open>Another intermediate value theorem formulation\<close>
lemma ivt_increasing_component_on_1:
- fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+ fixes f :: "real \<Rightarrow> 'a::euclidean_space"
assumes "a \<le> b"
- and "continuous_on (cbox a b) f"
+ and "continuous_on {a..b} f"
and "(f a)\<bullet>k \<le> y" "y \<le> (f b)\<bullet>k"
- shows "\<exists>x\<in>cbox a b. (f x)\<bullet>k = y"
+ shows "\<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
proof -
have "f a \<in> f ` cbox a b" "f b \<in> f ` cbox a b"
apply (rule_tac[!] imageI)
@@ -5730,24 +5808,22 @@
done
then show ?thesis
using connected_ivt_component[of "f ` cbox a b" "f a" "f b" k y]
- using connected_continuous_image[OF assms(2) convex_connected[OF convex_box(1)]]
- using assms
- by auto
+ by (simp add: Topology_Euclidean_Space.connected_continuous_image assms)
qed
lemma ivt_increasing_component_1:
fixes f :: "real \<Rightarrow> 'a::euclidean_space"
- shows "a \<le> b \<Longrightarrow> \<forall>x\<in>cbox a b. continuous (at x) f \<Longrightarrow>
- f a\<bullet>k \<le> y \<Longrightarrow> y \<le> f b\<bullet>k \<Longrightarrow> \<exists>x\<in>cbox a b. (f x)\<bullet>k = y"
+ shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a..b}. continuous (at x) f \<Longrightarrow>
+ f a\<bullet>k \<le> y \<Longrightarrow> y \<le> f b\<bullet>k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
by (rule ivt_increasing_component_on_1) (auto simp add: continuous_at_imp_continuous_on)
lemma ivt_decreasing_component_on_1:
fixes f :: "real \<Rightarrow> 'a::euclidean_space"
assumes "a \<le> b"
- and "continuous_on (cbox a b) f"
+ and "continuous_on {a..b} f"
and "(f b)\<bullet>k \<le> y"
and "y \<le> (f a)\<bullet>k"
- shows "\<exists>x\<in>cbox a b. (f x)\<bullet>k = y"
+ shows "\<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
apply (subst neg_equal_iff_equal[symmetric])
using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"]
using assms using continuous_on_minus
@@ -5756,8 +5832,8 @@
lemma ivt_decreasing_component_1:
fixes f :: "real \<Rightarrow> 'a::euclidean_space"
- shows "a \<le> b \<Longrightarrow> \<forall>x\<in>cbox a b. continuous (at x) f \<Longrightarrow>
- f b\<bullet>k \<le> y \<Longrightarrow> y \<le> f a\<bullet>k \<Longrightarrow> \<exists>x\<in>cbox a b. (f x)\<bullet>k = y"
+ shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a..b}. continuous (at x) f \<Longrightarrow>
+ f b\<bullet>k \<le> y \<Longrightarrow> y \<le> f a\<bullet>k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
by (rule ivt_decreasing_component_on_1) (auto simp: continuous_at_imp_continuous_on)
@@ -6234,12 +6310,12 @@
definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
-definition open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
- where "open_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 < u \<and> u < 1}"
-
definition closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
+definition open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
+ "open_segment a b \<equiv> closed_segment a b - {a,b}"
+
definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
lemmas segment = open_segment_def closed_segment_def
@@ -6291,7 +6367,7 @@
apply (simp add: scaleR_2)
done
show ?t3
- unfolding midpoint_def dist_norm
+ unfolding midpoint_def dist_norm
apply (rule *)
apply (simp add: scaleR_right_diff_distrib)
apply (simp add: scaleR_2)
@@ -6325,37 +6401,28 @@
"closed_segment a b = convex hull {a,b}"
proof -
have *: "\<And>x. {x} \<noteq> {}" by auto
- have **: "\<And>u v. u + v = 1 \<longleftrightarrow> u = 1 - (v::real)" by auto
show ?thesis
unfolding segment convex_hull_insert[OF *] convex_hull_singleton
- apply (rule set_eqI)
- unfolding mem_Collect_eq
- apply (rule, erule exE)
- apply (rule_tac x="1 - u" in exI)
- apply rule
- defer
- apply (rule_tac x=u in exI)
- defer
- apply (elim exE conjE)
- apply (rule_tac x="1 - u" in exI)
- unfolding **
- apply auto
- done
-qed
-
-lemma convex_segment [iff]: "convex (closed_segment a b)"
- unfolding segment_convex_hull by(rule convex_convex_hull)
-
-lemma connected_segment [iff]:
- fixes x :: "'a :: real_normed_vector"
- shows "connected (closed_segment x y)"
- by (simp add: convex_connected)
+ by (safe; rule_tac x="1 - u" in exI; force)
+qed
+
+lemma segment_open_subset_closed:
+ "open_segment a b \<subseteq> closed_segment a b"
+ by (auto simp: closed_segment_def open_segment_def)
+
+lemma bounded_closed_segment:
+ fixes a :: "'a::euclidean_space" shows "bounded (closed_segment a b)"
+ by (simp add: segment_convex_hull compact_convex_hull compact_imp_bounded)
+
+lemma bounded_open_segment:
+ fixes a :: "'a::euclidean_space" shows "bounded (open_segment a b)"
+ by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed])
+
+lemmas bounded_segment = bounded_closed_segment open_closed_segment
lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b"
unfolding segment_convex_hull
- apply (rule_tac[!] hull_subset[unfolded subset_eq, rule_format])
- apply auto
- done
+ by (auto intro!: hull_subset[unfolded subset_eq, rule_format])
lemma segment_furthest_le:
fixes a b x y :: "'a::euclidean_space"
@@ -6403,6 +6470,106 @@
fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}"
by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl)
+subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
+
+lemma segment_eq_compose:
+ fixes a :: "'a :: real_vector"
+ shows "(\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\<lambda>x. a + x) o (\<lambda>u. u *\<^sub>R (b - a))"
+ by (simp add: o_def algebra_simps)
+
+lemma segment_degen_1:
+ fixes a :: "'a :: real_vector"
+ shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1"
+proof -
+ { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b"
+ then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b"
+ by (simp add: algebra_simps)
+ then have "a=b \<or> u=1"
+ by simp
+ } then show ?thesis
+ by (auto simp: algebra_simps)
+qed
+
+lemma segment_degen_0:
+ fixes a :: "'a :: real_vector"
+ shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0"
+ using segment_degen_1 [of "1-u" b a]
+ by (auto simp: algebra_simps)
+
+lemma closed_segment_image_interval:
+ "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}"
+ by (auto simp: set_eq_iff image_iff closed_segment_def)
+
+lemma open_segment_image_interval:
+ "open_segment a b = (if a=b then {} else (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})"
+ by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1)
+
+lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval
+
+lemma closure_closed_segment [simp]:
+ fixes a :: "'a::euclidean_space"
+ shows "closure(closed_segment a b) = closed_segment a b"
+ by (simp add: closure_eq compact_imp_closed segment_convex_hull compact_convex_hull)
+
+lemma closure_open_segment [simp]:
+ fixes a :: "'a::euclidean_space"
+ shows "closure(open_segment a b) = (if a = b then {} else closed_segment a b)"
+proof -
+ have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}" if "a \<noteq> b"
+ apply (rule closure_injective_linear_image [symmetric])
+ apply (simp add:)
+ using that by (simp add: inj_on_def)
+ then show ?thesis
+ by (simp add: segment_image_interval segment_eq_compose closure_greaterThanLessThan [symmetric]
+ closure_translation image_comp [symmetric] del: closure_greaterThanLessThan)
+qed
+
+lemma closed_segment [simp]:
+ fixes a :: "'a::euclidean_space" shows "closed (closed_segment a b)"
+ using closure_subset_eq by fastforce
+
+lemma closed_open_segment_iff [simp]:
+ fixes a :: "'a::euclidean_space" shows "closed(open_segment a b) \<longleftrightarrow> a = b"
+ by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2))
+
+lemma compact_segment [simp]:
+ fixes a :: "'a::euclidean_space" shows "compact (closed_segment a b)"
+ by (simp add: compact_convex_hull segment_convex_hull)
+
+lemma compact_open_segment_iff [simp]:
+ fixes a :: "'a::euclidean_space" shows "compact(open_segment a b) \<longleftrightarrow> a = b"
+ by (simp add: bounded_open_segment compact_eq_bounded_closed)
+
+lemma convex_closed_segment [iff]: "convex (closed_segment a b)"
+ unfolding segment_convex_hull by(rule convex_convex_hull)
+
+lemma convex_open_segment [iff]: "convex(open_segment a b)"
+proof -
+ have "convex ((\<lambda>u. u *\<^sub>R (b-a)) ` {0<..<1})"
+ by (rule convex_linear_image) auto
+ then show ?thesis
+ apply (simp add: open_segment_image_interval segment_eq_compose)
+ by (metis image_comp convex_translation)
+qed
+
+lemmas convex_segment = convex_closed_segment convex_open_segment
+
+lemma connected_segment [iff]:
+ fixes x :: "'a :: real_normed_vector"
+ shows "connected (closed_segment x y)"
+ by (simp add: convex_connected)
+
+lemma affine_hull_closed_segment [simp]:
+ "affine hull (closed_segment a b) = affine hull {a,b}"
+ by (simp add: segment_convex_hull)
+
+lemma affine_hull_open_segment [simp]:
+ fixes a :: "'a::euclidean_space"
+ shows "affine hull (open_segment a b) = (if a = b then {} else affine hull {a,b})"
+by (metis affine_hull_convex_hull affine_hull_empty closure_open_segment closure_same_affine_hull segment_convex_hull)
+
+subsubsection\<open>Betweenness\<close>
+
lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
unfolding between_def by auto
@@ -6411,7 +6578,7 @@
case True
then show ?thesis
unfolding between_def split_conv
- by (auto simp add:segment_refl dist_commute)
+ by (auto simp add: dist_commute)
next
case False
then have Fal: "norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0"
@@ -7958,7 +8125,7 @@
also have "\<dots> = f ` (closure (rel_interior S))"
using convex_closure_rel_interior assms by auto
also have "\<dots> \<subseteq> closure (f ` (rel_interior S))"
- using closure_linear_image assms by auto
+ using closure_linear_image_subset assms by auto
finally have "closure (f ` S) = closure (f ` rel_interior S)"
using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
closure_mono[of "f ` rel_interior S" "f ` S"] *
@@ -8556,7 +8723,7 @@
fixes S T :: "'a::real_normed_vector set"
shows "closure S + closure T \<subseteq> closure (S + T)"
unfolding set_plus_image closure_Times [symmetric] split_def
- by (intro closure_bounded_linear_image bounded_linear_add
+ by (intro closure_bounded_linear_image_subset bounded_linear_add
bounded_linear_fst bounded_linear_snd)
lemma rel_interior_sum:
@@ -8929,11 +9096,11 @@
lemma interior_atLeastLessThan [simp]:
fixes a::real shows "interior {a..<b} = {a<..<b}"
- by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost interior_inter interior_interior interior_real_semiline)
+ by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost interior_Int interior_interior interior_real_semiline)
lemma interior_lessThanAtMost [simp]:
fixes a::real shows "interior {a<..b} = {a<..<b}"
- by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost interior_inter
+ by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost interior_Int
interior_interior interior_real_semiline)
lemma at_within_closed_interval:
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Oct 26 23:41:27 2015 +0000
@@ -24,9 +24,6 @@
by (rule netlimit_within [of a UNIV])
qed simp
-(* Because I do not want to type this all the time *)
-lemmas linear_linear = linear_conv_bounded_linear[symmetric]
-
declare has_derivative_bounded_linear[dest]
subsection \<open>Derivatives\<close>
--- a/src/HOL/Multivariate_Analysis/Integration.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Oct 26 23:41:27 2015 +0000
@@ -1211,7 +1211,7 @@
apply (rule arg_cong[of _ _ interior])
using p(8) uv by auto
also have "\<dots> = {}"
- unfolding interior_inter
+ unfolding interior_Int
apply (rule inter_interior_unions_intervals)
using p(6) p(7)[OF p(2)] p(3)
apply auto
@@ -4872,7 +4872,7 @@
"cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
have "(cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<inter> (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<subseteq> cbox m n \<inter> cbox u v"
by blast
- note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "cbox m n"]]
+ note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_Int[of "cbox m n"]]
then have "interior (cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}"
unfolding as Int_absorb by auto
then show "content (cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
@@ -7341,7 +7341,7 @@
guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = "min v v'"
have "box a ?v \<subseteq> k \<inter> k'"
unfolding v v' by (auto simp add: mem_box)
- note interior_mono[OF this,unfolded interior_inter]
+ note interior_mono[OF this,unfolded interior_Int]
moreover have "(a + ?v)/2 \<in> box a ?v"
using k(3-)
unfolding v v' content_eq_0 not_le
@@ -7372,7 +7372,7 @@
let ?v = "max v v'"
have "box ?v b \<subseteq> k \<inter> k'"
unfolding v v' by (auto simp: mem_box)
- note interior_mono[OF this,unfolded interior_inter]
+ note interior_mono[OF this,unfolded interior_Int]
moreover have " ((b + ?v)/2) \<in> box ?v b"
using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'"
@@ -8014,7 +8014,7 @@
apply (rule assms(1)[unfolded connected_clopen,rule_format])
apply rule
defer
- apply (rule continuous_closed_in_preimage[OF assms(4) closed_singleton])
+ apply (rule continuous_closedin_preimage[OF assms(4) closed_singleton])
apply (rule open_openin_trans[OF assms(2)])
unfolding open_contains_ball
proof safe
@@ -9427,7 +9427,7 @@
note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]]
from this(2)[OF as(4,1)] guess u v by (elim exE) note uv=this
have *: "interior (k \<inter> l) = {}"
- unfolding interior_inter
+ unfolding interior_Int
apply (rule q')
using as
unfolding r_def
@@ -10771,7 +10771,7 @@
proof goal_cases
case prems: (1 l y)
have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
- apply (subst(2) interior_inter)
+ apply (subst(2) interior_Int)
apply (rule Int_greatest)
defer
apply (subst prems(4))
@@ -10960,7 +10960,7 @@
from d'(4)[OF this(1)] d'(4)[OF this(2)]
guess u1 v1 u2 v2 by (elim exE) note uv=this
have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
- apply (subst interior_inter)
+ apply (subst interior_Int)
using d'(5)[OF prems(1-3)]
apply auto
done
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Oct 26 23:41:27 2015 +0000
@@ -1507,6 +1507,8 @@
show "linear f" ..
qed
+lemmas linear_linear = linear_conv_bounded_linear[symmetric]
+
lemma linear_bounded_pos:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes lf: "linear f"
--- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy Mon Oct 26 23:41:27 2015 +0000
@@ -7,6 +7,7 @@
Complex_Analysis_Basics
Bounded_Continuous_Function
Weierstrass
+ Cauchy_Integral_Thm
begin
end
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Oct 26 23:41:27 2015 +0000
@@ -576,7 +576,7 @@
by (rule ext) (auto simp: mult.commute)
-subsection\<open>Choosing a subpath of an existing path\<close>
+section\<open>Choosing a subpath of an existing path\<close>
definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
where "subpath a b g \<equiv> \<lambda>x. g((b - a) * x + a)"
@@ -747,6 +747,121 @@
lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)
+subsection\<open>There is a subpath to the frontier\<close>
+
+lemma subpath_to_frontier_explicit:
+ fixes S :: "'a::metric_space set"
+ assumes g: "path g" and "pathfinish g \<notin> S"
+ obtains u where "0 \<le> u" "u \<le> 1"
+ "\<And>x. 0 \<le> x \<and> x < u \<Longrightarrow> g x \<in> interior S"
+ "(g u \<notin> interior S)" "(u = 0 \<or> g u \<in> closure S)"
+proof -
+ have gcon: "continuous_on {0..1} g" using g by (simp add: path_def)
+ then have com: "compact ({0..1} \<inter> {u. g u \<in> closure (- S)})"
+ apply (simp add: Int_commute [of "{0..1}"] compact_eq_bounded_closed closed_vimage_Int [unfolded vimage_def])
+ using compact_eq_bounded_closed apply fastforce
+ done
+ have "1 \<in> {u. g u \<in> closure (- S)}"
+ using assms by (simp add: pathfinish_def closure_def)
+ then have dis: "{0..1} \<inter> {u. g u \<in> closure (- S)} \<noteq> {}"
+ using atLeastAtMost_iff zero_le_one by blast
+ then obtain u where "0 \<le> u" "u \<le> 1" and gu: "g u \<in> closure (- S)"
+ and umin: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; g t \<in> closure (- S)\<rbrakk> \<Longrightarrow> u \<le> t"
+ using compact_attains_inf [OF com dis] by fastforce
+ then have umin': "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; t < u\<rbrakk> \<Longrightarrow> g t \<in> S"
+ using closure_def by fastforce
+ { assume "u \<noteq> 0"
+ then have "u > 0" using `0 \<le> u` by auto
+ { fix e::real assume "e > 0"
+ obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {0..1}; dist x' u < d\<rbrakk> \<Longrightarrow> dist (g x') (g u) < e"
+ using continuous_onD [OF gcon _ `e > 0`] `0 \<le> _` `_ \<le> 1` atLeastAtMost_iff by auto
+ have *: "dist (max 0 (u - d / 2)) u < d"
+ using `0 \<le> u` `u \<le> 1` `d > 0` by (simp add: dist_real_def)
+ have "\<exists>y\<in>S. dist y (g u) < e"
+ using `0 < u` `u \<le> 1` `d > 0`
+ by (force intro: d [OF _ *] umin')
+ }
+ then have "g u \<in> closure S"
+ by (simp add: frontier_def closure_approachable)
+ }
+ then show ?thesis
+ apply (rule_tac u=u in that)
+ apply (auto simp: `0 \<le> u` `u \<le> 1` gu interior_closure umin)
+ using `_ \<le> 1` interior_closure umin apply fastforce
+ done
+qed
+
+lemma subpath_to_frontier_strong:
+ assumes g: "path g" and "pathfinish g \<notin> S"
+ obtains u where "0 \<le> u" "u \<le> 1" "g u \<notin> interior S"
+ "u = 0 \<or> (\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S) \<and> g u \<in> closure S"
+proof -
+ obtain u where "0 \<le> u" "u \<le> 1"
+ and gxin: "\<And>x. 0 \<le> x \<and> x < u \<Longrightarrow> g x \<in> interior S"
+ and gunot: "(g u \<notin> interior S)" and u0: "(u = 0 \<or> g u \<in> closure S)"
+ using subpath_to_frontier_explicit [OF assms] by blast
+ show ?thesis
+ apply (rule that [OF `0 \<le> u` `u \<le> 1`])
+ apply (simp add: gunot)
+ using `0 \<le> u` u0 by (force simp: subpath_def gxin)
+qed
+
+lemma subpath_to_frontier:
+ assumes g: "path g" and g0: "pathstart g \<in> closure S" and g1: "pathfinish g \<notin> S"
+ obtains u where "0 \<le> u" "u \<le> 1" "g u \<in> frontier S" "(path_image(subpath 0 u g) - {g u}) \<subseteq> interior S"
+proof -
+ obtain u where "0 \<le> u" "u \<le> 1"
+ and notin: "g u \<notin> interior S"
+ and disj: "u = 0 \<or>
+ (\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S) \<and> g u \<in> closure S"
+ using subpath_to_frontier_strong [OF g g1] by blast
+ show ?thesis
+ apply (rule that [OF `0 \<le> u` `u \<le> 1`])
+ apply (metis DiffI disj frontier_def g0 notin pathstart_def)
+ using `0 \<le> u` g0 disj
+ apply (simp add:)
+ apply (auto simp: closed_segment_eq_real_ivl pathstart_def pathfinish_def subpath_def)
+ apply (rename_tac y)
+ apply (drule_tac x="y/u" in spec)
+ apply (auto split: split_if_asm)
+ done
+qed
+
+lemma exists_path_subpath_to_frontier:
+ fixes S :: "'a::real_normed_vector set"
+ assumes "path g" "pathstart g \<in> closure S" "pathfinish g \<notin> S"
+ obtains h where "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g"
+ "path_image h - {pathfinish h} \<subseteq> interior S"
+ "pathfinish h \<in> frontier S"
+proof -
+ obtain u where u: "0 \<le> u" "u \<le> 1" "g u \<in> frontier S" "(path_image(subpath 0 u g) - {g u}) \<subseteq> interior S"
+ using subpath_to_frontier [OF assms] by blast
+ show ?thesis
+ apply (rule that [of "subpath 0 u g"])
+ using assms u
+ apply simp_all
+ apply (simp add: pathstart_def)
+ apply (force simp: closed_segment_eq_real_ivl path_image_def)
+ done
+qed
+
+lemma exists_path_subpath_to_frontier_closed:
+ fixes S :: "'a::real_normed_vector set"
+ assumes S: "closed S" and g: "path g" and g0: "pathstart g \<in> S" and g1: "pathfinish g \<notin> S"
+ obtains h where "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g \<inter> S"
+ "pathfinish h \<in> frontier S"
+proof -
+ obtain h where h: "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g"
+ "path_image h - {pathfinish h} \<subseteq> interior S"
+ "pathfinish h \<in> frontier S"
+ using exists_path_subpath_to_frontier [OF g _ g1] closure_closed [OF S] g0 by auto
+ show ?thesis
+ apply (rule that [OF `path h`])
+ using assms h
+ apply auto
+ apply (metis diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff)
+ done
+qed
subsection \<open>Reparametrizing a closed curve to start at some chosen point\<close>
@@ -937,7 +1052,7 @@
qed
-subsection \<open>Path component, considered as a "joinability" relation (from Tom Hales)\<close>
+section \<open>Path component, considered as a "joinability" relation (from Tom Hales)\<close>
definition "path_component s x y \<longleftrightarrow>
(\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
@@ -1079,8 +1194,8 @@
ultimately show False
using *[unfolded connected_local not_ex, rule_format,
of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"]
- using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)]
- using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)]
+ using continuous_openin_preimage[OF g(1)[unfolded path_def] as(1)]
+ using continuous_openin_preimage[OF g(1)[unfolded path_def] as(2)]
by auto
qed
@@ -1199,6 +1314,16 @@
done
qed
+lemma path_connected_segment:
+ fixes a :: "'a::real_normed_vector"
+ shows "path_connected (closed_segment a b)"
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_open_segment:
+ fixes a :: "'a::real_normed_vector"
+ shows "path_connected (open_segment a b)"
+ by (simp add: convex_imp_path_connected)
+
lemma homeomorphic_path_connectedness:
"s homeomorphic t \<Longrightarrow> path_connected s \<longleftrightarrow> path_connected t"
unfolding homeomorphic_def homeomorphism_def
@@ -1667,7 +1792,7 @@
by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq)
-subsection\<open>The "inside" and "outside" of a set\<close>
+section\<open>The "inside" and "outside" of a set\<close>
text\<open>The inside comprises the points in a bounded connected component of the set's complement.
The outside comprises the points in unbounded connected component of the complement.\<close>
@@ -1994,6 +2119,14 @@
by (metis Diff_subset assms convex_closure frontier_def outside_frontier_misses_closure
outside_subset_convex subset_antisym)
+lemma inside_frontier_eq_interior:
+ fixes s :: "'a :: {real_normed_vector, perfect_space} set"
+ shows "\<lbrakk>bounded s; convex s\<rbrakk> \<Longrightarrow> inside(frontier s) = interior s"
+ apply (simp add: inside_outside outside_frontier_eq_complement_closure)
+ using closure_subset interior_subset
+ apply (auto simp add: frontier_def)
+ done
+
lemma open_inside:
fixes s :: "'a::real_normed_vector set"
assumes "closed s"
@@ -2055,4 +2188,271 @@
by (simp add: frontier_def open_inside interior_open)
qed
+lemma closure_outside_subset:
+ fixes s :: "'a::real_normed_vector set"
+ assumes "closed s"
+ shows "closure(outside s) \<subseteq> s \<union> outside s"
+ apply (rule closure_minimal, simp)
+ by (metis assms closed_open inside_outside open_inside)
+
+lemma frontier_outside_subset:
+ fixes s :: "'a::real_normed_vector set"
+ assumes "closed s"
+ shows "frontier(outside s) \<subseteq> s"
+ apply (simp add: frontier_def open_outside interior_open)
+ by (metis Diff_subset_conv assms closure_outside_subset interior_eq open_outside sup.commute)
+
+lemma inside_complement_unbounded_connected_empty:
+ "\<lbrakk>connected (- s); \<not> bounded (- s)\<rbrakk> \<Longrightarrow> inside s = {}"
+ apply (simp add: inside_def)
+ by (meson Compl_iff bounded_subset connected_component_maximal order_refl)
+
+lemma inside_bounded_complement_connected_empty:
+ fixes s :: "'a::{real_normed_vector, perfect_space} set"
+ shows "\<lbrakk>connected (- s); bounded s\<rbrakk> \<Longrightarrow> inside s = {}"
+ by (metis inside_complement_unbounded_connected_empty cobounded_imp_unbounded)
+
+lemma inside_inside:
+ assumes "s \<subseteq> inside t"
+ shows "inside s - t \<subseteq> inside t"
+unfolding inside_def
+proof clarify
+ fix x
+ assume x: "x \<notin> t" "x \<notin> s" and bo: "bounded (connected_component_set (- s) x)"
+ show "bounded (connected_component_set (- t) x)"
+ proof (cases "s \<inter> connected_component_set (- t) x = {}")
+ case True show ?thesis
+ apply (rule bounded_subset [OF bo])
+ apply (rule connected_component_maximal)
+ using x True apply auto
+ done
+ next
+ case False then show ?thesis
+ using assms [unfolded inside_def] x
+ apply (simp add: disjoint_iff_not_equal, clarify)
+ apply (drule subsetD, assumption, auto)
+ by (metis (no_types, hide_lams) ComplI connected_component_eq_eq)
+ qed
+qed
+
+lemma inside_inside_subset: "inside(inside s) \<subseteq> s"
+ using inside_inside union_with_outside by fastforce
+
+lemma inside_outside_intersect_connected:
+ "\<lbrakk>connected t; inside s \<inter> t \<noteq> {}; outside s \<inter> t \<noteq> {}\<rbrakk> \<Longrightarrow> s \<inter> t \<noteq> {}"
+ apply (simp add: inside_def outside_def ex_in_conv [symmetric] disjoint_eq_subset_Compl, clarify)
+ by (metis (no_types, hide_lams) Compl_anti_mono connected_component_eq connected_component_maximal contra_subsetD double_compl)
+
+lemma outside_bounded_nonempty:
+ fixes s :: "'a :: {real_normed_vector, perfect_space} set"
+ assumes "bounded s" shows "outside s \<noteq> {}"
+ by (metis (no_types, lifting) Collect_empty_eq Collect_mem_eq Compl_eq_Diff_UNIV Diff_cancel
+ Diff_disjoint UNIV_I assms ball_eq_empty bounded_diff cobounded_outside convex_ball
+ double_complement order_refl outside_convex outside_def)
+
+lemma outside_compact_in_open:
+ fixes s :: "'a :: {real_normed_vector,perfect_space} set"
+ assumes s: "compact s" and t: "open t" and "s \<subseteq> t" "t \<noteq> {}"
+ shows "outside s \<inter> t \<noteq> {}"
+proof -
+ have "outside s \<noteq> {}"
+ by (simp add: compact_imp_bounded outside_bounded_nonempty s)
+ with assms obtain a b where a: "a \<in> outside s" and b: "b \<in> t" by auto
+ show ?thesis
+ proof (cases "a \<in> t")
+ case True with a show ?thesis by blast
+ next
+ case False
+ have front: "frontier t \<subseteq> - s"
+ using `s \<subseteq> t` frontier_disjoint_eq t by auto
+ { fix \<gamma>
+ assume "path \<gamma>" and pimg_sbs: "path_image \<gamma> - {pathfinish \<gamma>} \<subseteq> interior (- t)"
+ and pf: "pathfinish \<gamma> \<in> frontier t" and ps: "pathstart \<gamma> = a"
+ def c \<equiv> "pathfinish \<gamma>"
+ have "c \<in> -s" unfolding c_def using front pf by blast
+ moreover have "open (-s)" using s compact_imp_closed by blast
+ ultimately obtain \<epsilon>::real where "\<epsilon> > 0" and \<epsilon>: "cball c \<epsilon> \<subseteq> -s"
+ using open_contains_cball[of "-s"] s by blast
+ then obtain d where "d \<in> t" and d: "dist d c < \<epsilon>"
+ using closure_approachable [of c t] pf unfolding c_def
+ by (metis Diff_iff frontier_def)
+ then have "d \<in> -s" using \<epsilon>
+ using dist_commute by (metis contra_subsetD mem_cball not_le not_less_iff_gr_or_eq)
+ have pimg_sbs_cos: "path_image \<gamma> \<subseteq> -s"
+ using pimg_sbs apply (auto simp: path_image_def)
+ apply (drule subsetD)
+ using `c \<in> - s` `s \<subseteq> t` interior_subset apply (auto simp: c_def)
+ done
+ have "closed_segment c d \<le> cball c \<epsilon>"
+ apply (simp add: segment_convex_hull)
+ apply (rule hull_minimal)
+ using `\<epsilon> > 0` d apply (auto simp: dist_commute)
+ done
+ with \<epsilon> have "closed_segment c d \<subseteq> -s" by blast
+ moreover have con_gcd: "connected (path_image \<gamma> \<union> closed_segment c d)"
+ by (rule connected_Un) (auto simp: c_def `path \<gamma>` connected_path_image)
+ ultimately have "connected_component (- s) a d"
+ unfolding connected_component_def using pimg_sbs_cos ps by blast
+ then have "outside s \<inter> t \<noteq> {}"
+ using outside_same_component [OF _ a] by (metis IntI `d \<in> t` empty_iff)
+ } note * = this
+ have pal: "pathstart (linepath a b) \<in> closure (- t)"
+ by (auto simp: False closure_def)
+ show ?thesis
+ by (rule exists_path_subpath_to_frontier [OF path_linepath pal _ *]) (auto simp: b)
+ qed
+qed
+
+lemma inside_inside_compact_connected:
+ fixes s :: "'a :: euclidean_space set"
+ assumes s: "closed s" and t: "compact t" and "connected t" "s \<subseteq> inside t"
+ shows "inside s \<subseteq> inside t"
+proof (cases "inside t = {}")
+ case True with assms show ?thesis by auto
+next
+ case False
+ consider "DIM('a) = 1" | "DIM('a) \<ge> 2"
+ using antisym not_less_eq_eq by fastforce
+ then show ?thesis
+ proof cases
+ case 1 then show ?thesis
+ using connected_convex_1_gen assms False inside_convex by blast
+ next
+ case 2
+ have coms: "compact s"
+ using assms apply (simp add: s compact_eq_bounded_closed)
+ by (meson bounded_inside bounded_subset compact_imp_bounded)
+ then have bst: "bounded (s \<union> t)"
+ by (simp add: compact_imp_bounded t)
+ then obtain r where "0 < r" and r: "s \<union> t \<subseteq> ball 0 r"
+ using bounded_subset_ballD by blast
+ have outst: "outside s \<inter> outside t \<noteq> {}"
+ proof -
+ have "- ball 0 r \<subseteq> outside s"
+ apply (rule outside_subset_convex)
+ using r by auto
+ moreover have "- ball 0 r \<subseteq> outside t"
+ apply (rule outside_subset_convex)
+ using r by auto
+ ultimately show ?thesis
+ by (metis Compl_subset_Compl_iff Int_subset_iff bounded_ball inf.orderE outside_bounded_nonempty outside_no_overlap)
+ qed
+ have "s \<inter> t = {}" using assms
+ by (metis disjoint_iff_not_equal inside_no_overlap subsetCE)
+ moreover have "outside s \<inter> inside t \<noteq> {}"
+ by (meson False assms(4) compact_eq_bounded_closed coms open_inside outside_compact_in_open t)
+ ultimately have "inside s \<inter> t = {}"
+ using inside_outside_intersect_connected [OF `connected t`, of s]
+ by (metis "2" compact_eq_bounded_closed coms connected_outside inf.commute inside_outside_intersect_connected outst)
+ then show ?thesis
+ using inside_inside [OF `s \<subseteq> inside t`] by blast
+ qed
+qed
+
+lemma connected_with_inside:
+ fixes s :: "'a :: real_normed_vector set"
+ assumes s: "closed s" and cons: "connected s"
+ shows "connected(s \<union> inside s)"
+proof (cases "s \<union> inside s = UNIV")
+ case True with assms show ?thesis by auto
+next
+ case False
+ then obtain b where b: "b \<notin> s" "b \<notin> inside s" by blast
+ have *: "\<exists>y t. y \<in> s \<and> connected t \<and> a \<in> t \<and> y \<in> t \<and> t \<subseteq> (s \<union> inside s)" if "a \<in> (s \<union> inside s)" for a
+ using that proof
+ assume "a \<in> s" then show ?thesis
+ apply (rule_tac x=a in exI)
+ apply (rule_tac x="{a}" in exI)
+ apply (simp add:)
+ done
+ next
+ assume a: "a \<in> inside s"
+ show ?thesis
+ apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "inside s"])
+ using a apply (simp add: closure_def)
+ apply (simp add: b)
+ apply (rule_tac x="pathfinish h" in exI)
+ apply (rule_tac x="path_image h" in exI)
+ apply (simp add: pathfinish_in_path_image connected_path_image, auto)
+ using frontier_inside_subset s apply fastforce
+ by (metis (no_types, lifting) frontier_inside_subset insertE insert_Diff interior_eq open_inside pathfinish_in_path_image s subsetCE)
+ qed
+ show ?thesis
+ apply (simp add: connected_iff_connected_component)
+ apply (simp add: connected_component_def)
+ apply (clarify dest!: *)
+ apply (rename_tac u u' t t')
+ apply (rule_tac x="(s \<union> t \<union> t')" in exI)
+ apply (auto simp: intro!: connected_Un cons)
+ done
+qed
+
+text\<open>The proof is virtually the same as that above.\<close>
+lemma connected_with_outside:
+ fixes s :: "'a :: real_normed_vector set"
+ assumes s: "closed s" and cons: "connected s"
+ shows "connected(s \<union> outside s)"
+proof (cases "s \<union> outside s = UNIV")
+ case True with assms show ?thesis by auto
+next
+ case False
+ then obtain b where b: "b \<notin> s" "b \<notin> outside s" by blast
+ have *: "\<exists>y t. y \<in> s \<and> connected t \<and> a \<in> t \<and> y \<in> t \<and> t \<subseteq> (s \<union> outside s)" if "a \<in> (s \<union> outside s)" for a
+ using that proof
+ assume "a \<in> s" then show ?thesis
+ apply (rule_tac x=a in exI)
+ apply (rule_tac x="{a}" in exI)
+ apply (simp add:)
+ done
+ next
+ assume a: "a \<in> outside s"
+ show ?thesis
+ apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "outside s"])
+ using a apply (simp add: closure_def)
+ apply (simp add: b)
+ apply (rule_tac x="pathfinish h" in exI)
+ apply (rule_tac x="path_image h" in exI)
+ apply (simp add: pathfinish_in_path_image connected_path_image, auto)
+ using frontier_outside_subset s apply fastforce
+ by (metis (no_types, lifting) frontier_outside_subset insertE insert_Diff interior_eq open_outside pathfinish_in_path_image s subsetCE)
+ qed
+ show ?thesis
+ apply (simp add: connected_iff_connected_component)
+ apply (simp add: connected_component_def)
+ apply (clarify dest!: *)
+ apply (rename_tac u u' t t')
+ apply (rule_tac x="(s \<union> t \<union> t')" in exI)
+ apply (auto simp: intro!: connected_Un cons)
+ done
+qed
+
+lemma inside_inside_eq_empty [simp]:
+ fixes s :: "'a :: {real_normed_vector, perfect_space} set"
+ assumes s: "closed s" and cons: "connected s"
+ shows "inside (inside s) = {}"
+ by (metis (no_types) unbounded_outside connected_with_outside [OF assms] bounded_Un
+ inside_complement_unbounded_connected_empty unbounded_outside union_with_outside)
+
+lemma inside_in_components:
+ "inside s \<in> components (- s) \<longleftrightarrow> connected(inside s) \<and> inside s \<noteq> {}"
+ apply (simp add: in_components_maximal)
+ apply (auto intro: inside_same_component connected_componentI)
+ apply (metis IntI empty_iff inside_no_overlap)
+ done
+
+text\<open>The proof is virtually the same as that above.\<close>
+lemma outside_in_components:
+ "outside s \<in> components (- s) \<longleftrightarrow> connected(outside s) \<and> outside s \<noteq> {}"
+ apply (simp add: in_components_maximal)
+ apply (auto intro: outside_same_component connected_componentI)
+ apply (metis IntI empty_iff outside_no_overlap)
+ done
+
+lemma bounded_unique_outside:
+ fixes s :: "'a :: euclidean_space set"
+ shows "\<lbrakk>bounded s; DIM('a) \<ge> 2\<rbrakk> \<Longrightarrow> (c \<in> components (- s) \<and> ~bounded c \<longleftrightarrow> c = outside s)"
+ apply (rule iffI)
+ apply (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty outside_in_components unbounded_outside)
+ by (simp add: connected_outside outside_bounded_nonempty outside_in_components unbounded_outside)
+
end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Oct 26 23:41:27 2015 +0000
@@ -513,9 +513,6 @@
lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
using closedin_Inter[of "{S,T}" U] by auto
-lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B"
- by blast
-
lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)
apply (metis openin_subset subset_eq)
@@ -790,6 +787,13 @@
lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
by (auto simp add: closedin_closed intro: closedin_trans)
+lemma openin_subtopology_inter_subset:
+ "openin (subtopology euclidean u) (u \<inter> s) \<and> v \<subseteq> u \<Longrightarrow> openin (subtopology euclidean v) (v \<inter> s)"
+ by (auto simp: openin_subtopology)
+
+lemma openin_open_eq: "open s \<Longrightarrow> (openin (subtopology euclidean s) t \<longleftrightarrow> open t \<and> t \<subseteq> s)"
+ using open_subset openin_open_trans openin_subset by fastforce
+
subsection \<open>Open and closed balls\<close>
@@ -805,23 +809,29 @@
lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e"
by (simp add: cball_def)
-lemma mem_ball_0:
+lemma ball_trivial [simp]: "ball x 0 = {}"
+ by (simp add: ball_def)
+
+lemma cball_trivial [simp]: "cball x 0 = {x}"
+ by (simp add: cball_def)
+
+lemma mem_ball_0 [simp]:
fixes x :: "'a::real_normed_vector"
shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
by (simp add: dist_norm)
-lemma mem_cball_0:
+lemma mem_cball_0 [simp]:
fixes x :: "'a::real_normed_vector"
shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
by (simp add: dist_norm)
-lemma centre_in_ball: "x \<in> ball x e \<longleftrightarrow> 0 < e"
+lemma centre_in_ball [simp]: "x \<in> ball x e \<longleftrightarrow> 0 < e"
by simp
-lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
+lemma centre_in_cball [simp]: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
by simp
-lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e"
+lemma ball_subset_cball [simp,intro]: "ball x e \<subseteq> cball x e"
by (simp add: subset_eq)
lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e"
@@ -1547,7 +1557,12 @@
shows "interior S = T"
by (intro equalityI assms interior_subset open_interior interior_maximal)
-lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
+lemma interior_singleton [simp]:
+ fixes a :: "'a::perfect_space" shows "interior {a} = {}"
+ apply (rule interior_unique, simp_all)
+ using not_open_singleton subset_singletonD by fastforce
+
+lemma interior_Int [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
Int_lower2 interior_maximal interior_subset open_Int open_interior)
@@ -1801,6 +1816,10 @@
apply (force simp: closure_def)
done
+lemma closedin_closed_eq:
+ "closed s \<Longrightarrow> (closedin (subtopology euclidean s) t \<longleftrightarrow> closed t \<and> t \<subseteq> s)"
+ by (meson closed_in_limpt closed_subset closedin_closed_trans)
+
subsection\<open>Connected components, considered as a connectedness relation or a set\<close>
definition
@@ -2171,7 +2190,7 @@
then show ?thesis using frontier_subset_closed[of S] ..
qed
-lemma frontier_complement: "frontier (- S) = frontier S"
+lemma frontier_complement [simp]: "frontier (- S) = frontier S"
by (auto simp add: frontier_def closure_complement interior_complement)
lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
@@ -5128,6 +5147,11 @@
text\<open>Some simple consequential lemmas.\<close>
+lemma continuous_onD:
+ assumes "continuous_on s f" "x\<in>s" "e>0"
+ obtains d where "d>0" "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
+ using assms [unfolded continuous_on_iff] by blast
+
lemma uniformly_continuous_onE:
assumes "uniformly_continuous_on s f" "0 < e"
obtains d where "d>0" "\<And>x x'. \<lbrakk>x\<in>s; x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
@@ -5514,7 +5538,7 @@
text \<open>Half-global and completely global cases.\<close>
-lemma continuous_open_in_preimage:
+lemma continuous_openin_preimage:
assumes "continuous_on s f" "open t"
shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
proof -
@@ -5527,7 +5551,7 @@
using * by auto
qed
-lemma continuous_closed_in_preimage:
+lemma continuous_closedin_preimage:
assumes "continuous_on s f" and "closed t"
shows "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
proof -
@@ -5548,7 +5572,7 @@
shows "open {x \<in> s. f x \<in> t}"
proof-
obtain T where T: "open T" "{x \<in> s. f x \<in> t} = s \<inter> T"
- using continuous_open_in_preimage[OF assms(1,3)] unfolding openin_open by auto
+ using continuous_openin_preimage[OF assms(1,3)] unfolding openin_open by auto
then show ?thesis
using open_Int[of s T, OF assms(2)] by auto
qed
@@ -5560,7 +5584,7 @@
shows "closed {x \<in> s. f x \<in> t}"
proof-
obtain T where "closed T" "{x \<in> s. f x \<in> t} = s \<inter> T"
- using continuous_closed_in_preimage[OF assms(1,3)]
+ using continuous_closedin_preimage[OF assms(1,3)]
unfolding closedin_closed by auto
then show ?thesis using closed_Int[of s T, OF assms(2)] by auto
qed
@@ -5603,7 +5627,7 @@
lemma continuous_closed_in_preimage_constant:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
shows "continuous_on s f \<Longrightarrow> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
- using continuous_closed_in_preimage[of s f "{a}"] by auto
+ using continuous_closedin_preimage[of s f "{a}"] by auto
lemma continuous_closed_preimage_constant:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -5969,6 +5993,12 @@
then show ?thesis
unfolding connected_clopen by auto
qed
+
+lemma connected_linear_image:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+ assumes "linear f" and "connected s"
+ shows "connected (f ` s)"
+using connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear by blast
text \<open>Continuity implies uniform continuity on a compact domain.\<close>
@@ -5986,7 +6016,7 @@
proof safe
fix y
assume "y \<in> s"
- from continuous_open_in_preimage[OF f open_ball]
+ from continuous_openin_preimage[OF f open_ball]
obtain T where "open T" and T: "{x \<in> s. f x \<in> ball (f y) (e/2)} = T \<inter> s"
unfolding openin_subtopology open_openin by metis
then obtain d where "ball y d \<subseteq> T" "0 < d"
--- a/src/HOL/Set.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Set.thy Mon Oct 26 23:41:27 2015 +0000
@@ -1552,6 +1552,9 @@
lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"
by blast
+lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B"
+ by blast
+
lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
by blast
--- a/src/HOL/Transcendental.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Transcendental.thy Mon Oct 26 23:41:27 2015 +0000
@@ -1145,7 +1145,8 @@
apply (simp del: of_real_add)
done
-declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
+declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
+ DERIV_exp[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
proof -
@@ -1589,6 +1590,8 @@
by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
+ DERIV_ln_divide[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
+
lemma ln_series:
assumes "0 < x" and "x < 2"
@@ -2173,6 +2176,7 @@
qed
lemmas DERIV_log[THEN DERIV_chain2, derivative_intros]
+ DERIV_log[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
by (simp add: powr_def log_def)
@@ -2720,6 +2724,7 @@
done
declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
+ DERIV_sin[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
lemma DERIV_cos [simp]:
fixes x :: "'a::{real_normed_field,banach}"
@@ -2735,6 +2740,7 @@
done
declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
+ DERIV_cos[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
lemma isCont_sin:
fixes x :: "'a::{real_normed_field,banach}"
@@ -4528,8 +4534,11 @@
declare
DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
+ DERIV_arcsin[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
DERIV_arccos[THEN DERIV_chain2, derivative_intros]
+ DERIV_arccos[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
DERIV_arctan[THEN DERIV_chain2, derivative_intros]
+ DERIV_arctan[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])