author paulson Sat Apr 14 20:19:52 2018 +0100 (16 months ago) changeset 67981 349c639e593c parent 67980 a8177d098b74 child 67982 7643b005b29a
more new theorems on real^1, matrices, etc.
```     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.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"
```
```     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.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}"
```