--- a/NEWS Fri Aug 26 22:53:04 2011 +0900
+++ b/NEWS Fri Aug 26 10:38:29 2011 -0700
@@ -200,6 +200,38 @@
tendsto_vector ~> vec_tendstoI
Cauchy_vector ~> vec_CauchyI
+* Session Multivariate_Analysis: Several duplicate theorems have been
+removed, and other theorems have been renamed. INCOMPATIBILITY.
+
+ eventually_conjI ~> eventually_conj
+ eventually_and ~> eventually_conj_iff
+ eventually_false ~> eventually_False
+ Lim_ident_at ~> LIM_ident
+ Lim_const ~> tendsto_const
+ Lim_cmul ~> tendsto_scaleR [OF tendsto_const]
+ Lim_neg ~> tendsto_minus
+ Lim_add ~> tendsto_add
+ Lim_sub ~> tendsto_diff
+ Lim_mul ~> tendsto_scaleR
+ Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]
+ Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]
+ Lim_linear ~> bounded_linear.tendsto
+ Lim_component ~> tendsto_euclidean_component
+ Lim_component_cart ~> tendsto_vec_nth
+ Lim_inner ~> tendsto_inner [OF tendsto_const]
+ dot_lsum ~> inner_setsum_left
+ dot_rsum ~> inner_setsum_right
+ continuous_on_neg ~> continuous_on_minus
+ continuous_on_sub ~> continuous_on_diff
+ continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]
+ continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]
+ continuous_on_mul ~> continuous_on_scaleR
+ continuous_on_mul_real ~> continuous_on_mult
+ continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]
+ subset_interior ~> interior_mono
+ subset_closure ~> closure_mono
+ closure_univ ~> closure_UNIV
+
* Complex_Main: The locale interpretations for the bounded_linear and
bounded_bilinear locales have been removed, in order to reduce the
number of duplicate lemmas. Users must use the original names for
@@ -213,6 +245,16 @@
mult_right.setsum ~> setsum_right_distrib
mult_left.diff ~> left_diff_distrib
+* Complex_Main: Several redundant theorems about real numbers have
+been removed or generalized and renamed. INCOMPATIBILITY.
+
+ real_0_le_divide_iff ~> zero_le_divide_iff
+ realpow_two_disj ~> power2_eq_iff
+ real_squared_diff_one_factored ~> square_diff_one_factored
+ realpow_two_diff ~> square_diff_square_factored
+ exp_ln_eq ~> ln_unique
+ lemma_DERIV_subst ~> DERIV_cong
+
*** Document preparation ***
--- a/src/HOL/IsaMakefile Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/IsaMakefile Fri Aug 26 10:38:29 2011 -0700
@@ -1175,6 +1175,7 @@
Multivariate_Analysis/L2_Norm.thy \
Multivariate_Analysis/Linear_Algebra.thy \
Multivariate_Analysis/Multivariate_Analysis.thy \
+ Multivariate_Analysis/Norm_Arith.thy \
Multivariate_Analysis/Operator_Norm.thy \
Multivariate_Analysis/Path_Connected.thy \
Multivariate_Analysis/ROOT.ML \
--- a/src/HOL/Library/Extended_Real.thy Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Library/Extended_Real.thy Fri Aug 26 10:38:29 2011 -0700
@@ -2391,8 +2391,6 @@
shows "limsup X \<le> limsup Y"
using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto
-declare trivial_limit_sequentially[simp]
-
lemma
fixes X :: "nat \<Rightarrow> ereal"
shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
--- a/src/HOL/Lim.thy Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Lim.thy Fri Aug 26 10:38:29 2011 -0700
@@ -444,46 +444,51 @@
subsection {* Relation of LIM and LIMSEQ *}
+lemma sequentially_imp_eventually_within:
+ fixes a :: "'a::metric_space"
+ assumes "\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow>
+ eventually (\<lambda>n. P (f n)) sequentially"
+ shows "eventually P (at a within s)"
+proof (rule ccontr)
+ let ?I = "\<lambda>n. inverse (real (Suc n))"
+ def F \<equiv> "\<lambda>n::nat. SOME x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
+ assume "\<not> eventually P (at a within s)"
+ hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
+ unfolding Limits.eventually_within Limits.eventually_at by fast
+ hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
+ hence F: "\<And>n. F n \<in> s \<and> F n \<noteq> a \<and> dist (F n) a < ?I n \<and> \<not> P (F n)"
+ unfolding F_def by (rule someI_ex)
+ hence F0: "\<forall>n. F n \<in> s" and F1: "\<forall>n. F n \<noteq> a"
+ and F2: "\<forall>n. dist (F n) a < ?I n" and F3: "\<forall>n. \<not> P (F n)"
+ by fast+
+ from LIMSEQ_inverse_real_of_nat have "F ----> a"
+ by (rule metric_tendsto_imp_tendsto,
+ simp add: dist_norm F2 less_imp_le)
+ hence "eventually (\<lambda>n. P (F n)) sequentially"
+ using assms F0 F1 by simp
+ thus "False" by (simp add: F3)
+qed
+
+lemma sequentially_imp_eventually_at:
+ fixes a :: "'a::metric_space"
+ assumes "\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow>
+ eventually (\<lambda>n. P (f n)) sequentially"
+ shows "eventually P (at a)"
+ using assms sequentially_imp_eventually_within [where s=UNIV]
+ unfolding within_UNIV by simp
+
lemma LIMSEQ_SEQ_conv1:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
assumes f: "f -- a --> l"
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
using tendsto_compose_eventually [OF f, where F=sequentially] by simp
-lemma LIMSEQ_SEQ_conv2_lemma:
- fixes a :: "'a::metric_space"
- assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
- shows "eventually P (at a)"
-proof (rule ccontr)
- let ?I = "\<lambda>n. inverse (real (Suc n))"
- let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
- assume "\<not> eventually P (at a)"
- hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
- unfolding eventually_at by simp
- hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
- hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
- by (rule someI_ex)
- hence F1: "\<And>n. ?F n \<noteq> a"
- and F2: "\<And>n. dist (?F n) a < ?I n"
- and F3: "\<And>n. \<not> P (?F n)"
- by fast+
- have "?F ----> a"
- using LIMSEQ_inverse_real_of_nat
- by (rule metric_tendsto_imp_tendsto,
- simp add: dist_norm F2 [THEN less_imp_le])
- moreover have "\<forall>n. ?F n \<noteq> a"
- by (rule allI) (rule F1)
- ultimately have "eventually (\<lambda>n. P (?F n)) sequentially"
- using assms by simp
- thus "False" by (simp add: F3)
-qed
-
lemma LIMSEQ_SEQ_conv2:
fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
shows "f -- a --> l"
using assms unfolding tendsto_def [where l=l]
- by (simp add: LIMSEQ_SEQ_conv2_lemma)
+ by (simp add: sequentially_imp_eventually_at)
lemma LIMSEQ_SEQ_conv:
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 26 10:38:29 2011 -0700
@@ -792,7 +792,7 @@
have "subspace ?P"
by (auto simp add: subspace_def)
ultimately show ?thesis
- using x span_induct[of ?B ?P x] iS by blast
+ using x span_induct[of x ?B ?P] iS by blast
qed
lemma independent_stdbasis: "independent {cart_basis i ::real^'n |i. i\<in> (UNIV :: 'n set)}"
@@ -2001,8 +2001,4 @@
apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
-text {* Legacy theorem names *}
-
-lemmas Lim_component_cart = tendsto_vec_nth
-
end
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 26 10:38:29 2011 -0700
@@ -229,12 +229,18 @@
from g(1) gS giS gBC show ?thesis by blast
qed
+lemma closure_bounded_linear_image:
+ 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:
fixes f :: "('m::euclidean_space) => ('n::real_normed_vector)"
assumes "linear f"
shows "f ` (closure S) <= closure (f ` S)"
-using image_closure_subset[of S f "closure (f ` S)"] assms linear_conv_bounded_linear[of f]
-linear_continuous_on[of f "closure S"] closed_closure[of "f ` S"] closure_subset[of "f ` S"] by auto
+ using assms unfolding linear_conv_bounded_linear
+ by (rule closure_bounded_linear_image)
lemma closure_injective_linear_image:
fixes f :: "('n::euclidean_space) => ('n::euclidean_space)"
@@ -254,23 +260,16 @@
shows "closure (S <*> T) = closure S <*> closure T"
by (rule closure_Times)
-lemma closure_scaleR: (* TODO: generalize to real_normed_vector *)
-fixes S :: "('n::euclidean_space) set"
-shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
-proof-
-{ assume "c ~= 0" hence ?thesis using closure_injective_linear_image[of "(op *\<^sub>R c)" S]
- linear_scaleR injective_scaleR by auto
-}
-moreover
-{ assume zero: "c=0 & S ~= {}"
- hence "closure S ~= {}" using closure_subset by auto
- hence "op *\<^sub>R c ` (closure S) = {0}" using zero by auto
- moreover have "op *\<^sub>R 0 ` S = {0}" using zero by auto
- ultimately have ?thesis using zero by auto
-}
-moreover
-{ assume "S={}" hence ?thesis by auto }
-ultimately show ?thesis by blast
+lemma closure_scaleR:
+ fixes S :: "('a::real_normed_vector) set"
+ shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
+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)
+ 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
lemma fst_linear: "linear fst" unfolding linear_def by (simp add: algebra_simps)
@@ -859,9 +858,8 @@
qed
lemma cone_closure:
-fixes S :: "('m::euclidean_space) set"
-assumes "cone S"
-shows "cone (closure S)"
+ fixes S :: "('a::real_normed_vector) set"
+ assumes "cone S" shows "cone (closure S)"
proof-
{ assume "S = {}" hence ?thesis by auto }
moreover
@@ -2310,12 +2308,7 @@
lemma closure_affine_hull:
fixes S :: "('n::euclidean_space) set"
shows "closure S <= affine hull S"
-proof-
-have "closure S <= closure (affine hull S)" using subset_closure by auto
-moreover have "closure (affine hull S) = affine hull S"
- using affine_affine_hull affine_closed[of "affine hull S"] closure_eq by auto
-ultimately show ?thesis by auto
-qed
+ by (intro closure_minimal hull_subset affine_closed affine_affine_hull)
lemma closure_same_affine_hull:
fixes S :: "('n::euclidean_space) set"
@@ -2580,6 +2573,37 @@
done
qed
+lemma finite_imp_compact_convex_hull:
+ fixes s :: "('a::real_normed_vector) set"
+ assumes "finite s" shows "compact (convex hull s)"
+proof (cases "s = {}")
+ case True thus ?thesis by simp
+next
+ case False with assms show ?thesis
+ proof (induct rule: finite_ne_induct)
+ case (singleton x) show ?case by simp
+ next
+ case (insert x A)
+ let ?f = "\<lambda>(u, y::'a). u *\<^sub>R x + (1 - u) *\<^sub>R y"
+ let ?T = "{0..1::real} \<times> (convex hull A)"
+ have "continuous_on ?T ?f"
+ unfolding split_def continuous_on by (intro ballI tendsto_intros)
+ moreover have "compact ?T"
+ by (intro compact_Times compact_interval insert)
+ ultimately have "compact (?f ` ?T)"
+ by (rule compact_continuous_image)
+ also have "?f ` ?T = convex hull (insert x A)"
+ unfolding convex_hull_insert [OF `A \<noteq> {}`]
+ apply safe
+ apply (rule_tac x=a in exI, simp)
+ apply (rule_tac x="1 - a" in exI, simp)
+ apply fast
+ apply (rule_tac x="(u, b)" in image_eqI, simp_all)
+ done
+ finally show "compact (convex hull (insert x A))" .
+ qed
+qed
+
lemma compact_convex_hull: fixes s::"('a::euclidean_space) set"
assumes "compact s" shows "compact(convex hull s)"
proof(cases "s={}")
@@ -2654,11 +2678,6 @@
qed
qed
-lemma finite_imp_compact_convex_hull:
- fixes s :: "('a::euclidean_space) set"
- shows "finite s \<Longrightarrow> compact(convex hull s)"
-by (metis compact_convex_hull finite_imp_compact)
-
subsection {* Extremal points of a simplex are some vertices. *}
lemma dist_increases_online:
@@ -2738,7 +2757,7 @@
qed (auto simp add: assms)
lemma simplex_furthest_le:
- fixes s :: "('a::euclidean_space) set"
+ fixes s :: "('a::real_inner) set"
assumes "finite s" "s \<noteq> {}"
shows "\<exists>y\<in>s. \<forall>x\<in>(convex hull s). norm(x - a) \<le> norm(y - a)"
proof-
@@ -2754,12 +2773,12 @@
qed
lemma simplex_furthest_le_exists:
- fixes s :: "('a::euclidean_space) set"
+ fixes s :: "('a::real_inner) set"
shows "finite s \<Longrightarrow> (\<forall>x\<in>(convex hull s). \<exists>y\<in>s. norm(x - a) \<le> norm(y - a))"
using simplex_furthest_le[of s] by (cases "s={}")auto
lemma simplex_extremal_le:
- fixes s :: "('a::euclidean_space) set"
+ fixes s :: "('a::real_inner) set"
assumes "finite s" "s \<noteq> {}"
shows "\<exists>u\<in>s. \<exists>v\<in>s. \<forall>x\<in>convex hull s. \<forall>y \<in> convex hull s. norm(x - y) \<le> norm(u - v)"
proof-
@@ -2780,7 +2799,7 @@
qed
lemma simplex_extremal_le_exists:
- fixes s :: "('a::euclidean_space) set"
+ fixes s :: "('a::real_inner) set"
shows "finite s \<Longrightarrow> x \<in> convex hull s \<Longrightarrow> y \<in> convex hull s
\<Longrightarrow> (\<exists>u\<in>s. \<exists>v\<in>s. norm(x - y) \<le> norm(u - v))"
using convex_hull_empty simplex_extremal_le[of s] by(cases "s={}")auto
@@ -3094,7 +3113,6 @@
subsection {* Convexity of cone hulls *}
lemma convex_cone_hull:
-fixes S :: "('m::euclidean_space) set"
assumes "convex S"
shows "convex (cone hull S)"
proof-
@@ -3126,7 +3144,6 @@
qed
lemma cone_convex_hull:
-fixes S :: "('m::euclidean_space) set"
assumes "cone S"
shows "cone (convex hull S)"
proof-
@@ -3453,22 +3470,27 @@
ultimately show ?thesis using injpi by auto qed qed
qed auto qed
-lemma homeomorphic_convex_compact_lemma: fixes s::"('a::euclidean_space) set"
- assumes "convex s" "compact s" "cball 0 1 \<subseteq> s"
+lemma homeomorphic_convex_compact_lemma:
+ fixes s :: "('a::euclidean_space) set"
+ assumes "convex s" and "compact s" and "cball 0 1 \<subseteq> s"
shows "s homeomorphic (cball (0::'a) 1)"
- apply(rule starlike_compact_projective[OF assms(2-3)]) proof(rule,rule,rule,erule conjE)
- fix x u assume as:"x \<in> s" "0 \<le> u" "u < (1::real)"
- hence "u *\<^sub>R x \<in> interior s" unfolding interior_def mem_Collect_eq
- apply(rule_tac x="ball (u *\<^sub>R x) (1 - u)" in exI) apply(rule, rule open_ball)
- unfolding centre_in_ball apply rule defer apply(rule) unfolding mem_ball proof-
- fix y assume "dist (u *\<^sub>R x) y < 1 - u"
- hence "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s"
- using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
- unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR
- apply (rule mult_left_le_imp_le[of "1 - u"])
- unfolding mult_assoc[symmetric] using `u<1` by auto
- thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u]
- using as unfolding scaleR_scaleR by auto qed auto
+proof (rule starlike_compact_projective[OF assms(2-3)], clarify)
+ fix x u assume "x \<in> s" and "0 \<le> u" and "u < (1::real)"
+ have "open (ball (u *\<^sub>R x) (1 - u))" by (rule open_ball)
+ moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"
+ unfolding centre_in_ball using `u < 1` by simp
+ moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> s"
+ proof
+ fix y assume "y \<in> ball (u *\<^sub>R x) (1 - u)"
+ hence "dist (u *\<^sub>R x) y < 1 - u" unfolding mem_ball .
+ with `u < 1` have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
+ by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
+ with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
+ with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
+ using `x \<in> s` `0 \<le> u` `u < 1` [THEN less_imp_le] by (rule mem_convex)
+ thus "y \<in> s" using `u < 1` by simp
+ qed
+ ultimately have "u *\<^sub>R x \<in> interior s" ..
thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed
lemma homeomorphic_convex_compact_cball: fixes e::real and s::"('a::euclidean_space) set"
@@ -3621,8 +3643,8 @@
assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$$k \<le> y" "y \<le> (f a)$$k"
shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
apply(subst neg_equal_iff_equal[THEN sym])
- using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"] using assms using continuous_on_neg
- by auto
+ using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"]
+ using assms using continuous_on_minus by auto
lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
@@ -4042,7 +4064,7 @@
then obtain y where "y\<in>s" and y:"norm (y - x) * (1 - e) < e * d" by auto
def z \<equiv> "c + ((1 - e) / e) *\<^sub>R (x - y)"
have *:"x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)" unfolding z_def using `e>0` by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
- have "z\<in>interior s" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format])
+ have "z\<in>interior s" apply(rule interior_mono[OF d,unfolded subset_eq,rule_format])
unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
by(auto simp add:field_simps norm_minus_commute)
thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink)
@@ -4380,7 +4402,7 @@
shows "closure(rel_interior S) = closure S"
proof-
have h1: "closure(rel_interior S) <= closure S"
- using subset_closure[of "rel_interior S" S] rel_interior_subset[of S] by auto
+ using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto
{ assume "S ~= {}" from this obtain a where a_def: "a : rel_interior S"
using rel_interior_convex_nonempty assms by auto
{ fix x assume x_def: "x : closure S"
@@ -4517,7 +4539,7 @@
proof-
have "?A --> ?B" by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset)
moreover have "?B --> (closure S1 <= closure S2)"
- by (metis assms(1) convex_closure_rel_interior subset_closure)
+ by (metis assms(1) convex_closure_rel_interior closure_mono)
moreover have "?B --> (closure S1 >= closure S2)" by (metis closed_closure closure_minimal)
ultimately show ?thesis by blast
qed
@@ -4777,7 +4799,7 @@
using convex_closure_rel_interior_inter assms by auto
moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)"
using rel_interior_inter_aux
- subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
+ closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
ultimately show ?thesis using closure_inter[of I] by auto
qed
@@ -4790,7 +4812,7 @@
using convex_closure_rel_interior_inter assms by auto
moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)"
using rel_interior_inter_aux
- subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
+ closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
ultimately show ?thesis using closure_inter[of I] by auto
qed
@@ -4886,7 +4908,7 @@
proof-
have *: "S Int closure T = S" using assms by auto
have "~(rel_interior S <= rel_frontier T)"
- using subset_closure[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
+ using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}"
using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
@@ -4911,8 +4933,8 @@
also have "... = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto
also have "... <= closure (f ` (rel_interior S))" using closure_linear_image assms by auto
finally have "closure (f ` S) = closure (f ` rel_interior S)"
- using subset_closure[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
- subset_closure[of "f ` rel_interior S" "f ` S"] * by auto
+ using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
+ closure_mono[of "f ` rel_interior S" "f ` S"] * by auto
hence "rel_interior (f ` S) = rel_interior (f ` rel_interior S)" using assms convex_rel_interior
linear_conv_bounded_linear[of f] convex_linear_image[of S] convex_linear_image[of "rel_interior S"]
closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"] by auto
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Aug 26 10:38:29 2011 -0700
@@ -785,7 +785,7 @@
have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
apply(rule rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"])
defer
- apply(rule continuous_on_intros assms(2) continuous_on_cmul[where 'b=real, unfolded real_scaleR_def])+
+ apply(rule continuous_on_intros assms(2))+
proof
fix x assume x:"x \<in> {a<..<b}"
show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
@@ -869,7 +869,7 @@
unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
by (auto simp add: algebra_simps)
hence 1:"continuous_on {0..1} (f \<circ> ?p)" apply-
- apply(rule continuous_on_intros continuous_on_vmul)+
+ apply(rule continuous_on_intros)+
unfolding continuous_on_eq_continuous_within
apply(rule,rule differentiable_imp_continuous_within)
unfolding differentiable_def apply(rule_tac x="f' xa" in exI)
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Aug 26 10:38:29 2011 -0700
@@ -149,7 +149,7 @@
assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
proof -
from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
- by (simp add: euclidean_component_diff)
+ by simp
then show "x = y"
unfolding euclidean_component_def euclidean_all_zero by simp
qed
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Fri Aug 26 10:38:29 2011 -0700
@@ -44,7 +44,7 @@
have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+
prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding *
apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def)
- apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
+ apply(rule continuous_on_scaleR) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Aug 26 10:38:29 2011 -0700
@@ -378,7 +378,7 @@
interior(x1 \<inter> y1) \<subseteq> interior(x1) \<Longrightarrow> interior(x1 \<inter> y1) \<subseteq> interior(y1) \<Longrightarrow>
interior(x2 \<inter> y2) \<subseteq> interior(x2) \<Longrightarrow> interior(x2 \<inter> y2) \<subseteq> interior(y2)
\<Longrightarrow> interior(x1 \<inter> y1) \<inter> interior(x2 \<inter> y2) = {}" by auto
- show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] subset_interior)
+ show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] interior_mono)
using division_ofD(5)[OF assms(1) k1(2) k2(2)]
using division_ofD(5)[OF assms(2) k1(3) k2(3)] using th by auto qed qed
@@ -407,9 +407,9 @@
show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto
show "\<Union>(p1 \<union> p2) = s1 \<union> s2" using d1(6) d2(6) by auto
{ fix k1 k2 assume as:"k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2" moreover let ?g="interior k1 \<inter> interior k2 = {}"
- { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using subset_interior[OF d1(2)[OF as(1)]] subset_interior[OF d2(2)[OF as(2)]]
+ { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
using assms(3) by blast } moreover
- { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using subset_interior[OF d1(2)[OF as(2)]] subset_interior[OF d2(2)[OF as(1)]]
+ { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
using assms(3) by blast} ultimately
show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto }
fix k assume k:"k \<in> p1 \<union> p2" show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
@@ -573,7 +573,7 @@
show "finite (q k - {k})" "open (interior k)" "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}" using qk(5) using q(2)[OF k] by auto
have *:"\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
- apply(rule subset_interior *)+ using k by auto qed qed qed auto qed
+ apply(rule interior_mono *)+ using k by auto qed qed qed auto qed
lemma elementary_bounded[dest]: "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)"
unfolding division_of_def by(metis bounded_Union bounded_interval)
@@ -823,7 +823,7 @@
fix x k assume xk:"(x,k)\<in>p1\<union>p2" show "x\<in>k" "\<exists>a b. k = {a..b}" using xk p1(2,4) p2(2,4) by auto
show "k\<subseteq>s1\<union>s2" using xk p1(3) p2(3) by blast
fix x' k' assume xk':"(x',k')\<in>p1\<union>p2" "(x,k) \<noteq> (x',k')"
- have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) subset_interior by blast
+ have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) interior_mono by blast
show "interior k \<inter> interior k' = {}" apply(cases "(x,k)\<in>p1", case_tac[!] "(x',k')\<in>p1")
apply(rule p1(5)) prefer 4 apply(rule *) prefer 6 apply(subst Int_commute,rule *) prefer 8 apply(rule p2(5))
using p1(3) p2(3) using xk xk' by auto qed
@@ -842,7 +842,7 @@
show "x\<in>k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset" using assm(2-4)[OF i] using i(1) by auto
fix x' k' assume xk':"(x',k')\<in>\<Union>pfn ` iset" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto
have *:"\<And>a b. i\<noteq>i' \<Longrightarrow> a\<subseteq> i \<Longrightarrow> b\<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}" using i(1) i'(1)
- using assms(3)[rule_format] subset_interior by blast
+ using assms(3)[rule_format] interior_mono by blast
show "interior k \<inter> interior k' = {}" apply(cases "i=i'")
using assm(5)[OF i _ xk'(2)] i'(2) using assm(3)[OF i] assm(3)[OF i'] defer apply-apply(rule *) by auto
qed
@@ -1703,7 +1703,7 @@
by(rule le_less_trans[OF norm_le_l1])
hence "x + (\<chi>\<chi> i. if i = k then e/2 else 0) \<in> {x. x$$k = c}" using e by auto
thus False unfolding mem_Collect_eq using e x k by auto
- qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule subset_interior) by auto
+ qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule interior_mono) by auto
thus "content b *\<^sub>R f a = 0" by auto
qed auto
also have "\<dots> < e" by(rule k d(2) p12 fine_union p1 p2)+
@@ -2563,7 +2563,7 @@
proof(rule,rule,rule,rule,rule,rule,rule,erule conjE) fix m n u v
assume as:"{m..n} \<in> snd ` p" "{u..v} \<in> snd ` p" "{m..n} \<noteq> {u..v}" "{m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d} = {u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}"
have "({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<inter> ({u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<subseteq> {m..n} \<inter> {u..v}" by blast
- note subset_interior[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
+ note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
hence "interior ({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) = {}" unfolding as Int_absorb by auto
thus "content ({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) = 0" unfolding interval_doublesplit[OF k] content_eq_0_interior[THEN sym] .
qed qed
@@ -3516,7 +3516,7 @@
proof- fix x k k' assume k:"( a, k) \<in> p" "( a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
guess v using pa[OF k(1)] .. note v = conjunctD2[OF this]
guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (min (v) (v'))"
- have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter]
+ have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
moreover have " ((a + ?v)/2) \<in> { a <..< ?v}" using k(3-)
unfolding v v' content_eq_0 not_le by(auto simp add:not_le)
ultimately have " ((a + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
@@ -3528,7 +3528,7 @@
proof- fix x k k' assume k:"( b, k) \<in> p" "( b, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
guess v using pb[OF k(1)] .. note v = conjunctD2[OF this]
guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (max (v) (v'))"
- have "{?v <..< b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter]
+ have "{?v <..< b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
moreover have " ((b + ?v)/2) \<in> {?v <..< b}" using k(3-) unfolding v v' content_eq_0 not_le by auto
ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
hence *:"k = k'" apply- apply(rule ccontr) using p(5)[OF k(1-2)] by auto
@@ -4390,7 +4390,7 @@
from this(2) guess u v apply-by(erule exE)+ note uv=this
have "l\<in>snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto
hence "l\<in>q" "k\<in>q" "l\<noteq>k" using as(1,3) q(1) unfolding r_def by auto
- note q'(5)[OF this] hence "interior l = {}" using subset_interior[OF `l \<subseteq> k`] by blast
+ note q'(5)[OF this] hence "interior l = {}" using interior_mono[OF `l \<subseteq> k`] by blast
thus "content l *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto qed auto
hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x))
@@ -4403,7 +4403,7 @@
have *:"interior (k \<inter> l) = {}" unfolding interior_inter apply(rule q')
using as unfolding r_def by auto
have "interior m = {}" unfolding subset_empty[THEN sym] unfolding *[THEN sym]
- apply(rule subset_interior) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
+ apply(rule interior_mono) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
thus "content m *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto
qed(insert qq, auto)
@@ -4462,6 +4462,61 @@
proof safe case goal1 note * = henstock_lemma_part2[OF assms(1) * d this]
show ?case apply(rule le_less_trans[OF *]) using `e>0` by(auto simp add:field_simps) qed qed
+subsection {* Geometric progression *}
+
+text {* FIXME: Should one or more of these theorems be moved to @{file
+"~~/src/HOL/SetInterval.thy"}, alongside @{text geometric_sum}? *}
+
+lemma sum_gp_basic:
+ fixes x :: "'a::ring_1"
+ shows "(1 - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
+proof-
+ def y \<equiv> "1 - x"
+ have "y * (\<Sum>i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n"
+ by (induct n, simp, simp add: algebra_simps)
+ thus ?thesis
+ unfolding y_def by simp
+qed
+
+lemma sum_gp_multiplied: assumes mn: "m <= n"
+ shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
+ (is "?lhs = ?rhs")
+proof-
+ let ?S = "{0..(n - m)}"
+ from mn have mn': "n - m \<ge> 0" by arith
+ let ?f = "op + m"
+ have i: "inj_on ?f ?S" unfolding inj_on_def by auto
+ have f: "?f ` ?S = {m..n}"
+ using mn apply (auto simp add: image_iff Bex_def) by arith
+ have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"
+ by (rule ext, simp add: power_add power_mult)
+ from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
+ have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
+ then show ?thesis unfolding sum_gp_basic using mn
+ by (simp add: field_simps power_add[symmetric])
+qed
+
+lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
+ (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
+ else (x^ m - x^ (Suc n)) / (1 - x))"
+proof-
+ {assume nm: "n < m" hence ?thesis by simp}
+ moreover
+ {assume "\<not> n < m" hence nm: "m \<le> n" by arith
+ {assume x: "x = 1" hence ?thesis by simp}
+ moreover
+ {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
+ from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
+ ultimately have ?thesis by metis
+ }
+ ultimately show ?thesis by metis
+qed
+
+lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
+ (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
+ unfolding sum_gp[of x m "m + n"] power_Suc
+ by (simp add: field_simps power_add)
+
subsection {* monotone convergence (bounded interval first). *}
lemma monotone_convergence_interval: fixes f::"nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Aug 26 10:38:29 2011 -0700
@@ -8,11 +8,6 @@
imports
Euclidean_Space
"~~/src/HOL/Library/Infinite_Set"
- L2_Norm
- "~~/src/HOL/Library/Convex"
- "~~/src/HOL/Library/Sum_of_Squares"
-uses
- ("normarith.ML")
begin
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
@@ -66,7 +61,7 @@
*)
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
- by (simp add: setL2_def power2_eq_square)
+ by (simp add: power2_eq_square)
lemma norm_cauchy_schwarz:
shows "inner x y <= norm x * norm y"
@@ -154,111 +149,6 @@
then show "x = y" by (simp)
qed
-subsection{* General linear decision procedure for normed spaces. *}
-
-lemma norm_cmul_rule_thm:
- fixes x :: "'a::real_normed_vector"
- shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
- unfolding norm_scaleR
- apply (erule mult_left_mono)
- apply simp
- done
-
- (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
-lemma norm_add_rule_thm:
- fixes x1 x2 :: "'a::real_normed_vector"
- shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
- by (rule order_trans [OF norm_triangle_ineq add_mono])
-
-lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
- by (simp add: field_simps)
-
-lemma pth_1:
- fixes x :: "'a::real_normed_vector"
- shows "x == scaleR 1 x" by simp
-
-lemma pth_2:
- fixes x :: "'a::real_normed_vector"
- shows "x - y == x + -y" by (atomize (full)) simp
-
-lemma pth_3:
- fixes x :: "'a::real_normed_vector"
- shows "- x == scaleR (-1) x" by simp
-
-lemma pth_4:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
-
-lemma pth_5:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
-
-lemma pth_6:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR c (x + y) == scaleR c x + scaleR c y"
- by (simp add: scaleR_right_distrib)
-
-lemma pth_7:
- fixes x :: "'a::real_normed_vector"
- shows "0 + x == x" and "x + 0 == x" by simp_all
-
-lemma pth_8:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR c x + scaleR d x == scaleR (c + d) x"
- by (simp add: scaleR_left_distrib)
-
-lemma pth_9:
- fixes x :: "'a::real_normed_vector" shows
- "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
- "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
- "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
- by (simp_all add: algebra_simps)
-
-lemma pth_a:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR 0 x + y == y" by simp
-
-lemma pth_b:
- fixes x :: "'a::real_normed_vector" shows
- "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
- "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
- "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
- "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
- by (simp_all add: algebra_simps)
-
-lemma pth_c:
- fixes x :: "'a::real_normed_vector" shows
- "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
- "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
- "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
- "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
- by (simp_all add: algebra_simps)
-
-lemma pth_d:
- fixes x :: "'a::real_normed_vector"
- shows "x + 0 == x" by simp
-
-lemma norm_imp_pos_and_ge:
- fixes x :: "'a::real_normed_vector"
- shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
- by atomize auto
-
-lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
-
-lemma norm_pths:
- fixes x :: "'a::real_normed_vector" shows
- "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
- "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
- using norm_ge_zero[of "x - y"] by auto
-
-use "normarith.ML"
-
-method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
-*} "prove simple linear statements about vector norms"
-
-
-text{* Hence more metric properties. *}
-
lemma norm_triangle_half_r:
shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto
@@ -274,16 +164,6 @@
lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
by (metis basic_trans_rules(21) norm_triangle_ineq)
-lemma dist_triangle_add:
- fixes x y x' y' :: "'a::real_normed_vector"
- shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
- by norm
-
-lemma dist_triangle_add_half:
- fixes x x' y y' :: "'a::real_normed_vector"
- shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
- by norm
-
lemma setsum_clauses:
shows "setsum f {} = 0"
and "finite S \<Longrightarrow> setsum f (insert x S) =
@@ -311,12 +191,6 @@
apply (rule setsum_mono_zero_right[OF fT fST])
by (auto intro: setsum_0')
-lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> y = setsum (\<lambda>x. f x \<bullet> y) S "
- apply(induct rule: finite_induct) by(auto simp add: inner_add)
-
-lemma dot_rsum: "finite S \<Longrightarrow> y \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
- apply(induct rule: finite_induct) by(auto simp add: inner_add)
-
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
proof
assume "\<forall>x. x \<bullet> y = x \<bullet> z"
@@ -702,65 +576,6 @@
then show ?thesis by blast
qed
-subsection {* Geometric progression *}
-
-lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
- (is "?lhs = ?rhs")
-proof-
- {assume x1: "x = 1" hence ?thesis by simp}
- moreover
- {assume x1: "x\<noteq>1"
- hence x1': "x - 1 \<noteq> 0" "1 - x \<noteq> 0" "x - 1 = - (1 - x)" "- (1 - x) \<noteq> 0" by auto
- from geometric_sum[OF x1, of "Suc n", unfolded x1']
- have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))"
- unfolding atLeastLessThanSuc_atLeastAtMost
- using x1' apply (auto simp only: field_simps)
- apply (simp add: field_simps)
- done
- then have ?thesis by (simp add: field_simps) }
- ultimately show ?thesis by metis
-qed
-
-lemma sum_gp_multiplied: assumes mn: "m <= n"
- shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
- (is "?lhs = ?rhs")
-proof-
- let ?S = "{0..(n - m)}"
- from mn have mn': "n - m \<ge> 0" by arith
- let ?f = "op + m"
- have i: "inj_on ?f ?S" unfolding inj_on_def by auto
- have f: "?f ` ?S = {m..n}"
- using mn apply (auto simp add: image_iff Bex_def) by arith
- have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"
- by (rule ext, simp add: power_add power_mult)
- from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
- have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
- then show ?thesis unfolding sum_gp_basic using mn
- by (simp add: field_simps power_add[symmetric])
-qed
-
-lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
- (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
- else (x^ m - x^ (Suc n)) / (1 - x))"
-proof-
- {assume nm: "n < m" hence ?thesis by simp}
- moreover
- {assume "\<not> n < m" hence nm: "m \<le> n" by arith
- {assume x: "x = 1" hence ?thesis by simp}
- moreover
- {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
- from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
- ultimately have ?thesis by metis
- }
- ultimately show ?thesis by metis
-qed
-
-lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
- (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
- unfolding sum_gp[of x m "m + n"] power_Suc
- by (simp add: field_simps power_add)
-
-
subsection{* A bit of linear algebra. *}
definition (in real_vector)
@@ -807,6 +622,9 @@
apply (rule_tac x="c *\<^sub>R x" in bexI, auto)
done
+lemma subspace_linear_vimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace (f -` S)"
+ by (auto simp add: subspace_def linear_def linear_0[of f])
+
lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \<in> S}"
by (auto simp add: subspace_def linear_def linear_0[of f])
@@ -816,6 +634,11 @@
lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B ==> subspace (A \<inter> B)"
by (simp add: subspace_def)
+lemma subspace_Times: "\<lbrakk>subspace A; subspace B\<rbrakk> \<Longrightarrow> subspace (A \<times> B)"
+ unfolding subspace_def zero_prod_def by simp
+
+text {* Properties of span. *}
+
lemma (in real_vector) span_mono: "A \<subseteq> B ==> span A \<subseteq> span B"
by (metis span_def hull_mono)
@@ -834,8 +657,16 @@
by (metis span_def hull_subset subset_eq)
(metis subspace_span subspace_def)+
-lemma (in real_vector) span_induct: assumes SP: "\<And>x. x \<in> S ==> x \<in> P"
- and P: "subspace P" and x: "x \<in> span S" shows "x \<in> P"
+lemma span_unique:
+ "\<lbrakk>S \<subseteq> T; subspace T; \<And>T'. \<lbrakk>S \<subseteq> T'; subspace T'\<rbrakk> \<Longrightarrow> T \<subseteq> T'\<rbrakk> \<Longrightarrow> span S = T"
+ unfolding span_def by (rule hull_unique)
+
+lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T"
+ unfolding span_def by (rule hull_minimal)
+
+lemma (in real_vector) span_induct:
+ assumes x: "x \<in> span S" and P: "subspace P" and SP: "\<And>x. x \<in> S ==> x \<in> P"
+ shows "x \<in> P"
proof-
from SP have SP': "S \<subseteq> P" by (simp add: subset_eq)
from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]]
@@ -967,105 +798,76 @@
text {* Mapping under linear image. *}
-lemma span_linear_image: assumes lf: "linear f"
+lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
+ by auto (* TODO: move *)
+
+lemma span_linear_image:
+ assumes lf: "linear f"
shows "span (f ` S) = f ` (span S)"
-proof-
- {fix x
- assume x: "x \<in> span (f ` S)"
- have "x \<in> f ` span S"
- apply (rule span_induct[where x=x and S = "f ` S"])
- apply (clarsimp simp add: image_iff)
- apply (frule span_superset)
- apply blast
- apply (rule subspace_linear_image[OF lf])
- apply (rule subspace_span)
- apply (rule x)
- done}
- moreover
- {fix x assume x: "x \<in> span S"
- have "x \<in> {x. f x \<in> span (f ` S)}"
- apply (rule span_induct[where S=S])
- apply simp
- apply (rule span_superset)
- apply simp
- apply (rule subspace_linear_preimage[OF lf subspace_span, of "f ` S"])
- apply (rule x)
- done
- hence "f x \<in> span (f ` S)" by simp
- }
- ultimately show ?thesis by blast
+proof (rule span_unique)
+ show "f ` S \<subseteq> f ` span S"
+ by (intro image_mono span_inc)
+ show "subspace (f ` span S)"
+ using lf subspace_span by (rule subspace_linear_image)
+next
+ fix T assume "f ` S \<subseteq> T" and "subspace T" thus "f ` span S \<subseteq> T"
+ unfolding image_subset_iff_subset_vimage
+ by (intro span_minimal subspace_linear_vimage lf)
+qed
+
+lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
+proof (rule span_unique)
+ show "A \<union> B \<subseteq> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
+ by safe (force intro: span_clauses)+
+next
+ have "linear (\<lambda>(a, b). a + b)"
+ by (simp add: linear_def scaleR_add_right)
+ moreover have "subspace (span A \<times> span B)"
+ by (intro subspace_Times subspace_span)
+ ultimately show "subspace ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
+ by (rule subspace_linear_image)
+next
+ fix T assume "A \<union> B \<subseteq> T" and "subspace T"
+ thus "(\<lambda>(a, b). a + b) ` (span A \<times> span B) \<subseteq> T"
+ by (auto intro!: subspace_add elim: span_induct)
qed
text {* The key breakdown property. *}
+lemma span_singleton: "span {x} = range (\<lambda>k. k *\<^sub>R x)"
+proof (rule span_unique)
+ show "{x} \<subseteq> range (\<lambda>k. k *\<^sub>R x)"
+ by (fast intro: scaleR_one [symmetric])
+ show "subspace (range (\<lambda>k. k *\<^sub>R x))"
+ unfolding subspace_def
+ by (auto intro: scaleR_add_left [symmetric])
+ fix T assume "{x} \<subseteq> T" and "subspace T" thus "range (\<lambda>k. k *\<^sub>R x) \<subseteq> T"
+ unfolding subspace_def by auto
+qed
+
+lemma span_insert:
+ "span (insert a S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
+proof -
+ have "span ({a} \<union> S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
+ unfolding span_union span_singleton
+ apply safe
+ apply (rule_tac x=k in exI, simp)
+ apply (erule rev_image_eqI [OF SigmaI [OF rangeI]])
+ apply simp
+ apply (rule right_minus)
+ done
+ thus ?thesis by simp
+qed
+
lemma span_breakdown:
assumes bS: "b \<in> S" and aS: "a \<in> span S"
- shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})" (is "?P a")
-proof-
- {fix x assume xS: "x \<in> S"
- {assume ab: "x = b"
- then have "?P x"
- apply simp
- apply (rule exI[where x="1"], simp)
- by (rule span_0)}
- moreover
- {assume ab: "x \<noteq> b"
- then have "?P x" using xS
- apply -
- apply (rule exI[where x=0])
- apply (rule span_superset)
- by simp}
- ultimately have "x \<in> Collect ?P" by blast}
- moreover have "subspace (Collect ?P)"
- unfolding subspace_def
- apply auto
- apply (rule exI[where x=0])
- using span_0[of "S - {b}"]
- apply simp
- apply (rule_tac x="k + ka" in exI)
- apply (subgoal_tac "x + y - (k + ka) *\<^sub>R b = (x - k*\<^sub>R b) + (y - ka *\<^sub>R b)")
- apply (simp only: )
- apply (rule span_add)
- apply assumption+
- apply (simp add: algebra_simps)
- apply (rule_tac x= "c*k" in exI)
- apply (subgoal_tac "c *\<^sub>R x - (c * k) *\<^sub>R b = c*\<^sub>R (x - k*\<^sub>R b)")
- apply (simp only: )
- apply (rule span_mul)
- apply assumption
- by (simp add: algebra_simps)
- ultimately have "a \<in> Collect ?P" using aS by (rule span_induct)
- thus "?P a" by simp
-qed
+ shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})"
+ using assms span_insert [of b "S - {b}"]
+ by (simp add: insert_absorb)
lemma span_breakdown_eq:
- "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x - k *\<^sub>R a) \<in> span S)" (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
- {assume x: "x \<in> span (insert a S)"
- from x span_breakdown[of "a" "insert a S" "x"]
- have ?rhs apply clarsimp
- apply (rule_tac x= "k" in exI)
- apply (rule set_rev_mp[of _ "span (S - {a})" _])
- apply assumption
- apply (rule span_mono)
- apply blast
- done}
- moreover
- { fix k assume k: "x - k *\<^sub>R a \<in> span S"
- have eq: "x = (x - k *\<^sub>R a) + k *\<^sub>R a" by simp
- have "(x - k *\<^sub>R a) + k *\<^sub>R a \<in> span (insert a S)"
- apply (rule span_add)
- apply (rule set_rev_mp[of _ "span S" _])
- apply (rule k)
- apply (rule span_mono)
- apply blast
- apply (rule span_mul)
- apply (rule span_superset)
- apply blast
- done
- then have ?lhs using eq by metis}
- ultimately show ?thesis by blast
-qed
+ "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x - k *\<^sub>R a) \<in> span S)"
+ by (simp add: span_insert)
text {* Hence some "reversal" results. *}
@@ -1122,26 +924,16 @@
text {* Transitivity property. *}
+lemma span_redundant: "x \<in> span S \<Longrightarrow> span (insert x S) = span S"
+ unfolding span_def by (rule hull_redundant)
+
lemma span_trans:
assumes x: "x \<in> span S" and y: "y \<in> span (insert x S)"
shows "y \<in> span S"
-proof-
- from span_breakdown[of x "insert x S" y, OF insertI1 y]
- obtain k where k: "y -k*\<^sub>R x \<in> span (S - {x})" by auto
- have eq: "y = (y - k *\<^sub>R x) + k *\<^sub>R x" by simp
- show ?thesis
- apply (subst eq)
- apply (rule span_add)
- apply (rule set_rev_mp)
- apply (rule k)
- apply (rule span_mono)
- apply blast
- apply (rule span_mul)
- by (rule x)
-qed
+ using assms by (simp only: span_redundant)
lemma span_insert_0[simp]: "span (insert 0 S) = span S"
- using span_mono[of S "insert 0 S"] by (auto intro: span_trans span_0)
+ by (simp only: span_redundant span_0)
text {* An explicit expansion is sometimes needed. *}
@@ -1273,43 +1065,6 @@
ultimately show ?thesis by blast
qed
-lemma Int_Un_cancel: "(A \<union> B) \<inter> A = A" "(A \<union> B) \<inter> B = B" by auto
-
-lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
-proof safe
- fix x assume "x \<in> span (A \<union> B)"
- then obtain S u where S: "finite S" "S \<subseteq> A \<union> B" and x: "x = (\<Sum>v\<in>S. u v *\<^sub>R v)"
- unfolding span_explicit by auto
-
- let ?Sa = "\<Sum>v\<in>S\<inter>A. u v *\<^sub>R v"
- let ?Sb = "(\<Sum>v\<in>S\<inter>(B - A). u v *\<^sub>R v)"
- show "x \<in> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
- proof
- show "x = (case (?Sa, ?Sb) of (a, b) \<Rightarrow> a + b)"
- unfolding x using S
- by (simp, subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
-
- from S have "?Sa \<in> span A" unfolding span_explicit
- by (auto intro!: exI[of _ "S \<inter> A"])
- moreover from S have "?Sb \<in> span B" unfolding span_explicit
- by (auto intro!: exI[of _ "S \<inter> (B - A)"])
- ultimately show "(?Sa, ?Sb) \<in> span A \<times> span B" by simp
- qed
-next
- fix a b assume "a \<in> span A" and "b \<in> span B"
- then obtain Sa ua Sb ub where span:
- "finite Sa" "Sa \<subseteq> A" "a = (\<Sum>v\<in>Sa. ua v *\<^sub>R v)"
- "finite Sb" "Sb \<subseteq> B" "b = (\<Sum>v\<in>Sb. ub v *\<^sub>R v)"
- unfolding span_explicit by auto
- let "?u v" = "(if v \<in> Sa then ua v else 0) + (if v \<in> Sb then ub v else 0)"
- from span have "finite (Sa \<union> Sb)" "Sa \<union> Sb \<subseteq> A \<union> B"
- and "a + b = (\<Sum>v\<in>(Sa\<union>Sb). ?u v *\<^sub>R v)"
- unfolding setsum_addf scaleR_left_distrib
- by (auto simp add: if_distrib cond_application_beta setsum_cases Int_Un_cancel)
- thus "a + b \<in> span (A \<union> B)"
- unfolding span_explicit by (auto intro!: exI[of _ ?u])
-qed
-
text {* This is useful for building a basis step-by-step. *}
lemma independent_insert:
@@ -1495,30 +1250,6 @@
apply (simp add: inner_setsum_right dot_basis)
done
-lemma dimensionI:
- assumes "\<And>d. \<lbrakk> 0 < d; basis ` {d..} = {0::'a::euclidean_space};
- independent (basis ` {..<d} :: 'a set);
- inj_on (basis :: nat \<Rightarrow> 'a) {..<d} \<rbrakk> \<Longrightarrow> P d"
- shows "P DIM('a::euclidean_space)"
- using DIM_positive basis_finite independent_basis basis_inj
- by (rule assms)
-
-lemma (in euclidean_space) dimension_eq:
- assumes "\<And>i. i < d \<Longrightarrow> basis i \<noteq> 0"
- assumes "\<And>i. d \<le> i \<Longrightarrow> basis i = 0"
- shows "DIM('a) = d"
-proof (rule linorder_cases [of "DIM('a)" d])
- assume "DIM('a) < d"
- hence "basis DIM('a) \<noteq> 0" by (rule assms)
- thus ?thesis by simp
-next
- assume "d < DIM('a)"
- hence "basis d \<noteq> 0" by simp
- thus ?thesis by (simp add: assms)
-next
- assume "DIM('a) = d" thus ?thesis .
-qed
-
lemma (in euclidean_space) range_basis:
"range basis = insert 0 (basis ` {..<DIM('a)})"
proof -
@@ -1628,22 +1359,6 @@
ultimately show ?thesis by metis
qed
-subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
-
-class ordered_euclidean_space = ord + euclidean_space +
- assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i \<le> y $$ i)"
- and eucl_less: "x < y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i < y $$ i)"
-
-lemma eucl_less_not_refl[simp, intro!]: "\<not> x < (x::'a::ordered_euclidean_space)"
- unfolding eucl_less[where 'a='a] by auto
-
-lemma euclidean_trans[trans]:
- fixes x y z :: "'a::ordered_euclidean_space"
- shows "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
- and "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
- and "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
- by (force simp: eucl_less[where 'a='a] eucl_le[where 'a='a])+
-
subsection {* Linearity and Bilinearity continued *}
lemma linear_bounded:
@@ -2035,8 +1750,15 @@
lemma vector_sub_project_orthogonal: "(b::'a::euclidean_space) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *\<^sub>R b) = 0"
unfolding inner_simps by auto
+lemma pairwise_orthogonal_insert:
+ assumes "pairwise orthogonal S"
+ assumes "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
+ shows "pairwise orthogonal (insert x S)"
+ using assms unfolding pairwise_def
+ by (auto simp add: orthogonal_commute)
+
lemma basis_orthogonal:
- fixes B :: "('a::euclidean_space) set"
+ fixes B :: "('a::real_inner) set"
assumes fB: "finite B"
shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C"
(is " \<exists>C. ?P B C")
@@ -2064,48 +1786,20 @@
by (rule span_superset)}
then have SC: "span ?C = span (insert a B)"
unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto
- thm pairwise_def
- {fix x y assume xC: "x \<in> ?C" and yC: "y \<in> ?C" and xy: "x \<noteq> y"
- {assume xa: "x = ?a" and ya: "y = ?a"
- have "orthogonal x y" using xa ya xy by blast}
- moreover
- {assume xa: "x = ?a" and ya: "y \<noteq> ?a" "y \<in> C"
- from ya have Cy: "C = insert y (C - {y})" by blast
- have fth: "finite (C - {y})" using C by simp
- have "orthogonal x y"
- using xa ya
- unfolding orthogonal_def xa inner_simps diff_eq_0_iff_eq
- apply simp
- apply (subst Cy)
- using C(1) fth
- apply (simp only: setsum_clauses)
- apply (auto simp add: inner_add inner_commute[of y a] dot_lsum[OF fth])
- apply (rule setsum_0')
- apply clarsimp
- apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
- by auto}
- moreover
- {assume xa: "x \<noteq> ?a" "x \<in> C" and ya: "y = ?a"
- from xa have Cx: "C = insert x (C - {x})" by blast
- have fth: "finite (C - {x})" using C by simp
- have "orthogonal x y"
- using xa ya
- unfolding orthogonal_def ya inner_simps diff_eq_0_iff_eq
- apply simp
- apply (subst Cx)
- using C(1) fth
- apply (simp only: setsum_clauses)
- apply (subst inner_commute[of x])
- apply (auto simp add: inner_add inner_commute[of x a] dot_rsum[OF fth])
- apply (rule setsum_0')
- apply clarsimp
- apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
- by auto}
- moreover
- {assume xa: "x \<in> C" and ya: "y \<in> C"
- have "orthogonal x y" using xa ya xy C(4) unfolding pairwise_def by blast}
- ultimately have "orthogonal x y" using xC yC by blast}
- then have CPO: "pairwise orthogonal ?C" unfolding pairwise_def by blast
+ { fix y assume yC: "y \<in> C"
+ hence Cy: "C = insert y (C - {y})" by blast
+ have fth: "finite (C - {y})" using C by simp
+ have "orthogonal ?a y"
+ unfolding orthogonal_def
+ unfolding inner_diff inner_setsum_left diff_eq_0_iff_eq
+ unfolding setsum_diff1' [OF `finite C` `y \<in> C`]
+ apply (clarsimp simp add: inner_commute[of y a])
+ apply (rule setsum_0')
+ apply clarsimp
+ apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
+ using `y \<in> C` by auto }
+ with `pairwise orthogonal C` have CPO: "pairwise orthogonal ?C"
+ by (rule pairwise_orthogonal_insert)
from fC cC SC CPO have "?P (insert a B) ?C" by blast
then show ?case by blast
qed
@@ -2166,7 +1860,7 @@
apply (subst B') using fB fth
unfolding setsum_clauses(2)[OF fth]
apply simp unfolding inner_simps
- apply (clarsimp simp add: inner_add dot_lsum)
+ apply (clarsimp simp add: inner_add inner_setsum_left)
apply (rule setsum_0', rule ballI)
unfolding inner_commute
by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
@@ -3017,7 +2711,23 @@
apply simp
done
-subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
+subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
+
+class ordered_euclidean_space = ord + euclidean_space +
+ assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i \<le> y $$ i)"
+ and eucl_less: "x < y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i < y $$ i)"
+
+lemma eucl_less_not_refl[simp, intro!]: "\<not> x < (x::'a::ordered_euclidean_space)"
+ unfolding eucl_less[where 'a='a] by auto
+
+lemma euclidean_trans[trans]:
+ fixes x y z :: "'a::ordered_euclidean_space"
+ shows "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
+ and "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
+ and "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
+ unfolding eucl_less[where 'a='a] eucl_le[where 'a='a]
+ by (fast intro: less_trans, fast intro: le_less_trans,
+ fast intro: order_trans)
lemma basis_real_range: "basis ` {..<1} = {1::real}" by auto
@@ -3036,8 +2746,6 @@
shows "basis 0 = (1::complex)" and "basis 1 = ii" and "basis (Suc 0) = ii"
unfolding basis_complex_def by auto
-subsection {* Products Spaces *}
-
lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::euclidean_space) + DIM('a::euclidean_space)"
(* FIXME: why this orientation? Why not "DIM('a) + DIM('b)" ? *)
unfolding dimension_prod_def by (rule add_commute)
@@ -3051,5 +2759,4 @@
instance proof qed (auto simp: less_prod_def less_eq_prod_def)
end
-
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy Fri Aug 26 10:38:29 2011 -0700
@@ -0,0 +1,124 @@
+(* Title: HOL/Multivariate_Analysis/Norm_Arith.thy
+ Author: Amine Chaieb, University of Cambridge
+*)
+
+header {* General linear decision procedure for normed spaces *}
+
+theory Norm_Arith
+imports "~~/src/HOL/Library/Sum_of_Squares"
+uses ("normarith.ML")
+begin
+
+lemma norm_cmul_rule_thm:
+ fixes x :: "'a::real_normed_vector"
+ shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
+ unfolding norm_scaleR
+ apply (erule mult_left_mono)
+ apply simp
+ done
+
+ (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
+lemma norm_add_rule_thm:
+ fixes x1 x2 :: "'a::real_normed_vector"
+ shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
+ by (rule order_trans [OF norm_triangle_ineq add_mono])
+
+lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
+ by (simp add: field_simps)
+
+lemma pth_1:
+ fixes x :: "'a::real_normed_vector"
+ shows "x == scaleR 1 x" by simp
+
+lemma pth_2:
+ fixes x :: "'a::real_normed_vector"
+ shows "x - y == x + -y" by (atomize (full)) simp
+
+lemma pth_3:
+ fixes x :: "'a::real_normed_vector"
+ shows "- x == scaleR (-1) x" by simp
+
+lemma pth_4:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
+
+lemma pth_5:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
+
+lemma pth_6:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c (x + y) == scaleR c x + scaleR c y"
+ by (simp add: scaleR_right_distrib)
+
+lemma pth_7:
+ fixes x :: "'a::real_normed_vector"
+ shows "0 + x == x" and "x + 0 == x" by simp_all
+
+lemma pth_8:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c x + scaleR d x == scaleR (c + d) x"
+ by (simp add: scaleR_left_distrib)
+
+lemma pth_9:
+ fixes x :: "'a::real_normed_vector" shows
+ "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
+ "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
+ "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
+ by (simp_all add: algebra_simps)
+
+lemma pth_a:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR 0 x + y == y" by simp
+
+lemma pth_b:
+ fixes x :: "'a::real_normed_vector" shows
+ "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
+ "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
+ "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
+ "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
+ by (simp_all add: algebra_simps)
+
+lemma pth_c:
+ fixes x :: "'a::real_normed_vector" shows
+ "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
+ "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
+ "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
+ "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
+ by (simp_all add: algebra_simps)
+
+lemma pth_d:
+ fixes x :: "'a::real_normed_vector"
+ shows "x + 0 == x" by simp
+
+lemma norm_imp_pos_and_ge:
+ fixes x :: "'a::real_normed_vector"
+ shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
+ by atomize auto
+
+lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
+
+lemma norm_pths:
+ fixes x :: "'a::real_normed_vector" shows
+ "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
+ "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
+ using norm_ge_zero[of "x - y"] by auto
+
+use "normarith.ML"
+
+method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
+*} "prove simple linear statements about vector norms"
+
+text{* Hence more metric properties. *}
+
+lemma dist_triangle_add:
+ fixes x y x' y' :: "'a::real_normed_vector"
+ shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
+ by norm
+
+lemma dist_triangle_add_half:
+ fixes x x' y y' :: "'a::real_normed_vector"
+ shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
+ by norm
+
+end
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Aug 26 10:38:29 2011 -0700
@@ -92,7 +92,7 @@
lemma path_reversepath[simp]: "path(reversepath g) \<longleftrightarrow> path g" proof-
have *:"\<And>g. path g \<Longrightarrow> path(reversepath g)" unfolding path_def reversepath_def
apply(rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
- apply(rule continuous_on_sub, rule continuous_on_const, rule continuous_on_id)
+ apply(intro continuous_on_intros)
apply(rule continuous_on_subset[of "{0..1}"], assumption) by auto
show ?thesis using *[of "reversepath g"] *[of g] unfolding reversepath_reversepath by (rule iffI) qed
@@ -108,8 +108,9 @@
by auto
thus "continuous_on {0..1} g1 \<and> continuous_on {0..1} g2" apply -apply rule
apply(subst *) defer apply(subst *) apply (rule_tac[!] continuous_on_compose)
- apply (rule continuous_on_cmul, rule continuous_on_add, rule continuous_on_id, rule continuous_on_const) defer
- apply (rule continuous_on_cmul, rule continuous_on_id) apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
+ apply (intro continuous_on_intros) defer
+ apply (intro continuous_on_intros)
+ apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
apply(rule_tac[1-2] continuous_on_subset[of "{0 .. 1}"]) apply(rule as, assumption, rule as, assumption)
apply(rule) defer apply rule proof-
fix x assume "x \<in> op *\<^sub>R (1 / 2) ` {0::real..1}"
@@ -132,10 +133,10 @@
done
show "continuous_on {0..1} (g1 +++ g2)" unfolding * apply(rule continuous_on_union) apply (rule closed_real_atLeastAtMost)+ proof-
show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "\<lambda>x. g1 (2 *\<^sub>R x)"]) defer
- unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply(rule continuous_on_cmul, rule continuous_on_id)
+ unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply (intro continuous_on_intros)
unfolding ** apply(rule as(1)) unfolding joinpaths_def by auto next
show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "g2 \<circ> (\<lambda>x. 2 *\<^sub>R x - 1)"]) defer
- apply(rule continuous_on_compose) apply(rule continuous_on_sub, rule continuous_on_cmul, rule continuous_on_id, rule continuous_on_const)
+ apply(rule continuous_on_compose) apply (intro continuous_on_intros)
unfolding *** o_def joinpaths_def apply(rule as(2)) using assms[unfolded pathstart_def pathfinish_def]
by (auto simp add: mult_ac) qed qed
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 26 22:53:04 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 26 10:38:29 2011 -0700
@@ -7,7 +7,7 @@
header {* Elementary topology in Euclidean space. *}
theory Topology_Euclidean_Space
-imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs"
+imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm
begin
(* to be moved elsewhere *)
@@ -20,7 +20,7 @@
apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
apply(rule member_le_setL2) by auto
-subsection {* General notion of a topologies as values *}
+subsection {* General notion of a topology as a value *}
definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
@@ -555,37 +555,61 @@
subsection {* Interior of a Set *}
-definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
+definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
+
+lemma interiorI [intro?]:
+ assumes "open T" and "x \<in> T" and "T \<subseteq> S"
+ shows "x \<in> interior S"
+ using assms unfolding interior_def by fast
+
+lemma interiorE [elim?]:
+ assumes "x \<in> interior S"
+ obtains T where "open T" and "x \<in> T" and "T \<subseteq> S"
+ using assms unfolding interior_def by fast
+
+lemma open_interior [simp, intro]: "open (interior S)"
+ by (simp add: interior_def open_Union)
+
+lemma interior_subset: "interior S \<subseteq> S"
+ by (auto simp add: interior_def)
+
+lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S"
+ by (auto simp add: interior_def)
+
+lemma interior_open: "open S \<Longrightarrow> interior S = S"
+ by (intro equalityI interior_subset interior_maximal subset_refl)
lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
- apply (simp add: set_eq_iff interior_def)
- apply (subst (2) open_subopen) by (safe, blast+)
-
-lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq)
-
-lemma interior_empty[simp]: "interior {} = {}" by (simp add: interior_def)
-
-lemma open_interior[simp, intro]: "open(interior S)"
- apply (simp add: interior_def)
- apply (subst open_subopen) by blast
-
-lemma interior_interior[simp]: "interior(interior S) = interior S" by (metis interior_eq open_interior)
-lemma interior_subset: "interior S \<subseteq> S" by (auto simp add: interior_def)
-lemma subset_interior: "S \<subseteq> T ==> (interior S) \<subseteq> (interior T)" by (auto simp add: interior_def)
-lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T ==> T \<subseteq> (interior S)" by (auto simp add: interior_def)
-lemma interior_unique: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> (\<forall>T'. T' \<subseteq> S \<and> open T' \<longrightarrow> T' \<subseteq> T) \<Longrightarrow> interior S = T"
- by (metis equalityI interior_maximal interior_subset open_interior)
-lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e. 0 < e \<and> ball x e \<subseteq> S)"
- apply (simp add: interior_def)
- by (metis open_contains_ball centre_in_ball open_ball subset_trans)
-
-lemma open_subset_interior: "open S ==> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
+ by (metis open_interior interior_open)
+
+lemma open_subset_interior: "open S \<Longrightarrow> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
by (metis interior_maximal interior_subset subset_trans)
-lemma interior_inter[simp]: "interior(S \<inter> T) = interior S \<inter> interior T"
- apply (rule equalityI, simp)
- apply (metis Int_lower1 Int_lower2 subset_interior)
- by (metis Int_mono interior_subset open_Int open_interior open_subset_interior)
+lemma interior_empty [simp]: "interior {} = {}"
+ using open_empty by (rule interior_open)
+
+lemma interior_UNIV [simp]: "interior UNIV = UNIV"
+ using open_UNIV by (rule interior_open)
+
+lemma interior_interior [simp]: "interior (interior S) = interior S"
+ using open_interior by (rule interior_open)
+
+lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
+ by (auto simp add: interior_def)
+
+lemma interior_unique:
+ assumes "T \<subseteq> S" and "open T"
+ assumes "\<And>T'. T' \<subseteq> S \<Longrightarrow> open T' \<Longrightarrow> T' \<subseteq> T"
+ 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"
+ by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
+ Int_lower2 interior_maximal interior_subset open_Int open_interior)
+
+lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
+ using open_contains_ball_eq [where S="interior S"]
+ by (simp add: open_subset_interior)
lemma interior_limit_point [intro]:
fixes x :: "'a::perfect_space"
@@ -599,21 +623,20 @@
lemma interior_closed_Un_empty_interior:
assumes cS: "closed S" and iT: "interior T = {}"
- shows "interior(S \<union> T) = interior S"
+ shows "interior (S \<union> T) = interior S"
proof
- show "interior S \<subseteq> interior (S\<union>T)"
- by (rule subset_interior, blast)
+ show "interior S \<subseteq> interior (S \<union> T)"
+ by (rule interior_mono, rule Un_upper1)
next
show "interior (S \<union> T) \<subseteq> interior S"
proof
fix x assume "x \<in> interior (S \<union> T)"
- then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T"
- unfolding interior_def by fast
+ then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
show "x \<in> interior S"
proof (rule ccontr)
assume "x \<notin> interior S"
with `x \<in> R` `open R` obtain y where "y \<in> R - S"
- unfolding interior_def set_eq_iff by fast
+ unfolding interior_def by fast
from `open R` `closed S` have "open (R - S)" by (rule open_Diff)
from `R \<subseteq> S \<union> T` have "R - S \<subseteq> T" by fast
from `y \<in> R - S` `open (R - S)` `R - S \<subseteq> T` `interior T = {}`
@@ -628,15 +651,16 @@
by (intro Sigma_mono interior_subset)
show "open (interior A \<times> interior B)"
by (intro open_Times open_interior)
- show "\<forall>T. T \<subseteq> A \<times> B \<and> open T \<longrightarrow> T \<subseteq> interior A \<times> interior B"
- apply (simp add: open_prod_def, clarify)
- apply (drule (1) bspec, clarify, rename_tac C D)
- apply (simp add: interior_def, rule conjI)
- apply (rule_tac x=C in exI, clarsimp)
- apply (rule SigmaD1, erule subsetD, erule subsetD, erule (1) SigmaI)
- apply (rule_tac x=D in exI, clarsimp)
- apply (rule SigmaD2, erule subsetD, erule subsetD, erule (1) SigmaI)
- done
+ fix T assume "T \<subseteq> A \<times> B" and "open T" thus "T \<subseteq> interior A \<times> interior B"
+ proof (safe)
+ fix x y assume "(x, y) \<in> T"
+ then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
+ using `open T` unfolding open_prod_def by fast
+ hence "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
+ using `T \<subseteq> A \<times> B` by auto
+ thus "x \<in> interior A" and "y \<in> interior B"
+ by (auto intro: interiorI)
+ qed
qed
@@ -644,119 +668,50 @@
definition "closure S = S \<union> {x | x. x islimpt S}"
+lemma interior_closure: "interior S = - (closure (- S))"
+ unfolding interior_def closure_def islimpt_def by auto
+
lemma closure_interior: "closure S = - interior (- S)"
-proof-
- { fix x
- have "x\<in>- interior (- S) \<longleftrightarrow> x \<in> closure S" (is "?lhs = ?rhs")
- proof
- let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> - S)"
- assume "?lhs"
- hence *:"\<not> ?exT x"
- unfolding interior_def
- by simp
- { assume "\<not> ?rhs"
- hence False using *
- unfolding closure_def islimpt_def
- by blast
- }
- thus "?rhs"
- by blast
- next
- assume "?rhs" thus "?lhs"
- unfolding closure_def interior_def islimpt_def
- by blast
- qed
- }
- thus ?thesis
- by blast
-qed
-
-lemma interior_closure: "interior S = - (closure (- S))"
-proof-
- { fix x
- have "x \<in> interior S \<longleftrightarrow> x \<in> - (closure (- S))"
- unfolding interior_def closure_def islimpt_def
- by auto
- }
- thus ?thesis
- by blast
-qed
+ unfolding interior_closure by simp
lemma closed_closure[simp, intro]: "closed (closure S)"
-proof-
- have "closed (- interior (-S))" by blast
- thus ?thesis using closure_interior[of S] by simp
-qed
+ unfolding closure_interior by (simp add: closed_Compl)
+
+lemma closure_subset: "S \<subseteq> closure S"
+ unfolding closure_def by simp
lemma closure_hull: "closure S = closed hull S"
-proof-
- have "S \<subseteq> closure S"
- unfolding closure_def
- by blast
- moreover
- have "closed (closure S)"
- using closed_closure[of S]
- by assumption
- moreover
- { fix t
- assume *:"S \<subseteq> t" "closed t"
- { fix x
- assume "x islimpt S"
- hence "x islimpt t" using *(1)
- using islimpt_subset[of x, of S, of t]
- by blast
- }
- with * have "closure S \<subseteq> t"
- unfolding closure_def
- using closed_limpt[of t]
- by auto
- }
- ultimately show ?thesis
- using hull_unique[of S, of "closure S", of closed]
- by simp
-qed
+ unfolding hull_def closure_interior interior_def by auto
lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
- unfolding closure_hull
- using hull_eq[of closed, OF closed_Inter, of S]
- by metis
-
-lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S"
- using closure_eq[of S]
- by simp
-
-lemma closure_closure[simp]: "closure (closure S) = closure S"
- unfolding closure_hull
- using hull_hull[of closed S]
- by assumption
-
-lemma closure_subset: "S \<subseteq> closure S"
- unfolding closure_hull
- using hull_subset[of S closed]
- by assumption
-
-lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
- unfolding closure_hull
- using hull_mono[of S T closed]
- by assumption
-
-lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
- using hull_minimal[of S T closed]
- unfolding closure_hull
- by simp
-
-lemma closure_unique: "S \<subseteq> T \<and> closed T \<and> (\<forall> T'. S \<subseteq> T' \<and> closed T' \<longrightarrow> T \<subseteq> T') \<Longrightarrow> closure S = T"
- using hull_unique[of S T closed]
- unfolding closure_hull
- by simp
-
-lemma closure_empty[simp]: "closure {} = {}"
- using closed_empty closure_closed[of "{}"]
- by simp
-
-lemma closure_univ[simp]: "closure UNIV = UNIV"
- using closure_closed[of UNIV]
- by simp
+ unfolding closure_hull using closed_Inter by (rule hull_eq)
+
+lemma closure_closed [simp]: "closed S \<Longrightarrow> closure S = S"
+ unfolding closure_eq .
+
+lemma closure_closure [simp]: "closure (closure S) = closure S"
+ unfolding closure_hull by (rule hull_hull)
+
+lemma closure_mono: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
+ unfolding closure_hull by (rule hull_mono)
+
+lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
+ unfolding closure_hull by (rule hull_minimal)
+
+lemma closure_unique:
+ assumes "S \<subseteq> T" and "closed T"
+ assumes "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
+ shows "closure S = T"
+ using assms unfolding closure_hull by (rule hull_unique)
+
+lemma closure_empty [simp]: "closure {} = {}"
+ using closed_empty by (rule closure_closed)
+
+lemma closure_UNIV [simp]: "closure UNIV = UNIV"
+ using closed_UNIV by (rule closure_closed)
+
+lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
+ unfolding closure_interior by simp
lemma closure_eq_empty: "closure S = {} \<longleftrightarrow> S = {}"
using closure_empty closure_subset[of S]
@@ -797,26 +752,19 @@
by blast
qed
-lemma closure_complement: "closure(- S) = - interior(S)"
-proof-
- have "S = - (- S)"
- by auto
- thus ?thesis
- unfolding closure_interior
- by auto
-qed
-
-lemma interior_complement: "interior(- S) = - closure(S)"
- unfolding closure_interior
- by blast
+lemma closure_complement: "closure (- S) = - interior S"
+ unfolding closure_interior by simp
+
+lemma interior_complement: "interior (- S) = - closure S"
+ unfolding closure_interior by simp
lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
-proof (intro closure_unique conjI)
+proof (rule closure_unique)
show "A \<times> B \<subseteq> closure A \<times> closure B"
by (intro Sigma_mono closure_subset)
show "closed (closure A \<times> closure B)"
by (intro closed_Times closed_closure)
- show "\<forall>T. A \<times> B \<subseteq> T \<and> closed T \<longrightarrow> closure A \<times> closure B \<subseteq> T"
+ fix T assume "A \<times> B \<subseteq> T" and "closed T" thus "closure A \<times> closure B \<subseteq> T"
apply (simp add: closed_def open_prod_def, clarify)
apply (rule ccontr)
apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
@@ -1090,8 +1038,7 @@
assumes "x \<in> interior S"
shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
proof-
- from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
- unfolding interior_def by fast
+ from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
{ assume "?lhs"
then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
unfolding Limits.eventually_within Limits.eventually_at_topological
@@ -2783,8 +2730,8 @@
fixes x :: "'a::t1_space"
shows "closure (insert x s) = insert x (closure s)"
apply (rule closure_unique)
-apply (rule conjI [OF insert_mono [OF closure_subset]])
-apply (rule conjI [OF closed_insert [OF closed_closure]])
+apply (rule insert_mono [OF closure_subset])
+apply (rule closed_insert [OF closed_closure])
apply (simp add: closure_minimal)
done
@@ -3351,10 +3298,9 @@
unfolding continuous_on by (metis subset_eq Lim_within_subset)
lemma continuous_on_interior:
- shows "continuous_on s f \<Longrightarrow> x \<in> interior s ==> continuous (at x) f"
-unfolding interior_def
-apply simp
-by (meson continuous_on_eq_continuous_at continuous_on_subset)
+ shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
+ by (erule interiorE, drule (1) continuous_on_subset,
+ simp add: continuous_on_eq_continuous_at)
lemma continuous_on_eq:
"(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
@@ -3363,56 +3309,41 @@
text {* Characterization of various kinds of continuity in terms of sequences. *}
-(* \<longrightarrow> could be generalized, but \<longleftarrow> requires metric space *)
lemma continuous_within_sequentially:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
shows "continuous (at a within s) f \<longleftrightarrow>
(\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x ---> a) sequentially
--> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs")
proof
assume ?lhs
- { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (x n) a < e"
- fix e::real assume "e>0"
- from `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e" unfolding continuous_within Lim_within using `e>0` by auto
- from x(2) `d>0` obtain N where N:"\<forall>n\<ge>N. dist (x n) a < d" by auto
- hence "\<exists>N. \<forall>n\<ge>N. dist ((f \<circ> x) n) (f a) < e"
- apply(rule_tac x=N in exI) using N d apply auto using x(1)
- apply(erule_tac x=n in allE) apply(erule_tac x=n in allE)
- apply(erule_tac x="x n" in ballE) apply auto unfolding dist_nz[THEN sym] apply auto using `e>0` by auto
+ { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. eventually (\<lambda>n. dist (x n) a < e) sequentially"
+ fix T::"'b set" assume "open T" and "f a \<in> T"
+ with `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
+ unfolding continuous_within tendsto_def eventually_within by auto
+ have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
+ using x(2) `d>0` by simp
+ hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
+ proof (rule eventually_elim1)
+ fix n assume "dist (x n) a < d" thus "(f \<circ> x) n \<in> T"
+ using d x(1) `f a \<in> T` unfolding dist_nz[THEN sym] by auto
+ qed
}
- thus ?rhs unfolding continuous_within unfolding Lim_sequentially by simp
+ thus ?rhs unfolding tendsto_iff unfolding tendsto_def by simp
next
- assume ?rhs
- { fix e::real assume "e>0"
- assume "\<not> (\<exists>d>0. \<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e)"
- hence "\<forall>d. \<exists>x. d>0 \<longrightarrow> x\<in>s \<and> (0 < dist x a \<and> dist x a < d \<and> \<not> dist (f x) (f a) < e)" by blast
- then obtain x where x:"\<forall>d>0. x d \<in> s \<and> (0 < dist (x d) a \<and> dist (x d) a < d \<and> \<not> dist (f (x d)) (f a) < e)"
- using choice[of "\<lambda>d x.0<d \<longrightarrow> x\<in>s \<and> (0 < dist x a \<and> dist x a < d \<and> \<not> dist (f x) (f a) < e)"] by auto
- { fix d::real assume "d>0"
- hence "\<exists>N::nat. inverse (real (N + 1)) < d" using real_arch_inv[of d] by (auto, rule_tac x="n - 1" in exI)auto
- then obtain N::nat where N:"inverse (real (N + 1)) < d" by auto
- { fix n::nat assume n:"n\<ge>N"
- hence "dist (x (inverse (real (n + 1)))) a < inverse (real (n + 1))" using x[THEN spec[where x="inverse (real (n + 1))"]] by auto
- moreover have "inverse (real (n + 1)) < d" using N n by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero)
- ultimately have "dist (x (inverse (real (n + 1)))) a < d" by auto
- }
- hence "\<exists>N::nat. \<forall>n\<ge>N. dist (x (inverse (real (n + 1)))) a < d" by auto
- }
- hence "(\<forall>n::nat. x (inverse (real (n + 1))) \<in> s) \<and> (\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist (x (inverse (real (n + 1)))) a < e)" using x by auto
- hence "\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist (f (x (inverse (real (n + 1))))) (f a) < e" using `?rhs`[THEN spec[where x="\<lambda>n::nat. x (inverse (real (n+1)))"], unfolded Lim_sequentially] by auto
- hence "False" apply(erule_tac x=e in allE) using `e>0` using x by auto
- }
- thus ?lhs unfolding continuous_within unfolding Lim_within unfolding Lim_sequentially by blast
+ assume ?rhs thus ?lhs
+ unfolding continuous_within tendsto_def [where l="f a"]
+ by (simp add: sequentially_imp_eventually_within)
qed
lemma continuous_at_sequentially:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
shows "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
--> ((f o x) ---> f a) sequentially)"
- using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto
+ using continuous_within_sequentially[of a UNIV f]
+ unfolding within_UNIV by auto
lemma continuous_on_sequentially:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
shows "continuous_on s f \<longleftrightarrow>
(\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially
--> ((f o x) ---> f(a)) sequentially)" (is "?lhs = ?rhs")
@@ -3527,16 +3458,10 @@
text{* Same thing for setwise continuity. *}
-lemma continuous_on_const:
- "continuous_on s (\<lambda>x. c)"
+lemma continuous_on_const: "continuous_on s (\<lambda>x. c)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
-lemma continuous_on_cmul:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
- unfolding continuous_on_def by (auto intro: tendsto_intros)
-
-lemma continuous_on_neg:
+lemma continuous_on_minus:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
@@ -3547,12 +3472,46 @@
\<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
-lemma continuous_on_sub:
+lemma continuous_on_diff:
fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s g
\<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
+lemma (in bounded_linear) continuous_on:
+ "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
+ unfolding continuous_on_def by (fast intro: tendsto)
+
+lemma (in bounded_bilinear) continuous_on:
+ "\<lbrakk>continuous_on s f; continuous_on s g\<rbrakk> \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)"
+ unfolding continuous_on_def by (fast intro: tendsto)
+
+lemma continuous_on_scaleR:
+ fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ assumes "continuous_on s f" and "continuous_on s g"
+ shows "continuous_on s (\<lambda>x. f x *\<^sub>R g x)"
+ using bounded_bilinear_scaleR assms
+ by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_mult:
+ fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
+ assumes "continuous_on s f" and "continuous_on s g"
+ shows "continuous_on s (\<lambda>x. f x * g x)"
+ using bounded_bilinear_mult assms
+ by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_inner:
+ fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
+ assumes "continuous_on s f" and "continuous_on s g"
+ shows "continuous_on s (\<lambda>x. inner (f x) (g x))"
+ using bounded_bilinear_inner assms
+ by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_euclidean_component:
+ "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $$ i)"
+ using bounded_linear_euclidean_component
+ by (rule bounded_linear.continuous_on)
+
text{* Same thing for uniform continuity, using sequential formulations. *}
lemma uniformly_continuous_on_const:
@@ -3796,13 +3755,20 @@
lemma interior_image_subset:
assumes "\<forall>x. continuous (at x) f" "inj f"
shows "interior (f ` s) \<subseteq> f ` (interior s)"
- apply rule unfolding interior_def mem_Collect_eq image_iff apply safe
-proof- fix x T assume as:"open T" "x \<in> T" "T \<subseteq> f ` s"
- hence "x \<in> f ` s" by auto then guess y unfolding image_iff .. note y=this
- thus "\<exists>xa\<in>{x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> s}. x = f xa" apply(rule_tac x=y in bexI) using assms as
- apply safe apply(rule_tac x="{x. f x \<in> T}" in exI) apply(safe,rule continuous_open_preimage_univ)
- proof- fix x assume "f x \<in> T" hence "f x \<in> f ` s" using as by auto
- thus "x \<in> s" unfolding inj_image_mem_iff[OF assms(2)] . qed auto qed
+proof
+ fix x assume "x \<in> interior (f ` s)"
+ then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` s" ..
+ hence "x \<in> f ` s" by auto
+ then obtain y where y: "y \<in> s" "x = f y" by auto
+ have "open (vimage f T)"
+ using assms(1) `open T` by (rule continuous_open_vimage)
+ moreover have "y \<in> vimage f T"
+ using `x = f y` `x \<in> T` by simp
+ moreover have "vimage f T \<subseteq> s"
+ using `T \<subseteq> image f s` `inj f` unfolding inj_on_def subset_eq by auto
+ ultimately have "y \<in> interior s" ..
+ with `x = f y` show "x \<in> f ` interior s" ..
+qed
text {* Equality of continuous functions on closure and related results. *}
@@ -3989,28 +3955,10 @@
lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul
continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
-lemma continuous_on_vmul:
- fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
- shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R v)"
- unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto
-
-lemma continuous_on_mul:
- fixes c :: "'a::metric_space \<Rightarrow> real"
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s c \<Longrightarrow> continuous_on s f
- ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
- unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
-
-lemma continuous_on_mul_real:
- fixes f :: "'a::metric_space \<Rightarrow> real"
- fixes g :: "'a::metric_space \<Rightarrow> real"
- shows "continuous_on s f \<Longrightarrow> continuous_on s g
- ==> continuous_on s (\<lambda>x. f x * g x)"
- using continuous_on_mul[of s f g] unfolding real_scaleR_def .
-
lemmas continuous_on_intros = continuous_on_add continuous_on_const
- continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg
- continuous_on_sub continuous_on_mul continuous_on_vmul continuous_on_mul_real
+ continuous_on_id continuous_on_compose continuous_on_minus
+ continuous_on_diff continuous_on_scaleR continuous_on_mult
+ continuous_on_inner continuous_on_euclidean_component
uniformly_continuous_on_add uniformly_continuous_on_const
uniformly_continuous_on_id uniformly_continuous_on_compose
uniformly_continuous_on_cmul uniformly_continuous_on_neg
@@ -4870,13 +4818,15 @@
finally show "closed {a .. b}" .
qed
-lemma interior_closed_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows
- "interior {a .. b} = {a<..<b}" (is "?L = ?R")
+lemma interior_closed_interval [intro]:
+ fixes a b :: "'a::ordered_euclidean_space"
+ shows "interior {a..b} = {a<..<b}" (is "?L = ?R")
proof(rule subset_antisym)
- show "?R \<subseteq> ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto
+ show "?R \<subseteq> ?L" using interval_open_subset_closed open_interval
+ by (rule interior_maximal)
next
- { fix x assume "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {a..b}"
- then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" by auto
+ { fix x assume "x \<in> interior {a..b}"
+ then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" ..
then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}" unfolding open_dist and subset_eq by auto
{ fix i assume i:"i<DIM('a)"
have "dist (x - (e / 2) *\<^sub>R basis i) x < e"
@@ -4891,7 +4841,7 @@
hence "a $$ i < x $$ i" and "x $$ i < b $$ i" unfolding euclidean_simps
unfolding basis_component using `e>0` i by auto }
hence "x \<in> {a<..<b}" unfolding mem_interval by auto }
- thus "?L \<subseteq> ?R" unfolding interior_def and subset_eq by auto
+ thus "?L \<subseteq> ?R" ..
qed
lemma bounded_closed_interval: fixes a :: "'a::ordered_euclidean_space" shows "bounded {a .. b}"
@@ -5149,21 +5099,12 @@
finally show ?thesis .
qed
-lemma Lim_inner:
- assumes "(f ---> l) net" shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
- by (intro tendsto_intros assms)
-
lemma continuous_at_inner: "continuous (at x) (inner a)"
unfolding continuous_at by (intro tendsto_intros)
lemma continuous_at_euclidean_component[intro!, simp]: "continuous (at x) (\<lambda>x. x $$ i)"
unfolding euclidean_component_def by (rule continuous_at_inner)
-lemma continuous_on_inner:
- fixes s :: "'a::real_inner set"
- shows "continuous_on s (inner a)"
- unfolding continuous_on by (rule ballI) (intro tendsto_intros)
-
lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
by (simp add: closed_Collect_le)
@@ -5440,8 +5381,7 @@
unfolding homeomorphic_minimal
apply(rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
apply(rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI)
- using assms apply auto
- using continuous_on_cmul[OF continuous_on_id] by auto
+ using assms by (auto simp add: continuous_on_intros)
lemma homeomorphic_translation:
fixes s :: "'a::real_normed_vector set"
@@ -5763,15 +5703,13 @@
{ fix y assume "m > 0" "m *\<^sub>R a + c \<le> y" "y \<le> m *\<^sub>R b + c"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
- apply(auto simp add: pth_3[symmetric]
- intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
+ apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
} moreover
{ fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
- apply(auto simp add: pth_3[symmetric]
- intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
+ apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
}
ultimately show ?thesis using False by auto
@@ -6040,19 +5978,4 @@
declare tendsto_const [intro] (* FIXME: move *)
-text {* Legacy theorem names *}
-
-lemmas Lim_ident_at = LIM_ident
-lemmas Lim_const = tendsto_const
-lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
-lemmas Lim_neg = tendsto_minus
-lemmas Lim_add = tendsto_add
-lemmas Lim_sub = tendsto_diff
-lemmas Lim_mul = tendsto_scaleR
-lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
-lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
-lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
-lemmas Lim_component = tendsto_euclidean_component
-lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
-
end