--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue May 24 13:57:04 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue May 24 13:57:34 2016 +0100
@@ -11,30 +11,6 @@
"~~/src/HOL/Library/Set_Algebras"
begin
-lemma independent_injective_on_span_image:
- assumes iS: "independent S"
- and lf: "linear f"
- and fi: "inj_on f (span S)"
- shows "independent (f ` S)"
-proof -
- {
- fix a
- assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
- have eq: "f ` S - {f a} = f ` (S - {a})"
- using fi a span_inc by (auto simp add: inj_on_def)
- from a have "f a \<in> f ` span (S -{a})"
- unfolding eq span_linear_image [OF lf, of "S - {a}"] by blast
- moreover have "span (S - {a}) \<subseteq> span S"
- using span_mono[of "S - {a}" S] by auto
- ultimately have "a \<in> span (S - {a})"
- using fi a span_inc by (auto simp add: inj_on_def)
- with a(1) iS have False
- by (simp add: dependent_def)
- }
- then show ?thesis
- unfolding dependent_def by blast
-qed
-
lemma dim_image_eq:
fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
assumes lf: "linear f"
@@ -46,7 +22,7 @@
then have "span S = span B"
using span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto
then have "independent (f ` B)"
- using independent_injective_on_span_image[of B f] B assms by auto
+ using independent_inj_on_image[of B f] B assms by auto
moreover have "card (f ` B) = card B"
using assms card_image[of f B] subset_inj_on[of f "span S" B] B span_inc by auto
moreover have "(f ` B) \<subseteq> (f ` S)"
@@ -7503,6 +7479,20 @@
done
qed
+lemma in_interior_closure_convex_segment:
+ fixes S :: "'a::euclidean_space set"
+ assumes "convex S" and a: "a \<in> interior S" and b: "b \<in> closure S"
+ shows "open_segment a b \<subseteq> interior S"
+proof (clarsimp simp: in_segment)
+ fix u::real
+ assume u: "0 < u" "u < 1"
+ have "(1 - u) *\<^sub>R a + u *\<^sub>R b = b - (1 - u) *\<^sub>R (b - a)"
+ by (simp add: algebra_simps)
+ also have "... \<in> interior S" using mem_interior_closure_convex_shrink [OF assms] u
+ by simp
+ finally show "(1 - u) *\<^sub>R a + u *\<^sub>R b \<in> interior S" .
+qed
+
subsection \<open>Some obvious but surprisingly hard simplex lemmas\<close>
@@ -7516,7 +7506,7 @@
unfolding mem_Collect_eq
apply (erule_tac[!] exE)
apply (erule_tac[!] conjE)+
- unfolding setsum_clauses(2)[OF assms(1)]
+ unfolding setsum_clauses(2)[OF \<open>finite s\<close>]
apply (rule_tac x=u in exI)
defer
apply (rule_tac x="\<lambda>x. if x = 0 then 1 - setsum u s else u x" in exI)
@@ -8705,7 +8695,7 @@
then show ?thesis by auto
qed
-lemma closure_inter: "closure (\<Inter>I) \<le> \<Inter>{closure S |S. S \<in> I}"
+lemma closure_Int: "closure (\<Inter>I) \<le> \<Inter>{closure S |S. S \<in> I}"
proof -
{
fix y
@@ -8793,7 +8783,7 @@
using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
by auto
ultimately show ?thesis
- using closure_inter[of I] by auto
+ using closure_Int[of I] by auto
qed
lemma convex_inter_rel_interior_same_closure:
@@ -8808,7 +8798,7 @@
using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
by auto
ultimately show ?thesis
- using closure_inter[of I] by auto
+ using closure_Int[of I] by auto
qed
lemma convex_rel_interior_inter:
@@ -8898,7 +8888,7 @@
shows "rel_interior (S \<inter> T) = rel_interior S \<inter> rel_interior T"
using convex_rel_interior_finite_inter[of "{S,T}"] assms by auto
-lemma convex_affine_closure_inter:
+lemma convex_affine_closure_Int:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"
and "affine T"
@@ -8928,7 +8918,7 @@
shows "connected_component S a b \<longleftrightarrow> closed_segment a b \<subseteq> S"
by (simp add: connected_component_1_gen)
-lemma convex_affine_rel_interior_inter:
+lemma convex_affine_rel_interior_Int:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"
and "affine T"
@@ -8945,6 +8935,16 @@
using convex_rel_interior_inter_two[of S T] assms affine_imp_convex by auto
qed
+lemma convex_affine_rel_frontier_Int:
+ fixes S T :: "'n::euclidean_space set"
+ assumes "convex S"
+ and "affine T"
+ and "interior S \<inter> T \<noteq> {}"
+ shows "rel_frontier(S \<inter> T) = frontier S \<inter> T"
+using assms
+apply (simp add: rel_frontier_def convex_affine_closure_Int frontier_def)
+by (metis Diff_Int_distrib2 Int_emptyI convex_affine_closure_Int convex_affine_rel_interior_Int empty_iff interior_rel_interior_gen)
+
lemma subset_rel_interior_convex:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"
@@ -9087,7 +9087,7 @@
moreover have "affine (range f)"
by (metis assms(1) subspace_UNIV subspace_imp_affine subspace_linear_image)
ultimately have "f z \<in> rel_interior S"
- using convex_affine_rel_interior_inter[of S "range f"] assms by auto
+ using convex_affine_rel_interior_Int[of S "range f"] assms by auto
then have "z \<in> f -` (rel_interior S)"
by auto
}
@@ -9250,7 +9250,7 @@
moreover have aff: "affine (fst -` {y})"
unfolding affine_alt by (simp add: algebra_simps)
ultimately have **: "rel_interior (S \<inter> fst -` {y}) = rel_interior S \<inter> fst -` {y}"
- using convex_affine_rel_interior_inter[of S "fst -` {y}"] assms by auto
+ using convex_affine_rel_interior_Int[of S "fst -` {y}"] assms by auto
have conv: "convex (S \<inter> fst -` {y})"
using convex_Int assms aff affine_imp_convex by auto
{
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue May 24 13:57:04 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue May 24 13:57:34 2016 +0100
@@ -2606,7 +2606,7 @@
assume xc: "x > c"
let ?A' = "interior A \<inter> {c<..}"
from c have "c \<in> interior A \<inter> closure {c<..}" by auto
- also have "\<dots> \<subseteq> closure (interior A \<inter> {c<..})" by (intro open_inter_closure_subset) auto
+ also have "\<dots> \<subseteq> closure (interior A \<inter> {c<..})" by (intro open_Int_closure_subset) auto
finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> f') (at c within ?A')"
unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
@@ -2628,7 +2628,7 @@
assume xc: "x < c"
let ?A' = "interior A \<inter> {..<c}"
from c have "c \<in> interior A \<inter> closure {..<c}" by auto
- also have "\<dots> \<subseteq> closure (interior A \<inter> {..<c})" by (intro open_inter_closure_subset) auto
+ also have "\<dots> \<subseteq> closure (interior A \<inter> {..<c})" by (intro open_Int_closure_subset) auto
finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> f') (at c within ?A')"
unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue May 24 13:57:04 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue May 24 13:57:34 2016 +0100
@@ -1853,7 +1853,7 @@
unfolding closure_interior
by auto
-lemma open_inter_closure_subset:
+lemma open_Int_closure_subset:
"open S \<Longrightarrow> (S \<inter> (closure T)) \<subseteq> closure(S \<inter> T)"
proof
fix x
@@ -2643,6 +2643,29 @@
by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult)
qed
+lemma lim_null_scaleR_bounded:
+ assumes f: "(f \<longlongrightarrow> 0) net" and gB: "eventually (\<lambda>a. f a = 0 \<or> norm(g a) \<le> B) net"
+ shows "((\<lambda>n. f n *\<^sub>R g n) \<longlongrightarrow> 0) net"
+proof
+ fix \<epsilon>::real
+ assume "0 < \<epsilon>"
+ then have B: "0 < \<epsilon> / (abs B + 1)" by simp
+ have *: "\<bar>f x\<bar> * norm (g x) < \<epsilon>" if f: "\<bar>f x\<bar> * (\<bar>B\<bar> + 1) < \<epsilon>" and g: "norm (g x) \<le> B" for x
+ proof -
+ have "\<bar>f x\<bar> * norm (g x) \<le> \<bar>f x\<bar> * B"
+ by (simp add: mult_left_mono g)
+ also have "... \<le> \<bar>f x\<bar> * (\<bar>B\<bar> + 1)"
+ by (simp add: mult_left_mono)
+ also have "... < \<epsilon>"
+ by (rule f)
+ finally show ?thesis .
+ qed
+ show "\<forall>\<^sub>F x in net. dist (f x *\<^sub>R g x) 0 < \<epsilon>"
+ apply (rule eventually_mono [OF eventually_conj [OF tendstoD [OF f B] gB] ])
+ apply (auto simp: \<open>0 < \<epsilon>\<close> divide_simps * split: if_split_asm)
+ done
+qed
+
text\<open>Deducing things about the limit from the elements.\<close>
lemma Lim_in_closed_set:
@@ -3986,7 +4009,7 @@
with x have "x \<in> closure X - closure (-S)"
by auto
also have "\<dots> \<subseteq> closure (X \<inter> S)"
- using \<open>open S\<close> open_inter_closure_subset[of S X] by (simp add: closed_Compl ac_simps)
+ using \<open>open S\<close> open_Int_closure_subset[of S X] by (simp add: closed_Compl ac_simps)
finally have "X \<inter> S \<noteq> {}" by auto
then show False using \<open>X \<inter> A = {}\<close> \<open>S \<subseteq> A\<close> by auto
next
--- a/src/HOL/Real_Vector_Spaces.thy Tue May 24 13:57:04 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Tue May 24 13:57:34 2016 +0100
@@ -1754,7 +1754,7 @@
"(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
unfolding nhds_metric filterlim_INF filterlim_principal by auto
-lemma (in metric_space) tendstoI: "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F) \<Longrightarrow> (f \<longlongrightarrow> l) F"
+lemma (in metric_space) tendstoI [intro?]: "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F) \<Longrightarrow> (f \<longlongrightarrow> l) F"
by (auto simp: tendsto_iff)
lemma (in metric_space) tendstoD: "(f \<longlongrightarrow> l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"