# HG changeset patch # User Angeliki KoutsoukouArgyraki # Date 1548214174 0 # Node ID 9b9f203e0ba3d6d0efc962d226905001e05cbf62 # Parent b5163b2132c583a5f55d09f6b5919e7be79a27d3 tagged 2 theories ie Cartesian_Euclidean_Space Cartesian_Space diff -r b5163b2132c5 -r 9b9f203e0ba3 src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Tue Jan 22 22:57:16 2019 +0000 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Jan 23 03:29:34 2019 +0000 @@ -2,19 +2,19 @@ Some material by Jose Divasón, Tim Makarios and L C Paulson *) -section%important \Finite Cartesian Products of Euclidean Spaces\ +section \Finite Cartesian Products of Euclidean Spaces\ theory Cartesian_Euclidean_Space imports Cartesian_Space Derivative begin -lemma%unimportant subspace_special_hyperplane: "subspace {x. x $ k = 0}" +lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}" by (simp add: subspace_def) -lemma%important sum_mult_product: +lemma sum_mult_product: "sum h {..i\{..j\{..j. j + i * B) {..j. j + i * B) ` {.. cbox a b = {}" "box (vec a) (vec b) = {} \ box a b = {}" by (auto simp: Basis_vec_def mem_box box_eq_empty inner_axis) subsection\Closures and interiors of halfspaces\ -lemma%important interior_halfspace_le [simp]: +lemma interior_halfspace_le [simp]: assumes "a \ 0" shows "interior {x. a \ x \ b} = {x. a \ x < b}" -proof%unimportant - +proof - have *: "a \ x < b" if x: "x \ S" and S: "S \ {x. a \ x \ b}" and "open S" for S x proof - obtain e where "e>0" and e: "cball x e \ S" @@ -70,15 +70,15 @@ by (rule interior_unique) (auto simp: open_halfspace_lt *) qed -lemma%unimportant interior_halfspace_ge [simp]: +lemma interior_halfspace_ge [simp]: "a \ 0 \ interior {x. a \ x \ b} = {x. a \ x > b}" using interior_halfspace_le [of "-a" "-b"] by simp -lemma%important interior_halfspace_component_le [simp]: +lemma interior_halfspace_component_le [simp]: "interior {x. x$k \ a} = {x :: (real^'n). x$k < a}" (is "?LE") and interior_halfspace_component_ge [simp]: "interior {x. x$k \ a} = {x :: (real^'n). x$k > a}" (is "?GE") -proof%unimportant - +proof - have "axis k (1::real) \ 0" by (simp add: axis_def vec_eq_iff) moreover have "axis k (1::real) \ x = x$k" for x @@ -88,7 +88,7 @@ interior_halfspace_ge [of "axis k (1::real)" a] by auto qed -lemma%unimportant closure_halfspace_lt [simp]: +lemma closure_halfspace_lt [simp]: assumes "a \ 0" shows "closure {x. a \ x < b} = {x. a \ x \ b}" proof - @@ -99,15 +99,15 @@ by (force simp: closure_interior) qed -lemma%unimportant closure_halfspace_gt [simp]: +lemma closure_halfspace_gt [simp]: "a \ 0 \ closure {x. a \ x > b} = {x. a \ x \ b}" using closure_halfspace_lt [of "-a" "-b"] by simp -lemma%important closure_halfspace_component_lt [simp]: +lemma closure_halfspace_component_lt [simp]: "closure {x. x$k < a} = {x :: (real^'n). x$k \ a}" (is "?LE") and closure_halfspace_component_gt [simp]: "closure {x. x$k > a} = {x :: (real^'n). x$k \ a}" (is "?GE") -proof%unimportant - +proof - have "axis k (1::real) \ 0" by (simp add: axis_def vec_eq_iff) moreover have "axis k (1::real) \ x = x$k" for x @@ -117,17 +117,17 @@ closure_halfspace_gt [of "axis k (1::real)" a] by auto qed -lemma%unimportant interior_hyperplane [simp]: +lemma interior_hyperplane [simp]: assumes "a \ 0" shows "interior {x. a \ x = b} = {}" -proof%unimportant - +proof - have [simp]: "{x. a \ x = b} = {x. a \ x \ b} \ {x. a \ x \ b}" by (force simp:) then show ?thesis by (auto simp: assms) qed -lemma%unimportant frontier_halfspace_le: +lemma frontier_halfspace_le: assumes "a \ 0 \ b \ 0" shows "frontier {x. a \ x \ b} = {x. a \ x = b}" proof (cases "a = 0") @@ -137,7 +137,7 @@ by (force simp: frontier_def closed_halfspace_le) qed -lemma%unimportant frontier_halfspace_ge: +lemma frontier_halfspace_ge: assumes "a \ 0 \ b \ 0" shows "frontier {x. a \ x \ b} = {x. a \ x = b}" proof (cases "a = 0") @@ -147,7 +147,7 @@ by (force simp: frontier_def closed_halfspace_ge) qed -lemma%unimportant frontier_halfspace_lt: +lemma frontier_halfspace_lt: assumes "a \ 0 \ b \ 0" shows "frontier {x. a \ x < b} = {x. a \ x = b}" proof (cases "a = 0") @@ -157,19 +157,19 @@ by (force simp: frontier_def interior_open open_halfspace_lt) qed -lemma%important frontier_halfspace_gt: +lemma frontier_halfspace_gt: assumes "a \ 0 \ b \ 0" shows "frontier {x. a \ x > b} = {x. a \ x = b}" -proof%unimportant (cases "a = 0") +proof (cases "a = 0") case True with assms show ?thesis by simp next case False then show ?thesis by (force simp: frontier_def interior_open open_halfspace_gt) qed -lemma%important interior_standard_hyperplane: +lemma interior_standard_hyperplane: "interior {x :: (real^'n). x$k = a} = {}" -proof%unimportant - +proof - have "axis k (1::real) \ 0" by (simp add: axis_def vec_eq_iff) moreover have "axis k (1::real) \ x = x$k" for x @@ -179,11 +179,11 @@ by force qed -lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear ((*v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m" +lemma 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 +lemma 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)" @@ -192,10 +192,10 @@ subsection\Bounds on components etc.\ relative to operator norm\ -lemma%important norm_column_le_onorm: +lemma norm_column_le_onorm: fixes A :: "real^'n^'m" shows "norm(column i A) \ onorm((*v) A)" -proof%unimportant - +proof - have "norm (\ j. A $ j $ i) \ norm (A *v axis i 1)" by (simp add: matrix_mult_dot cart_eq_inner_axis) also have "\ \ onorm ((*v) A)" @@ -205,10 +205,10 @@ unfolding column_def . qed -lemma%important matrix_component_le_onorm: +lemma matrix_component_le_onorm: fixes A :: "real^'n^'m" shows "\A $ i $ j\ \ onorm((*v) A)" -proof%unimportant - +proof - have "\A $ i $ j\ \ norm (\ n. (A $ n $ j))" by (metis (full_types, lifting) component_le_norm_cart vec_lambda_beta) also have "\ \ onorm ((*v) A)" @@ -216,15 +216,15 @@ finally show ?thesis . qed -lemma%unimportant component_le_onorm: +lemma component_le_onorm: fixes f :: "real^'m \ real^'n" shows "linear f \ \matrix f $ i $ j\ \ onorm f" by (metis linear_matrix_vector_mul_eq matrix_component_le_onorm matrix_vector_mul) -lemma%important onorm_le_matrix_component_sum: +lemma onorm_le_matrix_component_sum: fixes A :: "real^'n^'m" shows "onorm((*v) A) \ (\i\UNIV. \j\UNIV. \A $ i $ j\)" -proof%unimportant (rule onorm_le) +proof (rule onorm_le) fix x have "norm (A *v x) \ (\i\UNIV. $A *v x) $ i$" by (rule norm_le_l1_cart) @@ -243,11 +243,11 @@ by (simp add: sum_distrib_right) qed -lemma%important onorm_le_matrix_component: +lemma onorm_le_matrix_component: fixes A :: "real^'n^'m" assumes "\i j. abs(A$i$j) \ B" shows "onorm((*v) A) \ real (CARD('m)) * real (CARD('n)) * B" -proof%unimportant (rule onorm_le) +proof (rule onorm_le) fix x :: "real^'n::_" have "norm (A *v x) \ (\i\UNIV. $A *v x) $ i$" by (rule norm_le_l1_cart) @@ -268,16 +268,16 @@ qed -lemma%unimportant rational_approximation: +lemma rational_approximation: assumes "e > 0" obtains r::real where "r \ \" "\r - x\ < e" using Rats_dense_in_real [of "x - e/2" "x + e/2"] assms by auto -lemma%important matrix_rational_approximation: +proposition matrix_rational_approximation: fixes A :: "real^'n^'m" assumes "e > 0" obtains B where "\i j. B$i$j \ \" "onorm(\x. (A - B) *v x) < e" -proof%unimportant - +proof - have "\i j. \q \ \. \q - A $ i $ j\ < e / (2 * CARD('m) * CARD('n))" using assms by (force intro: rational_approximation [of "e / (2 * CARD('m) * CARD('n))"]) then obtain B where B: "\i j. B$i$j \ \" and Bclo: "\i j. \B$i$j - A $ i $ j\ < e / (2 * CARD('m) * CARD('n))" @@ -294,30 +294,30 @@ qed (use B in auto) qed -lemma%unimportant vector_sub_project_orthogonal_cart: "(b::real^'n) \ (x - ((b \ x) / (b \ b)) *s b) = 0" +lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \ (x - ((b \ x) / (b \ b)) *s b) = 0" unfolding inner_simps scalar_mult_eq_scaleR by auto -lemma%unimportant infnorm_cart:"infnorm (x::real^'n) = Sup {\x$i\ |i. i\UNIV}" +lemma infnorm_cart:"infnorm (x::real^'n) = Sup {\x$i\ |i. i\UNIV}" by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right) -lemma%unimportant component_le_infnorm_cart: "\x$i\ \ infnorm (x::real^'n)" +lemma component_le_infnorm_cart: "\x$i\ \ infnorm (x::real^'n)" using Basis_le_infnorm[of "axis i 1" x] by (simp add: Basis_vec_def axis_eq_axis inner_axis) -lemma%unimportant continuous_component[continuous_intros]: "continuous F f \ continuous F (\x. f x $ i)" +lemma continuous_component[continuous_intros]: "continuous F f \ continuous F (\x. f x $ i)" unfolding continuous_def by (rule tendsto_vec_nth) -lemma%unimportant continuous_on_component[continuous_intros]: "continuous_on s f \ continuous_on s (\x. f x $ i)" +lemma continuous_on_component[continuous_intros]: "continuous_on s f \ continuous_on s (\x. f x $ i)" unfolding continuous_on_def by (fast intro: tendsto_vec_nth) -lemma%unimportant continuous_on_vec_lambda[continuous_intros]: +lemma continuous_on_vec_lambda[continuous_intros]: "(\i. continuous_on S (f i)) \ continuous_on S (\x. \ i. f i x)" unfolding continuous_on_def by (auto intro: tendsto_vec_lambda) -lemma%unimportant closed_positive_orthant: "closed {x::real^'n. \i. 0 \x$i}" +lemma closed_positive_orthant: "closed {x::real^'n. \i. 0 \x$i}" by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) -lemma%unimportant bounded_component_cart: "bounded s \ bounded ((\x. x $ i) ` s)" +lemma bounded_component_cart: "bounded s \ bounded ((\x. x $ i) ` s)" unfolding bounded_def apply clarify apply (rule_tac x="x $ i" in exI) @@ -326,13 +326,13 @@ apply (rule order_trans [OF dist_vec_nth_le], simp) done -lemma%important compact_lemma_cart: +lemma compact_lemma_cart: fixes f :: "nat \ 'a::heine_borel ^ 'n" assumes f: "bounded (range f)" shows "\l r. strict_mono r \ (\e>0. eventually (\n. \i\d. dist (f (r n) $ i) (l $ i) < e) sequentially)" (is "?th d") -proof%unimportant - +proof - have "\d' \ d. ?th d'" by (rule compact_lemma_general[where unproj=vec_lambda]) (auto intro!: f bounded_component_cart simp: vec_lambda_eta) @@ -368,19 +368,19 @@ with r show "\l r. strict_mono r \ ((f \ r) \ l) sequentially" by auto qed -lemma%unimportant interval_cart: +lemma interval_cart: fixes a :: "real^'n" shows "box a b = {x::real^'n. \i. a$i < x$i \ x$i < b$i}" and "cbox a b = {x::real^'n. \i. a$i \ x$i \ x$i \ b$i}" by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def mem_box Basis_vec_def inner_axis) -lemma%unimportant mem_box_cart: +lemma mem_box_cart: fixes a :: "real^'n" shows "x \ box a b \ (\i. a$i < x$i \ x$i < b$i)" and "x \ cbox a b \ (\i. a$i \ x$i \ x$i \ b$i)" using interval_cart[of a b] by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def) -lemma%unimportant interval_eq_empty_cart: +lemma interval_eq_empty_cart: fixes a :: "real^'n" shows "(box a b = {} \ (\i. b$i \ a$i))" (is ?th1) and "(cbox a b = {} \ (\i. b$i < a$i))" (is ?th2) @@ -416,14 +416,14 @@ ultimately show ?th2 by blast qed -lemma%unimportant interval_ne_empty_cart: +lemma interval_ne_empty_cart: fixes a :: "real^'n" shows "cbox a b \ {} \ (\i. a$i \ b$i)" and "box a b \ {} \ (\i. a$i < b$i)" unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le) (* BH: Why doesn't just "auto" work here? *) -lemma%unimportant subset_interval_imp_cart: +lemma subset_interval_imp_cart: fixes a :: "real^'n" shows "(\i. a$i \ c$i \ d$i \ b$i) \ cbox c d \ cbox a b" and "(\i. a$i < c$i \ d$i < b$i) \ cbox c d \ box a b" @@ -432,13 +432,13 @@ unfolding subset_eq[unfolded Ball_def] unfolding mem_box_cart by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *) -lemma%unimportant interval_sing: +lemma interval_sing: fixes a :: "'a::linorder^'n" shows "{a .. a} = {a} \ {a<.. cbox a b \ (\i. c$i \ d$i) --> (\i. a$i \ c$i \ d$i \ b$i)" (is ?th1) and "cbox c d \ box a b \ (\i. c$i \ d$i) --> (\i. a$i < c$i \ d$i < b$i)" (is ?th2) @@ -446,7 +446,7 @@ and "box c d \ box a b \ (\i. c$i < d$i) --> (\i. a$i \ c$i \ d$i \ b$i)" (is ?th4) using subset_box[of c d a b] by (simp_all add: Basis_vec_def inner_axis) -lemma%unimportant disjoint_interval_cart: +lemma disjoint_interval_cart: fixes a::"real^'n" shows "cbox a b \ cbox c d = {} \ (\i. (b$i < a$i \ d$i < c$i \ b$i < c$i \ d$i < a$i))" (is ?th1) and "cbox a b \ box c d = {} \ (\i. (b$i < a$i \ d$i \ c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th2) @@ -454,53 +454,53 @@ and "box a b \ box c d = {} \ (\i. (b$i \ a$i \ d$i \ c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th4) using disjoint_interval[of a b c d] by (simp_all add: Basis_vec_def inner_axis) -lemma%unimportant Int_interval_cart: +lemma Int_interval_cart: fixes a :: "real^'n" shows "cbox a b \ cbox c d = {(\ i. max (a$i) (c$i)) .. (\ i. min (b$i) (d$i))}" unfolding Int_interval by (auto simp: mem_box less_eq_vec_def) (auto simp: Basis_vec_def inner_axis) -lemma%unimportant closed_interval_left_cart: +lemma closed_interval_left_cart: fixes b :: "real^'n" shows "closed {x::real^'n. \i. x$i \ b$i}" by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) -lemma%unimportant closed_interval_right_cart: +lemma closed_interval_right_cart: fixes a::"real^'n" shows "closed {x::real^'n. \i. a$i \ x$i}" by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) -lemma%unimportant is_interval_cart: +lemma is_interval_cart: "is_interval (s::(real^'n) set) \ (\a\s. \b\s. \x. (\i. ((a$i \ x$i \ x$i \ b$i) \ (b$i \ x$i \ x$i \ a$i))) \ x \ s)" 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 \ a}" +lemma closed_halfspace_component_le_cart: "closed {x::real^'n. x$i \ a}" by (simp add: closed_Collect_le continuous_on_component) -lemma%unimportant closed_halfspace_component_ge_cart: "closed {x::real^'n. x$i \ a}" +lemma closed_halfspace_component_ge_cart: "closed {x::real^'n. x$i \ a}" by (simp add: closed_Collect_le continuous_on_component) -lemma%unimportant open_halfspace_component_lt_cart: "open {x::real^'n. x$i < a}" +lemma open_halfspace_component_lt_cart: "open {x::real^'n. x$i < a}" by (simp add: open_Collect_less continuous_on_component) -lemma%unimportant open_halfspace_component_gt_cart: "open {x::real^'n. x$i > a}" +lemma open_halfspace_component_gt_cart: "open {x::real^'n. x$i > a}" by (simp add: open_Collect_less continuous_on_component) -lemma%unimportant Lim_component_le_cart: +lemma Lim_component_le_cart: fixes f :: "'a \ real^'n" assumes "(f \ l) net" "\ (trivial_limit net)" "eventually (\x. f x $i \ b) net" shows "l$i \ b" by (rule tendsto_le[OF assms(2) tendsto_const tendsto_vec_nth, OF assms(1, 3)]) -lemma%unimportant Lim_component_ge_cart: +lemma Lim_component_ge_cart: fixes f :: "'a \ real^'n" assumes "(f \ l) net" "\ (trivial_limit net)" "eventually (\x. b \ (f x)$i) net" shows "b \ l$i" by (rule tendsto_le[OF assms(2) tendsto_vec_nth tendsto_const, OF assms(1, 3)]) -lemma%unimportant Lim_component_eq_cart: +lemma Lim_component_eq_cart: fixes f :: "'a \ real^'n" assumes net: "(f \ l) net" "\ trivial_limit net" and ev:"eventually (\x. f(x)$i = b) net" shows "l$i = b" @@ -508,18 +508,18 @@ Lim_component_ge_cart[OF net, of b i] and Lim_component_le_cart[OF net, of i b] by auto -lemma%unimportant connected_ivt_component_cart: +lemma connected_ivt_component_cart: fixes x :: "real^'n" shows "connected s \ x \ s \ y \ s \ x$k \ a \ a \ y$k \ (\z\s. z$k = a)" using connected_ivt_hyperplane[of s x y "axis k 1" a] by (auto simp add: inner_axis inner_commute) -lemma%unimportant subspace_substandard_cart: "vec.subspace {x. (\i. P i \ x$i = 0)}" +lemma subspace_substandard_cart: "vec.subspace {x. (\i. P i \ x$i = 0)}" unfolding vec.subspace_def by auto -lemma%important closed_substandard_cart: +lemma closed_substandard_cart: "closed {x::'a::real_normed_vector ^ 'n. \i. P i \ x$i = 0}" -proof%unimportant - +proof - { fix i::'n have "closed {x::'a ^ 'n. P i \ x$i = 0}" by (cases "P i") (simp_all add: closed_Collect_eq continuous_on_const continuous_on_id continuous_on_component) } @@ -529,32 +529,32 @@ subsection "Convex Euclidean Space" -lemma%unimportant Cart_1:"(1::real^'n) = \Basis" +lemma Cart_1:"(1::real^'n) = \Basis" using const_vector_cart[of 1] by (simp add: one_vec_def) declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp] declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp] -lemmas%unimportant vector_component_simps = vector_minus_component vector_smult_component vector_add_component less_eq_vec_def vec_lambda_beta vector_uminus_component +lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component less_eq_vec_def vec_lambda_beta vector_uminus_component -lemma%unimportant convex_box_cart: +lemma convex_box_cart: assumes "\i. convex {x. P i x}" shows "convex {x. \i. P i (x$i)}" using assms unfolding convex_def by auto -lemma%unimportant convex_positive_orthant_cart: "convex {x::real^'n. (\i. 0 \ x$i)}" +lemma convex_positive_orthant_cart: "convex {x::real^'n. (\i. 0 \ x$i)}" by (rule convex_box_cart) (simp add: atLeast_def[symmetric]) -lemma%unimportant unit_interval_convex_hull_cart: +lemma unit_interval_convex_hull_cart: "cbox (0::real^'n) 1 = convex hull {x. \i. (x$i = 0) \ (x$i = 1)}" unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"] box_real[symmetric] by (rule arg_cong[where f="\x. convex hull x"]) (simp add: Basis_vec_def inner_axis) -lemma%important cube_convex_hull_cart: +proposition cube_convex_hull_cart: assumes "0 < d" obtains s::"(real^'n) set" where "finite s" "cbox (x - (\ i. d)) (x + (\ i. d)) = convex hull s" -proof%unimportant - +proof - from assms obtain s where "finite s" and "cbox (x - sum ((*\<^sub>R) d) Basis) (x + sum ((*\<^sub>R) d) Basis) = convex hull s" by (rule cube_convex_hull) @@ -567,10 +567,10 @@ definition%important "jacobian f net = matrix(frechet_derivative f net)" -lemma%important jacobian_works: +proposition jacobian_works: "(f::(real^'a) \ (real^'b)) differentiable net \ (f has_derivative (\h. (jacobian f net) *v h)) net" (is "?lhs = ?rhs") -proof%unimportant +proof assume ?lhs then show ?rhs by (simp add: frechet_derivative_works has_derivative_linear jacobian_def) next @@ -579,10 +579,10 @@ qed -text%important \Component of the differential must be zero if it exists at a local +text \Component of the differential must be zero if it exists at a local maximum or minimum for that corresponding component\ -lemma%important differential_zero_maxmin_cart: +proposition differential_zero_maxmin_cart: fixes f::"real^'a \ real^'b" assumes "0 < e" "((\y \ ball x e. (f y)$k \ (f x)$k) \ (\y\ball x e. (f x)$k \ (f y)$k))" "f differentiable (at x)" diff -r b5163b2132c5 -r 9b9f203e0ba3 src/HOL/Analysis/Cartesian_Space.thy --- a/src/HOL/Analysis/Cartesian_Space.thy Tue Jan 22 22:57:16 2019 +0000 +++ b/src/HOL/Analysis/Cartesian_Space.thy Wed Jan 23 03:29:34 2019 +0000 @@ -13,21 +13,22 @@ Finite_Cartesian_Product Linear_Algebra begin -subsection \Type @{typ \'a ^ 'n\} and fields as vector spaces\ +subsection%unimportant \Type @{typ \'a ^ 'n\} and fields as vector spaces\ (*much of the following +is really basic linear algebra, check for overlap? rename subsection? *) -definition%unimportant "cart_basis = {axis i 1 | i. i\UNIV}" +definition "cart_basis = {axis i 1 | i. i\UNIV}" -lemma%unimportant finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def +lemma finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def using finite_Atleast_Atmost_nat by fastforce -lemma%unimportant card_cart_basis: "card (cart_basis::('a::zero_neq_one^'i) set) = CARD('i)" +lemma card_cart_basis: "card (cart_basis::('a::zero_neq_one^'i) set) = CARD('i)" unfolding cart_basis_def Setcompr_eq_image by (rule card_image) (auto simp: inj_on_def axis_eq_axis) -interpretation%important vec: vector_space "(*s) " +interpretation vec: vector_space "(*s) " by unfold_locales (vector algebra_simps)+ -lemma%unimportant independent_cart_basis: +lemma independent_cart_basis: "vec.independent (cart_basis)" proof (rule vec.independent_if_scalars_zero) show "finite (cart_basis)" using finite_cart_basis . @@ -52,7 +53,7 @@ finally show "f x = 0" .. qed -lemma%unimportant span_cart_basis: +lemma span_cart_basis: "vec.span (cart_basis) = UNIV" proof (auto) fix x::"('a, 'b) vec" @@ -97,12 +98,12 @@ interpretation vec: finite_dimensional_vector_space "(*s)" "cart_basis" by (unfold_locales, auto simp add: finite_cart_basis independent_cart_basis span_cart_basis) -lemma%unimportant matrix_vector_mul_linear_gen[intro, simp]: +lemma matrix_vector_mul_linear_gen[intro, simp]: "Vector_Spaces.linear (*s) (*s) ((*v) A)" by unfold_locales (vector matrix_vector_mult_def sum.distrib algebra_simps)+ -lemma%important span_vec_eq: "vec.span X = span X" +lemma span_vec_eq: "vec.span X = span X" and dim_vec_eq: "vec.dim X = dim X" and dependent_vec_eq: "vec.dependent X = dependent X" and subspace_vec_eq: "vec.subspace X = subspace X" @@ -110,11 +111,11 @@ unfolding span_raw_def dim_raw_def dependent_raw_def subspace_raw_def by (auto simp: scalar_mult_eq_scaleR) -lemma%important linear_componentwise: +lemma linear_componentwise: fixes f:: "'a::field ^'m \ 'a ^ 'n" assumes lf: "Vector_Spaces.linear (*s) (*s) f" shows "(f x)$j = sum (\i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") -proof%unimportant - +proof - interpret lf: Vector_Spaces.linear "(*s)" "(*s)" f using lf . let ?M = "(UNIV :: 'm set)" @@ -132,7 +133,7 @@ interpretation vec: finite_dimensional_vector_space_pair "(*s)" cart_basis "(*s)" cart_basis .. -lemma%unimportant matrix_works: +lemma matrix_works: assumes lf: "Vector_Spaces.linear (*s) (*s) f" shows "matrix f *v x = f (x::'a::field ^ 'n)" apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute) @@ -140,45 +141,45 @@ apply (rule linear_componentwise[OF lf, symmetric]) done -lemma%unimportant matrix_of_matrix_vector_mul[simp]: "matrix(\x. A *v (x :: 'a::field ^ 'n)) = A" +lemma matrix_of_matrix_vector_mul[simp]: "matrix(\x. A *v (x :: 'a::field ^ 'n)) = A" by (simp add: matrix_eq matrix_works) -lemma%unimportant matrix_compose_gen: +lemma matrix_compose_gen: assumes lf: "Vector_Spaces.linear (*s) (*s) (f::'a::{field}^'n \ 'a^'m)" and lg: "Vector_Spaces.linear (*s) (*s) (g::'a^'m \ 'a^_)" shows "matrix (g o f) = matrix g ** matrix f" using lf lg Vector_Spaces.linear_compose[OF lf lg] matrix_works[OF Vector_Spaces.linear_compose[OF lf lg]] by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) -lemma%unimportant matrix_compose: +lemma matrix_compose: assumes "linear (f::real^'n \ real^'m)" "linear (g::real^'m \ real^_)" shows "matrix (g o f) = matrix g ** matrix f" using matrix_compose_gen[of f g] assms by (simp add: linear_def scalar_mult_eq_scaleR) -lemma%unimportant left_invertible_transpose: +lemma left_invertible_transpose: "(\(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \ (\(B). A ** B = mat 1)" by (metis matrix_transpose_mul transpose_mat transpose_transpose) -lemma%unimportant right_invertible_transpose: +lemma right_invertible_transpose: "(\(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \ (\(B). B ** A = mat 1)" by (metis matrix_transpose_mul transpose_mat transpose_transpose) -lemma%unimportant linear_matrix_vector_mul_eq: +lemma linear_matrix_vector_mul_eq: "Vector_Spaces.linear (*s) (*s) f \ linear (f :: real^'n \ real ^'m)" by (simp add: scalar_mult_eq_scaleR linear_def) -lemma%unimportant matrix_vector_mul[simp]: +lemma matrix_vector_mul[simp]: "Vector_Spaces.linear (*s) (*s) g \ (\y. matrix g *v y) = g" "linear f \ (\x. matrix f *v x) = f" "bounded_linear f \ (\x. matrix f *v x) = f" for f :: "real^'n \ real ^'m" by (simp_all add: ext matrix_works linear_matrix_vector_mul_eq linear_linear) -lemma%important matrix_left_invertible_injective: +lemma matrix_left_invertible_injective: fixes A :: "'a::field^'n^'m" shows "(\B. B ** A = mat 1) \ inj ((*v) A)" -proof%unimportant safe +proof safe fix B assume B: "B ** A = mat 1" show "inj ((*v) A)" @@ -196,15 +197,15 @@ by metis qed -lemma%unimportant matrix_left_invertible_ker: +lemma matrix_left_invertible_ker: "(\B. (B::'a::{field} ^'m^'n) ** (A::'a::{field}^'n^'m) = mat 1) \