--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Jan 16 17:56:29 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Jan 16 18:54:18 2019 +0100
@@ -179,92 +179,18 @@
by force
qed
-lemma%unimportant matrix_mult_transpose_dot_column:
- shows "transpose A ** A = (\<chi> i j. inner (column i A) (column j A))"
- by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)
-
-lemma%unimportant matrix_mult_transpose_dot_row:
- shows "A ** transpose A = (\<chi> i j. inner (row i A) (row j A))"
- by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)
-
lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear ((*v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
using matrix_vector_mul_linear[of A]
by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq)
-lemma%unimportant (* FIX ME needs name*)
+lemma%unimportant
fixes A :: "'a::{euclidean_space,real_algebra_1}^'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_continuous_at linear_continuous_on)
-lemma%unimportant scalar_invertible:
- fixes A :: "('a::real_algebra_1)^'m^'n"
- assumes "k \<noteq> 0" and "invertible A"
- shows "invertible (k *\<^sub>R A)"
-proof -
- obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
- using assms unfolding invertible_def by auto
- with \<open>k \<noteq> 0\<close>
- have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1"
- by (simp_all add: assms matrix_scalar_ac)
- thus "invertible (k *\<^sub>R A)"
- unfolding invertible_def by auto
-qed
-lemma%unimportant scalar_invertible_iff:
- fixes A :: "('a::real_algebra_1)^'m^'n"
- assumes "k \<noteq> 0" and "invertible A"
- shows "invertible (k *\<^sub>R A) \<longleftrightarrow> k \<noteq> 0 \<and> invertible A"
- by (simp add: assms scalar_invertible)
-
-lemma%unimportant vector_transpose_matrix [simp]: "x v* transpose A = A *v x"
- unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
- by simp
-
-lemma%unimportant transpose_matrix_vector [simp]: "transpose A *v x = x v* A"
- unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
- by simp
-
-lemma%unimportant vector_scalar_commute:
- fixes A :: "'a::{field}^'m^'n"
- shows "A *v (c *s x) = c *s (A *v x)"
- by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left)
-
-lemma%unimportant scalar_vector_matrix_assoc:
- fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n"
- shows "(k *s x) v* A = k *s (x v* A)"
- by (metis transpose_matrix_vector vector_scalar_commute)
-
-lemma%unimportant vector_matrix_mult_0 [simp]: "0 v* A = 0"
- unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
-
-lemma%unimportant vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
- unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
-
-lemma%unimportant vector_matrix_mul_rid [simp]:
- fixes v :: "('a::semiring_1)^'n"
- shows "v v* mat 1 = v"
- by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix)
-
-lemma%unimportant scaleR_vector_matrix_assoc:
- fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
- shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)"
- by (metis matrix_vector_mult_scaleR transpose_matrix_vector)
-
-lemma%important vector_scaleR_matrix_ac:
- fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
- shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
-proof%unimportant -
- have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A"
- unfolding vector_matrix_mult_def
- by (simp add: algebra_simps)
- with scaleR_vector_matrix_assoc
- show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
- by auto
-qed
-
-
-subsection%important\<open>Some bounds on components etc. relative to operator norm\<close>
+subsection%important\<open>Bounds on components etc.\ relative to operator norm\<close>
lemma%important norm_column_le_onorm:
fixes A :: "real^'n^'m"
@@ -341,26 +267,6 @@
finally show "norm (A *v x) \<le> CARD('m) * real (CARD('n)) * B * norm x" .
qed
-subsection%important \<open>lambda skolemization on cartesian products\<close>
-
-lemma%important lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
- (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")
-proof%unimportant -
- let ?S = "(UNIV :: 'n set)"
- { assume H: "?rhs"
- then have ?lhs by auto }
- moreover
- { assume H: "?lhs"
- then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis
- let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
- { fix i
- from f have "P i (f i)" by metis
- then have "P i (?x $ i)" by auto
- }
- hence "\<forall>i. P i (?x$i)" by metis
- hence ?rhs by metis }
- ultimately show ?thesis by metis
-qed
lemma%unimportant rational_approximation:
assumes "e > 0"
@@ -391,36 +297,6 @@
lemma%unimportant vector_sub_project_orthogonal_cart: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
unfolding inner_simps scalar_mult_eq_scaleR by auto
-
-text \<open>The same result in terms of square matrices.\<close>
-
-
-text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close>
-
-definition%unimportant "rowvector v = (\<chi> i j. (v$j))"
-
-definition%unimportant "columnvector v = (\<chi> i j. (v$i))"
-
-lemma%unimportant transpose_columnvector: "transpose(columnvector v) = rowvector v"
- by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff)
-
-lemma%unimportant transpose_rowvector: "transpose(rowvector v) = columnvector v"
- by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff)
-
-lemma%unimportant dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v"
- by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)
-
-lemma%unimportant dot_matrix_product:
- "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1"
- by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def)
-
-lemma%unimportant dot_matrix_vector_mul:
- fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
- shows "(A *v x) \<bullet> (B *v y) =
- (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1"
- unfolding dot_matrix_product transpose_columnvector[symmetric]
- dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
-
lemma%unimportant infnorm_cart:"infnorm (x::real^'n) = Sup {\<bar>x$i\<bar> |i. i\<in>UNIV}"
by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right)
@@ -601,16 +477,16 @@
by (simp add: is_interval_def Ball_def Basis_vec_def inner_axis imp_ex)
lemma%unimportant closed_halfspace_component_le_cart: "closed {x::real^'n. x$i \<le> a}"
- by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)
+ by (simp add: closed_Collect_le continuous_on_component)
lemma%unimportant closed_halfspace_component_ge_cart: "closed {x::real^'n. x$i \<ge> a}"
- by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)
+ by (simp add: closed_Collect_le continuous_on_component)
lemma%unimportant open_halfspace_component_lt_cart: "open {x::real^'n. x$i < a}"
- by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component)
+ by (simp add: open_Collect_less continuous_on_component)
lemma%unimportant open_halfspace_component_gt_cart: "open {x::real^'n. x$i > a}"
- by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component)
+ by (simp add: open_Collect_less continuous_on_component)
lemma%unimportant Lim_component_le_cart:
fixes f :: "'a \<Rightarrow> real^'n"
@@ -651,69 +527,6 @@
unfolding Collect_all_eq by (simp add: closed_INT)
qed
-lemma%important dim_substandard_cart: "vec.dim {x::'a::field^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d"
- (is "vec.dim ?A = _")
-proof%unimportant (rule vec.dim_unique)
- let ?B = "((\<lambda>x. axis x 1) ` d)"
- have subset_basis: "?B \<subseteq> cart_basis"
- by (auto simp: cart_basis_def)
- show "?B \<subseteq> ?A"
- by (auto simp: axis_def)
- show "vec.independent ((\<lambda>x. axis x 1) ` d)"
- using subset_basis
- by (rule vec.independent_mono[OF vec.independent_Basis])
- have "x \<in> vec.span ?B" if "\<forall>i. i \<notin> d \<longrightarrow> x $ i = 0" for x::"'a^'n"
- proof -
- have "finite ?B"
- using subset_basis finite_cart_basis
- by (rule finite_subset)
- have "x = (\<Sum>i\<in>UNIV. x $ i *s axis i 1)"
- by (rule basis_expansion[symmetric])
- also have "\<dots> = (\<Sum>i\<in>d. (x $ i) *s axis i 1)"
- by (rule sum.mono_neutral_cong_right) (auto simp: that)
- also have "\<dots> \<in> vec.span ?B"
- by (simp add: vec.span_sum vec.span_clauses)
- finally show "x \<in> vec.span ?B" .
- qed
- then show "?A \<subseteq> vec.span ?B" by auto
-qed (simp add: card_image inj_on_def axis_eq_axis)
-
-lemma%unimportant affinity_inverses:
- assumes m0: "m \<noteq> (0::'a::field)"
- shows "(\<lambda>x. m *s x + c) \<circ> (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
- "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) \<circ> (\<lambda>x. m *s x + c) = id"
- using m0
- by (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff)
-
-lemma%important vector_affinity_eq:
- assumes m0: "(m::'a::field) \<noteq> 0"
- shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)"
-proof%unimportant
- assume h: "m *s x + c = y"
- hence "m *s x = y - c" by (simp add: field_simps)
- hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp
- then show "x = inverse m *s y + - (inverse m *s c)"
- using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
-next
- assume h: "x = inverse m *s y + - (inverse m *s c)"
- show "m *s x + c = y" unfolding h
- using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
-qed
-
-lemma%unimportant vector_eq_affinity:
- "(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)"
- using vector_affinity_eq[where m=m and x=x and y=y and c=c]
- by metis
-
-lemma%unimportant vector_cart:
- fixes f :: "real^'n \<Rightarrow> real"
- shows "(\<chi> i. f (axis i 1)) = (\<Sum>i\<in>Basis. f i *\<^sub>R i)"
- unfolding euclidean_eq_iff[where 'a="real^'n"]
- by simp (simp add: Basis_vec_def inner_axis)
-
-lemma%unimportant const_vector_cart:"((\<chi> i. d)::real^'n) = (\<Sum>i\<in>Basis. d *\<^sub>R i)"
- by (rule vector_cart)
-
subsection%important "Convex Euclidean Space"
lemma%unimportant Cart_1:"(1::real^'n) = \<Sum>Basis"
@@ -778,83 +591,8 @@
vector_cart[of "\<lambda>j. frechet_derivative f (at x) j $ k"]
by (simp add: Basis_vec_def axis_eq_axis inner_axis jacobian_def matrix_def)
-subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3\<close>\<close>
-
-lemma exhaust_2:
- fixes x :: 2
- shows "x = 1 \<or> x = 2"
-proof (induct x)
- case (of_int z)
- then have "0 \<le> z" and "z < 2" by simp_all
- then have "z = 0 | z = 1" by arith
- then show ?case by auto
-qed
-
-lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
- by (metis exhaust_2)
-
-lemma exhaust_3:
- fixes x :: 3
- shows "x = 1 \<or> x = 2 \<or> x = 3"
-proof (induct x)
- case (of_int z)
- then have "0 \<le> z" and "z < 3" by simp_all
- then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
- then show ?case by auto
-qed
-
-lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
- by (metis exhaust_3)
-
-lemma UNIV_1 [simp]: "UNIV = {1::1}"
- by (auto simp add: num1_eq_iff)
-
-lemma UNIV_2: "UNIV = {1::2, 2::2}"
- using exhaust_2 by auto
-
-lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
- using exhaust_3 by auto
-
-lemma sum_1: "sum f (UNIV::1 set) = f 1"
- unfolding UNIV_1 by simp
-
-lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2"
- unfolding UNIV_2 by simp
-
-lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
- unfolding UNIV_3 by (simp add: ac_simps)
-
-subsection%unimportant\<open>The collapse of the general concepts to dimension one\<close>
-
-lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
- by (simp add: vec_eq_iff)
-
-lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
- apply auto
- apply (erule_tac x= "x$1" in allE)
- apply (simp only: vector_one[symmetric])
- done
-
-lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
- by (simp add: norm_vec_def)
-
-lemma dist_vector_1:
- fixes x :: "'a::real_normed_vector^1"
- shows "dist x y = dist (x$1) (y$1)"
- by (simp add: dist_norm norm_vector_1)
-
-lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>"
- by (simp add: norm_vector_1)
-
-lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>"
- by (auto simp add: norm_real dist_norm)
-
subsection%unimportant\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close>
-lemma vector_one_nth [simp]:
- fixes x :: "'a^1" shows "vec (x $ 1) = x"
- by (metis vec_def vector_one)
-
lemma vec_cbox_1_eq [simp]:
shows "vec ` cbox u v = cbox (vec u) (vec v ::real^1)"
by (force simp: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box)
@@ -885,76 +623,6 @@
qed
qed simp
-lemma tendsto_at_within_vector_1:
- fixes S :: "'a :: metric_space set"
- assumes "(f \<longlongrightarrow> fx) (at x within S)"
- shows "((\<lambda>y::'a^1. \<chi> i. f (y $ 1)) \<longlongrightarrow> (vec fx::'a^1)) (at (vec x) within vec ` S)"
-proof (rule topological_tendstoI)
- fix T :: "('a^1) set"
- assume "open T" "vec fx \<in> T"
- have "\<forall>\<^sub>F x in at x within S. f x \<in> (\<lambda>x. x $ 1) ` T"
- using \<open>open T\<close> \<open>vec fx \<in> T\<close> assms open_image_vec_nth tendsto_def by fastforce
- then show "\<forall>\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\<chi> i. f (x $ 1)) \<in> T"
- unfolding eventually_at dist_norm [symmetric]
- by (rule ex_forward)
- (use \<open>open T\<close> in
- \<open>fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\<close>)
-qed
-
-lemma has_derivative_vector_1:
- assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
- shows "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a))
- (at ((vec a)::real^1) within vec ` S)"
- using der_g
- apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
- apply (drule tendsto_at_within_vector_1, vector)
- apply (auto simp: algebra_simps eventually_at tendsto_def)
- done
-
-
-subsection%unimportant\<open>Explicit vector construction from lists\<close>
-
-definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
-
-lemma vector_1 [simp]: "(vector[x]) $1 = x"
- unfolding vector_def by simp
-
-lemma vector_2 [simp]: "(vector[x,y]) $1 = x" "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
- unfolding vector_def by simp_all
-
-lemma vector_3 [simp]:
- "(vector [x,y,z] ::('a::zero)^3)$1 = x"
- "(vector [x,y,z] ::('a::zero)^3)$2 = y"
- "(vector [x,y,z] ::('a::zero)^3)$3 = z"
- unfolding vector_def by simp_all
-
-lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
- by (metis vector_1 vector_one)
-
-lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
- apply auto
- apply (erule_tac x="v$1" in allE)
- apply (erule_tac x="v$2" in allE)
- apply (subgoal_tac "vector [v$1, v$2] = v")
- apply simp
- apply (vector vector_def)
- apply (simp add: forall_2)
- done
-
-lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
- apply auto
- apply (erule_tac x="v$1" in allE)
- apply (erule_tac x="v$2" in allE)
- apply (erule_tac x="v$3" in allE)
- apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
- apply simp
- apply (vector vector_def)
- apply (simp add: forall_3)
- done
-
-lemma bounded_linear_component_cart[intro]: "bounded_linear (\<lambda>x::real^'n. x $ k)"
- apply (rule bounded_linear_intro[where K=1])
- using component_le_norm_cart[of _ k] unfolding real_norm_def by auto
lemma interval_split_cart:
"{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
@@ -967,6 +635,5 @@
lemmas cartesian_euclidean_space_uniform_limit_intros[uniform_limit_intros] =
bounded_linear.uniform_limit[OF blinfun.bounded_linear_right]
bounded_linear.uniform_limit[OF bounded_linear_vec_nth]
- bounded_linear.uniform_limit[OF bounded_linear_component_cart]
end
--- a/src/HOL/Analysis/Cartesian_Space.thy Wed Jan 16 17:56:29 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Space.thy Wed Jan 16 18:54:18 2019 +0100
@@ -13,6 +13,8 @@
Finite_Cartesian_Product Linear_Algebra
begin
+subsection \<open>Type @{typ \<open>'a ^ 'n\<close>} and fields as vector spaces\<close>
+
definition%unimportant "cart_basis = {axis i 1 | i. i\<in>UNIV}"
lemma%unimportant finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def
@@ -22,7 +24,7 @@
unfolding cart_basis_def Setcompr_eq_image
by (rule card_image) (auto simp: inj_on_def axis_eq_axis)
-interpretation vec: vector_space "(*s) "
+interpretation%important vec: vector_space "(*s) "
by unfold_locales (vector algebra_simps)+
lemma%unimportant independent_cart_basis:
@@ -450,8 +452,8 @@
finally show ?thesis .
qed
-interpretation vector_space_over_itself: vector_space "(*) :: 'a::field => 'a => 'a"
- by unfold_locales (simp_all add: algebra_simps)
+interpretation%important vector_space_over_itself: vector_space "(*) :: 'a::field \<Rightarrow> 'a \<Rightarrow> 'a"
+by unfold_locales (simp_all add: algebra_simps)
lemmas [simp del] = vector_space_over_itself.scale_scale
@@ -667,4 +669,265 @@
shows "rank(A ** B) \<le> rank A"
by (metis matrix_transpose_mul rank_mul_le_right rank_transpose)
+
+subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3\<close>\<close>
+
+lemma exhaust_2:
+ fixes x :: 2
+ shows "x = 1 \<or> x = 2"
+proof (induct x)
+ case (of_int z)
+ then have "0 \<le> z" and "z < 2" by simp_all
+ then have "z = 0 | z = 1" by arith
+ then show ?case by auto
+qed
+
+lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
+ by (metis exhaust_2)
+
+lemma exhaust_3:
+ fixes x :: 3
+ shows "x = 1 \<or> x = 2 \<or> x = 3"
+proof (induct x)
+ case (of_int z)
+ then have "0 \<le> z" and "z < 3" by simp_all
+ then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
+ then show ?case by auto
+qed
+
+lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
+ by (metis exhaust_3)
+
+lemma UNIV_1 [simp]: "UNIV = {1::1}"
+ by (auto simp add: num1_eq_iff)
+
+lemma UNIV_2: "UNIV = {1::2, 2::2}"
+ using exhaust_2 by auto
+
+lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
+ using exhaust_3 by auto
+
+lemma sum_1: "sum f (UNIV::1 set) = f 1"
+ unfolding UNIV_1 by simp
+
+lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2"
+ unfolding UNIV_2 by simp
+
+lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
+ unfolding UNIV_3 by (simp add: ac_simps)
+
+subsection%unimportant\<open>The collapse of the general concepts to dimension one\<close>
+
+lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
+ by (simp add: vec_eq_iff)
+
+lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
+ apply auto
+ apply (erule_tac x= "x$1" in allE)
+ apply (simp only: vector_one[symmetric])
+ done
+
+lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
+ by (simp add: norm_vec_def)
+
+lemma dist_vector_1:
+ fixes x :: "'a::real_normed_vector^1"
+ shows "dist x y = dist (x$1) (y$1)"
+ by (simp add: dist_norm norm_vector_1)
+
+lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>"
+ by (simp add: norm_vector_1)
+
+lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>"
+ by (auto simp add: norm_real dist_norm)
+
+
+subsection%unimportant\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close>
+
+lemma vector_one_nth [simp]:
+ fixes x :: "'a^1" shows "vec (x $ 1) = x"
+ by (metis vec_def vector_one)
+
+lemma tendsto_at_within_vector_1:
+ fixes S :: "'a :: metric_space set"
+ assumes "(f \<longlongrightarrow> fx) (at x within S)"
+ shows "((\<lambda>y::'a^1. \<chi> i. f (y $ 1)) \<longlongrightarrow> (vec fx::'a^1)) (at (vec x) within vec ` S)"
+proof (rule topological_tendstoI)
+ fix T :: "('a^1) set"
+ assume "open T" "vec fx \<in> T"
+ have "\<forall>\<^sub>F x in at x within S. f x \<in> (\<lambda>x. x $ 1) ` T"
+ using \<open>open T\<close> \<open>vec fx \<in> T\<close> assms open_image_vec_nth tendsto_def by fastforce
+ then show "\<forall>\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\<chi> i. f (x $ 1)) \<in> T"
+ unfolding eventually_at dist_norm [symmetric]
+ by (rule ex_forward)
+ (use \<open>open T\<close> in
+ \<open>fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\<close>)
+qed
+
+lemma has_derivative_vector_1:
+ assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
+ shows "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a))
+ (at ((vec a)::real^1) within vec ` S)"
+ using der_g
+ apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
+ apply (drule tendsto_at_within_vector_1, vector)
+ apply (auto simp: algebra_simps eventually_at tendsto_def)
+ done
+
+
+subsection%unimportant\<open>Explicit vector construction from lists\<close>
+
+definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
+
+lemma vector_1 [simp]: "(vector[x]) $1 = x"
+ unfolding vector_def by simp
+
+lemma vector_2 [simp]: "(vector[x,y]) $1 = x" "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
+ unfolding vector_def by simp_all
+
+lemma vector_3 [simp]:
+ "(vector [x,y,z] ::('a::zero)^3)$1 = x"
+ "(vector [x,y,z] ::('a::zero)^3)$2 = y"
+ "(vector [x,y,z] ::('a::zero)^3)$3 = z"
+ unfolding vector_def by simp_all
+
+lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
+ by (metis vector_1 vector_one)
+
+lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
+ apply auto
+ apply (erule_tac x="v$1" in allE)
+ apply (erule_tac x="v$2" in allE)
+ apply (subgoal_tac "vector [v$1, v$2] = v")
+ apply simp
+ apply (vector vector_def)
+ apply (simp add: forall_2)
+ done
+
+lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
+ apply auto
+ apply (erule_tac x="v$1" in allE)
+ apply (erule_tac x="v$2" in allE)
+ apply (erule_tac x="v$3" in allE)
+ apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
+ apply simp
+ apply (vector vector_def)
+ apply (simp add: forall_3)
+ done
+
+subsection%unimportant \<open>lambda skolemization on cartesian products\<close>
+
+lemma%important lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
+ (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")
+proof%unimportant -
+ let ?S = "(UNIV :: 'n set)"
+ { assume H: "?rhs"
+ then have ?lhs by auto }
+ moreover
+ { assume H: "?lhs"
+ then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis
+ let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
+ { fix i
+ from f have "P i (f i)" by metis
+ then have "P i (?x $ i)" by auto
+ }
+ hence "\<forall>i. P i (?x$i)" by metis
+ hence ?rhs by metis }
+ ultimately show ?thesis by metis
+qed
+
+
+text \<open>The same result in terms of square matrices.\<close>
+
+
+text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close>
+
+definition%unimportant "rowvector v = (\<chi> i j. (v$j))"
+
+definition%unimportant "columnvector v = (\<chi> i j. (v$i))"
+
+lemma%unimportant transpose_columnvector: "transpose(columnvector v) = rowvector v"
+ by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff)
+
+lemma%unimportant transpose_rowvector: "transpose(rowvector v) = columnvector v"
+ by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff)
+
+lemma%unimportant dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v"
+ by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)
+
+lemma%unimportant dot_matrix_product:
+ "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1"
+ by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def)
+
+lemma%unimportant dot_matrix_vector_mul:
+ fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
+ shows "(A *v x) \<bullet> (B *v y) =
+ (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1"
+ unfolding dot_matrix_product transpose_columnvector[symmetric]
+ dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
+
+
+lemma%important dim_substandard_cart: "vec.dim {x::'a::field^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d"
+ (is "vec.dim ?A = _")
+proof%unimportant (rule vec.dim_unique)
+ let ?B = "((\<lambda>x. axis x 1) ` d)"
+ have subset_basis: "?B \<subseteq> cart_basis"
+ by (auto simp: cart_basis_def)
+ show "?B \<subseteq> ?A"
+ by (auto simp: axis_def)
+ show "vec.independent ((\<lambda>x. axis x 1) ` d)"
+ using subset_basis
+ by (rule vec.independent_mono[OF vec.independent_Basis])
+ have "x \<in> vec.span ?B" if "\<forall>i. i \<notin> d \<longrightarrow> x $ i = 0" for x::"'a^'n"
+ proof -
+ have "finite ?B"
+ using subset_basis finite_cart_basis
+ by (rule finite_subset)
+ have "x = (\<Sum>i\<in>UNIV. x $ i *s axis i 1)"
+ by (rule basis_expansion[symmetric])
+ also have "\<dots> = (\<Sum>i\<in>d. (x $ i) *s axis i 1)"
+ by (rule sum.mono_neutral_cong_right) (auto simp: that)
+ also have "\<dots> \<in> vec.span ?B"
+ by (simp add: vec.span_sum vec.span_clauses)
+ finally show "x \<in> vec.span ?B" .
+ qed
+ then show "?A \<subseteq> vec.span ?B" by auto
+qed (simp add: card_image inj_on_def axis_eq_axis)
+
+lemma%unimportant affinity_inverses:
+ assumes m0: "m \<noteq> (0::'a::field)"
+ shows "(\<lambda>x. m *s x + c) \<circ> (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
+ "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) \<circ> (\<lambda>x. m *s x + c) = id"
+ using m0
+ by (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff)
+
+lemma%important vector_affinity_eq:
+ assumes m0: "(m::'a::field) \<noteq> 0"
+ shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)"
+proof%unimportant
+ assume h: "m *s x + c = y"
+ hence "m *s x = y - c" by (simp add: field_simps)
+ hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp
+ then show "x = inverse m *s y + - (inverse m *s c)"
+ using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
+next
+ assume h: "x = inverse m *s y + - (inverse m *s c)"
+ show "m *s x + c = y" unfolding h
+ using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
+qed
+
+lemma%unimportant vector_eq_affinity:
+ "(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)"
+ using vector_affinity_eq[where m=m and x=x and y=y and c=c]
+ by metis
+
+lemma%unimportant vector_cart:
+ fixes f :: "real^'n \<Rightarrow> real"
+ shows "(\<chi> i. f (axis i 1)) = (\<Sum>i\<in>Basis. f i *\<^sub>R i)"
+ unfolding euclidean_eq_iff[where 'a="real^'n"]
+ by simp (simp add: Basis_vec_def inner_axis)
+
+lemma%unimportant const_vector_cart:"((\<chi> i. d)::real^'n) = (\<Sum>i\<in>Basis. d *\<^sub>R i)"
+ by (rule vector_cart)
+
end
\ No newline at end of file
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Jan 16 17:56:29 2019 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Jan 16 18:54:18 2019 +0100
@@ -626,7 +626,7 @@
lemma%unimportant norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
by (simp add: norm_vec_def L2_set_le_sum)
-lemma%unimportant bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
+lemma%unimportant bounded_linear_vec_nth[intro]: "bounded_linear (\<lambda>x. x $ i)"
apply standard
apply (rule vector_add_component)
apply (rule vector_scaleR_component)
@@ -1082,6 +1082,14 @@
"transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult.commute)
+lemma%unimportant matrix_mult_transpose_dot_column:
+ shows "transpose A ** A = (\<chi> i j. inner (column i A) (column j A))"
+ by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)
+
+lemma%unimportant matrix_mult_transpose_dot_row:
+ shows "A ** transpose A = (\<chi> i j. inner (row i A) (row j A))"
+ by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)
+
lemma%unimportant matrix_eq:
fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"
shows "A = B \<longleftrightarrow> (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Jan 16 17:56:29 2019 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Jan 16 18:54:18 2019 +0100
@@ -7489,7 +7489,7 @@
fixes f :: "'n::euclidean_space \<Rightarrow> real^'m"
assumes "f integrable_on s"
shows "integral s (\<lambda>x. f x $ k) = integral s f $ k"
- using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] .
+ using integral_linear[OF assms(1) bounded_linear_vec_nth,unfolded o_def] .
lemma content_closed_interval:
fixes a :: "'a::ordered_euclidean_space"