quite a few more results about negligibility, etc., and a bit of tidying up
authorpaulson <lp15@cam.ac.uk>
Sun Apr 15 21:41:40 2018 +0100 (16 months ago)
changeset 67986b65c4a6a015e
parent 67985 7811748de271
child 67987 9044e1f1d324
quite a few more results about negligibility, etc., and a bit of tidying up
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Determinants.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Inner_Product.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Weierstrass_Theorems.thy
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Apr 15 17:22:58 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Apr 15 21:41:40 2018 +0100
     1.3 @@ -540,7 +540,6 @@
     1.4      mult_1_left mult_zero_left if_True UNIV_I)
     1.5    done
     1.6  
     1.7 -
     1.8  lemma matrix_mul_rid [simp]:
     1.9    fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
    1.10    shows "A ** mat 1 = A"
    1.11 @@ -672,6 +671,12 @@
    1.12  definition matrix :: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
    1.13    where "matrix f = (\<chi> i j. (f(axis j 1))$i)"
    1.14  
    1.15 +lemma matrix_id_mat_1: "matrix id = mat 1"
    1.16 +  by (simp add: mat_def matrix_def axis_def)
    1.17 +
    1.18 +lemma matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r"
    1.19 +  by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
    1.20 +
    1.21  lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"
    1.22    by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
    1.23        field_simps sum_distrib_left sum.distrib)
    1.24 @@ -896,22 +901,23 @@
    1.25    by (metis matrix_transpose_mul transpose_mat transpose_transpose)
    1.26  
    1.27  lemma matrix_left_invertible_injective:
    1.28 -  "(\<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)"
    1.29 -proof -
    1.30 -  { fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y"
    1.31 -    from xy have "B*v (A *v x) = B *v (A*v y)" by simp
    1.32 -    hence "x = y"
    1.33 -      unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid . }
    1.34 -  moreover
    1.35 -  { assume A: "\<forall>x y. A *v x = A *v y \<longrightarrow> x = y"
    1.36 -    hence i: "inj (( *v) A)" unfolding inj_on_def by auto
    1.37 -    from linear_injective_left_inverse[OF matrix_vector_mul_linear i]
    1.38 -    obtain g where g: "linear g" "g \<circ> ( *v) A = id" by blast
    1.39 -    have "matrix g ** A = mat 1"
    1.40 -      unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
    1.41 -      using g(2) by (simp add: fun_eq_iff)
    1.42 -    then have "\<exists>B. (B::real ^'m^'n) ** A = mat 1" by blast }
    1.43 -  ultimately show ?thesis by blast
    1.44 +  fixes A :: "real^'n^'m"
    1.45 +  shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj (( *v) A)"
    1.46 +proof safe
    1.47 +  fix B
    1.48 +  assume B: "B ** A = mat 1"
    1.49 +  show "inj (( *v) A)"
    1.50 +    unfolding inj_on_def
    1.51 +      by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid)
    1.52 +next
    1.53 +  assume "inj (( *v) A)"
    1.54 +  with linear_injective_left_inverse[OF matrix_vector_mul_linear]
    1.55 +  obtain g where "linear g" and g: "g \<circ> ( *v) A = id"
    1.56 +    by blast
    1.57 +  have "matrix g ** A = mat 1"
    1.58 +    by (metis \<open>linear g\<close> g matrix_compose matrix_id_mat_1 matrix_of_matrix_vector_mul matrix_vector_mul_linear)
    1.59 +  then show "\<exists>B. B ** A = mat 1"
    1.60 +    by metis
    1.61  qed
    1.62  
    1.63  lemma matrix_left_invertible_ker:
    1.64 @@ -1443,15 +1449,14 @@
    1.65  
    1.66  lemma jacobian_works:
    1.67    "(f::(real^'a) \<Rightarrow> (real^'b)) differentiable net \<longleftrightarrow>
    1.68 -    (f has_derivative (\<lambda>h. (jacobian f net) *v h)) net"
    1.69 -  apply rule
    1.70 -  unfolding jacobian_def
    1.71 -  apply (simp only: matrix_works[OF linear_frechet_derivative]) defer
    1.72 -  apply (rule differentiableI)
    1.73 -  apply assumption
    1.74 -  unfolding frechet_derivative_works
    1.75 -  apply assumption
    1.76 -  done
    1.77 +    (f has_derivative (\<lambda>h. (jacobian f net) *v h)) net" (is "?lhs = ?rhs")
    1.78 +proof
    1.79 +  assume ?lhs then show ?rhs
    1.80 +    by (simp add: frechet_derivative_works has_derivative_linear jacobian_def)
    1.81 +next
    1.82 +  assume ?rhs then show ?lhs
    1.83 +    by (rule differentiableI)
    1.84 +qed
    1.85  
    1.86  
    1.87  subsection \<open>Component of the differential must be zero if it exists at a local
    1.88 @@ -1571,6 +1576,153 @@
    1.89  lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>"
    1.90    by (auto simp add: norm_real dist_norm)
    1.91  
    1.92 +subsection\<open> Rank of a matrix\<close>
    1.93 +
    1.94 +text\<open>Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\<close>
    1.95 +
    1.96 +lemma matrix_vector_mult_in_columnspace:
    1.97 +  fixes A :: "real^'n^'m"
    1.98 +  shows "(A *v x) \<in> span(columns A)"
    1.99 +  apply (simp add: matrix_vector_column columns_def transpose_def column_def)
   1.100 +  apply (intro span_sum span_mul)
   1.101 +  apply (force intro: span_superset)
   1.102 +  done
   1.103 +
   1.104 +lemma orthogonal_nullspace_rowspace:
   1.105 +  fixes A :: "real^'n^'m"
   1.106 +  assumes 0: "A *v x = 0" and y: "y \<in> span(rows A)"
   1.107 +  shows "orthogonal x y"
   1.108 +proof (rule span_induct [OF y])
   1.109 +  show "subspace {a. orthogonal x a}"
   1.110 +    by (simp add: subspace_orthogonal_to_vector)
   1.111 +next
   1.112 +  fix v
   1.113 +  assume "v \<in> rows A"
   1.114 +  then obtain i where "v = row i A"
   1.115 +    by (auto simp: rows_def)
   1.116 +  with 0 show "orthogonal x v"
   1.117 +    unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def
   1.118 +    by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index)
   1.119 +qed
   1.120 +
   1.121 +lemma nullspace_inter_rowspace:
   1.122 +  fixes A :: "real^'n^'m"
   1.123 +  shows "A *v x = 0 \<and> x \<in> span(rows A) \<longleftrightarrow> x = 0"
   1.124 +  using orthogonal_nullspace_rowspace orthogonal_self by auto
   1.125 +
   1.126 +lemma matrix_vector_mul_injective_on_rowspace:
   1.127 +  fixes A :: "real^'n^'m"
   1.128 +  shows "\<lbrakk>A *v x = A *v y; x \<in> span(rows A); y \<in> span(rows A)\<rbrakk> \<Longrightarrow> x = y"
   1.129 +  using nullspace_inter_rowspace [of A "x-y"]
   1.130 +  by (metis eq_iff_diff_eq_0 matrix_vector_mult_diff_distrib span_diff)
   1.131 +
   1.132 +definition rank :: "real^'n^'m=>nat"
   1.133 +  where "rank A \<equiv> dim(columns A)"
   1.134 +
   1.135 +lemma dim_rows_le_dim_columns:
   1.136 +  fixes A :: "real^'n^'m"
   1.137 +  shows "dim(rows A) \<le> dim(columns A)"
   1.138 +proof -
   1.139 +  have "dim (span (rows A)) \<le> dim (span (columns A))"
   1.140 +  proof -
   1.141 +    obtain B where "independent B" "span(rows A) \<subseteq> span B"
   1.142 +              and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))"
   1.143 +      using basis_exists [of "span(rows A)"] by blast
   1.144 +    with span_subspace have eq: "span B = span(rows A)"
   1.145 +      by auto
   1.146 +    then have inj: "inj_on (( *v) A) (span B)"
   1.147 +      using inj_on_def matrix_vector_mul_injective_on_rowspace by blast
   1.148 +    then have ind: "independent (( *v) A ` B)"
   1.149 +      by (rule independent_inj_on_image [OF \<open>independent B\<close> matrix_vector_mul_linear])
   1.150 +    then have "finite (( *v) A ` B) \<and> card (( *v) A ` B) \<le> dim (( *v) A ` B)"
   1.151 +      by (rule independent_bound_general)
   1.152 +    then show ?thesis
   1.153 +      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)
   1.154 +  qed
   1.155 +  then show ?thesis
   1.156 +    by simp
   1.157 +qed
   1.158 +
   1.159 +lemma rank_row:
   1.160 +  fixes A :: "real^'n^'m"
   1.161 +  shows "rank A = dim(rows A)"
   1.162 +  unfolding rank_def
   1.163 +  by (metis dim_rows_le_dim_columns columns_transpose dual_order.antisym rows_transpose)
   1.164 +
   1.165 +lemma rank_transpose:
   1.166 +  fixes A :: "real^'n^'m"
   1.167 +  shows "rank(transpose A) = rank A"
   1.168 +  by (metis rank_def rank_row rows_transpose)
   1.169 +
   1.170 +lemma matrix_vector_mult_basis:
   1.171 +  fixes A :: "real^'n^'m"
   1.172 +  shows "A *v (axis k 1) = column k A"
   1.173 +  by (simp add: cart_eq_inner_axis column_def matrix_mult_dot)
   1.174 +
   1.175 +lemma columns_image_basis:
   1.176 +  fixes A :: "real^'n^'m"
   1.177 +  shows "columns A = ( *v) A ` (range (\<lambda>i. axis i 1))"
   1.178 +  by (force simp: columns_def matrix_vector_mult_basis [symmetric])
   1.179 +
   1.180 +lemma rank_dim_range:
   1.181 +  fixes A :: "real^'n^'m"
   1.182 +  shows "rank A = dim(range (\<lambda>x. A *v x))"
   1.183 +  unfolding rank_def
   1.184 +proof (rule span_eq_dim)
   1.185 +  show "span (columns A) = span (range (( *v) A))"
   1.186 +    apply (auto simp: columns_image_basis span_linear_image matrix_vector_mul_linear)
   1.187 +    by (metis columns_image_basis matrix_vector_mul_linear matrix_vector_mult_in_columnspace span_linear_image)
   1.188 +qed
   1.189 +
   1.190 +lemma rank_bound:
   1.191 +  fixes A :: "real^'n^'m"
   1.192 +  shows "rank A \<le> min CARD('m) (CARD('n))"
   1.193 +  by (metis (mono_tags, hide_lams) min.bounded_iff DIM_cart DIM_real dim_subset_UNIV mult.right_neutral rank_def rank_transpose)
   1.194 +
   1.195 +lemma full_rank_injective:
   1.196 +  fixes A :: "real^'n^'m"
   1.197 +  shows "rank A = CARD('n) \<longleftrightarrow> inj (( *v) A)"
   1.198 +  by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows rank_row dim_eq_full [symmetric])
   1.199 +
   1.200 +lemma full_rank_surjective:
   1.201 +  fixes A :: "real^'n^'m"
   1.202 +  shows "rank A = CARD('m) \<longleftrightarrow> surj (( *v) A)"
   1.203 +  by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric]
   1.204 +                matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose)
   1.205 +
   1.206 +lemma rank_I: "rank(mat 1::real^'n^'n) = CARD('n)"
   1.207 +  by (simp add: full_rank_injective inj_on_def)
   1.208 +
   1.209 +lemma less_rank_noninjective:
   1.210 +  fixes A :: "real^'n^'m"
   1.211 +  shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj (( *v) A)"
   1.212 +using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
   1.213 +
   1.214 +lemma matrix_nonfull_linear_equations_eq:
   1.215 +  fixes A :: "real^'n^'m"
   1.216 +  shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> ~(rank A = CARD('n))"
   1.217 +  by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker)
   1.218 +
   1.219 +lemma rank_eq_0: "rank A = 0 \<longleftrightarrow> A = 0" and rank_0 [simp]: "rank 0 = 0"
   1.220 +  by (auto simp: rank_dim_range matrix_eq)
   1.221 +
   1.222 +
   1.223 +lemma rank_mul_le_right:
   1.224 +  fixes A :: "real^'n^'m" and B :: "real^'p^'n"
   1.225 +  shows "rank(A ** B) \<le> rank B"
   1.226 +proof -
   1.227 +  have "rank(A ** B) \<le> dim (( *v) A ` range (( *v) B))"
   1.228 +    by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc)
   1.229 +  also have "\<dots> \<le> rank B"
   1.230 +    by (simp add: rank_dim_range matrix_vector_mul_linear dim_image_le)
   1.231 +  finally show ?thesis .
   1.232 +qed
   1.233 +
   1.234 +lemma rank_mul_le_left:
   1.235 +  fixes A :: "real^'n^'m" and B :: "real^'p^'n"
   1.236 +  shows "rank(A ** B) \<le> rank A"
   1.237 +  by (metis matrix_transpose_mul rank_mul_le_right rank_transpose)
   1.238 +
   1.239  subsection\<open>Routine results connecting the types @{typ "real^1"} and @{typ real}\<close>
   1.240  
   1.241  lemma vector_one_nth [simp]:
     2.1 --- a/src/HOL/Analysis/Determinants.thy	Sun Apr 15 17:22:58 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Determinants.thy	Sun Apr 15 21:41:40 2018 +0100
     2.3 @@ -464,15 +464,9 @@
     2.4      done
     2.5  qed
     2.6  
     2.7 -lemma matrix_id_mat_1: "matrix id = mat 1"
     2.8 -  by (simp add: mat_def matrix_def axis_def)
     2.9 -
    2.10  lemma matrix_id [simp]: "det (matrix id) = 1"
    2.11    by (simp add: matrix_id_mat_1)
    2.12  
    2.13 -lemma matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r"
    2.14 -  by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
    2.15 -
    2.16  lemma det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
    2.17    apply (subst det_diagonal)
    2.18     apply (auto simp: matrix_def mat_def prod_constant)
     3.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Apr 15 17:22:58 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Apr 15 21:41:40 2018 +0100
     3.3 @@ -1337,6 +1337,31 @@
     3.4      by (metis S Un_commute add.right_neutral lmeasurable_negligible_symdiff measure_Un2 neg negligible_Un_eq negligible_imp_measure0)
     3.5  qed
     3.6  
     3.7 +text\<open>Negligibility of image under non-injective linear map\<close>
     3.8 +lemma negligible_Union_nat:
     3.9 +  assumes "\<And>n::nat. negligible(S n)"
    3.10 +  shows "negligible(\<Union>n. S n)"
    3.11 +proof -
    3.12 +  have "negligible (\<Union>m\<le>k. S m)" for k
    3.13 +    using assms by blast
    3.14 +  then have 0:  "integral UNIV (indicat_real (\<Union>m\<le>k. S m)) = 0"
    3.15 +    and 1: "(indicat_real (\<Union>m\<le>k. S m)) integrable_on UNIV" for k
    3.16 +    by (auto simp: negligible has_integral_iff)
    3.17 +  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)"
    3.18 +    by (simp add: indicator_def)
    3.19 +  have 3: "\<And>x. (\<lambda>k. indicat_real (\<Union>m\<le>k. S m) x) \<longlonglongrightarrow> (indicat_real (\<Union>n. S n) x)"
    3.20 +    by (force simp: indicator_def eventually_sequentially intro: Lim_eventually)
    3.21 +  have 4: "bounded (range (\<lambda>k. integral UNIV (indicat_real (\<Union>m\<le>k. S m))))"
    3.22 +    by (simp add: 0 image_def)
    3.23 +  have *: "indicat_real (\<Union>n. S n) integrable_on UNIV \<and>
    3.24 +        (\<lambda>k. integral UNIV (indicat_real (\<Union>m\<le>k. S m))) \<longlonglongrightarrow> (integral UNIV (indicat_real (\<Union>n. S n)))"
    3.25 +    by (intro monotone_convergence_increasing 1 2 3 4)
    3.26 +  then have "integral UNIV (indicat_real (\<Union>n. S n)) = (0::real)"
    3.27 +    using LIMSEQ_unique by (auto simp: 0)
    3.28 +  then show ?thesis
    3.29 +    using * by (simp add: negligible_UNIV has_integral_iff)
    3.30 +qed
    3.31 +
    3.32  subsection \<open>Negligibility of a Lipschitz image of a negligible set\<close>
    3.33  
    3.34  text\<open>The bound will be eliminated by a sort of onion argument\<close>
     4.1 --- a/src/HOL/Analysis/Inner_Product.thy	Sun Apr 15 17:22:58 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Sun Apr 15 21:41:40 2018 +0100
     4.3 @@ -49,6 +49,9 @@
     4.4  lemma inner_sum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
     4.5    by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
     4.6  
     4.7 +lemma all_zero_iff [simp]: "(\<forall>u. inner x u = 0) \<longleftrightarrow> (x = 0)"
     4.8 +  by auto (use inner_eq_zero_iff in blast)
     4.9 +
    4.10  text \<open>Transfer distributivity rules to right argument.\<close>
    4.11  
    4.12  lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
    4.13 @@ -420,32 +423,12 @@
    4.14  lemma GDERIV_inverse:
    4.15      "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
    4.16       \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df"
    4.17 -  apply (erule GDERIV_DERIV_compose)
    4.18 -  apply (erule DERIV_inverse [folded numeral_2_eq_2])
    4.19 -  done
    4.20 -
    4.21 +  by (metis DERIV_inverse GDERIV_DERIV_compose numerals(2))
    4.22 +  
    4.23  lemma GDERIV_norm:
    4.24    assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
    4.25 -proof -
    4.26 -  have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
    4.27 -    by (intro has_derivative_inner has_derivative_ident)
    4.28 -  have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
    4.29 -    by (simp add: fun_eq_iff inner_commute)
    4.30 -  have "0 < inner x x" using \<open>x \<noteq> 0\<close> by simp
    4.31 -  then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
    4.32 -    by (rule DERIV_real_sqrt)
    4.33 -  have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
    4.34 -    by (simp add: sgn_div_norm norm_eq_sqrt_inner)
    4.35 -  show ?thesis
    4.36 -    unfolding norm_eq_sqrt_inner
    4.37 -    apply (rule GDERIV_subst [OF _ 4])
    4.38 -    apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
    4.39 -    apply (subst gderiv_def)
    4.40 -    apply (rule has_derivative_subst [OF _ 2])
    4.41 -    apply (rule 1)
    4.42 -    apply (rule 3)
    4.43 -    done
    4.44 -qed
    4.45 +    unfolding gderiv_def norm_eq_sqrt_inner
    4.46 +    by (rule derivative_eq_intros | force simp add: inner_commute sgn_div_norm norm_eq_sqrt_inner assms)+
    4.47  
    4.48  lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
    4.49  
     5.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Apr 15 17:22:58 2018 +0100
     5.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Apr 15 21:41:40 2018 +0100
     5.3 @@ -1004,6 +1004,83 @@
     5.4    assumes "bounded S" "S \<in> sets lebesgue" shows "S \<in> lmeasurable"
     5.5    by (metis assms bounded_Un emeasure_bounded_finite emeasure_completion fmeasurableI main_part_null_part_Un)
     5.6  
     5.7 +
     5.8 +subsection\<open>Translation preserves Lebesgue measure\<close>
     5.9 +
    5.10 +lemma sigma_sets_image:
    5.11 +  assumes S: "S \<in> sigma_sets \<Omega> M" and "M \<subseteq> Pow \<Omega>" "f ` \<Omega> = \<Omega>" "inj_on f \<Omega>"
    5.12 +    and M: "\<And>y. y \<in> M \<Longrightarrow> f ` y \<in> M"
    5.13 +  shows "(f ` S) \<in> sigma_sets \<Omega> M"
    5.14 +  using S
    5.15 +proof (induct S rule: sigma_sets.induct)
    5.16 +  case (Basic a) then show ?case
    5.17 +    by (simp add: M)
    5.18 +next
    5.19 +  case Empty then show ?case
    5.20 +    by (simp add: sigma_sets.Empty)
    5.21 +next
    5.22 +  case (Compl a)
    5.23 +  then have "\<Omega> - a \<subseteq> \<Omega>" "a \<subseteq> \<Omega>"
    5.24 +    by (auto simp: sigma_sets_into_sp [OF \<open>M \<subseteq> Pow \<Omega>\<close>])
    5.25 +  then show ?case
    5.26 +    by (auto simp: inj_on_image_set_diff [OF \<open>inj_on f \<Omega>\<close>] assms intro: Compl sigma_sets.Compl)
    5.27 +next
    5.28 +  case (Union a) then show ?case
    5.29 +    by (metis image_UN sigma_sets.simps)
    5.30 +qed
    5.31 +
    5.32 +lemma null_sets_translation:
    5.33 +  assumes "N \<in> null_sets lborel" shows "{x. x - a \<in> N} \<in> null_sets lborel"
    5.34 +proof -
    5.35 +  have [simp]: "(\<lambda>x. x + a) ` N = {x. x - a \<in> N}"
    5.36 +    by force
    5.37 +  show ?thesis
    5.38 +    using assms emeasure_lebesgue_affine [of 1 a N] by (auto simp: null_sets_def)
    5.39 +qed
    5.40 +
    5.41 +lemma lebesgue_sets_translation:
    5.42 +  fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
    5.43 +  assumes S: "S \<in> sets lebesgue"
    5.44 +  shows "((\<lambda>x. a + x) ` S) \<in> sets lebesgue"
    5.45 +proof -
    5.46 +  have im_eq: "(+) a ` A = {x. x - a \<in> A}" for A
    5.47 +    by force
    5.48 +  have "((\<lambda>x. a + x) ` S) = ((\<lambda>x. -a + x) -` S) \<inter> (space lebesgue)"
    5.49 +    using image_iff by fastforce
    5.50 +  also have "\<dots> \<in> sets lebesgue"
    5.51 +  proof (rule measurable_sets [OF measurableI assms])
    5.52 +    fix A :: "'b set"
    5.53 +    assume A: "A \<in> sets lebesgue"
    5.54 +    have vim_eq: "(\<lambda>x. x - a) -` A = (+) a ` A" for A
    5.55 +      by force
    5.56 +    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'"
    5.57 +      if "S \<in> sets borel" and "N' \<in> null_sets lborel" and "N \<subseteq> N'" for S N N'
    5.58 +    proof (intro exI conjI)
    5.59 +      show "(+) a ` (S \<union> N) = (\<lambda>x. a + x) ` S \<union> (\<lambda>x. a + x) ` N"
    5.60 +        by auto
    5.61 +      show "(\<lambda>x. a + x) ` N' \<in> null_sets lborel"
    5.62 +        using that by (auto simp: null_sets_translation im_eq)
    5.63 +    qed (use that im_eq in auto)
    5.64 +    with A have "(\<lambda>x. x - a) -` A \<in> sets lebesgue"
    5.65 +      by (force simp: vim_eq completion_def intro!: sigma_sets_image)
    5.66 +    then show "(+) (- a) -` A \<inter> space lebesgue \<in> sets lebesgue"
    5.67 +      by (auto simp: vimage_def im_eq)
    5.68 +  qed auto
    5.69 +  finally show ?thesis .
    5.70 +qed
    5.71 +
    5.72 +lemma measurable_translation:
    5.73 +   "S \<in> lmeasurable \<Longrightarrow> ((\<lambda>x. a + x) ` S) \<in> lmeasurable"
    5.74 +  unfolding fmeasurable_def
    5.75 +apply (auto intro: lebesgue_sets_translation)
    5.76 +  using  emeasure_lebesgue_affine [of 1 a S]
    5.77 +  by (auto simp: add.commute [of _ a])
    5.78 +
    5.79 +lemma measure_translation:
    5.80 +   "measure lebesgue ((\<lambda>x. a + x) ` S) = measure lebesgue S"
    5.81 +  using measure_lebesgue_affine [of 1 a S]
    5.82 +  by (auto simp: add.commute [of _ a])
    5.83 +
    5.84  subsection \<open>A nice lemma for negligibility proofs\<close>
    5.85  
    5.86  lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top"
     6.1 --- a/src/HOL/Analysis/Starlike.thy	Sun Apr 15 17:22:58 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Starlike.thy	Sun Apr 15 21:41:40 2018 +0100
     6.3 @@ -8302,5 +8302,125 @@
     6.4      using that by metis
     6.5  qed
     6.6  
     6.7 +
     6.8 +subsection{*Orthogonal complement*}
     6.9 +
    6.10 +definition orthogonal_comp ("_\<^sup>\<bottom>" [80] 80)
    6.11 +  where "orthogonal_comp W \<equiv> {x. \<forall>y \<in> W. orthogonal y x}"
    6.12 +
    6.13 +lemma subspace_orthogonal_comp: "subspace (W\<^sup>\<bottom>)"
    6.14 +  unfolding subspace_def orthogonal_comp_def orthogonal_def
    6.15 +  by (auto simp: inner_right_distrib)
    6.16 +
    6.17 +lemma orthogonal_comp_anti_mono:
    6.18 +  assumes "A \<subseteq> B"
    6.19 +  shows "B\<^sup>\<bottom> \<subseteq> A\<^sup>\<bottom>"
    6.20 +proof
    6.21 +  fix x assume x: "x \<in> B\<^sup>\<bottom>"
    6.22 +  show "x \<in> orthogonal_comp A" using x unfolding orthogonal_comp_def
    6.23 +    by (simp add: orthogonal_def, metis assms in_mono)
    6.24 +qed
    6.25 +
    6.26 +lemma orthogonal_comp_null [simp]: "{0}\<^sup>\<bottom> = UNIV"
    6.27 +  by (auto simp: orthogonal_comp_def orthogonal_def)
    6.28 +
    6.29 +lemma orthogonal_comp_UNIV [simp]: "UNIV\<^sup>\<bottom> = {0}"
    6.30 +  unfolding orthogonal_comp_def orthogonal_def
    6.31 +  by auto (use inner_eq_zero_iff in blast)
    6.32 +
    6.33 +lemma orthogonal_comp_subset: "U \<subseteq> U\<^sup>\<bottom>\<^sup>\<bottom>"
    6.34 +  by (auto simp: orthogonal_comp_def orthogonal_def inner_commute)
    6.35 +
    6.36 +lemma subspace_sum_minimal:
    6.37 +  assumes "S \<subseteq> U" "T \<subseteq> U" "subspace U"
    6.38 +  shows "S + T \<subseteq> U"
    6.39 +proof
    6.40 +  fix x
    6.41 +  assume "x \<in> S + T"
    6.42 +  then obtain xs xt where "xs \<in> S" "xt \<in> T" "x = xs+xt"
    6.43 +    by (meson set_plus_elim)
    6.44 +  then show "x \<in> U"
    6.45 +    by (meson assms subsetCE subspace_add)
    6.46 +qed
    6.47 +
    6.48 +lemma subspace_sum_orthogonal_comp:
    6.49 +  fixes U :: "'a :: euclidean_space set"
    6.50 +  assumes "subspace U"
    6.51 +  shows "U + U\<^sup>\<bottom> = UNIV"
    6.52 +proof -
    6.53 +  obtain B where "B \<subseteq> U"
    6.54 +    and ortho: "pairwise orthogonal B" "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
    6.55 +    and "independent B" "card B = dim U" "span B = U"
    6.56 +    using orthonormal_basis_subspace [OF assms] by metis
    6.57 +  then have "finite B"
    6.58 +    by (simp add: indep_card_eq_dim_span)
    6.59 +  have *: "\<forall>x\<in>B. \<forall>y\<in>B. x \<bullet> y = (if x=y then 1 else 0)"
    6.60 +    using ortho norm_eq_1 by (auto simp: orthogonal_def pairwise_def)
    6.61 +  { fix v
    6.62 +    let ?u = "\<Sum>b\<in>B. (v \<bullet> b) *\<^sub>R b"
    6.63 +    have "v = ?u + (v - ?u)"
    6.64 +      by simp
    6.65 +    moreover have "?u \<in> U"
    6.66 +      by (metis (no_types, lifting) \<open>span B = U\<close> assms real_vector_class.subspace_sum span_clauses(1) span_mul)
    6.67 +    moreover have "(v - ?u) \<in> U\<^sup>\<bottom>"
    6.68 +    proof (clarsimp simp: orthogonal_comp_def orthogonal_def)
    6.69 +      fix y
    6.70 +      assume "y \<in> U"
    6.71 +      with \<open>span B = U\<close> span_finite [OF \<open>finite B\<close>]
    6.72 +      obtain u where u: "y = (\<Sum>b\<in>B. u b *\<^sub>R b)"
    6.73 +        by auto
    6.74 +      have "b \<bullet> (v - ?u) = 0" if "b \<in> B" for b
    6.75 +        using that \<open>finite B\<close>
    6.76 +        by (simp add: * algebra_simps inner_sum_right if_distrib [of "( *)v" for v] inner_commute cong: if_cong)
    6.77 +      then show "y \<bullet> (v - ?u) = 0"
    6.78 +        by (simp add: u inner_sum_left)
    6.79 +    qed
    6.80 +    ultimately have "v \<in> U + U\<^sup>\<bottom>"
    6.81 +      using set_plus_intro by fastforce
    6.82 +  } then show ?thesis
    6.83 +    by auto
    6.84 +qed
    6.85 +
    6.86 +lemma orthogonal_Int_0:
    6.87 +  assumes "subspace U"
    6.88 +  shows "U \<inter> U\<^sup>\<bottom> = {0}"
    6.89 +  using orthogonal_comp_def orthogonal_self
    6.90 +  by (force simp: assms subspace_0 subspace_orthogonal_comp)
    6.91 +
    6.92 +lemma orthogonal_comp_self:
    6.93 +  fixes U :: "'a :: euclidean_space set"
    6.94 +  assumes "subspace U"
    6.95 +  shows "U\<^sup>\<bottom>\<^sup>\<bottom> = U"
    6.96 +proof
    6.97 +  have ssU': "subspace (U\<^sup>\<bottom>)"
    6.98 +    by (simp add: subspace_orthogonal_comp)
    6.99 +  have "u \<in> U" if "u \<in> U\<^sup>\<bottom>\<^sup>\<bottom>" for u
   6.100 +  proof -
   6.101 +    obtain v w where "u = v+w" "v \<in> U" "w \<in> U\<^sup>\<bottom>"
   6.102 +      using subspace_sum_orthogonal_comp [OF assms] set_plus_elim by blast
   6.103 +    then have "u-v \<in> U\<^sup>\<bottom>"
   6.104 +      by simp
   6.105 +    moreover have "v \<in> U\<^sup>\<bottom>\<^sup>\<bottom>"
   6.106 +      using \<open>v \<in> U\<close> orthogonal_comp_subset by blast
   6.107 +    then have "u-v \<in> U\<^sup>\<bottom>\<^sup>\<bottom>"
   6.108 +      by (simp add: subspace_diff subspace_orthogonal_comp that)
   6.109 +    ultimately have "u-v = 0"
   6.110 +      using orthogonal_Int_0 ssU' by blast
   6.111 +    with \<open>v \<in> U\<close> show ?thesis
   6.112 +      by auto
   6.113 +  qed
   6.114 +  then show "U\<^sup>\<bottom>\<^sup>\<bottom> \<subseteq> U"
   6.115 +    by auto
   6.116 +qed (use orthogonal_comp_subset in auto)
   6.117 +
   6.118 +lemma ker_orthogonal_comp_adjoint:
   6.119 +  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   6.120 +  assumes "linear f"
   6.121 +  shows "f -` {0} =  (range (adjoint f))\<^sup>\<bottom>"
   6.122 +  apply (auto simp: orthogonal_comp_def orthogonal_def)
   6.123 +  apply (simp add: adjoint_works assms(1) inner_commute)
   6.124 +  by (metis adjoint_works all_zero_iff assms(1) inner_commute)
   6.125 +
   6.126 +
   6.127  end
   6.128    
     7.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Sun Apr 15 17:22:58 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Sun Apr 15 21:41:40 2018 +0100
     7.3 @@ -1375,7 +1375,8 @@
     7.4         apply (simp add: \<open>finite B\<close>)
     7.5        using \<open>polynomial_function g\<close>  by auto
     7.6      show "(\<lambda>x. \<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i) ` S \<subseteq> T"
     7.7 -      using \<open>B \<subseteq> T\<close> by (blast intro: subspace_sum subspace_mul \<open>subspace T\<close>)
     7.8 +      using \<open>B \<subseteq> T\<close>
     7.9 +      by (blast intro: real_vector_class.subspace_sum subspace_mul \<open>subspace T\<close>)
    7.10      show "norm (f x - (\<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i)) < e" if "x \<in> S" for x
    7.11      proof -
    7.12        have orth': "pairwise (\<lambda>i j. orthogonal ((f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i)