more new theorems on real^1, matrices, etc.
authorpaulson <lp15@cam.ac.uk>
Sat Apr 14 20:19:52 2018 +0100 (16 months ago)
changeset 67981349c639e593c
parent 67980 a8177d098b74
child 67982 7643b005b29a
more new theorems on real^1, matrices, etc.
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Determinants.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Ordered_Euclidean_Space.thy
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sat Apr 14 15:36:49 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sat Apr 14 20:19:52 2018 +0100
     1.3 @@ -741,6 +741,12 @@
     1.4    apply rule
     1.5    done
     1.6  
     1.7 +lemma inj_matrix_vector_mult:
     1.8 +  fixes A::"'a::field^'n^'m"
     1.9 +  assumes "invertible A"
    1.10 +  shows "inj (( *v) A)"
    1.11 +  by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid)
    1.12 +
    1.13  
    1.14  subsection\<open>Some bounds on components etc. relative to operator norm\<close>
    1.15  
    1.16 @@ -1555,6 +1561,41 @@
    1.17  lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>"
    1.18    by (auto simp add: norm_real dist_norm)
    1.19  
    1.20 +subsection\<open>Routine results connecting the types @{typ "real^1"} and @{typ real}\<close>
    1.21 +
    1.22 +lemma vector_one_nth [simp]:
    1.23 +  fixes x :: "'a^1" shows "vec (x $ 1) = x"
    1.24 +  by (metis vec_def vector_one)
    1.25 +
    1.26 +lemma vec_cbox_1_eq [simp]:
    1.27 +  shows "vec ` cbox u v = cbox (vec u) (vec v ::real^1)"
    1.28 +  by (force simp: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box)
    1.29 +
    1.30 +lemma vec_nth_cbox_1_eq [simp]:
    1.31 +  fixes u v :: "'a::euclidean_space^1"
    1.32 +  shows "(\<lambda>x. x $ 1) ` cbox u v = cbox (u$1) (v$1)"
    1.33 +    by (auto simp: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box image_iff Bex_def inner_axis) (metis vec_component)
    1.34 +
    1.35 +lemma vec_nth_1_iff_cbox [simp]:
    1.36 +  fixes a b :: "'a::euclidean_space"
    1.37 +  shows "(\<lambda>x::'a^1. x $ 1) ` S = cbox a b \<longleftrightarrow> S = cbox (vec a) (vec b)"
    1.38 +    (is "?lhs = ?rhs")
    1.39 +proof
    1.40 +  assume L: ?lhs show ?rhs
    1.41 +  proof (intro equalityI subsetI)
    1.42 +    fix x 
    1.43 +    assume "x \<in> S"
    1.44 +    then have "x $ 1 \<in> (\<lambda>v. v $ (1::1)) ` cbox (vec a) (vec b)"
    1.45 +      using L by auto
    1.46 +    then show "x \<in> cbox (vec a) (vec b)"
    1.47 +      by (metis (no_types, lifting) imageE vector_one_nth)
    1.48 +  next
    1.49 +    fix x :: "'a^1"
    1.50 +    assume "x \<in> cbox (vec a) (vec b)"
    1.51 +    then show "x \<in> S"
    1.52 +      by (metis (no_types, lifting) L imageE imageI vec_component vec_nth_cbox_1_eq vector_one_nth)
    1.53 +  qed
    1.54 +qed simp
    1.55  
    1.56  lemma tendsto_at_within_vector_1:
    1.57    fixes S :: "'a :: metric_space set"
     2.1 --- a/src/HOL/Analysis/Determinants.thy	Sat Apr 14 15:36:49 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Determinants.thy	Sat Apr 14 20:19:52 2018 +0100
     2.3 @@ -773,7 +773,7 @@
     2.4    finally show ?thesis unfolding th2 .
     2.5  qed
     2.6  
     2.7 -text \<open>Relation to invertibility.\<close>
     2.8 +subsection \<open>Relation to invertibility.\<close>
     2.9  
    2.10  lemma invertible_left_inverse:
    2.11    fixes A :: "real^'n^'n"
    2.12 @@ -838,7 +838,75 @@
    2.13      by blast
    2.14  qed
    2.15  
    2.16 -text \<open>Cramer's rule.\<close>
    2.17 +subsubsection\<open>Invertibility of matrices and corresponding linear functions\<close>
    2.18 +
    2.19 +lemma matrix_left_invertible:
    2.20 +  fixes f :: "real^'m \<Rightarrow> real^'n"
    2.21 +  assumes "linear f"
    2.22 +  shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. linear g \<and> g \<circ> f = id))"
    2.23 +proof safe
    2.24 +  fix B
    2.25 +  assume 1: "B ** matrix f = mat 1"
    2.26 +  show "\<exists>g. linear g \<and> g \<circ> f = id"
    2.27 +  proof (intro exI conjI)
    2.28 +    show "linear (\<lambda>y. B *v y)"
    2.29 +      by (simp add: matrix_vector_mul_linear)
    2.30 +    show "(( *v) B) \<circ> f = id"
    2.31 +      unfolding o_def
    2.32 +      by (metis assms 1 eq_id_iff matrix_vector_mul matrix_vector_mul_assoc matrix_vector_mul_lid)
    2.33 +  qed
    2.34 +next
    2.35 +  fix g
    2.36 +  assume "linear g" "g \<circ> f = id"
    2.37 +  then have "matrix g ** matrix f = mat 1"
    2.38 +    by (metis assms matrix_compose matrix_id_mat_1)
    2.39 +  then show "\<exists>B. B ** matrix f = mat 1" ..
    2.40 +qed
    2.41 +
    2.42 +lemma matrix_right_invertible:
    2.43 +  fixes f :: "real^'m \<Rightarrow> real^'n"
    2.44 +  assumes "linear f"
    2.45 +  shows "((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. linear g \<and> f \<circ> g = id))"
    2.46 +proof safe
    2.47 +  fix B
    2.48 +  assume 1: "matrix f ** B = mat 1"
    2.49 +  show "\<exists>g. linear g \<and> f \<circ> g = id"
    2.50 +  proof (intro exI conjI)
    2.51 +    show "linear (( *v) B)"
    2.52 +      by (simp add: matrix_vector_mul_linear)
    2.53 +    show "f \<circ> ( *v) B = id"
    2.54 +      by (metis 1 assms comp_apply eq_id_iff linear_id matrix_id_mat_1 matrix_vector_mul_assoc matrix_works)
    2.55 +  qed
    2.56 +next
    2.57 +  fix g
    2.58 +  assume "linear g" and "f \<circ> g = id"
    2.59 +  then have "matrix f ** matrix g = mat 1"
    2.60 +    by (metis assms matrix_compose matrix_id_mat_1)
    2.61 +  then show "\<exists>B. matrix f ** B = mat 1" ..
    2.62 +qed
    2.63 +
    2.64 +lemma matrix_invertible:
    2.65 +  fixes f :: "real^'m \<Rightarrow> real^'n"
    2.66 +  assumes "linear f"
    2.67 +  shows  "invertible (matrix f) \<longleftrightarrow> (\<exists>g. linear g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
    2.68 +    (is "?lhs = ?rhs")
    2.69 +proof
    2.70 +  assume ?lhs then show ?rhs
    2.71 +    by (metis assms invertible_def left_right_inverse_eq matrix_left_invertible matrix_right_invertible)
    2.72 +next
    2.73 +  assume ?rhs then show ?lhs
    2.74 +    by (metis assms invertible_def matrix_compose matrix_id_mat_1)
    2.75 +qed
    2.76 +
    2.77 +lemma invertible_eq_bij:
    2.78 +  fixes m :: "real^'m^'n"
    2.79 +  shows "invertible m \<longleftrightarrow> bij (( *v) m)"
    2.80 +  using matrix_invertible [OF matrix_vector_mul_linear] o_bij
    2.81 +  apply (auto simp: bij_betw_def)
    2.82 +  by (metis left_right_inverse_eq  linear_injective_left_inverse [OF matrix_vector_mul_linear]
    2.83 +            linear_surjective_right_inverse[OF matrix_vector_mul_linear])
    2.84 +
    2.85 +subsection \<open>Cramer's rule.\<close>
    2.86  
    2.87  lemma cramer_lemma_transpose:
    2.88    fixes A:: "real^'n^'n"
    2.89 @@ -929,6 +997,9 @@
    2.90  
    2.91  definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
    2.92  
    2.93 +definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
    2.94 +  transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
    2.95 +
    2.96  lemma orthogonal_transformation:
    2.97    "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v. norm (f v) = norm v)"
    2.98    unfolding orthogonal_transformation_def
    2.99 @@ -938,9 +1009,6 @@
   2.100    apply (simp add: dot_norm  linear_add[symmetric])
   2.101    done
   2.102  
   2.103 -definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
   2.104 -  transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
   2.105 -
   2.106  lemma orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
   2.107    by (simp add: linear_iff orthogonal_transformation_def)
   2.108  
   2.109 @@ -956,6 +1024,9 @@
   2.110    "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
   2.111    by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
   2.112  
   2.113 +lemma orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v"
   2.114 +  by (simp add: linear_iff orthogonal_transformation_def)
   2.115 +
   2.116  lemma orthogonal_transformation_linear:
   2.117     "orthogonal_transformation f \<Longrightarrow> linear f"
   2.118    by (simp add: orthogonal_transformation_def)
     3.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Apr 14 15:36:49 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Apr 14 20:19:52 2018 +0100
     3.3 @@ -2434,7 +2434,6 @@
     3.4    then show ?thesis
     3.5      by (simp add: euclidean_representation)
     3.6  qed
     3.7 -
     3.8    
     3.9  lemma absolutely_integrable_component_ubound:
    3.10    fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
    3.11 @@ -2450,7 +2449,6 @@
    3.12      by simp
    3.13  qed
    3.14  
    3.15 -
    3.16  lemma absolutely_integrable_component_lbound:
    3.17    fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
    3.18    assumes f: "f absolutely_integrable_on A" and g: "g integrable_on A"
    3.19 @@ -2465,6 +2463,165 @@
    3.20      by simp
    3.21  qed
    3.22  
    3.23 +lemma integrable_on_1_iff:
    3.24 +  fixes f :: "'a::euclidean_space \<Rightarrow> real^1"
    3.25 +  shows "f integrable_on S \<longleftrightarrow> (\<lambda>x. f x $ 1) integrable_on S"
    3.26 +  by (auto simp: integrable_componentwise_iff [of f] Basis_vec_def cart_eq_inner_axis)
    3.27 +
    3.28 +lemma integral_on_1_eq:
    3.29 +  fixes f :: "'a::euclidean_space \<Rightarrow> real^1"
    3.30 +  shows "integral S f = vec (integral S (\<lambda>x. f x $ 1))"
    3.31 +by (cases "f integrable_on S") (simp_all add: integrable_on_1_iff vec_eq_iff not_integrable_integral)
    3.32 +
    3.33 +lemma absolutely_integrable_on_1_iff:
    3.34 +  fixes f :: "'a::euclidean_space \<Rightarrow> real^1"
    3.35 +  shows "f absolutely_integrable_on S \<longleftrightarrow> (\<lambda>x. f x $ 1) absolutely_integrable_on S"
    3.36 +  unfolding absolutely_integrable_on_def
    3.37 +  by (auto simp: integrable_on_1_iff norm_real)
    3.38 +
    3.39 +lemma absolutely_integrable_absolutely_integrable_lbound:
    3.40 +  fixes f :: "'m::euclidean_space \<Rightarrow> real"
    3.41 +  assumes f: "f integrable_on S" and g: "g absolutely_integrable_on S"
    3.42 +    and *: "\<And>x. x \<in> S \<Longrightarrow> g x \<le> f x"
    3.43 +  shows "f absolutely_integrable_on S"
    3.44 +  by (rule absolutely_integrable_component_lbound [OF g f]) (simp add: *)
    3.45 +
    3.46 +lemma absolutely_integrable_absolutely_integrable_ubound:
    3.47 +  fixes f :: "'m::euclidean_space \<Rightarrow> real"
    3.48 +  assumes fg: "f integrable_on S" "g absolutely_integrable_on S"
    3.49 +    and *: "\<And>x. x \<in> S \<Longrightarrow> f x \<le> g x"
    3.50 +  shows "f absolutely_integrable_on S"
    3.51 +  by (rule absolutely_integrable_component_ubound [OF fg]) (simp add: *)
    3.52 +
    3.53 +lemma has_integral_vec1_I_cbox:
    3.54 +  fixes f :: "real^1 \<Rightarrow> 'a::real_normed_vector"
    3.55 +  assumes "(f has_integral y) (cbox a b)"
    3.56 +  shows "((f \<circ> vec) has_integral y) {a$1..b$1}"
    3.57 +proof -
    3.58 +  have "((\<lambda>x. f(vec x)) has_integral (1 / 1) *\<^sub>R y) ((\<lambda>x. x $ 1) ` cbox a b)"
    3.59 +  proof (rule has_integral_twiddle)
    3.60 +    show "\<exists>w z::real^1. vec ` cbox u v = cbox w z"
    3.61 +         "content (vec ` cbox u v :: (real^1) set) = 1 * content (cbox u v)" for u v
    3.62 +      unfolding vec_cbox_1_eq
    3.63 +      by (auto simp: content_cbox_if_cart interval_eq_empty_cart)
    3.64 +    show "\<exists>w z. (\<lambda>x. x $ 1) ` cbox u v = cbox w z" for u v :: "real^1"
    3.65 +      using vec_nth_cbox_1_eq by blast
    3.66 +  qed (auto simp: continuous_vec assms)
    3.67 +  then show ?thesis
    3.68 +    by (simp add: o_def)
    3.69 +qed
    3.70 +
    3.71 +lemma has_integral_vec1_I:
    3.72 +  fixes f :: "real^1 \<Rightarrow> 'a::real_normed_vector"
    3.73 +  assumes "(f has_integral y) S"
    3.74 +  shows "(f \<circ> vec has_integral y) ((\<lambda>x. x $ 1) ` S)"
    3.75 +proof -
    3.76 +  have *: "\<exists>z. ((\<lambda>x. if x \<in> (\<lambda>x. x $ 1) ` S then (f \<circ> vec) x else 0) has_integral z) {a..b} \<and> norm (z - y) < e"
    3.77 +    if int: "\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow>
    3.78 +                    (\<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e)"
    3.79 +      and B: "ball 0 B \<subseteq> {a..b}" for e B a b
    3.80 +  proof -
    3.81 +    have [simp]: "(\<exists>y\<in>S. x = y $ 1) \<longleftrightarrow> vec x \<in> S" for x
    3.82 +      by force
    3.83 +    have B': "ball (0::real^1) B \<subseteq> cbox (vec a) (vec b)"
    3.84 +      using B by (simp add: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box norm_real subset_iff)
    3.85 +    show ?thesis
    3.86 +      using int [OF B'] by (auto simp: image_iff o_def cong: if_cong dest!: has_integral_vec1_I_cbox)
    3.87 +  qed
    3.88 +  show ?thesis
    3.89 +    using assms 
    3.90 +    apply (subst has_integral_alt)
    3.91 +    apply (subst (asm) has_integral_alt)
    3.92 +    apply (simp add: has_integral_vec1_I_cbox split: if_split_asm)
    3.93 +    apply (metis vector_one_nth)
    3.94 +    apply (erule all_forward imp_forward asm_rl ex_forward conj_forward)+
    3.95 +    apply (blast intro!: *)
    3.96 +    done
    3.97 +qed
    3.98 +
    3.99 +lemma has_integral_vec1_nth_cbox:
   3.100 +  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   3.101 +  assumes "(f has_integral y) {a..b}"
   3.102 +  shows "((\<lambda>x::real^1. f(x$1)) has_integral y) (cbox (vec a) (vec b))"
   3.103 +proof -
   3.104 +  have "((\<lambda>x::real^1. f(x$1)) has_integral (1 / 1) *\<^sub>R y) (vec ` cbox a b)"
   3.105 +  proof (rule has_integral_twiddle)
   3.106 +    show "\<exists>w z::real. (\<lambda>x. x $ 1) ` cbox u v = cbox w z"
   3.107 +         "content ((\<lambda>x. x $ 1) ` cbox u v) = 1 * content (cbox u v)" for u v::"real^1"
   3.108 +      unfolding vec_cbox_1_eq by (auto simp: content_cbox_if_cart interval_eq_empty_cart)
   3.109 +    show "\<exists>w z::real^1. vec ` cbox u v = cbox w z" for u v :: "real"
   3.110 +      using vec_cbox_1_eq by auto
   3.111 +  qed (auto simp: continuous_vec assms)
   3.112 +  then show ?thesis
   3.113 +    using vec_cbox_1_eq by auto
   3.114 +qed
   3.115 +
   3.116 +lemma has_integral_vec1_D_cbox:
   3.117 +  fixes f :: "real^1 \<Rightarrow> 'a::real_normed_vector"
   3.118 +  assumes "((f \<circ> vec) has_integral y) {a$1..b$1}"
   3.119 +  shows "(f has_integral y) (cbox a b)"
   3.120 +  by (metis (mono_tags, lifting) assms comp_apply has_integral_eq has_integral_vec1_nth_cbox vector_one_nth)
   3.121 +
   3.122 +lemma has_integral_vec1_D:
   3.123 +  fixes f :: "real^1 \<Rightarrow> 'a::real_normed_vector"
   3.124 +  assumes "((f \<circ> vec) has_integral y) ((\<lambda>x. x $ 1) ` S)"
   3.125 +  shows "(f has_integral y) S"
   3.126 +proof -
   3.127 +  have *: "\<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e"
   3.128 +    if int: "\<And>a b. ball 0 B \<subseteq> {a..b} \<Longrightarrow>
   3.129 +                             (\<exists>z. ((\<lambda>x. if x \<in> (\<lambda>x. x $ 1) ` S then (f \<circ> vec) x else 0) has_integral z) {a..b} \<and> norm (z - y) < e)"
   3.130 +      and B: "ball 0 B \<subseteq> cbox a b" for e B and a b::"real^1"
   3.131 +  proof -
   3.132 +    have B': "ball 0 B \<subseteq> {a$1..b$1}"
   3.133 +      using B
   3.134 +      apply (simp add: subset_iff Basis_vec_def cart_eq_inner_axis [symmetric] mem_box)
   3.135 +      apply (metis (full_types) norm_real vec_component)
   3.136 +      done
   3.137 +    have eq: "(\<lambda>x. if vec x \<in> S then f (vec x) else 0) = (\<lambda>x. if x \<in> S then f x else 0) \<circ> vec"
   3.138 +      by force
   3.139 +    have [simp]: "(\<exists>y\<in>S. x = y $ 1) \<longleftrightarrow> vec x \<in> S" for x
   3.140 +      by force
   3.141 +    show ?thesis
   3.142 +      using int [OF B'] by (auto simp: image_iff eq cong: if_cong dest!: has_integral_vec1_D_cbox)
   3.143 +qed
   3.144 +  show ?thesis
   3.145 +    using assms
   3.146 +    apply (subst has_integral_alt)
   3.147 +    apply (subst (asm) has_integral_alt)
   3.148 +    apply (simp add: has_integral_vec1_D_cbox eq_cbox split: if_split_asm, blast)
   3.149 +    apply (intro conjI impI)
   3.150 +     apply (metis vector_one_nth)
   3.151 +    apply (erule thin_rl)
   3.152 +    apply (erule all_forward imp_forward asm_rl ex_forward conj_forward)+
   3.153 +    using * apply blast
   3.154 +    done
   3.155 +qed
   3.156 +
   3.157 +
   3.158 +lemma integral_vec1_eq:
   3.159 +  fixes f :: "real^1 \<Rightarrow> 'a::real_normed_vector"
   3.160 +  shows "integral S f = integral ((\<lambda>x. x $ 1) ` S) (f \<circ> vec)"
   3.161 +  using has_integral_vec1_I [of f] has_integral_vec1_D [of f]
   3.162 +  by (metis has_integral_iff not_integrable_integral)
   3.163 +
   3.164 +lemma absolutely_integrable_drop:
   3.165 +  fixes f :: "real^1 \<Rightarrow> 'b::euclidean_space"
   3.166 +  shows "f absolutely_integrable_on S \<longleftrightarrow> (f \<circ> vec) absolutely_integrable_on (\<lambda>x. x $ 1) ` S"
   3.167 +  unfolding absolutely_integrable_on_def integrable_on_def
   3.168 +proof safe
   3.169 +  fix y r
   3.170 +  assume "(f has_integral y) S" "((\<lambda>x. norm (f x)) has_integral r) S"
   3.171 +  then show "\<exists>y. (f \<circ> vec has_integral y) ((\<lambda>x. x $ 1) ` S)"
   3.172 +            "\<exists>y. ((\<lambda>x. norm ((f \<circ> vec) x)) has_integral y) ((\<lambda>x. x $ 1) ` S)"
   3.173 +    by (force simp: o_def dest!: has_integral_vec1_I)+
   3.174 +next
   3.175 +  fix y :: "'b" and r :: "real"
   3.176 +  assume "(f \<circ> vec has_integral y) ((\<lambda>x. x $ 1) ` S)"
   3.177 +         "((\<lambda>x. norm ((f \<circ> vec) x)) has_integral r) ((\<lambda>x. x $ 1) ` S)"
   3.178 +  then show "\<exists>y. (f has_integral y) S"  "\<exists>y. ((\<lambda>x. norm (f x)) has_integral y) S"
   3.179 +    by (force simp: o_def intro: has_integral_vec1_D)+
   3.180 +qed
   3.181 +
   3.182  subsection \<open>Dominated convergence\<close>
   3.183  
   3.184  lemma dominated_convergence:
   3.185 @@ -2582,7 +2739,6 @@
   3.186    qed (use b in auto)
   3.187  qed
   3.188  
   3.189 -
   3.190  lemma dominated_convergence_absolutely_integrable:
   3.191    fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   3.192    assumes f: "\<And>k. f k absolutely_integrable_on S"
   3.193 @@ -2597,6 +2753,37 @@
   3.194      by (blast intro:  absolutely_integrable_integrable_bound [where g=h])
   3.195  qed
   3.196  
   3.197 +
   3.198 +proposition integral_countable_UN:
   3.199 +  fixes f :: "real^'m \<Rightarrow> real^'n"
   3.200 +  assumes f: "f absolutely_integrable_on (\<Union>(range s))"
   3.201 +    and s: "\<And>m. s m \<in> sets lebesgue"
   3.202 +  shows "\<And>n. f absolutely_integrable_on (\<Union>m\<le>n. s m)"
   3.203 +    and "(\<lambda>n. integral (\<Union>m\<le>n. s m) f) \<longlonglongrightarrow> integral (UNION UNIV s) f" (is "?F \<longlonglongrightarrow> ?I")
   3.204 +proof -
   3.205 +  show fU: "f absolutely_integrable_on (\<Union>m\<le>n. s m)" for n
   3.206 +    using assms by (blast intro: set_integrable_subset [OF f])
   3.207 +  have fint: "f integrable_on (\<Union> (range s))"
   3.208 +    using absolutely_integrable_on_def f by blast
   3.209 +  let ?h = "\<lambda>x. if x \<in> UNION UNIV s then norm(f x) else 0"
   3.210 +  have "(\<lambda>n. integral UNIV (\<lambda>x. if x \<in> (\<Union>m\<le>n. s m) then f x else 0))
   3.211 +        \<longlonglongrightarrow> integral UNIV (\<lambda>x. if x \<in> UNION UNIV s then f x else 0)"
   3.212 +  proof (rule dominated_convergence)
   3.213 +    show "(\<lambda>x. if x \<in> (\<Union>m\<le>n. s m) then f x else 0) integrable_on UNIV" for n
   3.214 +      unfolding integrable_restrict_UNIV
   3.215 +      using fU absolutely_integrable_on_def by blast
   3.216 +    show "(\<lambda>x. if x \<in> UNION UNIV s then norm(f x) else 0) integrable_on UNIV"
   3.217 +      by (metis (no_types) absolutely_integrable_on_def f integrable_restrict_UNIV)
   3.218 +    show "\<forall>x\<in>UNIV.
   3.219 +         (\<lambda>n. if x \<in> (\<Union>m\<le>n. s m) then f x else 0)
   3.220 +         \<longlonglongrightarrow> (if x \<in> UNION UNIV s then f x else 0)"
   3.221 +      by (force intro: Lim_eventually eventually_sequentiallyI)
   3.222 +  qed auto
   3.223 +  then show "?F \<longlonglongrightarrow> ?I"
   3.224 +    by (simp only: integral_restrict_UNIV)
   3.225 +qed
   3.226 +
   3.227 +
   3.228  subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
   3.229  
   3.230  text \<open>
     4.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sat Apr 14 15:36:49 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sat Apr 14 20:19:52 2018 +0100
     4.3 @@ -182,6 +182,11 @@
     4.4      and eucl_le_atLeast: "{x. \<forall>i\<in>Basis. a \<bullet> i <= x \<bullet> i} = {a..}"
     4.5      by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
     4.6  
     4.7 +lemma vec_nth_real_1_iff_cbox [simp]:
     4.8 +  fixes a b :: real
     4.9 +  shows "(\<lambda>x::real^1. x $ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)"
    4.10 +  by (metis interval_cbox vec_nth_1_iff_cbox)
    4.11 +
    4.12  lemma closed_eucl_atLeastAtMost[simp, intro]:
    4.13    fixes a :: "'a::ordered_euclidean_space"
    4.14    shows "closed {a..b}"