# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1523824900 -3600
# Node ID b65c4a6a015e902288085ec24c71a73e238ae2c9
# Parent  7811748de2719d2b33b668ba5cc187d252bbd73b
quite a few more results about negligibility, etc., and a bit of tidying up

diff -r 7811748de271 -r b65c4a6a015e src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- 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]:
diff -r 7811748de271 -r b65c4a6a015e src/HOL/Analysis/Determinants.thy
--- 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)
diff -r 7811748de271 -r b65c4a6a015e src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- 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>
diff -r 7811748de271 -r b65c4a6a015e src/HOL/Analysis/Inner_Product.thy
--- 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]
 
diff -r 7811748de271 -r b65c4a6a015e src/HOL/Analysis/Lebesgue_Measure.thy
--- 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"
diff -r 7811748de271 -r b65c4a6a015e src/HOL/Analysis/Starlike.thy
--- 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
   
diff -r 7811748de271 -r b65c4a6a015e src/HOL/Analysis/Weierstrass_Theorems.thy
--- 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)