--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Sun Apr 15 17:22:58 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Sun Apr 15 21:41:40 2018 +0100
@@ -540,7 +540,6 @@
mult_1_left mult_zero_left if_True UNIV_I)
done
-
lemma matrix_mul_rid [simp]:
fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
shows "A ** mat 1 = A"
@@ -672,6 +671,12 @@
definition matrix :: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
where "matrix f = (\<chi> i j. (f(axis j 1))$i)"
+lemma matrix_id_mat_1: "matrix id = mat 1"
+ by (simp add: mat_def matrix_def axis_def)
+
+lemma matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r"
+ by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
+
lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"
by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
field_simps sum_distrib_left sum.distrib)
@@ -896,22 +901,23 @@
by (metis matrix_transpose_mul transpose_mat transpose_transpose)
lemma matrix_left_invertible_injective:
- "(\<exists>B. (B::real^'m^'n) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x y. A *v x = A *v y \<longrightarrow> x = y)"
-proof -
- { fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y"
- from xy have "B*v (A *v x) = B *v (A*v y)" by simp
- hence "x = y"
- unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid . }
- moreover
- { assume A: "\<forall>x y. A *v x = A *v y \<longrightarrow> x = y"
- hence i: "inj (( *v) A)" unfolding inj_on_def by auto
- from linear_injective_left_inverse[OF matrix_vector_mul_linear i]
- obtain g where g: "linear g" "g \<circ> ( *v) A = id" by blast
- have "matrix g ** A = mat 1"
- unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
- using g(2) by (simp add: fun_eq_iff)
- then have "\<exists>B. (B::real ^'m^'n) ** A = mat 1" by blast }
- ultimately show ?thesis by blast
+ fixes A :: "real^'n^'m"
+ shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj (( *v) A)"
+proof safe
+ fix B
+ assume B: "B ** A = mat 1"
+ show "inj (( *v) A)"
+ unfolding inj_on_def
+ by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid)
+next
+ assume "inj (( *v) A)"
+ with linear_injective_left_inverse[OF matrix_vector_mul_linear]
+ obtain g where "linear g" and g: "g \<circ> ( *v) A = id"
+ by blast
+ have "matrix g ** A = mat 1"
+ by (metis \<open>linear g\<close> g matrix_compose matrix_id_mat_1 matrix_of_matrix_vector_mul matrix_vector_mul_linear)
+ then show "\<exists>B. B ** A = mat 1"
+ by metis
qed
lemma matrix_left_invertible_ker:
@@ -1443,15 +1449,14 @@
lemma jacobian_works:
"(f::(real^'a) \<Rightarrow> (real^'b)) differentiable net \<longleftrightarrow>
- (f has_derivative (\<lambda>h. (jacobian f net) *v h)) net"
- apply rule
- unfolding jacobian_def
- apply (simp only: matrix_works[OF linear_frechet_derivative]) defer
- apply (rule differentiableI)
- apply assumption
- unfolding frechet_derivative_works
- apply assumption
- done
+ (f has_derivative (\<lambda>h. (jacobian f net) *v h)) net" (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ by (simp add: frechet_derivative_works has_derivative_linear jacobian_def)
+next
+ assume ?rhs then show ?lhs
+ by (rule differentiableI)
+qed
subsection \<open>Component of the differential must be zero if it exists at a local
@@ -1571,6 +1576,153 @@
lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>"
by (auto simp add: norm_real dist_norm)
+subsection\<open> Rank of a matrix\<close>
+
+text\<open>Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\<close>
+
+lemma matrix_vector_mult_in_columnspace:
+ fixes A :: "real^'n^'m"
+ shows "(A *v x) \<in> span(columns A)"
+ apply (simp add: matrix_vector_column columns_def transpose_def column_def)
+ apply (intro span_sum span_mul)
+ apply (force intro: span_superset)
+ done
+
+lemma orthogonal_nullspace_rowspace:
+ fixes A :: "real^'n^'m"
+ assumes 0: "A *v x = 0" and y: "y \<in> span(rows A)"
+ shows "orthogonal x y"
+proof (rule span_induct [OF y])
+ show "subspace {a. orthogonal x a}"
+ by (simp add: subspace_orthogonal_to_vector)
+next
+ fix v
+ assume "v \<in> rows A"
+ then obtain i where "v = row i A"
+ by (auto simp: rows_def)
+ with 0 show "orthogonal x v"
+ unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def
+ by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index)
+qed
+
+lemma nullspace_inter_rowspace:
+ fixes A :: "real^'n^'m"
+ shows "A *v x = 0 \<and> x \<in> span(rows A) \<longleftrightarrow> x = 0"
+ using orthogonal_nullspace_rowspace orthogonal_self by auto
+
+lemma matrix_vector_mul_injective_on_rowspace:
+ fixes A :: "real^'n^'m"
+ shows "\<lbrakk>A *v x = A *v y; x \<in> span(rows A); y \<in> span(rows A)\<rbrakk> \<Longrightarrow> x = y"
+ using nullspace_inter_rowspace [of A "x-y"]
+ by (metis eq_iff_diff_eq_0 matrix_vector_mult_diff_distrib span_diff)
+
+definition rank :: "real^'n^'m=>nat"
+ where "rank A \<equiv> dim(columns A)"
+
+lemma dim_rows_le_dim_columns:
+ fixes A :: "real^'n^'m"
+ shows "dim(rows A) \<le> dim(columns A)"
+proof -
+ have "dim (span (rows A)) \<le> dim (span (columns A))"
+ proof -
+ obtain B where "independent B" "span(rows A) \<subseteq> span B"
+ and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))"
+ using basis_exists [of "span(rows A)"] by blast
+ with span_subspace have eq: "span B = span(rows A)"
+ by auto
+ then have inj: "inj_on (( *v) A) (span B)"
+ using inj_on_def matrix_vector_mul_injective_on_rowspace by blast
+ then have ind: "independent (( *v) A ` B)"
+ by (rule independent_inj_on_image [OF \<open>independent B\<close> matrix_vector_mul_linear])
+ then have "finite (( *v) A ` B) \<and> card (( *v) A ` B) \<le> dim (( *v) A ` B)"
+ by (rule independent_bound_general)
+ then show ?thesis
+ by (metis (no_types, lifting) B ind inj eq card_image image_subset_iff independent_card_le_dim inj_on_subset matrix_vector_mult_in_columnspace)
+ qed
+ then show ?thesis
+ by simp
+qed
+
+lemma rank_row:
+ fixes A :: "real^'n^'m"
+ shows "rank A = dim(rows A)"
+ unfolding rank_def
+ by (metis dim_rows_le_dim_columns columns_transpose dual_order.antisym rows_transpose)
+
+lemma rank_transpose:
+ fixes A :: "real^'n^'m"
+ shows "rank(transpose A) = rank A"
+ by (metis rank_def rank_row rows_transpose)
+
+lemma matrix_vector_mult_basis:
+ fixes A :: "real^'n^'m"
+ shows "A *v (axis k 1) = column k A"
+ by (simp add: cart_eq_inner_axis column_def matrix_mult_dot)
+
+lemma columns_image_basis:
+ fixes A :: "real^'n^'m"
+ shows "columns A = ( *v) A ` (range (\<lambda>i. axis i 1))"
+ by (force simp: columns_def matrix_vector_mult_basis [symmetric])
+
+lemma rank_dim_range:
+ fixes A :: "real^'n^'m"
+ shows "rank A = dim(range (\<lambda>x. A *v x))"
+ unfolding rank_def
+proof (rule span_eq_dim)
+ show "span (columns A) = span (range (( *v) A))"
+ apply (auto simp: columns_image_basis span_linear_image matrix_vector_mul_linear)
+ by (metis columns_image_basis matrix_vector_mul_linear matrix_vector_mult_in_columnspace span_linear_image)
+qed
+
+lemma rank_bound:
+ fixes A :: "real^'n^'m"
+ shows "rank A \<le> min CARD('m) (CARD('n))"
+ by (metis (mono_tags, hide_lams) min.bounded_iff DIM_cart DIM_real dim_subset_UNIV mult.right_neutral rank_def rank_transpose)
+
+lemma full_rank_injective:
+ fixes A :: "real^'n^'m"
+ shows "rank A = CARD('n) \<longleftrightarrow> inj (( *v) A)"
+ by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows rank_row dim_eq_full [symmetric])
+
+lemma full_rank_surjective:
+ fixes A :: "real^'n^'m"
+ shows "rank A = CARD('m) \<longleftrightarrow> surj (( *v) A)"
+ by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric]
+ matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose)
+
+lemma rank_I: "rank(mat 1::real^'n^'n) = CARD('n)"
+ by (simp add: full_rank_injective inj_on_def)
+
+lemma less_rank_noninjective:
+ fixes A :: "real^'n^'m"
+ shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj (( *v) A)"
+using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
+
+lemma matrix_nonfull_linear_equations_eq:
+ fixes A :: "real^'n^'m"
+ shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> ~(rank A = CARD('n))"
+ by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker)
+
+lemma rank_eq_0: "rank A = 0 \<longleftrightarrow> A = 0" and rank_0 [simp]: "rank 0 = 0"
+ by (auto simp: rank_dim_range matrix_eq)
+
+
+lemma rank_mul_le_right:
+ fixes A :: "real^'n^'m" and B :: "real^'p^'n"
+ shows "rank(A ** B) \<le> rank B"
+proof -
+ have "rank(A ** B) \<le> dim (( *v) A ` range (( *v) B))"
+ by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc)
+ also have "\<dots> \<le> rank B"
+ by (simp add: rank_dim_range matrix_vector_mul_linear dim_image_le)
+ finally show ?thesis .
+qed
+
+lemma rank_mul_le_left:
+ fixes A :: "real^'n^'m" and B :: "real^'p^'n"
+ shows "rank(A ** B) \<le> rank A"
+ by (metis matrix_transpose_mul rank_mul_le_right rank_transpose)
+
subsection\<open>Routine results connecting the types @{typ "real^1"} and @{typ real}\<close>
lemma vector_one_nth [simp]:
--- a/src/HOL/Analysis/Determinants.thy Sun Apr 15 17:22:58 2018 +0100
+++ b/src/HOL/Analysis/Determinants.thy Sun Apr 15 21:41:40 2018 +0100
@@ -464,15 +464,9 @@
done
qed
-lemma matrix_id_mat_1: "matrix id = mat 1"
- by (simp add: mat_def matrix_def axis_def)
-
lemma matrix_id [simp]: "det (matrix id) = 1"
by (simp add: matrix_id_mat_1)
-lemma matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r"
- by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
-
lemma det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
apply (subst det_diagonal)
apply (auto simp: matrix_def mat_def prod_constant)
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sun Apr 15 17:22:58 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sun Apr 15 21:41:40 2018 +0100
@@ -1337,6 +1337,31 @@
by (metis S Un_commute add.right_neutral lmeasurable_negligible_symdiff measure_Un2 neg negligible_Un_eq negligible_imp_measure0)
qed
+text\<open>Negligibility of image under non-injective linear map\<close>
+lemma negligible_Union_nat:
+ assumes "\<And>n::nat. negligible(S n)"
+ shows "negligible(\<Union>n. S n)"
+proof -
+ have "negligible (\<Union>m\<le>k. S m)" for k
+ using assms by blast
+ then have 0: "integral UNIV (indicat_real (\<Union>m\<le>k. S m)) = 0"
+ and 1: "(indicat_real (\<Union>m\<le>k. S m)) integrable_on UNIV" for k
+ by (auto simp: negligible has_integral_iff)
+ have 2: "\<And>k x. indicat_real (\<Union>m\<le>k. S m) x \<le> (indicat_real (\<Union>m\<le>Suc k. S m) x)"
+ by (simp add: indicator_def)
+ have 3: "\<And>x. (\<lambda>k. indicat_real (\<Union>m\<le>k. S m) x) \<longlonglongrightarrow> (indicat_real (\<Union>n. S n) x)"
+ by (force simp: indicator_def eventually_sequentially intro: Lim_eventually)
+ have 4: "bounded (range (\<lambda>k. integral UNIV (indicat_real (\<Union>m\<le>k. S m))))"
+ by (simp add: 0 image_def)
+ have *: "indicat_real (\<Union>n. S n) integrable_on UNIV \<and>
+ (\<lambda>k. integral UNIV (indicat_real (\<Union>m\<le>k. S m))) \<longlonglongrightarrow> (integral UNIV (indicat_real (\<Union>n. S n)))"
+ by (intro monotone_convergence_increasing 1 2 3 4)
+ then have "integral UNIV (indicat_real (\<Union>n. S n)) = (0::real)"
+ using LIMSEQ_unique by (auto simp: 0)
+ then show ?thesis
+ using * by (simp add: negligible_UNIV has_integral_iff)
+qed
+
subsection \<open>Negligibility of a Lipschitz image of a negligible set\<close>
text\<open>The bound will be eliminated by a sort of onion argument\<close>
--- a/src/HOL/Analysis/Inner_Product.thy Sun Apr 15 17:22:58 2018 +0100
+++ b/src/HOL/Analysis/Inner_Product.thy Sun Apr 15 21:41:40 2018 +0100
@@ -49,6 +49,9 @@
lemma inner_sum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
+lemma all_zero_iff [simp]: "(\<forall>u. inner x u = 0) \<longleftrightarrow> (x = 0)"
+ by auto (use inner_eq_zero_iff in blast)
+
text \<open>Transfer distributivity rules to right argument.\<close>
lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
@@ -420,32 +423,12 @@
lemma GDERIV_inverse:
"\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
\<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df"
- apply (erule GDERIV_DERIV_compose)
- apply (erule DERIV_inverse [folded numeral_2_eq_2])
- done
-
+ by (metis DERIV_inverse GDERIV_DERIV_compose numerals(2))
+
lemma GDERIV_norm:
assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
-proof -
- have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
- by (intro has_derivative_inner has_derivative_ident)
- have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
- by (simp add: fun_eq_iff inner_commute)
- have "0 < inner x x" using \<open>x \<noteq> 0\<close> by simp
- then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
- by (rule DERIV_real_sqrt)
- have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
- by (simp add: sgn_div_norm norm_eq_sqrt_inner)
- show ?thesis
- unfolding norm_eq_sqrt_inner
- apply (rule GDERIV_subst [OF _ 4])
- apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
- apply (subst gderiv_def)
- apply (rule has_derivative_subst [OF _ 2])
- apply (rule 1)
- apply (rule 3)
- done
-qed
+ unfolding gderiv_def norm_eq_sqrt_inner
+ by (rule derivative_eq_intros | force simp add: inner_commute sgn_div_norm norm_eq_sqrt_inner assms)+
lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Sun Apr 15 17:22:58 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Sun Apr 15 21:41:40 2018 +0100
@@ -1004,6 +1004,83 @@
assumes "bounded S" "S \<in> sets lebesgue" shows "S \<in> lmeasurable"
by (metis assms bounded_Un emeasure_bounded_finite emeasure_completion fmeasurableI main_part_null_part_Un)
+
+subsection\<open>Translation preserves Lebesgue measure\<close>
+
+lemma sigma_sets_image:
+ assumes S: "S \<in> sigma_sets \<Omega> M" and "M \<subseteq> Pow \<Omega>" "f ` \<Omega> = \<Omega>" "inj_on f \<Omega>"
+ and M: "\<And>y. y \<in> M \<Longrightarrow> f ` y \<in> M"
+ shows "(f ` S) \<in> sigma_sets \<Omega> M"
+ using S
+proof (induct S rule: sigma_sets.induct)
+ case (Basic a) then show ?case
+ by (simp add: M)
+next
+ case Empty then show ?case
+ by (simp add: sigma_sets.Empty)
+next
+ case (Compl a)
+ then have "\<Omega> - a \<subseteq> \<Omega>" "a \<subseteq> \<Omega>"
+ by (auto simp: sigma_sets_into_sp [OF \<open>M \<subseteq> Pow \<Omega>\<close>])
+ then show ?case
+ by (auto simp: inj_on_image_set_diff [OF \<open>inj_on f \<Omega>\<close>] assms intro: Compl sigma_sets.Compl)
+next
+ case (Union a) then show ?case
+ by (metis image_UN sigma_sets.simps)
+qed
+
+lemma null_sets_translation:
+ assumes "N \<in> null_sets lborel" shows "{x. x - a \<in> N} \<in> null_sets lborel"
+proof -
+ have [simp]: "(\<lambda>x. x + a) ` N = {x. x - a \<in> N}"
+ by force
+ show ?thesis
+ using assms emeasure_lebesgue_affine [of 1 a N] by (auto simp: null_sets_def)
+qed
+
+lemma lebesgue_sets_translation:
+ fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
+ assumes S: "S \<in> sets lebesgue"
+ shows "((\<lambda>x. a + x) ` S) \<in> sets lebesgue"
+proof -
+ have im_eq: "(+) a ` A = {x. x - a \<in> A}" for A
+ by force
+ have "((\<lambda>x. a + x) ` S) = ((\<lambda>x. -a + x) -` S) \<inter> (space lebesgue)"
+ using image_iff by fastforce
+ also have "\<dots> \<in> sets lebesgue"
+ proof (rule measurable_sets [OF measurableI assms])
+ fix A :: "'b set"
+ assume A: "A \<in> sets lebesgue"
+ have vim_eq: "(\<lambda>x. x - a) -` A = (+) a ` A" for A
+ by force
+ have "\<exists>s n N'. (+) a ` (S \<union> N) = s \<union> n \<and> s \<in> sets borel \<and> N' \<in> null_sets lborel \<and> n \<subseteq> N'"
+ if "S \<in> sets borel" and "N' \<in> null_sets lborel" and "N \<subseteq> N'" for S N N'
+ proof (intro exI conjI)
+ show "(+) a ` (S \<union> N) = (\<lambda>x. a + x) ` S \<union> (\<lambda>x. a + x) ` N"
+ by auto
+ show "(\<lambda>x. a + x) ` N' \<in> null_sets lborel"
+ using that by (auto simp: null_sets_translation im_eq)
+ qed (use that im_eq in auto)
+ with A have "(\<lambda>x. x - a) -` A \<in> sets lebesgue"
+ by (force simp: vim_eq completion_def intro!: sigma_sets_image)
+ then show "(+) (- a) -` A \<inter> space lebesgue \<in> sets lebesgue"
+ by (auto simp: vimage_def im_eq)
+ qed auto
+ finally show ?thesis .
+qed
+
+lemma measurable_translation:
+ "S \<in> lmeasurable \<Longrightarrow> ((\<lambda>x. a + x) ` S) \<in> lmeasurable"
+ unfolding fmeasurable_def
+apply (auto intro: lebesgue_sets_translation)
+ using emeasure_lebesgue_affine [of 1 a S]
+ by (auto simp: add.commute [of _ a])
+
+lemma measure_translation:
+ "measure lebesgue ((\<lambda>x. a + x) ` S) = measure lebesgue S"
+ using measure_lebesgue_affine [of 1 a S]
+ by (auto simp: add.commute [of _ a])
+
subsection \<open>A nice lemma for negligibility proofs\<close>
lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top"
--- a/src/HOL/Analysis/Starlike.thy Sun Apr 15 17:22:58 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy Sun Apr 15 21:41:40 2018 +0100
@@ -8302,5 +8302,125 @@
using that by metis
qed
+
+subsection{*Orthogonal complement*}
+
+definition orthogonal_comp ("_\<^sup>\<bottom>" [80] 80)
+ where "orthogonal_comp W \<equiv> {x. \<forall>y \<in> W. orthogonal y x}"
+
+lemma subspace_orthogonal_comp: "subspace (W\<^sup>\<bottom>)"
+ unfolding subspace_def orthogonal_comp_def orthogonal_def
+ by (auto simp: inner_right_distrib)
+
+lemma orthogonal_comp_anti_mono:
+ assumes "A \<subseteq> B"
+ shows "B\<^sup>\<bottom> \<subseteq> A\<^sup>\<bottom>"
+proof
+ fix x assume x: "x \<in> B\<^sup>\<bottom>"
+ show "x \<in> orthogonal_comp A" using x unfolding orthogonal_comp_def
+ by (simp add: orthogonal_def, metis assms in_mono)
+qed
+
+lemma orthogonal_comp_null [simp]: "{0}\<^sup>\<bottom> = UNIV"
+ by (auto simp: orthogonal_comp_def orthogonal_def)
+
+lemma orthogonal_comp_UNIV [simp]: "UNIV\<^sup>\<bottom> = {0}"
+ unfolding orthogonal_comp_def orthogonal_def
+ by auto (use inner_eq_zero_iff in blast)
+
+lemma orthogonal_comp_subset: "U \<subseteq> U\<^sup>\<bottom>\<^sup>\<bottom>"
+ by (auto simp: orthogonal_comp_def orthogonal_def inner_commute)
+
+lemma subspace_sum_minimal:
+ assumes "S \<subseteq> U" "T \<subseteq> U" "subspace U"
+ shows "S + T \<subseteq> U"
+proof
+ fix x
+ assume "x \<in> S + T"
+ then obtain xs xt where "xs \<in> S" "xt \<in> T" "x = xs+xt"
+ by (meson set_plus_elim)
+ then show "x \<in> U"
+ by (meson assms subsetCE subspace_add)
+qed
+
+lemma subspace_sum_orthogonal_comp:
+ fixes U :: "'a :: euclidean_space set"
+ assumes "subspace U"
+ shows "U + U\<^sup>\<bottom> = UNIV"
+proof -
+ obtain B where "B \<subseteq> U"
+ and ortho: "pairwise orthogonal B" "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
+ and "independent B" "card B = dim U" "span B = U"
+ using orthonormal_basis_subspace [OF assms] by metis
+ then have "finite B"
+ by (simp add: indep_card_eq_dim_span)
+ have *: "\<forall>x\<in>B. \<forall>y\<in>B. x \<bullet> y = (if x=y then 1 else 0)"
+ using ortho norm_eq_1 by (auto simp: orthogonal_def pairwise_def)
+ { fix v
+ let ?u = "\<Sum>b\<in>B. (v \<bullet> b) *\<^sub>R b"
+ have "v = ?u + (v - ?u)"
+ by simp
+ moreover have "?u \<in> U"
+ by (metis (no_types, lifting) \<open>span B = U\<close> assms real_vector_class.subspace_sum span_clauses(1) span_mul)
+ moreover have "(v - ?u) \<in> U\<^sup>\<bottom>"
+ proof (clarsimp simp: orthogonal_comp_def orthogonal_def)
+ fix y
+ assume "y \<in> U"
+ with \<open>span B = U\<close> span_finite [OF \<open>finite B\<close>]
+ obtain u where u: "y = (\<Sum>b\<in>B. u b *\<^sub>R b)"
+ by auto
+ have "b \<bullet> (v - ?u) = 0" if "b \<in> B" for b
+ using that \<open>finite B\<close>
+ by (simp add: * algebra_simps inner_sum_right if_distrib [of "( *)v" for v] inner_commute cong: if_cong)
+ then show "y \<bullet> (v - ?u) = 0"
+ by (simp add: u inner_sum_left)
+ qed
+ ultimately have "v \<in> U + U\<^sup>\<bottom>"
+ using set_plus_intro by fastforce
+ } then show ?thesis
+ by auto
+qed
+
+lemma orthogonal_Int_0:
+ assumes "subspace U"
+ shows "U \<inter> U\<^sup>\<bottom> = {0}"
+ using orthogonal_comp_def orthogonal_self
+ by (force simp: assms subspace_0 subspace_orthogonal_comp)
+
+lemma orthogonal_comp_self:
+ fixes U :: "'a :: euclidean_space set"
+ assumes "subspace U"
+ shows "U\<^sup>\<bottom>\<^sup>\<bottom> = U"
+proof
+ have ssU': "subspace (U\<^sup>\<bottom>)"
+ by (simp add: subspace_orthogonal_comp)
+ have "u \<in> U" if "u \<in> U\<^sup>\<bottom>\<^sup>\<bottom>" for u
+ proof -
+ obtain v w where "u = v+w" "v \<in> U" "w \<in> U\<^sup>\<bottom>"
+ using subspace_sum_orthogonal_comp [OF assms] set_plus_elim by blast
+ then have "u-v \<in> U\<^sup>\<bottom>"
+ by simp
+ moreover have "v \<in> U\<^sup>\<bottom>\<^sup>\<bottom>"
+ using \<open>v \<in> U\<close> orthogonal_comp_subset by blast
+ then have "u-v \<in> U\<^sup>\<bottom>\<^sup>\<bottom>"
+ by (simp add: subspace_diff subspace_orthogonal_comp that)
+ ultimately have "u-v = 0"
+ using orthogonal_Int_0 ssU' by blast
+ with \<open>v \<in> U\<close> show ?thesis
+ by auto
+ qed
+ then show "U\<^sup>\<bottom>\<^sup>\<bottom> \<subseteq> U"
+ by auto
+qed (use orthogonal_comp_subset in auto)
+
+lemma ker_orthogonal_comp_adjoint:
+ fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
+ assumes "linear f"
+ shows "f -` {0} = (range (adjoint f))\<^sup>\<bottom>"
+ apply (auto simp: orthogonal_comp_def orthogonal_def)
+ apply (simp add: adjoint_works assms(1) inner_commute)
+ by (metis adjoint_works all_zero_iff assms(1) inner_commute)
+
+
end
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Sun Apr 15 17:22:58 2018 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Sun Apr 15 21:41:40 2018 +0100
@@ -1375,7 +1375,8 @@
apply (simp add: \<open>finite B\<close>)
using \<open>polynomial_function g\<close> by auto
show "(\<lambda>x. \<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i) ` S \<subseteq> T"
- using \<open>B \<subseteq> T\<close> by (blast intro: subspace_sum subspace_mul \<open>subspace T\<close>)
+ using \<open>B \<subseteq> T\<close>
+ by (blast intro: real_vector_class.subspace_sum subspace_mul \<open>subspace T\<close>)
show "norm (f x - (\<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i)) < e" if "x \<in> S" for x
proof -
have orth': "pairwise (\<lambda>i j. orthogonal ((f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i)