--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Feb 22 18:01:08 2018 +0100
@@ -277,14 +277,22 @@
by (simp add: vec_eq_iff)
lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
+
+lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
+ by (simp add: inner_axis' norm_eq_1)
+
lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
by vector
+
lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)
+
lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)
+
lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==> a *s x = a *s y ==> (x = y)"
by (metis vector_mul_lcancel)
+
lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
by (metis vector_mul_rcancel)
@@ -563,7 +571,7 @@
lemma transpose_mat [simp]: "transpose (mat n) = mat n"
by (vector transpose_def mat_def)
-lemma transpose_transpose: "transpose(transpose A) = A"
+lemma transpose_transpose [simp]: "transpose(transpose A) = A"
by (vector transpose_def)
lemma row_transpose [simp]:
@@ -576,10 +584,10 @@
shows "column i (transpose A) = row i A"
by (simp add: row_def column_def transpose_def vec_eq_iff)
-lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
+lemma rows_transpose [simp]: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
by (auto simp add: rows_def columns_def row_transpose intro: set_eqI)
-lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A"
+lemma columns_transpose [simp]: "columns(transpose (A::'a::semiring_1^_^_)) = rows A"
by (metis transpose_transpose rows_transpose)
lemma matrix_mult_transpose_dot_column:
@@ -642,6 +650,12 @@
by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
field_simps sum_distrib_left sum.distrib)
+lemma
+ fixes A :: "real^'n^'m"
+ shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z"
+ and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)"
+ by (simp_all add: linear_linear linear_continuous_at linear_continuous_on matrix_vector_mul_linear)
+
lemma matrix_vector_mult_add_distrib [algebra_simps]:
fixes A :: "real^'n^'m"
shows "A *v (x + y) = A *v x + A *v y"
@@ -682,6 +696,8 @@
lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))"
by (simp add: ext matrix_works)
+declare matrix_vector_mul [symmetric, simp]
+
lemma matrix_of_matrix_vector_mul [simp]: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A"
by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)
--- a/src/HOL/Analysis/Connected.thy Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy Thu Feb 22 18:01:08 2018 +0100
@@ -4783,6 +4783,21 @@
by (simp add: \<open>countable \<F>'\<close> countable_subset)
qed
+lemma countable_disjoint_nonempty_interior_subsets:
+ fixes \<F> :: "'a::euclidean_space set set"
+ assumes pw: "pairwise disjnt \<F>" and int: "\<And>S. \<lbrakk>S \<in> \<F>; interior S = {}\<rbrakk> \<Longrightarrow> S = {}"
+ shows "countable \<F>"
+proof (rule countable_image_inj_on)
+ have "disjoint (interior ` \<F>)"
+ using pw by (simp add: disjoint_image_subset interior_subset)
+ then show "countable (interior ` \<F>)"
+ by (auto intro: countable_disjoint_open_subsets)
+ show "inj_on interior \<F>"
+ using pw apply (clarsimp simp: inj_on_def pairwise_def)
+ apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset)
+ done
+qed
+
lemma closedin_compact:
"\<lbrakk>compact S; closedin (subtopology euclidean S) T\<rbrakk> \<Longrightarrow> compact T"
by (metis closedin_closed compact_Int_closed)
--- a/src/HOL/Analysis/Determinants.thy Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Determinants.thy Thu Feb 22 18:01:08 2018 +0100
@@ -929,7 +929,7 @@
by auto
qed
-text \<open>Orthogonality of a transformation and matrix.\<close>
+subsection \<open>Orthogonality of a transformation and matrix.\<close>
definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
@@ -945,6 +945,51 @@
definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
+lemma orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
+ by (simp add: linear_iff orthogonal_transformation_def)
+
+lemma orthogonal_orthogonal_transformation:
+ "orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y"
+ by (simp add: orthogonal_def orthogonal_transformation_def)
+
+lemma orthogonal_transformation_compose:
+ "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
+ by (simp add: orthogonal_transformation_def linear_compose)
+
+lemma orthogonal_transformation_neg:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
+ by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
+
+lemma orthogonal_transformation_linear:
+ "orthogonal_transformation f \<Longrightarrow> linear f"
+ by (simp add: orthogonal_transformation_def)
+
+lemma orthogonal_transformation_inj:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation f \<Longrightarrow> inj f"
+ unfolding orthogonal_transformation_def inj_on_def by (metis euclidean_eqI)
+
+lemma orthogonal_transformation_surj:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation f \<Longrightarrow> surj f"
+ by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear)
+
+lemma orthogonal_transformation_bij:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation f \<Longrightarrow> bij f"
+ by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj)
+
+lemma orthogonal_transformation_inv:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
+ by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
+
+lemma orthogonal_transformation_norm:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
+ by (metis orthogonal_transformation)
+
lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
by (metis matrix_left_right_inverse orthogonal_matrix_def)
@@ -1038,7 +1083,13 @@
then show ?thesis unfolding th .
qed
-text \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
+lemma orthogonal_transformation_det [simp]:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1"
+ using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
+
+
+subsection \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
lemma scaling_linear:
fixes f :: "real ^'n \<Rightarrow> real ^'n"
@@ -1071,20 +1122,138 @@
lemma orthogonal_transformation_isometry:
"orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
unfolding orthogonal_transformation
- apply (rule iffI)
- apply clarify
- apply (clarsimp simp add: linear_0 linear_diff[symmetric] dist_norm)
- apply (rule conjI)
- apply (rule isometry_linear)
- apply simp
- apply simp
- apply clarify
- apply (erule_tac x=v in allE)
- apply (erule_tac x=0 in allE)
- apply (simp add: dist_norm)
- done
+ apply (auto simp: linear_0 isometry_linear)
+ apply (metis (no_types, hide_lams) dist_norm linear_diff)
+ by (metis dist_0_norm)
+
+
+lemma image_orthogonal_transformation_ball:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ assumes "orthogonal_transformation f"
+ shows "f ` ball x r = ball (f x) r"
+proof (intro equalityI subsetI)
+ fix y assume "y \<in> f ` ball x r"
+ with assms show "y \<in> ball (f x) r"
+ by (auto simp: orthogonal_transformation_isometry)
+next
+ fix y assume y: "y \<in> ball (f x) r"
+ then obtain z where z: "y = f z"
+ using assms orthogonal_transformation_surj by blast
+ with y assms show "y \<in> f ` ball x r"
+ by (auto simp: orthogonal_transformation_isometry)
+qed
+
+lemma image_orthogonal_transformation_cball:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ assumes "orthogonal_transformation f"
+ shows "f ` cball x r = cball (f x) r"
+proof (intro equalityI subsetI)
+ fix y assume "y \<in> f ` cball x r"
+ with assms show "y \<in> cball (f x) r"
+ by (auto simp: orthogonal_transformation_isometry)
+next
+ fix y assume y: "y \<in> cball (f x) r"
+ then obtain z where z: "y = f z"
+ using assms orthogonal_transformation_surj by blast
+ with y assms show "y \<in> f ` cball x r"
+ by (auto simp: orthogonal_transformation_isometry)
+qed
+
+subsection\<open> We can find an orthogonal matrix taking any unit vector to any other.\<close>
+
+lemma orthogonal_matrix_transpose [simp]:
+ "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
+ by (auto simp: orthogonal_matrix_def)
+
+lemma orthogonal_matrix_orthonormal_columns:
+ fixes A :: "real^'n^'n"
+ shows "orthogonal_matrix A \<longleftrightarrow>
+ (\<forall>i. norm(column i A) = 1) \<and>
+ (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (column i A) (column j A))"
+ by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def)
+
+lemma orthogonal_matrix_orthonormal_rows:
+ fixes A :: "real^'n^'n"
+ shows "orthogonal_matrix A \<longleftrightarrow>
+ (\<forall>i. norm(row i A) = 1) \<and>
+ (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))"
+ using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
-text \<open>Can extend an isometry from unit sphere.\<close>
+lemma orthogonal_matrix_exists_basis:
+ fixes a :: "real^'n"
+ assumes "norm a = 1"
+ obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
+proof -
+ obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
+ and "independent S" "card S = CARD('n)" "span S = UNIV"
+ using vector_in_orthonormal_basis assms by force
+ with independent_imp_finite obtain f0 where "bij_betw f0 (UNIV::'n set) S"
+ by (metis finite_class.finite_UNIV finite_same_card_bij)
+ then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
+ using bij_swap_iff [of k "inv f0 a" f0]
+ by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply1)
+ show thesis
+ proof
+ have [simp]: "\<And>i. norm (f i) = 1"
+ using bij_betwE [OF \<open>bij_betw f UNIV S\<close>] by (blast intro: noS)
+ have [simp]: "\<And>i j. i \<noteq> j \<Longrightarrow> orthogonal (f i) (f j)"
+ using \<open>pairwise orthogonal S\<close> \<open>bij_betw f UNIV S\<close>
+ by (auto simp: pairwise_def bij_betw_def inj_on_def)
+ show "orthogonal_matrix (\<chi> i j. f j $ i)"
+ by (simp add: orthogonal_matrix_orthonormal_columns column_def)
+ show "(\<chi> i j. f j $ i) *v axis k 1 = a"
+ by (simp add: matrix_vector_mult_def axis_def a if_distrib cong: if_cong)
+ qed
+qed
+
+lemma orthogonal_transformation_exists_1:
+ fixes a b :: "real^'n"
+ assumes "norm a = 1" "norm b = 1"
+ obtains f where "orthogonal_transformation f" "f a = b"
+proof -
+ obtain k::'n where True
+ by simp
+ obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
+ using orthogonal_matrix_exists_basis assms by metis
+ let ?f = "\<lambda>x. (B ** transpose A) *v x"
+ show thesis
+ proof
+ show "orthogonal_transformation ?f"
+ by (simp add: AB orthogonal_matrix_mul matrix_vector_mul_linear orthogonal_transformation_matrix)
+ next
+ show "?f a = b"
+ using \<open>orthogonal_matrix A\<close> unfolding orthogonal_matrix_def
+ by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
+ qed
+qed
+
+lemma orthogonal_transformation_exists:
+ fixes a b :: "real^'n"
+ assumes "norm a = norm b"
+ obtains f where "orthogonal_transformation f" "f a = b"
+proof (cases "a = 0 \<or> b = 0")
+ case True
+ with assms show ?thesis
+ using orthogonal_transformation_isometry that by fastforce
+next
+ case False
+ then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)"
+ by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"])
+ show ?thesis
+ proof
+ have "linear f"
+ using f by (simp add: orthogonal_transformation_linear)
+ then have "f a /\<^sub>R norm a = f (a /\<^sub>R norm a)"
+ by (simp add: linear_cmul [of f])
+ also have "\<dots> = b /\<^sub>R norm a"
+ by (simp add: eq assms [symmetric])
+ finally show "f a = b"
+ using False by auto
+ qed (use f in auto)
+qed
+
+
+subsection \<open>Can extend an isometry from unit sphere.\<close>
lemma isometry_sphere_extend:
fixes f:: "real ^'n \<Rightarrow> real ^'n"
@@ -1182,7 +1351,7 @@
done
qed
-text \<open>Rotation, reflection, rotoinversion.\<close>
+subsection \<open>Rotation, reflection, rotoinversion.\<close>
definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
@@ -1238,4 +1407,111 @@
by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
qed
+text\<open> Slightly stronger results giving rotation, but only in two or more dimensions.\<close>
+
+lemma rotation_matrix_exists_basis:
+ fixes a :: "real^'n"
+ assumes 2: "2 \<le> CARD('n)" and "norm a = 1"
+ obtains A where "rotation_matrix A" "A *v (axis k 1) = a"
+proof -
+ obtain A where "orthogonal_matrix A" and A: "A *v (axis k 1) = a"
+ using orthogonal_matrix_exists_basis assms by metis
+ with orthogonal_rotation_or_rotoinversion
+ consider "rotation_matrix A" | "rotoinversion_matrix A"
+ by metis
+ then show thesis
+ proof cases
+ assume "rotation_matrix A"
+ then show ?thesis
+ using \<open>A *v axis k 1 = a\<close> that by auto
+ next
+ obtain j where "j \<noteq> k"
+ by (metis (full_types) 2 card_2_exists ex_card)
+ let ?TA = "transpose A"
+ let ?A = "\<chi> i. if i = j then - 1 *\<^sub>R (?TA $ i) else ?TA $i"
+ assume "rotoinversion_matrix A"
+ then have [simp]: "det A = -1"
+ by (simp add: rotoinversion_matrix_def)
+ show ?thesis
+ proof
+ have [simp]: "row i (\<chi> i. if i = j then - 1 *\<^sub>R ?TA $ i else ?TA $ i) = (if i = j then - row i ?TA else row i ?TA)" for i
+ by (auto simp: row_def)
+ have "orthogonal_matrix ?A"
+ unfolding orthogonal_matrix_orthonormal_rows
+ using \<open>orthogonal_matrix A\<close> by (auto simp: orthogonal_matrix_orthonormal_columns orthogonal_clauses)
+ then show "rotation_matrix (transpose ?A)"
+ unfolding rotation_matrix_def
+ by (simp add: det_row_mul[of j _ "\<lambda>i. ?TA $ i", unfolded scalar_mult_eq_scaleR])
+ show "transpose ?A *v axis k 1 = a"
+ using \<open>j \<noteq> k\<close> A by (simp add: matrix_vector_column axis_def scalar_mult_eq_scaleR if_distrib [of "\<lambda>z. z *\<^sub>R c" for c] cong: if_cong)
+ qed
+ qed
+qed
+
+lemma rotation_exists_1:
+ fixes a :: "real^'n"
+ assumes "2 \<le> CARD('n)" "norm a = 1" "norm b = 1"
+ obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
+proof -
+ obtain k::'n where True
+ by simp
+ obtain A B where AB: "rotation_matrix A" "rotation_matrix B"
+ and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
+ using rotation_matrix_exists_basis assms by metis
+ let ?f = "\<lambda>x. (B ** transpose A) *v x"
+ show thesis
+ proof
+ show "orthogonal_transformation ?f"
+ using AB orthogonal_matrix_mul orthogonal_transformation_matrix rotation_matrix_def matrix_vector_mul_linear by force
+ show "det (matrix ?f) = 1"
+ using AB by (auto simp: det_mul rotation_matrix_def)
+ show "?f a = b"
+ using AB unfolding orthogonal_matrix_def rotation_matrix_def
+ by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
+ qed
+qed
+
+lemma rotation_exists:
+ fixes a :: "real^'n"
+ assumes 2: "2 \<le> CARD('n)" and eq: "norm a = norm b"
+ obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
+proof (cases "a = 0 \<or> b = 0")
+ case True
+ with assms have "a = 0" "b = 0"
+ by auto
+ then show ?thesis
+ by (metis eq_id_iff matrix_id orthogonal_transformation_id that)
+next
+ case False
+ with that show thesis
+ by (auto simp: eq linear_cmul orthogonal_transformation_def
+ intro: rotation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b", OF 2])
+qed
+
+lemma rotation_rightward_line:
+ fixes a :: "real^'n"
+ obtains f where "orthogonal_transformation f" "2 \<le> CARD('n) \<Longrightarrow> det(matrix f) = 1"
+ "f(norm a *\<^sub>R axis k 1) = a"
+proof (cases "CARD('n) = 1")
+ case True
+ obtain f where "orthogonal_transformation f" "f (norm a *\<^sub>R axis k (1::real)) = a"
+ proof (rule orthogonal_transformation_exists)
+ show "norm (norm a *\<^sub>R axis k (1::real)) = norm a"
+ by simp
+ qed auto
+ then show thesis
+ using True that by auto
+next
+ case False
+ obtain f where "orthogonal_transformation f" "det(matrix f) = 1" "f (norm a *\<^sub>R axis k 1) = a"
+ proof (rule rotation_exists)
+ show "2 \<le> CARD('n)"
+ using False one_le_card_finite [where 'a='n] by linarith
+ show "norm (norm a *\<^sub>R axis k (1::real)) = norm a"
+ by simp
+ qed auto
+ then show thesis
+ using that by blast
+qed
+
end
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Feb 22 18:01:08 2018 +0100
@@ -144,6 +144,28 @@
qed
qed (simp_all add: infinite_UNIV_vec)
+lemma countable_vector:
+ fixes B:: "'n::finite \<Rightarrow> 'a set"
+ assumes "\<And>i. countable (B i)"
+ shows "countable {V. \<forall>i::'n::finite. V $ i \<in> B i}"
+proof -
+ have "f \<in> ($) ` {V. \<forall>i. V $ i \<in> B i}" if "f \<in> Pi\<^sub>E UNIV B" for f
+ proof -
+ have "\<exists>W. (\<forall>i. W $ i \<in> B i) \<and> ($) W = f"
+ by (metis that PiE_iff UNIV_I vec_lambda_inverse)
+ then show "f \<in> ($) ` {v. \<forall>i. v $ i \<in> B i}"
+ by blast
+ qed
+ then have "Pi\<^sub>E UNIV B = vec_nth ` {V. \<forall>i::'n. V $ i \<in> B i}"
+ by blast
+ then have "countable (vec_nth ` {V. \<forall>i. V $ i \<in> B i})"
+ by (metis finite_class.finite_UNIV countable_PiE assms)
+ then have "countable (vec_lambda ` vec_nth ` {V. \<forall>i. V $ i \<in> B i})"
+ by auto
+ then show ?thesis
+ by (simp add: image_comp o_def vec_nth_inverse)
+qed
+
subsection \<open>Group operations and class instances\<close>
instantiation vec :: (zero, finite) zero
@@ -601,6 +623,9 @@
apply (simp add: axis_def)
done
+lemma inner_axis': "inner(axis i y) x = inner y (x $ i)"
+ by (simp add: inner_axis inner_commute)
+
instantiation vec :: (euclidean_space, finite) euclidean_space
begin
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Feb 22 18:01:08 2018 +0100
@@ -5221,7 +5221,7 @@
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
assumes \<T>: "finite \<T>"
and int: "\<And>S. S \<in> \<T> \<Longrightarrow> (f has_integral (i S)) S"
- and neg: "\<And>S S'. \<lbrakk>S \<in> \<T>; S' \<in> \<T>; S \<noteq> S'\<rbrakk> \<Longrightarrow> negligible (S \<inter> S')"
+ and neg: "pairwise (\<lambda>S S'. negligible (S \<inter> S')) \<T>"
shows "(f has_integral (sum i \<T>)) (\<Union>\<T>)"
proof -
let ?\<U> = "((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> \<T> \<and> b \<in> {y. y \<in> \<T> \<and> a \<noteq> y}})"
@@ -5236,7 +5236,7 @@
ultimately show "finite ?\<U>"
by (blast intro: finite_subset[of _ "\<T> \<times> \<T>"])
show "\<And>t. t \<in> ?\<U> \<Longrightarrow> negligible t"
- using neg by auto
+ using neg unfolding pairwise_def by auto
qed
next
show "(if x \<in> \<Union>\<T> then f x else 0) = (\<Sum>A\<in>\<T>. if x \<in> A then f x else 0)"
@@ -5247,7 +5247,7 @@
using that by blast
ultimately show "f x = (\<Sum>A\<in>\<T>. if x \<in> A then f x else 0)"
by (simp add: sum.delta[OF \<T>])
- qed
+ qed
next
show "((\<lambda>x. \<Sum>A\<in>\<T>. if x \<in> A then f x else 0) has_integral (\<Sum>A\<in>\<T>. i A)) UNIV"
apply (rule has_integral_sum [OF \<T>])
@@ -5277,7 +5277,7 @@
qed
show ?thesis
unfolding \<D>(6)[symmetric]
- by (auto intro: \<D> neg assms has_integral_Union)
+ by (auto intro: \<D> neg assms has_integral_Union pairwiseI)
qed
lemma integral_combine_division_bottomup:
--- a/src/HOL/Analysis/Starlike.thy Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy Thu Feb 22 18:01:08 2018 +0100
@@ -7281,6 +7281,66 @@
with assms show ?thesis by auto
qed
+lemma vector_in_orthogonal_spanningset:
+ fixes a :: "'a::euclidean_space"
+ obtains S where "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
+ by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def pairwise_orthogonal_insert span_UNIV subsetI subset_antisym)
+
+lemma vector_in_orthogonal_basis:
+ fixes a :: "'a::euclidean_space"
+ assumes "a \<noteq> 0"
+ obtains S where "a \<in> S" "0 \<notin> S" "pairwise orthogonal S" "independent S" "finite S"
+ "span S = UNIV" "card S = DIM('a)"
+proof -
+ obtain S where S: "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
+ using vector_in_orthogonal_spanningset .
+ show thesis
+ proof
+ show "pairwise orthogonal (S - {0})"
+ using pairwise_mono S(2) by blast
+ show "independent (S - {0})"
+ by (simp add: \<open>pairwise orthogonal (S - {0})\<close> pairwise_orthogonal_independent)
+ show "finite (S - {0})"
+ using \<open>independent (S - {0})\<close> independent_finite by blast
+ show "card (S - {0}) = DIM('a)"
+ using span_delete_0 [of S] S
+ by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span)
+ qed (use S \<open>a \<noteq> 0\<close> in auto)
+qed
+
+lemma vector_in_orthonormal_basis:
+ fixes a :: "'a::euclidean_space"
+ assumes "norm a = 1"
+ obtains S where "a \<in> S" "pairwise orthogonal S" "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
+ "independent S" "card S = DIM('a)" "span S = UNIV"
+proof -
+ have "a \<noteq> 0"
+ using assms by auto
+ then obtain S where "a \<in> S" "0 \<notin> S" "finite S"
+ and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)"
+ by (metis vector_in_orthogonal_basis)
+ let ?S = "(\<lambda>x. x /\<^sub>R norm x) ` S"
+ show thesis
+ proof
+ show "a \<in> ?S"
+ using \<open>a \<in> S\<close> assms image_iff by fastforce
+ next
+ show "pairwise orthogonal ?S"
+ using \<open>pairwise orthogonal S\<close> by (auto simp: pairwise_def orthogonal_def)
+ show "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` S \<Longrightarrow> norm x = 1"
+ using \<open>0 \<notin> S\<close> by (auto simp: divide_simps)
+ then show "independent ?S"
+ by (metis \<open>pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` S)\<close> norm_zero pairwise_orthogonal_independent zero_neq_one)
+ have "inj_on (\<lambda>x. x /\<^sub>R norm x) S"
+ unfolding inj_on_def
+ by (metis (full_types) S(1) \<open>0 \<notin> S\<close> inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def)
+ then show "card ?S = DIM('a)"
+ by (simp add: card_image S)
+ show "span ?S = UNIV"
+ by (metis (no_types) \<open>0 \<notin> S\<close> \<open>finite S\<close> \<open>span S = UNIV\<close> field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale zero_less_norm_iff)
+ qed
+qed
+
proposition dim_orthogonal_sum:
fixes A :: "'a::euclidean_space set"
assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Feb 22 18:01:08 2018 +0100
@@ -3652,12 +3652,26 @@
using assms by (fastforce simp: bounded_iff)
qed
+lemma bounded_plus:
+ fixes S ::"'a::real_normed_vector set"
+ assumes "bounded S" "bounded T"
+ shows "bounded ((\<lambda>(x,y). x + y) ` (S \<times> T))"
+ using bounded_plus_comp [of fst "S \<times> T" snd] assms
+ by (auto simp: split_def split: if_split_asm)
+
lemma bounded_minus_comp:
"bounded (f ` S) \<Longrightarrow> bounded (g ` S) \<Longrightarrow> bounded ((\<lambda>x. f x - g x) ` S)"
for f g::"'a \<Rightarrow> 'b::real_normed_vector"
using bounded_plus_comp[of "f" S "\<lambda>x. - g x"]
by auto
+lemma bounded_minus:
+ fixes S ::"'a::real_normed_vector set"
+ assumes "bounded S" "bounded T"
+ shows "bounded ((\<lambda>(x,y). x - y) ` (S \<times> T))"
+ using bounded_minus_comp [of fst "S \<times> T" snd] assms
+ by (auto simp: split_def split: if_split_asm)
+
subsection \<open>Compactness\<close>
@@ -4014,7 +4028,6 @@
\<Longrightarrow> openin (subtopology euclidean u) (s - {a})"
by (metis Int_Diff open_delete openin_open)
-
text\<open>Compactness expressed with filters\<close>
lemma closure_iff_nhds_not_empty:
@@ -4643,6 +4656,27 @@
shows "~ compact (UNIV::'a set)"
by (simp add: compact_eq_bounded_closed)
+text\<open>Representing sets as the union of a chain of compact sets.\<close>
+lemma closed_Union_compact_subsets:
+ fixes S :: "'a::{heine_borel,real_normed_vector} set"
+ assumes "closed S"
+ obtains F where "\<And>n. compact(F n)" "\<And>n. F n \<subseteq> S" "\<And>n. F n \<subseteq> F(Suc n)"
+ "(\<Union>n. F n) = S" "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n \<ge> N. K \<subseteq> F n"
+proof
+ show "compact (S \<inter> cball 0 (of_nat n))" for n
+ using assms compact_eq_bounded_closed by auto
+next
+ show "(\<Union>n. S \<inter> cball 0 (real n)) = S"
+ by (auto simp: real_arch_simple)
+next
+ fix K :: "'a set"
+ assume "compact K" "K \<subseteq> S"
+ then obtain N where "K \<subseteq> cball 0 N"
+ by (meson bounded_pos mem_cball_0 compact_imp_bounded subsetI)
+ then show "\<exists>N. \<forall>n\<ge>N. K \<subseteq> S \<inter> cball 0 (real n)"
+ by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans)
+qed auto
+
instance real :: heine_borel
proof
fix f :: "nat \<Rightarrow> real"
@@ -5062,10 +5096,7 @@
lemma continuous_within_eps_delta:
"continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s. dist x' x < d --> dist (f x') (f x) < e)"
- unfolding continuous_within and Lim_within
- apply auto
- apply (metis dist_nz dist_self, blast)
- done
+ unfolding continuous_within and Lim_within by fastforce
corollary continuous_at_eps_delta:
"continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
--- a/src/HOL/Groups_Big.thy Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Groups_Big.thy Thu Feb 22 18:01:08 2018 +0100
@@ -332,34 +332,6 @@
by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
qed
-lemma delta [simp]:
- assumes fS: "finite S"
- shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
-proof -
- let ?f = "(\<lambda>k. if k = a then b k else \<^bold>1)"
- show ?thesis
- proof (cases "a \<in> S")
- case False
- then have "\<forall>k\<in>S. ?f k = \<^bold>1" by simp
- with False show ?thesis by simp
- next
- case True
- let ?A = "S - {a}"
- let ?B = "{a}"
- from True have eq: "S = ?A \<union> ?B" by blast
- have dj: "?A \<inter> ?B = {}" by simp
- from fS have fAB: "finite ?A" "finite ?B" by auto
- have "F ?f S = F ?f ?A \<^bold>* F ?f ?B"
- using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp
- with True show ?thesis by simp
- qed
-qed
-
-lemma delta' [simp]:
- assumes fin: "finite S"
- shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
- using delta [OF fin, of a b, symmetric] by (auto intro: cong)
-
lemma delta_remove:
assumes fS: "finite S"
shows "F (\<lambda>k. if k = a then b k else c k) S = (if a \<in> S then b a \<^bold>* F c (S-{a}) else F c (S-{a}))"
@@ -384,6 +356,16 @@
qed
qed
+lemma delta [simp]:
+ assumes fS: "finite S"
+ shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
+ by (simp add: delta_remove [OF assms])
+
+lemma delta' [simp]:
+ assumes fin: "finite S"
+ shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
+ using delta [OF fin, of a b, symmetric] by (auto intro: cong)
+
lemma If_cases:
fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
assumes fin: "finite A"
--- a/src/HOL/Library/Indicator_Function.thy Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Thu Feb 22 18:01:08 2018 +0100
@@ -10,6 +10,9 @@
definition "indicator S x = (if x \<in> S then 1 else 0)"
+text\<open>Type constrained version\<close>
+abbreviation indicat_real :: "'a set \<Rightarrow> 'a \<Rightarrow> real" where "indicat_real S \<equiv> indicator S"
+
lemma indicator_simps[simp]:
"x \<in> S \<Longrightarrow> indicator S x = 1"
"x \<notin> S \<Longrightarrow> indicator S x = 0"