author paulson Sun Apr 15 21:41:40 2018 +0100 (16 months ago) changeset 67986 b65c4a6a015e parent 67985 7811748de271 child 67987 9044e1f1d324
quite a few more results about negligibility, etc., and a bit of tidying up
```     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)
```