changeset 69679 | a8faf6f15da7 |
parent 69677 | a06b204527e6 |
parent 69675 | 880ab0f27ddf |
child 69683 | 8b3458ca0762 |
69678:0f4d4a13dc16 | 69679:a8faf6f15da7 |
---|---|
7 theory Change_Of_Vars |
7 theory Change_Of_Vars |
8 imports Vitali_Covering_Theorem Determinants |
8 imports Vitali_Covering_Theorem Determinants |
9 |
9 |
10 begin |
10 begin |
11 |
11 |
12 subsection%important\<open>Induction on matrix row operations\<close> |
12 subsection%unimportant \<open>Orthogonal Transformation of Balls\<close> |
13 (*FIX move first 3 lemmas of subsection to linear algebra, contain technical tools on matrix operations. |
13 |
14 Keep the rest of the subsection contents in this theory but rename the subsection, they refer |
14 lemma%unimportant image_orthogonal_transformation_ball: |
15 to lebesgue measure |
15 fixes f :: "'a::euclidean_space \<Rightarrow> 'a" |
16 *) |
16 assumes "orthogonal_transformation f" |
17 lemma induct_matrix_row_operations: |
17 shows "f ` ball x r = ball (f x) r" |
18 fixes P :: "real^'n^'n \<Rightarrow> bool" |
18 proof (intro equalityI subsetI) |
19 assumes zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A" |
19 fix y assume "y \<in> f ` ball x r" |
20 and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A" |
20 with assms show "y \<in> ball (f x) r" |
21 and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A $ i $ Fun.swap m n id j)" |
21 by (auto simp: orthogonal_transformation_isometry) |
22 and row_op: "\<And>A m n c. \<lbrakk>P A; m \<noteq> n\<rbrakk> |
22 next |
23 \<Longrightarrow> P(\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)" |
23 fix y assume y: "y \<in> ball (f x) r" |
24 shows "P A" |
24 then obtain z where z: "y = f z" |
25 proof - |
25 using assms orthogonal_transformation_surj by blast |
26 have "P A" if "(\<And>i j. \<lbrakk>j \<in> -K; i \<noteq> j\<rbrakk> \<Longrightarrow> A$i$j = 0)" for A K |
26 with y assms show "y \<in> f ` ball x r" |
27 proof - |
27 by (auto simp: orthogonal_transformation_isometry) |
28 have "finite K" |
28 qed |
29 by simp |
29 |
30 then show ?thesis using that |
30 lemma%unimportant image_orthogonal_transformation_cball: |
31 proof (induction arbitrary: A rule: finite_induct) |
31 fixes f :: "'a::euclidean_space \<Rightarrow> 'a" |
32 case empty |
32 assumes "orthogonal_transformation f" |
33 with diagonal show ?case |
33 shows "f ` cball x r = cball (f x) r" |
34 by simp |
34 proof (intro equalityI subsetI) |
35 next |
35 fix y assume "y \<in> f ` cball x r" |
36 case (insert k K) |
36 with assms show "y \<in> cball (f x) r" |
37 note insertK = insert |
37 by (auto simp: orthogonal_transformation_isometry) |
38 have "P A" if kk: "A$k$k \<noteq> 0" |
38 next |
39 and 0: "\<And>i j. \<lbrakk>j \<in> - insert k K; i \<noteq> j\<rbrakk> \<Longrightarrow> A$i$j = 0" |
39 fix y assume y: "y \<in> cball (f x) r" |
40 "\<And>i. \<lbrakk>i \<in> -L; i \<noteq> k\<rbrakk> \<Longrightarrow> A$i$k = 0" for A L |
40 then obtain z where z: "y = f z" |
41 proof - |
41 using assms orthogonal_transformation_surj by blast |
42 have "finite L" |
42 with y assms show "y \<in> f ` cball x r" |
43 by simp |
43 by (auto simp: orthogonal_transformation_isometry) |
44 then show ?thesis using 0 kk |
44 qed |
45 proof (induction arbitrary: A rule: finite_induct) |
45 |
46 case (empty B) |
46 |
47 show ?case |
47 subsection \<open>Measurable Shear and Stretch\<close> |
48 proof (rule insertK) |
48 |
49 fix i j |
49 proposition%important |
50 assume "i \<in> - K" "j \<noteq> i" |
|
51 show "B $ j $ i = 0" |
|
52 using \<open>j \<noteq> i\<close> \<open>i \<in> - K\<close> empty |
|
53 by (metis ComplD ComplI Compl_eq_Diff_UNIV Diff_empty UNIV_I insert_iff) |
|
54 qed |
|
55 next |
|
56 case (insert l L B) |
|
57 show ?case |
|
58 proof (cases "k = l") |
|
59 case True |
|
60 with insert show ?thesis |
|
61 by auto |
|
62 next |
|
63 case False |
|
64 let ?C = "\<chi> i. if i = l then row l B - (B $ l $ k / B $ k $ k) *\<^sub>R row k B else row i B" |
|
65 have 1: "\<lbrakk>j \<in> - insert k K; i \<noteq> j\<rbrakk> \<Longrightarrow> ?C $ i $ j = 0" for j i |
|
66 by (auto simp: insert.prems(1) row_def) |
|
67 have 2: "?C $ i $ k = 0" |
|
68 if "i \<in> - L" "i \<noteq> k" for i |
|
69 proof (cases "i=l") |
|
70 case True |
|
71 with that insert.prems show ?thesis |
|
72 by (simp add: row_def) |
|
73 next |
|
74 case False |
|
75 with that show ?thesis |
|
76 by (simp add: insert.prems(2) row_def) |
|
77 qed |
|
78 have 3: "?C $ k $ k \<noteq> 0" |
|
79 by (auto simp: insert.prems row_def \<open>k \<noteq> l\<close>) |
|
80 have PC: "P ?C" |
|
81 using insert.IH [OF 1 2 3] by auto |
|
82 have eqB: "(\<chi> i. if i = l then row l ?C + (B $ l $ k / B $ k $ k) *\<^sub>R row k ?C else row i ?C) = B" |
|
83 using \<open>k \<noteq> l\<close> by (simp add: vec_eq_iff row_def) |
|
84 show ?thesis |
|
85 using row_op [OF PC, of l k, where c = "B$l$k / B$k$k"] eqB \<open>k \<noteq> l\<close> |
|
86 by (simp add: cong: if_cong) |
|
87 qed |
|
88 qed |
|
89 qed |
|
90 then have nonzero_hyp: "P A" |
|
91 if kk: "A$k$k \<noteq> 0" and zeroes: "\<And>i j. j \<in> - insert k K \<and> i\<noteq>j \<Longrightarrow> A$i$j = 0" for A |
|
92 by (auto simp: intro!: kk zeroes) |
|
93 show ?case |
|
94 proof (cases "row k A = 0") |
|
95 case True |
|
96 with zero_row show ?thesis by auto |
|
97 next |
|
98 case False |
|
99 then obtain l where l: "A$k$l \<noteq> 0" |
|
100 by (auto simp: row_def zero_vec_def vec_eq_iff) |
|
101 show ?thesis |
|
102 proof (cases "k = l") |
|
103 case True |
|
104 with l nonzero_hyp insert.prems show ?thesis |
|
105 by blast |
|
106 next |
|
107 case False |
|
108 have *: "A $ i $ Fun.swap k l id j = 0" if "j \<noteq> k" "j \<notin> K" "i \<noteq> j" for i j |
|
109 using False l insert.prems that |
|
110 by (auto simp: swap_def insert split: if_split_asm) |
|
111 have "P (\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j)" |
|
112 by (rule swap_cols [OF nonzero_hyp False]) (auto simp: l *) |
|
113 moreover |
|
114 have "(\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j) = A" |
|
115 by (metis (no_types, lifting) id_apply o_apply swap_id_idempotent vec_lambda_unique vec_lambda_unique) |
|
116 ultimately show ?thesis |
|
117 by simp |
|
118 qed |
|
119 qed |
|
120 qed |
|
121 qed |
|
122 then show ?thesis |
|
123 by blast |
|
124 qed |
|
125 |
|
126 lemma induct_matrix_elementary: |
|
127 fixes P :: "real^'n^'n \<Rightarrow> bool" |
|
128 assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)" |
|
129 and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A" |
|
130 and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A" |
|
131 and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)" |
|
132 and idplus: "\<And>m n c. m \<noteq> n \<Longrightarrow> P(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))" |
|
133 shows "P A" |
|
134 proof - |
|
135 have swap: "P (\<chi> i j. A $ i $ Fun.swap m n id j)" (is "P ?C") |
|
136 if "P A" "m \<noteq> n" for A m n |
|
137 proof - |
|
138 have "A ** (\<chi> i j. mat 1 $ i $ Fun.swap m n id j) = ?C" |
|
139 by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff if_distrib sum.delta_remove) |
|
140 then show ?thesis |
|
141 using mult swap1 that by metis |
|
142 qed |
|
143 have row: "P (\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)" (is "P ?C") |
|
144 if "P A" "m \<noteq> n" for A m n c |
|
145 proof - |
|
146 let ?B = "\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j)" |
|
147 have "?B ** A = ?C" |
|
148 using \<open>m \<noteq> n\<close> unfolding matrix_matrix_mult_def row_def of_bool_def |
|
149 by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong) |
|
150 then show ?thesis |
|
151 by (rule subst) (auto simp: that mult idplus) |
|
152 qed |
|
153 show ?thesis |
|
154 by (rule induct_matrix_row_operations [OF zero_row diagonal swap row]) |
|
155 qed |
|
156 |
|
157 lemma induct_matrix_elementary_alt: |
|
158 fixes P :: "real^'n^'n \<Rightarrow> bool" |
|
159 assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)" |
|
160 and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A" |
|
161 and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A" |
|
162 and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)" |
|
163 and idplus: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j))" |
|
164 shows "P A" |
|
165 proof - |
|
166 have *: "P (\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))" |
|
167 if "m \<noteq> n" for m n c |
|
168 proof (cases "c = 0") |
|
169 case True |
|
170 with diagonal show ?thesis by auto |
|
171 next |
|
172 case False |
|
173 then have eq: "(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j)) = |
|
174 (\<chi> i j. if i = j then (if j = n then inverse c else 1) else 0) ** |
|
175 (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)) ** |
|
176 (\<chi> i j. if i = j then if j = n then c else 1 else 0)" |
|
177 using \<open>m \<noteq> n\<close> |
|
178 apply (simp add: matrix_matrix_mult_def vec_eq_iff of_bool_def if_distrib [of "\<lambda>x. y * x" for y] cong: if_cong) |
|
179 apply (simp add: if_if_eq_conj sum.neutral conj_commute cong: conj_cong) |
|
180 done |
|
181 show ?thesis |
|
182 apply (subst eq) |
|
183 apply (intro mult idplus that) |
|
184 apply (auto intro: diagonal) |
|
185 done |
|
186 qed |
|
187 show ?thesis |
|
188 by (rule induct_matrix_elementary) (auto intro: assms *) |
|
189 qed |
|
190 |
|
191 lemma matrix_vector_mult_matrix_matrix_mult_compose: |
|
192 "(*v) (A ** B) = (*v) A \<circ> (*v) B" |
|
193 by (auto simp: matrix_vector_mul_assoc) |
|
194 |
|
195 lemma induct_linear_elementary: |
|
196 fixes f :: "real^'n \<Rightarrow> real^'n" |
|
197 assumes "linear f" |
|
198 and comp: "\<And>f g. \<lbrakk>linear f; linear g; P f; P g\<rbrakk> \<Longrightarrow> P(f \<circ> g)" |
|
199 and zeroes: "\<And>f i. \<lbrakk>linear f; \<And>x. (f x) $ i = 0\<rbrakk> \<Longrightarrow> P f" |
|
200 and const: "\<And>c. P(\<lambda>x. \<chi> i. c i * x$i)" |
|
201 and swap: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. x $ Fun.swap m n id i)" |
|
202 and idplus: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i)" |
|
203 shows "P f" |
|
204 proof - |
|
205 have "P ((*v) A)" for A |
|
206 proof (rule induct_matrix_elementary_alt) |
|
207 fix A B |
|
208 assume "P ((*v) A)" and "P ((*v) B)" |
|
209 then show "P ((*v) (A ** B))" |
|
210 by (auto simp add: matrix_vector_mult_matrix_matrix_mult_compose matrix_vector_mul_linear |
|
211 intro!: comp) |
|
212 next |
|
213 fix A :: "real^'n^'n" and i |
|
214 assume "row i A = 0" |
|
215 show "P ((*v) A)" |
|
216 using matrix_vector_mul_linear |
|
217 by (rule zeroes[where i=i]) |
|
218 (metis \<open>row i A = 0\<close> inner_zero_left matrix_vector_mul_component row_def vec_lambda_eta) |
|
219 next |
|
220 fix A :: "real^'n^'n" |
|
221 assume 0: "\<And>i j. i \<noteq> j \<Longrightarrow> A $ i $ j = 0" |
|
222 have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x and i :: "'n" |
|
223 by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i]) |
|
224 then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = ((*v) A)" |
|
225 by (auto simp: 0 matrix_vector_mult_def) |
|
226 then show "P ((*v) A)" |
|
227 using const [of "\<lambda>i. A $ i $ i"] by simp |
|
228 next |
|
229 fix m n :: "'n" |
|
230 assume "m \<noteq> n" |
|
231 have eq: "(\<Sum>j\<in>UNIV. if i = Fun.swap m n id j then x $ j else 0) = |
|
232 (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)" |
|
233 for i and x :: "real^'n" |
|
234 unfolding swap_def by (rule sum.cong) auto |
|
235 have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = ((*v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))" |
|
236 by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong) |
|
237 with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))" |
|
238 by (simp add: mat_def matrix_vector_mult_def) |
|
239 next |
|
240 fix m n :: "'n" |
|
241 assume "m \<noteq> n" |
|
242 then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "real^'n" |
|
243 by (auto simp: of_bool_def if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong) |
|
244 then have "(\<lambda>x::real^'n. \<chi> i. if i = m then x $ m + x $ n else x $ i) = |
|
245 ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))" |
|
246 unfolding matrix_vector_mult_def of_bool_def |
|
247 by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong) |
|
248 then show "P ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))" |
|
249 using idplus [OF \<open>m \<noteq> n\<close>] by simp |
|
250 qed |
|
251 then show ?thesis |
|
252 by (metis \<open>linear f\<close> matrix_vector_mul) |
|
253 qed |
|
254 |
|
255 |
|
256 proposition (*FIX needs name *) |
|
257 fixes a :: "real^'n" |
50 fixes a :: "real^'n" |
258 assumes "m \<noteq> n" and ab_ne: "cbox a b \<noteq> {}" and an: "0 \<le> a$n" |
51 assumes "m \<noteq> n" and ab_ne: "cbox a b \<noteq> {}" and an: "0 \<le> a$n" |
259 shows measurable_shear_interval: "(\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i) ` (cbox a b) \<in> lmeasurable" |
52 shows measurable_shear_interval: "(\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i) ` (cbox a b) \<in> lmeasurable" |
260 (is "?f ` _ \<in> _") |
53 (is "?f ` _ \<in> _") |
261 and measure_shear_interval: "measure lebesgue ((\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i) ` cbox a b) |
54 and measure_shear_interval: "measure lebesgue ((\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i) ` cbox a b) |
262 = measure lebesgue (cbox a b)" (is "?Q") |
55 = measure lebesgue (cbox a b)" (is "?Q") |
263 proof - |
56 proof%unimportant - |
264 have lin: "linear ?f" |
57 have lin: "linear ?f" |
265 by (rule linearI) (auto simp: plus_vec_def scaleR_vec_def algebra_simps) |
58 by (rule linearI) (auto simp: plus_vec_def scaleR_vec_def algebra_simps) |
266 show fab: "?f ` cbox a b \<in> lmeasurable" |
59 show fab: "?f ` cbox a b \<in> lmeasurable" |
267 by (simp add: lin measurable_linear_image_interval) |
60 by (simp add: lin measurable_linear_image_interval) |
268 let ?c = "\<chi> i. if i = m then b$m + b$n else b$i" |
61 let ?c = "\<chi> i. if i = m then b$m + b$n else b$i" |
360 using eq1 eq2 eq3 |
153 using eq1 eq2 eq3 |
361 by (simp add: algebra_simps) |
154 by (simp add: algebra_simps) |
362 qed |
155 qed |
363 |
156 |
364 |
157 |
365 proposition (*FIX needs name *) |
158 proposition%important |
366 fixes S :: "(real^'n) set" |
159 fixes S :: "(real^'n) set" |
367 assumes "S \<in> lmeasurable" |
160 assumes "S \<in> lmeasurable" |
368 shows measurable_stretch: "((\<lambda>x. \<chi> k. m k * x$k) ` S) \<in> lmeasurable" (is "?f ` S \<in> _") |
161 shows measurable_stretch: "((\<lambda>x. \<chi> k. m k * x$k) ` S) \<in> lmeasurable" (is "?f ` S \<in> _") |
369 and measure_stretch: "measure lebesgue ((\<lambda>x. \<chi> k. m k * x$k) ` S) = \<bar>prod m UNIV\<bar> * measure lebesgue S" |
162 and measure_stretch: "measure lebesgue ((\<lambda>x. \<chi> k. m k * x$k) ` S) = \<bar>prod m UNIV\<bar> * measure lebesgue S" |
370 (is "?MEQ") |
163 (is "?MEQ") |
371 proof - |
164 proof%unimportant - |
372 have "(?f ` S) \<in> lmeasurable \<and> ?MEQ" |
165 have "(?f ` S) \<in> lmeasurable \<and> ?MEQ" |
373 proof (cases "\<forall>k. m k \<noteq> 0") |
166 proof (cases "\<forall>k. m k \<noteq> 0") |
374 case True |
167 case True |
375 have m0: "0 < \<bar>prod m UNIV\<bar>" |
168 have m0: "0 < \<bar>prod m UNIV\<bar>" |
376 using True by simp |
169 using True by simp |
464 then show "(?f ` S) \<in> lmeasurable" ?MEQ |
257 then show "(?f ` S) \<in> lmeasurable" ?MEQ |
465 by metis+ |
258 by metis+ |
466 qed |
259 qed |
467 |
260 |
468 |
261 |
469 proposition (*FIX needs name *) |
262 proposition%important |
470 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
263 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
471 assumes "linear f" "S \<in> lmeasurable" |
264 assumes "linear f" "S \<in> lmeasurable" |
472 shows measurable_linear_image: "(f ` S) \<in> lmeasurable" |
265 shows measurable_linear_image: "(f ` S) \<in> lmeasurable" |
473 and measure_linear_image: "measure lebesgue (f ` S) = \<bar>det (matrix f)\<bar> * measure lebesgue S" (is "?Q f S") |
266 and measure_linear_image: "measure lebesgue (f ` S) = \<bar>det (matrix f)\<bar> * measure lebesgue S" (is "?Q f S") |
474 proof - |
267 proof%unimportant - |
475 have "\<forall>S \<in> lmeasurable. (f ` S) \<in> lmeasurable \<and> ?Q f S" |
268 have "\<forall>S \<in> lmeasurable. (f ` S) \<in> lmeasurable \<and> ?Q f S" |
476 proof (rule induct_linear_elementary [OF \<open>linear f\<close>]; intro ballI) |
269 proof (rule induct_linear_elementary [OF \<open>linear f\<close>]; intro ballI) |
477 fix f g and S :: "(real,'n) vec set" |
270 fix f g and S :: "(real,'n) vec set" |
478 assume "linear f" and "linear g" |
271 assume "linear f" and "linear g" |
479 and f [rule_format]: "\<forall>S \<in> lmeasurable. f ` S \<in> lmeasurable \<and> ?Q f S" |
272 and f [rule_format]: "\<forall>S \<in> lmeasurable. f ` S \<in> lmeasurable \<and> ?Q f S" |
612 with assms show "(f ` S) \<in> lmeasurable" "?Q f S" |
405 with assms show "(f ` S) \<in> lmeasurable" "?Q f S" |
613 by metis+ |
406 by metis+ |
614 qed |
407 qed |
615 |
408 |
616 |
409 |
617 lemma (* needs name *) |
410 lemma%unimportant |
618 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
411 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
619 assumes f: "orthogonal_transformation f" and S: "S \<in> lmeasurable" |
412 assumes f: "orthogonal_transformation f" and S: "S \<in> lmeasurable" |
620 shows measurable_orthogonal_image: "f ` S \<in> lmeasurable" |
413 shows measurable_orthogonal_image: "f ` S \<in> lmeasurable" |
621 and measure_orthogonal_image: "measure lebesgue (f ` S) = measure lebesgue S" |
414 and measure_orthogonal_image: "measure lebesgue (f ` S) = measure lebesgue S" |
622 proof - |
415 proof - |
635 "(\<And>n::nat. closed (F n)) \<Longrightarrow> fsigma (\<Union>(F ` UNIV))" |
428 "(\<And>n::nat. closed (F n)) \<Longrightarrow> fsigma (\<Union>(F ` UNIV))" |
636 |
429 |
637 inductive%important gdelta :: "'a::topological_space set \<Rightarrow> bool" where |
430 inductive%important gdelta :: "'a::topological_space set \<Rightarrow> bool" where |
638 "(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (\<Inter>(F ` UNIV))" |
431 "(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (\<Inter>(F ` UNIV))" |
639 |
432 |
640 proposition fsigma_Union_compact: |
433 lemma%important fsigma_Union_compact: |
641 fixes S :: "'a::{real_normed_vector,heine_borel} set" |
434 fixes S :: "'a::{real_normed_vector,heine_borel} set" |
642 shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = \<Union>(F ` UNIV))" |
435 shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = \<Union>(F ` UNIV))" |
643 proof safe |
436 proof%unimportant safe |
644 assume "fsigma S" |
437 assume "fsigma S" |
645 then obtain F :: "nat \<Rightarrow> 'a set" where F: "range F \<subseteq> Collect closed" "S = \<Union>(F ` UNIV)" |
438 then obtain F :: "nat \<Rightarrow> 'a set" where F: "range F \<subseteq> Collect closed" "S = \<Union>(F ` UNIV)" |
646 by (meson fsigma.cases image_subsetI mem_Collect_eq) |
439 by (meson fsigma.cases image_subsetI mem_Collect_eq) |
647 then have "\<exists>D::nat \<Rightarrow> 'a set. range D \<subseteq> Collect compact \<and> \<Union>(D ` UNIV) = F i" for i |
440 then have "\<exists>D::nat \<Rightarrow> 'a set. range D \<subseteq> Collect compact \<and> \<Union>(D ` UNIV) = F i" for i |
648 using closed_Union_compact_subsets [of "F i"] |
441 using closed_Union_compact_subsets [of "F i"] |
669 assume "range F \<subseteq> Collect compact" and "S = \<Union>(F ` UNIV)" |
462 assume "range F \<subseteq> Collect compact" and "S = \<Union>(F ` UNIV)" |
670 then show "fsigma (\<Union>(F ` UNIV))" |
463 then show "fsigma (\<Union>(F ` UNIV))" |
671 by (simp add: compact_imp_closed fsigma.intros image_subset_iff) |
464 by (simp add: compact_imp_closed fsigma.intros image_subset_iff) |
672 qed |
465 qed |
673 |
466 |
674 lemma gdelta_imp_fsigma: "gdelta S \<Longrightarrow> fsigma (- S)" |
467 lemma%unimportant gdelta_imp_fsigma: "gdelta S \<Longrightarrow> fsigma (- S)" |
675 proof (induction rule: gdelta.induct) |
468 proof (induction rule: gdelta.induct) |
676 case (1 F) |
469 case (1 F) |
677 have "- \<Inter>(F ` UNIV) = (\<Union>i. -(F i))" |
470 have "- \<Inter>(F ` UNIV) = (\<Union>i. -(F i))" |
678 by auto |
471 by auto |
679 then show ?case |
472 then show ?case |
680 by (simp add: fsigma.intros closed_Compl 1) |
473 by (simp add: fsigma.intros closed_Compl 1) |
681 qed |
474 qed |
682 |
475 |
683 lemma fsigma_imp_gdelta: "fsigma S \<Longrightarrow> gdelta (- S)" |
476 lemma%unimportant fsigma_imp_gdelta: "fsigma S \<Longrightarrow> gdelta (- S)" |
684 proof (induction rule: fsigma.induct) |
477 proof (induction rule: fsigma.induct) |
685 case (1 F) |
478 case (1 F) |
686 have "- \<Union>(F ` UNIV) = (\<Inter>i. -(F i))" |
479 have "- \<Union>(F ` UNIV) = (\<Inter>i. -(F i))" |
687 by auto |
480 by auto |
688 then show ?case |
481 then show ?case |
689 by (simp add: 1 gdelta.intros open_closed) |
482 by (simp add: 1 gdelta.intros open_closed) |
690 qed |
483 qed |
691 |
484 |
692 lemma gdelta_complement: "gdelta(- S) \<longleftrightarrow> fsigma S" |
485 lemma%unimportant gdelta_complement: "gdelta(- S) \<longleftrightarrow> fsigma S" |
693 using fsigma_imp_gdelta gdelta_imp_fsigma by force |
486 using fsigma_imp_gdelta gdelta_imp_fsigma by force |
694 |
487 |
695 text\<open>A Lebesgue set is almost an \<open>F_sigma\<close> or \<open>G_delta\<close>.\<close> |
488 text\<open>A Lebesgue set is almost an \<open>F_sigma\<close> or \<open>G_delta\<close>.\<close> |
696 lemma lebesgue_set_almost_fsigma: |
489 lemma%unimportant lebesgue_set_almost_fsigma: |
697 assumes "S \<in> sets lebesgue" |
490 assumes "S \<in> sets lebesgue" |
698 obtains C T where "fsigma C" "negligible T" "C \<union> T = S" "disjnt C T" |
491 obtains C T where "fsigma C" "negligible T" "C \<union> T = S" "disjnt C T" |
699 proof - |
492 proof - |
700 { fix n::nat |
493 { fix n::nat |
701 have "\<exists>T. closed T \<and> T \<subseteq> S \<and> S - T \<in> lmeasurable \<and> measure lebesgue (S-T) < 1 / Suc n" |
494 have "\<exists>T. closed T \<and> T \<subseteq> S \<and> S - T \<in> lmeasurable \<and> measure lebesgue (S-T) < 1 / Suc n" |
726 show "disjnt ?C (S - ?C)" |
519 show "disjnt ?C (S - ?C)" |
727 by (auto simp: disjnt_def) |
520 by (auto simp: disjnt_def) |
728 qed |
521 qed |
729 qed |
522 qed |
730 |
523 |
731 lemma lebesgue_set_almost_gdelta: |
524 lemma%unimportant lebesgue_set_almost_gdelta: |
732 assumes "S \<in> sets lebesgue" |
525 assumes "S \<in> sets lebesgue" |
733 obtains C T where "gdelta C" "negligible T" "S \<union> T = C" "disjnt S T" |
526 obtains C T where "gdelta C" "negligible T" "S \<union> T = C" "disjnt S T" |
734 proof - |
527 proof - |
735 have "-S \<in> sets lebesgue" |
528 have "-S \<in> sets lebesgue" |
736 using assms Compl_in_sets_lebesgue by blast |
529 using assms Compl_in_sets_lebesgue by blast |
744 using C by (auto simp: disjnt_def) |
537 using C by (auto simp: disjnt_def) |
745 qed (use C in auto) |
538 qed (use C in auto) |
746 qed |
539 qed |
747 |
540 |
748 |
541 |
749 proposition measure_semicontinuous_with_hausdist_explicit: |
542 proposition%important measure_semicontinuous_with_hausdist_explicit: |
750 assumes "bounded S" and neg: "negligible(frontier S)" and "e > 0" |
543 assumes "bounded S" and neg: "negligible(frontier S)" and "e > 0" |
751 obtains d where "d > 0" |
544 obtains d where "d > 0" |
752 "\<And>T. \<lbrakk>T \<in> lmeasurable; \<And>y. y \<in> T \<Longrightarrow> \<exists>x. x \<in> S \<and> dist x y < d\<rbrakk> |
545 "\<And>T. \<lbrakk>T \<in> lmeasurable; \<And>y. y \<in> T \<Longrightarrow> \<exists>x. x \<in> S \<and> dist x y < d\<rbrakk> |
753 \<Longrightarrow> measure lebesgue T < measure lebesgue S + e" |
546 \<Longrightarrow> measure lebesgue T < measure lebesgue S + e" |
754 proof (cases "S = {}") |
547 proof%unimportant (cases "S = {}") |
755 case True |
548 case True |
756 with that \<open>e > 0\<close> show ?thesis by force |
549 with that \<open>e > 0\<close> show ?thesis by force |
757 next |
550 next |
758 case False |
551 case False |
759 then have frS: "frontier S \<noteq> {}" |
552 then have frS: "frontier S \<noteq> {}" |
813 with mU show "measure lebesgue T < measure lebesgue S + e" |
606 with mU show "measure lebesgue T < measure lebesgue S + e" |
814 by linarith |
607 by linarith |
815 qed |
608 qed |
816 qed |
609 qed |
817 |
610 |
818 proposition lebesgue_regular_inner: |
611 proposition%important lebesgue_regular_inner: |
819 assumes "S \<in> sets lebesgue" |
612 assumes "S \<in> sets lebesgue" |
820 obtains K C where "negligible K" "\<And>n::nat. compact(C n)" "S = (\<Union>n. C n) \<union> K" |
613 obtains K C where "negligible K" "\<And>n::nat. compact(C n)" "S = (\<Union>n. C n) \<union> K" |
821 proof - |
614 proof%unimportant - |
822 have "\<exists>T. closed T \<and> T \<subseteq> S \<and> (S - T) \<in> lmeasurable \<and> measure lebesgue (S - T) < (1/2)^n" for n |
615 have "\<exists>T. closed T \<and> T \<subseteq> S \<and> (S - T) \<in> lmeasurable \<and> measure lebesgue (S - T) < (1/2)^n" for n |
823 using sets_lebesgue_inner_closed assms |
616 using sets_lebesgue_inner_closed assms |
824 by (metis sets_lebesgue_inner_closed zero_less_divide_1_iff zero_less_numeral zero_less_power) |
617 by (metis sets_lebesgue_inner_closed zero_less_divide_1_iff zero_less_numeral zero_less_power) |
825 then obtain C where clo: "\<And>n. closed (C n)" and subS: "\<And>n. C n \<subseteq> S" |
618 then obtain C where clo: "\<And>n. closed (C n)" and subS: "\<And>n. C n \<subseteq> S" |
826 and mea: "\<And>n. (S - C n) \<in> lmeasurable" |
619 and mea: "\<And>n. (S - C n) \<in> lmeasurable" |
866 qed |
659 qed |
867 qed |
660 qed |
868 qed |
661 qed |
869 |
662 |
870 |
663 |
871 lemma sets_lebesgue_continuous_image: |
664 lemma%unimportant sets_lebesgue_continuous_image: |
872 assumes T: "T \<in> sets lebesgue" and contf: "continuous_on S f" |
665 assumes T: "T \<in> sets lebesgue" and contf: "continuous_on S f" |
873 and negim: "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible(f ` T)" and "T \<subseteq> S" |
666 and negim: "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible(f ` T)" and "T \<subseteq> S" |
874 shows "f ` T \<in> sets lebesgue" |
667 shows "f ` T \<in> sets lebesgue" |
875 proof - |
668 proof - |
876 obtain K C where "negligible K" and com: "\<And>n::nat. compact(C n)" and Teq: "T = (\<Union>n. C n) \<union> K" |
669 obtain K C where "negligible K" and com: "\<And>n::nat. compact(C n)" and Teq: "T = (\<Union>n. C n) \<union> K" |
891 qed |
684 qed |
892 then show ?thesis |
685 then show ?thesis |
893 by (simp add: Teq image_Un image_Union) |
686 by (simp add: Teq image_Un image_Union) |
894 qed |
687 qed |
895 |
688 |
896 lemma differentiable_image_in_sets_lebesgue: |
689 lemma%unimportant differentiable_image_in_sets_lebesgue: |
897 fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space" |
690 fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space" |
898 assumes S: "S \<in> sets lebesgue" and dim: "DIM('m) \<le> DIM('n)" and f: "f differentiable_on S" |
691 assumes S: "S \<in> sets lebesgue" and dim: "DIM('m) \<le> DIM('n)" and f: "f differentiable_on S" |
899 shows "f`S \<in> sets lebesgue" |
692 shows "f`S \<in> sets lebesgue" |
900 proof (rule sets_lebesgue_continuous_image [OF S]) |
693 proof (rule sets_lebesgue_continuous_image [OF S]) |
901 show "continuous_on S f" |
694 show "continuous_on S f" |
903 show "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible (f ` T)" |
696 show "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible (f ` T)" |
904 using differentiable_on_subset f |
697 using differentiable_on_subset f |
905 by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim]) |
698 by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim]) |
906 qed auto |
699 qed auto |
907 |
700 |
908 lemma sets_lebesgue_on_continuous_image: |
701 lemma%unimportant sets_lebesgue_on_continuous_image: |
909 assumes S: "S \<in> sets lebesgue" and X: "X \<in> sets (lebesgue_on S)" and contf: "continuous_on S f" |
702 assumes S: "S \<in> sets lebesgue" and X: "X \<in> sets (lebesgue_on S)" and contf: "continuous_on S f" |
910 and negim: "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible(f ` T)" |
703 and negim: "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible(f ` T)" |
911 shows "f ` X \<in> sets (lebesgue_on (f ` S))" |
704 shows "f ` X \<in> sets (lebesgue_on (f ` S))" |
912 proof - |
705 proof - |
913 have "X \<subseteq> S" |
706 have "X \<subseteq> S" |
918 by (metis S X contf negim sets_lebesgue_continuous_image sets_restrict_space_iff space_restrict_space space_restrict_space2) |
711 by (metis S X contf negim sets_lebesgue_continuous_image sets_restrict_space_iff space_restrict_space space_restrict_space2) |
919 ultimately show ?thesis |
712 ultimately show ?thesis |
920 by (auto simp: sets_restrict_space_iff) |
713 by (auto simp: sets_restrict_space_iff) |
921 qed |
714 qed |
922 |
715 |
923 lemma differentiable_image_in_sets_lebesgue_on: |
716 lemma%unimportant differentiable_image_in_sets_lebesgue_on: |
924 fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space" |
717 fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space" |
925 assumes S: "S \<in> sets lebesgue" and X: "X \<in> sets (lebesgue_on S)" and dim: "DIM('m) \<le> DIM('n)" |
718 assumes S: "S \<in> sets lebesgue" and X: "X \<in> sets (lebesgue_on S)" and dim: "DIM('m) \<le> DIM('n)" |
926 and f: "f differentiable_on S" |
719 and f: "f differentiable_on S" |
927 shows "f ` X \<in> sets (lebesgue_on (f`S))" |
720 shows "f ` X \<in> sets (lebesgue_on (f`S))" |
928 proof (rule sets_lebesgue_on_continuous_image [OF S X]) |
721 proof (rule sets_lebesgue_on_continuous_image [OF S X]) |
932 using differentiable_on_subset f |
725 using differentiable_on_subset f |
933 by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim]) |
726 by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim]) |
934 qed |
727 qed |
935 |
728 |
936 |
729 |
937 proposition (*FIX needs name *) |
730 proposition%important |
938 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
731 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
939 assumes S: "S \<in> lmeasurable" |
732 assumes S: "S \<in> lmeasurable" |
940 and deriv: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
733 and deriv: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
941 and int: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S" |
734 and int: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S" |
942 and bounded: "\<And>x. x \<in> S \<Longrightarrow> \<bar>det (matrix (f' x))\<bar> \<le> B" |
735 and bounded: "\<And>x. x \<in> S \<Longrightarrow> \<bar>det (matrix (f' x))\<bar> \<le> B" |
943 shows measurable_bounded_differentiable_image: |
736 shows measurable_bounded_differentiable_image: |
944 "f ` S \<in> lmeasurable" |
737 "f ` S \<in> lmeasurable" |
945 and measure_bounded_differentiable_image: |
738 and measure_bounded_differentiable_image: |
946 "measure lebesgue (f ` S) \<le> B * measure lebesgue S" (is "?M") |
739 "measure lebesgue (f ` S) \<le> B * measure lebesgue S" (is "?M") |
947 proof - |
740 proof%unimportant - |
948 have "f ` S \<in> lmeasurable \<and> measure lebesgue (f ` S) \<le> B * measure lebesgue S" |
741 have "f ` S \<in> lmeasurable \<and> measure lebesgue (f ` S) \<le> B * measure lebesgue S" |
949 proof (cases "B < 0") |
742 proof (cases "B < 0") |
950 case True |
743 case True |
951 then have "S = {}" |
744 then have "S = {}" |
952 by (meson abs_ge_zero bounded empty_iff equalityI less_le_trans linorder_not_less subsetI) |
745 by (meson abs_ge_zero bounded empty_iff equalityI less_le_trans linorder_not_less subsetI) |
1168 qed |
961 qed |
1169 qed |
962 qed |
1170 then show "f ` S \<in> lmeasurable" ?M by blast+ |
963 then show "f ` S \<in> lmeasurable" ?M by blast+ |
1171 qed |
964 qed |
1172 |
965 |
1173 proposition (*FIX needs name *) |
966 lemma%important |
1174 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
967 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
1175 assumes S: "S \<in> lmeasurable" |
968 assumes S: "S \<in> lmeasurable" |
1176 and deriv: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
969 and deriv: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
1177 and int: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S" |
970 and int: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S" |
1178 shows m_diff_image_weak: "f ` S \<in> lmeasurable \<and> measure lebesgue (f ` S) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" |
971 shows m_diff_image_weak: "f ` S \<in> lmeasurable \<and> measure lebesgue (f ` S) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" |
1179 proof - |
972 proof%unimportant - |
1180 let ?\<mu> = "measure lebesgue" |
973 let ?\<mu> = "measure lebesgue" |
1181 have aint_S: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) absolutely_integrable_on S" |
974 have aint_S: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) absolutely_integrable_on S" |
1182 using int unfolding absolutely_integrable_on_def by auto |
975 using int unfolding absolutely_integrable_on_def by auto |
1183 define m where "m \<equiv> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" |
976 define m where "m \<equiv> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" |
1184 have *: "f ` S \<in> lmeasurable" "?\<mu> (f ` S) \<le> m + e * ?\<mu> S" |
977 have *: "f ` S \<in> lmeasurable" "?\<mu> (f ` S) \<le> m + e * ?\<mu> S" |
1366 by fastforce |
1159 by fastforce |
1367 qed |
1160 qed |
1368 qed |
1161 qed |
1369 |
1162 |
1370 |
1163 |
1371 theorem (*FIX needs name *) |
1164 theorem%important |
1372 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
1165 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
1373 assumes S: "S \<in> sets lebesgue" |
1166 assumes S: "S \<in> sets lebesgue" |
1374 and deriv: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
1167 and deriv: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
1375 and int: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S" |
1168 and int: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S" |
1376 shows measurable_differentiable_image: "f ` S \<in> lmeasurable" |
1169 shows measurable_differentiable_image: "f ` S \<in> lmeasurable" |
1377 and measure_differentiable_image: |
1170 and measure_differentiable_image: |
1378 "measure lebesgue (f ` S) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" (is "?M") |
1171 "measure lebesgue (f ` S) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" (is "?M") |
1379 proof - |
1172 proof%unimportant - |
1380 let ?I = "\<lambda>n::nat. cbox (vec (-n)) (vec n) \<inter> S" |
1173 let ?I = "\<lambda>n::nat. cbox (vec (-n)) (vec n) \<inter> S" |
1381 let ?\<mu> = "measure lebesgue" |
1174 let ?\<mu> = "measure lebesgue" |
1382 have "x \<in> cbox (vec (- real (nat \<lceil>norm x\<rceil>))) (vec (real (nat \<lceil>norm x\<rceil>)))" for x :: "real^'n::_" |
1175 have "x \<in> cbox (vec (- real (nat \<lceil>norm x\<rceil>))) (vec (real (nat \<lceil>norm x\<rceil>)))" for x :: "real^'n::_" |
1383 apply (auto simp: mem_box_cart) |
1176 apply (auto simp: mem_box_cart) |
1384 apply (metis abs_le_iff component_le_norm_cart minus_le_iff of_nat_ceiling order.trans) |
1177 apply (metis abs_le_iff component_le_norm_cart minus_le_iff of_nat_ceiling order.trans) |
1419 then show "f ` S \<in> lmeasurable" ?M |
1212 then show "f ` S \<in> lmeasurable" ?M |
1420 by (metis Seq image_UN)+ |
1213 by (metis Seq image_UN)+ |
1421 qed |
1214 qed |
1422 |
1215 |
1423 |
1216 |
1424 lemma borel_measurable_simple_function_limit_increasing: |
1217 lemma%unimportant borel_measurable_simple_function_limit_increasing: |
1425 fixes f :: "'a::euclidean_space \<Rightarrow> real" |
1218 fixes f :: "'a::euclidean_space \<Rightarrow> real" |
1426 shows "(f \<in> borel_measurable lebesgue \<and> (\<forall>x. 0 \<le> f x)) \<longleftrightarrow> |
1219 shows "(f \<in> borel_measurable lebesgue \<and> (\<forall>x. 0 \<le> f x)) \<longleftrightarrow> |
1427 (\<exists>g. (\<forall>n x. 0 \<le> g n x \<and> g n x \<le> f x) \<and> (\<forall>n x. g n x \<le> (g(Suc n) x)) \<and> |
1220 (\<exists>g. (\<forall>n x. 0 \<le> g n x \<and> g n x \<le> f x) \<and> (\<forall>n x. g n x \<le> (g(Suc n) x)) \<and> |
1428 (\<forall>n. g n \<in> borel_measurable lebesgue) \<and> (\<forall>n. finite(range (g n))) \<and> |
1221 (\<forall>n. g n \<in> borel_measurable lebesgue) \<and> (\<forall>n. finite(range (g n))) \<and> |
1429 (\<forall>x. (\<lambda>n. g n x) \<longlonglongrightarrow> f x))" |
1222 (\<forall>x. (\<lambda>n. g n x) \<longlonglongrightarrow> f x))" |
1618 by (blast intro: order_trans) |
1411 by (blast intro: order_trans) |
1619 qed |
1412 qed |
1620 |
1413 |
1621 subsection%important\<open>Borel measurable Jacobian determinant\<close> |
1414 subsection%important\<open>Borel measurable Jacobian determinant\<close> |
1622 |
1415 |
1623 lemma lemma_partial_derivatives0: |
1416 lemma%unimportant lemma_partial_derivatives0: |
1624 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
1417 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
1625 assumes "linear f" and lim0: "((\<lambda>x. f x /\<^sub>R norm x) \<longlongrightarrow> 0) (at 0 within S)" |
1418 assumes "linear f" and lim0: "((\<lambda>x. f x /\<^sub>R norm x) \<longlongrightarrow> 0) (at 0 within S)" |
1626 and lb: "\<And>v. v \<noteq> 0 \<Longrightarrow> (\<exists>k>0. \<forall>e>0. \<exists>x. x \<in> S - {0} \<and> norm x < e \<and> k * norm x \<le> \<bar>v \<bullet> x\<bar>)" |
1419 and lb: "\<And>v. v \<noteq> 0 \<Longrightarrow> (\<exists>k>0. \<forall>e>0. \<exists>x. x \<in> S - {0} \<and> norm x < e \<and> k * norm x \<le> \<bar>v \<bullet> x\<bar>)" |
1627 shows "f x = 0" |
1420 shows "f x = 0" |
1628 proof - |
1421 proof - |
1691 using dim_eq_full |
1484 using dim_eq_full |
1692 by (metis (mono_tags, lifting) eq_0_on_span eucl.span_Basis linear_axioms linear_eq_stdbasis |
1485 by (metis (mono_tags, lifting) eq_0_on_span eucl.span_Basis linear_axioms linear_eq_stdbasis |
1693 mem_Collect_eq module_hom_zero span_base span_raw_def) |
1486 mem_Collect_eq module_hom_zero span_base span_raw_def) |
1694 qed |
1487 qed |
1695 |
1488 |
1696 lemma lemma_partial_derivatives: |
1489 lemma%unimportant lemma_partial_derivatives: |
1697 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
1490 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
1698 assumes "linear f" and lim: "((\<lambda>x. f (x - a) /\<^sub>R norm (x - a)) \<longlongrightarrow> 0) (at a within S)" |
1491 assumes "linear f" and lim: "((\<lambda>x. f (x - a) /\<^sub>R norm (x - a)) \<longlongrightarrow> 0) (at a within S)" |
1699 and lb: "\<And>v. v \<noteq> 0 \<Longrightarrow> (\<exists>k>0. \<forall>e>0. \<exists>x \<in> S - {a}. norm(a - x) < e \<and> k * norm(a - x) \<le> \<bar>v \<bullet> (x - a)\<bar>)" |
1492 and lb: "\<And>v. v \<noteq> 0 \<Longrightarrow> (\<exists>k>0. \<forall>e>0. \<exists>x \<in> S - {a}. norm(a - x) < e \<and> k * norm(a - x) \<le> \<bar>v \<bullet> (x - a)\<bar>)" |
1700 shows "f x = 0" |
1493 shows "f x = 0" |
1701 proof - |
1494 proof - |
1709 using lb [OF v] by (force simp: norm_minus_commute) |
1502 using lb [OF v] by (force simp: norm_minus_commute) |
1710 qed |
1503 qed |
1711 qed |
1504 qed |
1712 |
1505 |
1713 |
1506 |
1714 proposition borel_measurable_partial_derivatives: |
1507 proposition%important borel_measurable_partial_derivatives: |
1715 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" |
1508 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" |
1716 assumes S: "S \<in> sets lebesgue" |
1509 assumes S: "S \<in> sets lebesgue" |
1717 and f: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
1510 and f: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
1718 shows "(\<lambda>x. (matrix(f' x)$m$n)) \<in> borel_measurable (lebesgue_on S)" |
1511 shows "(\<lambda>x. (matrix(f' x)$m$n)) \<in> borel_measurable (lebesgue_on S)" |
1719 proof - |
1512 proof%unimportant - |
1720 have contf: "continuous_on S f" |
1513 have contf: "continuous_on S f" |
1721 using continuous_on_eq_continuous_within f has_derivative_continuous by blast |
1514 using continuous_on_eq_continuous_within f has_derivative_continuous by blast |
1722 have "{x \<in> S. (matrix (f' x)$m$n) \<le> b} \<in> sets lebesgue" for b |
1515 have "{x \<in> S. (matrix (f' x)$m$n) \<le> b} \<in> sets lebesgue" for b |
1723 proof (rule sets_negligible_symdiff) |
1516 proof (rule sets_negligible_symdiff) |
1724 let ?T = "{x \<in> S. \<forall>e>0. \<exists>d>0. \<exists>A. A$m$n < b \<and> (\<forall>i j. A$i$j \<in> \<rat>) \<and> |
1517 let ?T = "{x \<in> S. \<forall>e>0. \<exists>d>0. \<exists>A. A$m$n < b \<and> (\<forall>i j. A$i$j \<in> \<rat>) \<and> |
2300 then show ?thesis |
2093 then show ?thesis |
2301 by (simp add: borel_measurable_vimage_halfspace_component_le sets_restrict_space_iff assms) |
2094 by (simp add: borel_measurable_vimage_halfspace_component_le sets_restrict_space_iff assms) |
2302 qed |
2095 qed |
2303 |
2096 |
2304 |
2097 |
2305 theorem borel_measurable_det_Jacobian: |
2098 theorem%important borel_measurable_det_Jacobian: |
2306 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
2099 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
2307 assumes S: "S \<in> sets lebesgue" and f: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
2100 assumes S: "S \<in> sets lebesgue" and f: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
2308 shows "(\<lambda>x. det(matrix(f' x))) \<in> borel_measurable (lebesgue_on S)" |
2101 shows "(\<lambda>x. det(matrix(f' x))) \<in> borel_measurable (lebesgue_on S)" |
2309 unfolding det_def |
2102 unfolding det_def |
2310 by%unimportant (intro measurable) (auto intro: f borel_measurable_partial_derivatives [OF S]) |
2103 by%unimportant (intro measurable) (auto intro: f borel_measurable_partial_derivatives [OF S]) |
2314 lemma%important borel_measurable_lebesgue_on_preimage_borel: |
2107 lemma%important borel_measurable_lebesgue_on_preimage_borel: |
2315 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
2108 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
2316 assumes "S \<in> sets lebesgue" |
2109 assumes "S \<in> sets lebesgue" |
2317 shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow> |
2110 shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow> |
2318 (\<forall>T. T \<in> sets borel \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets lebesgue)" |
2111 (\<forall>T. T \<in> sets borel \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets lebesgue)" |
2319 proof - |
2112 proof%unimportant - |
2320 have "{x. (if x \<in> S then f x else 0) \<in> T} \<in> sets lebesgue \<longleftrightarrow> {x \<in> S. f x \<in> T} \<in> sets lebesgue" |
2113 have "{x. (if x \<in> S then f x else 0) \<in> T} \<in> sets lebesgue \<longleftrightarrow> {x \<in> S. f x \<in> T} \<in> sets lebesgue" |
2321 if "T \<in> sets borel" for T |
2114 if "T \<in> sets borel" for T |
2322 proof (cases "0 \<in> T") |
2115 proof (cases "0 \<in> T") |
2323 case True |
2116 case True |
2324 then have "{x \<in> S. f x \<in> T} = {x. (if x \<in> S then f x else 0) \<in> T} \<inter> S" |
2117 then have "{x \<in> S. f x \<in> T} = {x. (if x \<in> S then f x else 0) \<in> T} \<inter> S" |
2336 then show ?thesis |
2129 then show ?thesis |
2337 unfolding borel_measurable_lebesgue_preimage_borel borel_measurable_UNIV [OF assms, symmetric] |
2130 unfolding borel_measurable_lebesgue_preimage_borel borel_measurable_UNIV [OF assms, symmetric] |
2338 by blast |
2131 by blast |
2339 qed |
2132 qed |
2340 |
2133 |
2341 lemma sets_lebesgue_almost_borel: |
2134 lemma%unimportant sets_lebesgue_almost_borel: |
2342 assumes "S \<in> sets lebesgue" |
2135 assumes "S \<in> sets lebesgue" |
2343 obtains B N where "B \<in> sets borel" "negligible N" "B \<union> N = S" |
2136 obtains B N where "B \<in> sets borel" "negligible N" "B \<union> N = S" |
2344 proof - |
2137 proof - |
2345 obtain T N N' where "S = T \<union> N" "N \<subseteq> N'" "N' \<in> null_sets lborel" "T \<in> sets borel" |
2138 obtain T N N' where "S = T \<union> N" "N \<subseteq> N'" "N' \<in> null_sets lborel" "T \<in> sets borel" |
2346 using sets_completionE [OF assms] by auto |
2139 using sets_completionE [OF assms] by auto |
2347 then show thesis |
2140 then show thesis |
2348 by (metis negligible_iff_null_sets negligible_subset null_sets_completionI that) |
2141 by (metis negligible_iff_null_sets negligible_subset null_sets_completionI that) |
2349 qed |
2142 qed |
2350 |
2143 |
2351 lemma double_lebesgue_sets: |
2144 lemma%unimportant double_lebesgue_sets: |
2352 assumes S: "S \<in> sets lebesgue" and T: "T \<in> sets lebesgue" and fim: "f ` S \<subseteq> T" |
2145 assumes S: "S \<in> sets lebesgue" and T: "T \<in> sets lebesgue" and fim: "f ` S \<subseteq> T" |
2353 shows "(\<forall>U. U \<in> sets lebesgue \<and> U \<subseteq> T \<longrightarrow> {x \<in> S. f x \<in> U} \<in> sets lebesgue) \<longleftrightarrow> |
2146 shows "(\<forall>U. U \<in> sets lebesgue \<and> U \<subseteq> T \<longrightarrow> {x \<in> S. f x \<in> U} \<in> sets lebesgue) \<longleftrightarrow> |
2354 f \<in> borel_measurable (lebesgue_on S) \<and> |
2147 f \<in> borel_measurable (lebesgue_on S) \<and> |
2355 (\<forall>U. negligible U \<and> U \<subseteq> T \<longrightarrow> {x \<in> S. f x \<in> U} \<in> sets lebesgue)" |
2148 (\<forall>U. negligible U \<and> U \<subseteq> T \<longrightarrow> {x \<in> S. f x \<in> U} \<in> sets lebesgue)" |
2356 (is "?lhs \<longleftrightarrow> _ \<and> ?rhs") |
2149 (is "?lhs \<longleftrightarrow> _ \<and> ?rhs") |
2391 qed |
2184 qed |
2392 |
2185 |
2393 |
2186 |
2394 subsection%important\<open>Simplest case of Sard's theorem (we don't need continuity of derivative)\<close> |
2187 subsection%important\<open>Simplest case of Sard's theorem (we don't need continuity of derivative)\<close> |
2395 |
2188 |
2396 lemma Sard_lemma00: |
2189 lemma%important Sard_lemma00: |
2397 fixes P :: "'b::euclidean_space set" |
2190 fixes P :: "'b::euclidean_space set" |
2398 assumes "a \<ge> 0" and a: "a *\<^sub>R i \<noteq> 0" and i: "i \<in> Basis" |
2191 assumes "a \<ge> 0" and a: "a *\<^sub>R i \<noteq> 0" and i: "i \<in> Basis" |
2399 and P: "P \<subseteq> {x. a *\<^sub>R i \<bullet> x = 0}" |
2192 and P: "P \<subseteq> {x. a *\<^sub>R i \<bullet> x = 0}" |
2400 and "0 \<le> m" "0 \<le> e" |
2193 and "0 \<le> m" "0 \<le> e" |
2401 obtains S where "S \<in> lmeasurable" |
2194 obtains S where "S \<in> lmeasurable" |
2402 and "{z. norm z \<le> m \<and> (\<exists>t \<in> P. norm(z - t) \<le> e)} \<subseteq> S" |
2195 and "{z. norm z \<le> m \<and> (\<exists>t \<in> P. norm(z - t) \<le> e)} \<subseteq> S" |
2403 and "measure lebesgue S \<le> (2 * e) * (2 * m) ^ (DIM('b) - 1)" |
2196 and "measure lebesgue S \<le> (2 * e) * (2 * m) ^ (DIM('b) - 1)" |
2404 proof - |
2197 proof%unimportant - |
2405 have "a > 0" |
2198 have "a > 0" |
2406 using assms by simp |
2199 using assms by simp |
2407 let ?v = "(\<Sum>j\<in>Basis. (if j = i then e else m) *\<^sub>R j)" |
2200 let ?v = "(\<Sum>j\<in>Basis. (if j = i then e else m) *\<^sub>R j)" |
2408 show thesis |
2201 show thesis |
2409 proof |
2202 proof |
2427 by (simp add: content_cbox [OF *] prod.distrib prod.If_cases Diff_eq [symmetric] 2) |
2220 by (simp add: content_cbox [OF *] prod.distrib prod.If_cases Diff_eq [symmetric] 2) |
2428 qed blast |
2221 qed blast |
2429 qed |
2222 qed |
2430 |
2223 |
2431 text\<open>As above, but reorienting the vector (HOL Light's @text{GEOM\_BASIS\_MULTIPLE\_TAC})\<close> |
2224 text\<open>As above, but reorienting the vector (HOL Light's @text{GEOM\_BASIS\_MULTIPLE\_TAC})\<close> |
2432 lemma Sard_lemma0: |
2225 lemma%unimportant Sard_lemma0: |
2433 fixes P :: "(real^'n::{finite,wellorder}) set" |
2226 fixes P :: "(real^'n::{finite,wellorder}) set" |
2434 assumes "a \<noteq> 0" |
2227 assumes "a \<noteq> 0" |
2435 and P: "P \<subseteq> {x. a \<bullet> x = 0}" and "0 \<le> m" "0 \<le> e" |
2228 and P: "P \<subseteq> {x. a \<bullet> x = 0}" and "0 \<le> m" "0 \<le> e" |
2436 obtains S where "S \<in> lmeasurable" |
2229 obtains S where "S \<in> lmeasurable" |
2437 and "{z. norm z \<le> m \<and> (\<exists>t \<in> P. norm(z - t) \<le> e)} \<subseteq> S" |
2230 and "{z. norm z \<le> m \<and> (\<exists>t \<in> P. norm(z - t) \<le> e)} \<subseteq> S" |
2487 using mS T by (simp add: S measure_orthogonal_image) |
2280 using mS T by (simp add: S measure_orthogonal_image) |
2488 qed |
2281 qed |
2489 qed |
2282 qed |
2490 |
2283 |
2491 text\<open>As above, but translating the sets (HOL Light's @text{GEN\_GEOM\_ORIGIN\_TAC})\<close> |
2284 text\<open>As above, but translating the sets (HOL Light's @text{GEN\_GEOM\_ORIGIN\_TAC})\<close> |
2492 lemma Sard_lemma1: |
2285 lemma%important Sard_lemma1: |
2493 fixes P :: "(real^'n::{finite,wellorder}) set" |
2286 fixes P :: "(real^'n::{finite,wellorder}) set" |
2494 assumes P: "dim P < CARD('n)" and "0 \<le> m" "0 \<le> e" |
2287 assumes P: "dim P < CARD('n)" and "0 \<le> m" "0 \<le> e" |
2495 obtains S where "S \<in> lmeasurable" |
2288 obtains S where "S \<in> lmeasurable" |
2496 and "{z. norm(z - w) \<le> m \<and> (\<exists>t \<in> P. norm(z - w - t) \<le> e)} \<subseteq> S" |
2289 and "{z. norm(z - w) \<le> m \<and> (\<exists>t \<in> P. norm(z - w - t) \<le> e)} \<subseteq> S" |
2497 and "measure lebesgue S \<le> (2 * e) * (2 * m) ^ (CARD('n) - 1)" |
2290 and "measure lebesgue S \<le> (2 * e) * (2 * m) ^ (CARD('n) - 1)" |
2498 proof - |
2291 proof%unimportant - |
2499 obtain a where "a \<noteq> 0" "P \<subseteq> {x. a \<bullet> x = 0}" |
2292 obtain a where "a \<noteq> 0" "P \<subseteq> {x. a \<bullet> x = 0}" |
2500 using lowdim_subset_hyperplane [of P] P span_base by auto |
2293 using lowdim_subset_hyperplane [of P] P span_base by auto |
2501 then obtain S where S: "S \<in> lmeasurable" |
2294 then obtain S where S: "S \<in> lmeasurable" |
2502 and subS: "{z. norm z \<le> m \<and> (\<exists>t \<in> P. norm(z - t) \<le> e)} \<subseteq> S" |
2295 and subS: "{z. norm z \<le> m \<and> (\<exists>t \<in> P. norm(z - t) \<le> e)} \<subseteq> S" |
2503 and mS: "measure lebesgue S \<le> (2 * e) * (2 * m) ^ (CARD('n) - 1)" |
2296 and mS: "measure lebesgue S \<le> (2 * e) * (2 * m) ^ (CARD('n) - 1)" |
2511 show "measure lebesgue ((+)w ` S) \<le> 2 * e * (2 * m) ^ (CARD('n) - 1)" |
2304 show "measure lebesgue ((+)w ` S) \<le> 2 * e * (2 * m) ^ (CARD('n) - 1)" |
2512 by (metis measure_translation mS) |
2305 by (metis measure_translation mS) |
2513 qed |
2306 qed |
2514 qed |
2307 qed |
2515 |
2308 |
2516 lemma Sard_lemma2: |
2309 lemma%important Sard_lemma2: |
2517 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n::{finite,wellorder}" |
2310 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n::{finite,wellorder}" |
2518 assumes mlen: "CARD('m) \<le> CARD('n)" (is "?m \<le> ?n") |
2311 assumes mlen: "CARD('m) \<le> CARD('n)" (is "?m \<le> ?n") |
2519 and "B > 0" "bounded S" |
2312 and "B > 0" "bounded S" |
2520 and derS: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
2313 and derS: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
2521 and rank: "\<And>x. x \<in> S \<Longrightarrow> rank(matrix(f' x)) < CARD('n)" |
2314 and rank: "\<And>x. x \<in> S \<Longrightarrow> rank(matrix(f' x)) < CARD('n)" |
2522 and B: "\<And>x. x \<in> S \<Longrightarrow> onorm(f' x) \<le> B" |
2315 and B: "\<And>x. x \<in> S \<Longrightarrow> onorm(f' x) \<le> B" |
2523 shows "negligible(f ` S)" |
2316 shows "negligible(f ` S)" |
2524 proof - |
2317 proof%unimportant - |
2525 have lin_f': "\<And>x. x \<in> S \<Longrightarrow> linear(f' x)" |
2318 have lin_f': "\<And>x. x \<in> S \<Longrightarrow> linear(f' x)" |
2526 using derS has_derivative_linear by blast |
2319 using derS has_derivative_linear by blast |
2527 show ?thesis |
2320 show ?thesis |
2528 proof (clarsimp simp add: negligible_outer_le) |
2321 proof (clarsimp simp add: negligible_outer_le) |
2529 fix e :: "real" |
2322 fix e :: "real" |
2726 qed |
2519 qed |
2727 qed |
2520 qed |
2728 qed |
2521 qed |
2729 |
2522 |
2730 |
2523 |
2731 theorem baby_Sard: |
2524 theorem%important baby_Sard: |
2732 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n::{finite,wellorder}" |
2525 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n::{finite,wellorder}" |
2733 assumes mlen: "CARD('m) \<le> CARD('n)" |
2526 assumes mlen: "CARD('m) \<le> CARD('n)" |
2734 and der: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
2527 and der: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
2735 and rank: "\<And>x. x \<in> S \<Longrightarrow> rank(matrix(f' x)) < CARD('n)" |
2528 and rank: "\<And>x. x \<in> S \<Longrightarrow> rank(matrix(f' x)) < CARD('n)" |
2736 shows "negligible(f ` S)" |
2529 shows "negligible(f ` S)" |
2737 proof - |
2530 proof%unimportant - |
2738 let ?U = "\<lambda>n. {x \<in> S. norm(x) \<le> n \<and> onorm(f' x) \<le> real n}" |
2531 let ?U = "\<lambda>n. {x \<in> S. norm(x) \<le> n \<and> onorm(f' x) \<le> real n}" |
2739 have "\<And>x. x \<in> S \<Longrightarrow> \<exists>n. norm x \<le> real n \<and> onorm (f' x) \<le> real n" |
2532 have "\<And>x. x \<in> S \<Longrightarrow> \<exists>n. norm x \<le> real n \<and> onorm (f' x) \<le> real n" |
2740 by (meson linear order_trans real_arch_simple) |
2533 by (meson linear order_trans real_arch_simple) |
2741 then have eq: "S = (\<Union>n. ?U n)" |
2534 then have eq: "S = (\<Union>n. ?U n)" |
2742 by auto |
2535 by auto |
2754 qed |
2547 qed |
2755 |
2548 |
2756 |
2549 |
2757 subsection%important\<open>A one-way version of change-of-variables not assuming injectivity. \<close> |
2550 subsection%important\<open>A one-way version of change-of-variables not assuming injectivity. \<close> |
2758 |
2551 |
2759 lemma integral_on_image_ubound_weak: |
2552 lemma%important integral_on_image_ubound_weak: |
2760 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" |
2553 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" |
2761 assumes S: "S \<in> sets lebesgue" |
2554 assumes S: "S \<in> sets lebesgue" |
2762 and f: "f \<in> borel_measurable (lebesgue_on (g ` S))" |
2555 and f: "f \<in> borel_measurable (lebesgue_on (g ` S))" |
2763 and nonneg_fg: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f(g x)" |
2556 and nonneg_fg: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f(g x)" |
2764 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
2557 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
2765 and det_int_fg: "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x)) integrable_on S" |
2558 and det_int_fg: "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x)) integrable_on S" |
2766 and meas_gim: "\<And>T. \<lbrakk>T \<subseteq> g ` S; T \<in> sets lebesgue\<rbrakk> \<Longrightarrow> {x \<in> S. g x \<in> T} \<in> sets lebesgue" |
2559 and meas_gim: "\<And>T. \<lbrakk>T \<subseteq> g ` S; T \<in> sets lebesgue\<rbrakk> \<Longrightarrow> {x \<in> S. g x \<in> T} \<in> sets lebesgue" |
2767 shows "f integrable_on (g ` S) \<and> |
2560 shows "f integrable_on (g ` S) \<and> |
2768 integral (g ` S) f \<le> integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x))" |
2561 integral (g ` S) f \<le> integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x))" |
2769 (is "_ \<and> _ \<le> ?b") |
2562 (is "_ \<and> _ \<le> ?b") |
2770 proof - |
2563 proof%unimportant - |
2771 let ?D = "\<lambda>x. \<bar>det (matrix (g' x))\<bar>" |
2564 let ?D = "\<lambda>x. \<bar>det (matrix (g' x))\<bar>" |
2772 have cont_g: "continuous_on S g" |
2565 have cont_g: "continuous_on S g" |
2773 using der_g has_derivative_continuous_on by blast |
2566 using der_g has_derivative_continuous_on by blast |
2774 have [simp]: "space (lebesgue_on S) = S" |
2567 have [simp]: "space (lebesgue_on S) = S" |
2775 by (simp add: S) |
2568 by (simp add: S) |
2943 ultimately show ?thesis |
2736 ultimately show ?thesis |
2944 by (auto intro: Lim_bounded) |
2737 by (auto intro: Lim_bounded) |
2945 qed |
2738 qed |
2946 |
2739 |
2947 |
2740 |
2948 lemma integral_on_image_ubound_nonneg: |
2741 lemma%important integral_on_image_ubound_nonneg: |
2949 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" |
2742 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" |
2950 assumes nonneg_fg: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f(g x)" |
2743 assumes nonneg_fg: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f(g x)" |
2951 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
2744 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
2952 and intS: "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x)) integrable_on S" |
2745 and intS: "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x)) integrable_on S" |
2953 shows "f integrable_on (g ` S) \<and> integral (g ` S) f \<le> integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x))" |
2746 shows "f integrable_on (g ` S) \<and> integral (g ` S) f \<le> integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x))" |
2954 (is "_ \<and> _ \<le> ?b") |
2747 (is "_ \<and> _ \<le> ?b") |
2955 proof - |
2748 proof%unimportant - |
2956 let ?D = "\<lambda>x. det (matrix (g' x))" |
2749 let ?D = "\<lambda>x. det (matrix (g' x))" |
2957 define S' where "S' \<equiv> {x \<in> S. ?D x * f(g x) \<noteq> 0}" |
2750 define S' where "S' \<equiv> {x \<in> S. ?D x * f(g x) \<noteq> 0}" |
2958 then have der_gS': "\<And>x. x \<in> S' \<Longrightarrow> (g has_derivative g' x) (at x within S')" |
2751 then have der_gS': "\<And>x. x \<in> S' \<Longrightarrow> (g has_derivative g' x) (at x within S')" |
2959 by (metis (mono_tags, lifting) der_g has_derivative_within_subset mem_Collect_eq subset_iff) |
2752 by (metis (mono_tags, lifting) der_g has_derivative_within_subset mem_Collect_eq subset_iff) |
2960 have "(\<lambda>x. if x \<in> S then \<bar>?D x\<bar> * f (g x) else 0) integrable_on UNIV" |
2753 have "(\<lambda>x. if x \<in> S then \<bar>?D x\<bar> * f (g x) else 0) integrable_on UNIV" |
3073 finally show "integral (g ` S) f \<le> ?b" . |
2866 finally show "integral (g ` S) f \<le> ?b" . |
3074 qed |
2867 qed |
3075 qed |
2868 qed |
3076 |
2869 |
3077 |
2870 |
3078 proposition absolutely_integrable_on_image_real: |
2871 lemma%unimportant absolutely_integrable_on_image_real: |
3079 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" and g :: "real^'n::_ \<Rightarrow> real^'n::_" |
2872 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" and g :: "real^'n::_ \<Rightarrow> real^'n::_" |
3080 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
2873 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3081 and intS: "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x)) absolutely_integrable_on S" |
2874 and intS: "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x)) absolutely_integrable_on S" |
3082 shows "f absolutely_integrable_on (g ` S)" |
2875 shows "f absolutely_integrable_on (g ` S)" |
3083 proof - |
2876 proof - |
3148 using absolutely_integrable_Un [OF N P] absolutely_integrable_restrict_UNIV [symmetric, where f=f] |
2941 using absolutely_integrable_Un [OF N P] absolutely_integrable_restrict_UNIV [symmetric, where f=f] |
3149 by simp |
2942 by simp |
3150 qed |
2943 qed |
3151 |
2944 |
3152 |
2945 |
3153 proposition absolutely_integrable_on_image: |
2946 proposition%important absolutely_integrable_on_image: |
3154 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
2947 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3155 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
2948 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3156 and intS: "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S" |
2949 and intS: "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S" |
3157 shows "f absolutely_integrable_on (g ` S)" |
2950 shows "f absolutely_integrable_on (g ` S)" |
3158 apply (rule absolutely_integrable_componentwise [OF absolutely_integrable_on_image_real [OF der_g]]) |
2951 apply (rule absolutely_integrable_componentwise [OF absolutely_integrable_on_image_real [OF der_g]]) |
3159 using%unimportant absolutely_integrable_component [OF intS] by%unimportant auto |
2952 using%unimportant absolutely_integrable_component [OF intS] by%unimportant auto |
3160 |
2953 |
3161 proposition integral_on_image_ubound: |
2954 proposition%important integral_on_image_ubound: |
3162 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" and g :: "real^'n::_ \<Rightarrow> real^'n::_" |
2955 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" and g :: "real^'n::_ \<Rightarrow> real^'n::_" |
3163 assumes"\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f(g x)" |
2956 assumes"\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f(g x)" |
3164 and "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
2957 and "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3165 and "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x)) integrable_on S" |
2958 and "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x)) integrable_on S" |
3166 shows "integral (g ` S) f \<le> integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x))" |
2959 shows "integral (g ` S) f \<le> integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x))" |
3170 subsection%important\<open>Change-of-variables theorem\<close> |
2963 subsection%important\<open>Change-of-variables theorem\<close> |
3171 |
2964 |
3172 text\<open>The classic change-of-variables theorem. We have two versions with quite general hypotheses, |
2965 text\<open>The classic change-of-variables theorem. We have two versions with quite general hypotheses, |
3173 the first that the transforming function has a continuous inverse, the second that the base set is |
2966 the first that the transforming function has a continuous inverse, the second that the base set is |
3174 Lebesgue measurable.\<close> |
2967 Lebesgue measurable.\<close> |
3175 lemma cov_invertible_nonneg_le: |
2968 lemma%unimportant cov_invertible_nonneg_le: |
3176 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" and g :: "real^'n::_ \<Rightarrow> real^'n::_" |
2969 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" and g :: "real^'n::_ \<Rightarrow> real^'n::_" |
3177 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
2970 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3178 and der_h: "\<And>y. y \<in> T \<Longrightarrow> (h has_derivative h' y) (at y within T)" |
2971 and der_h: "\<And>y. y \<in> T \<Longrightarrow> (h has_derivative h' y) (at y within T)" |
3179 and f0: "\<And>y. y \<in> T \<Longrightarrow> 0 \<le> f y" |
2972 and f0: "\<And>y. y \<in> T \<Longrightarrow> 0 \<le> f y" |
3180 and hg: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> h(g x) = x" |
2973 and hg: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> h(g x) = x" |
3241 using R by (simp add: Teq) |
3034 using R by (simp add: Teq) |
3242 qed |
3035 qed |
3243 qed |
3036 qed |
3244 |
3037 |
3245 |
3038 |
3246 lemma cov_invertible_nonneg_eq: |
3039 lemma%unimportant cov_invertible_nonneg_eq: |
3247 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" and g :: "real^'n::_ \<Rightarrow> real^'n::_" |
3040 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" and g :: "real^'n::_ \<Rightarrow> real^'n::_" |
3248 assumes "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3041 assumes "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3249 and "\<And>y. y \<in> T \<Longrightarrow> (h has_derivative h' y) (at y within T)" |
3042 and "\<And>y. y \<in> T \<Longrightarrow> (h has_derivative h' y) (at y within T)" |
3250 and "\<And>y. y \<in> T \<Longrightarrow> 0 \<le> f y" |
3043 and "\<And>y. y \<in> T \<Longrightarrow> 0 \<le> f y" |
3251 and "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> h(g x) = x" |
3044 and "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> h(g x) = x" |
3254 shows "((\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x)) has_integral b) S \<longleftrightarrow> (f has_integral b) T" |
3047 shows "((\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x)) has_integral b) S \<longleftrightarrow> (f has_integral b) T" |
3255 using cov_invertible_nonneg_le [OF assms] |
3048 using cov_invertible_nonneg_le [OF assms] |
3256 by (simp add: has_integral_iff) (meson eq_iff) |
3049 by (simp add: has_integral_iff) (meson eq_iff) |
3257 |
3050 |
3258 |
3051 |
3259 lemma cov_invertible_real: |
3052 lemma%unimportant cov_invertible_real: |
3260 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" and g :: "real^'n::_ \<Rightarrow> real^'n::_" |
3053 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" and g :: "real^'n::_ \<Rightarrow> real^'n::_" |
3261 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3054 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3262 and der_h: "\<And>y. y \<in> T \<Longrightarrow> (h has_derivative h' y) (at y within T)" |
3055 and der_h: "\<And>y. y \<in> T \<Longrightarrow> (h has_derivative h' y) (at y within T)" |
3263 and hg: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> h(g x) = x" |
3056 and hg: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> h(g x) = x" |
3264 and gh: "\<And>y. y \<in> T \<Longrightarrow> h y \<in> S \<and> g(h y) = y" |
3057 and gh: "\<And>y. y \<in> T \<Longrightarrow> h y \<in> S \<and> g(h y) = y" |
3420 qed |
3213 qed |
3421 qed |
3214 qed |
3422 qed |
3215 qed |
3423 |
3216 |
3424 |
3217 |
3425 lemma cv_inv_version3: |
3218 lemma%unimportant cv_inv_version3: |
3426 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3219 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3427 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3220 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3428 and der_h: "\<And>y. y \<in> T \<Longrightarrow> (h has_derivative h' y) (at y within T)" |
3221 and der_h: "\<And>y. y \<in> T \<Longrightarrow> (h has_derivative h' y) (at y within T)" |
3429 and hg: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> h(g x) = x" |
3222 and hg: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> h(g x) = x" |
3430 and gh: "\<And>y. y \<in> T \<Longrightarrow> h y \<in> S \<and> g(h y) = y" |
3223 and gh: "\<And>y. y \<in> T \<Longrightarrow> h y \<in> S \<and> g(h y) = y" |
3446 then show ?thesis |
3239 then show ?thesis |
3447 using absolutely_integrable_on_def by blast |
3240 using absolutely_integrable_on_def by blast |
3448 qed |
3241 qed |
3449 |
3242 |
3450 |
3243 |
3451 lemma cv_inv_version4: |
3244 lemma%unimportant cv_inv_version4: |
3452 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3245 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3453 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S) \<and> invertible(matrix(g' x))" |
3246 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S) \<and> invertible(matrix(g' x))" |
3454 and hg: "\<And>x. x \<in> S \<Longrightarrow> continuous_on (g ` S) h \<and> h(g x) = x" |
3247 and hg: "\<And>x. x \<in> S \<Longrightarrow> continuous_on (g ` S) h \<and> h(g x) = x" |
3455 shows "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and> |
3248 shows "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and> |
3456 integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) = b |
3249 integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) = b |
3471 by (force simp: continuous_on_eq_continuous_within intro!: has_derivative_inverse_within) |
3264 by (force simp: continuous_on_eq_continuous_within intro!: has_derivative_inverse_within) |
3472 qed (use h' hg in auto) |
3265 qed (use h' hg in auto) |
3473 qed |
3266 qed |
3474 |
3267 |
3475 |
3268 |
3476 proposition has_absolute_integral_change_of_variables_invertible: |
3269 proposition%important has_absolute_integral_change_of_variables_invertible: |
3477 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3270 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3478 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3271 assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3479 and hg: "\<And>x. x \<in> S \<Longrightarrow> h(g x) = x" |
3272 and hg: "\<And>x. x \<in> S \<Longrightarrow> h(g x) = x" |
3480 and conth: "continuous_on (g ` S) h" |
3273 and conth: "continuous_on (g ` S) h" |
3481 shows "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and> integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) = b \<longleftrightarrow> |
3274 shows "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and> integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) = b \<longleftrightarrow> |
3482 f absolutely_integrable_on (g ` S) \<and> integral (g ` S) f = b" |
3275 f absolutely_integrable_on (g ` S) \<and> integral (g ` S) f = b" |
3483 (is "?lhs = ?rhs") |
3276 (is "?lhs = ?rhs") |
3484 proof - |
3277 proof%unimportant - |
3485 let ?S = "{x \<in> S. invertible (matrix (g' x))}" and ?D = "\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)" |
3278 let ?S = "{x \<in> S. invertible (matrix (g' x))}" and ?D = "\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)" |
3486 have *: "?D absolutely_integrable_on ?S \<and> integral ?S ?D = b |
3279 have *: "?D absolutely_integrable_on ?S \<and> integral ?S ?D = b |
3487 \<longleftrightarrow> f absolutely_integrable_on (g ` ?S) \<and> integral (g ` ?S) f = b" |
3280 \<longleftrightarrow> f absolutely_integrable_on (g ` ?S) \<and> integral (g ` ?S) f = b" |
3488 proof (rule cv_inv_version4) |
3281 proof (rule cv_inv_version4) |
3489 show "(g has_derivative g' x) (at x within ?S) \<and> invertible (matrix (g' x))" |
3282 show "(g has_derivative g' x) (at x within ?S) \<and> invertible (matrix (g' x))" |
3515 using "*" by blast |
3308 using "*" by blast |
3516 qed |
3309 qed |
3517 |
3310 |
3518 |
3311 |
3519 |
3312 |
3520 proposition has_absolute_integral_change_of_variables_compact: |
3313 lemma%unimportant has_absolute_integral_change_of_variables_compact: |
3521 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3314 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3522 assumes "compact S" |
3315 assumes "compact S" |
3523 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3316 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3524 and inj: "inj_on g S" |
3317 and inj: "inj_on g S" |
3525 shows "((\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and> |
3318 shows "((\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and> |
3533 show ?thesis |
3326 show ?thesis |
3534 by (rule has_absolute_integral_change_of_variables_invertible [OF der_g hg conth]) |
3327 by (rule has_absolute_integral_change_of_variables_invertible [OF der_g hg conth]) |
3535 qed |
3328 qed |
3536 |
3329 |
3537 |
3330 |
3538 lemma has_absolute_integral_change_of_variables_compact_family: |
3331 lemma%unimportant has_absolute_integral_change_of_variables_compact_family: |
3539 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3332 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3540 assumes compact: "\<And>n::nat. compact (F n)" |
3333 assumes compact: "\<And>n::nat. compact (F n)" |
3541 and der_g: "\<And>x. x \<in> (\<Union>n. F n) \<Longrightarrow> (g has_derivative g' x) (at x within (\<Union>n. F n))" |
3334 and der_g: "\<And>x. x \<in> (\<Union>n. F n) \<Longrightarrow> (g has_derivative g' x) (at x within (\<Union>n. F n))" |
3542 and inj: "inj_on g (\<Union>n. F n)" |
3335 and inj: "inj_on g (\<Union>n. F n)" |
3543 shows "((\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on (\<Union>n. F n) \<and> |
3336 shows "((\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on (\<Union>n. F n) \<and> |
3712 qed |
3505 qed |
3713 qed |
3506 qed |
3714 qed |
3507 qed |
3715 |
3508 |
3716 |
3509 |
3717 proposition has_absolute_integral_change_of_variables: |
3510 proposition%important has_absolute_integral_change_of_variables: |
3718 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3511 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3719 assumes S: "S \<in> sets lebesgue" |
3512 assumes S: "S \<in> sets lebesgue" |
3720 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3513 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3721 and inj: "inj_on g S" |
3514 and inj: "inj_on g S" |
3722 shows "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and> |
3515 shows "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and> |
3723 integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) = b |
3516 integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) = b |
3724 \<longleftrightarrow> f absolutely_integrable_on (g ` S) \<and> integral (g ` S) f = b" |
3517 \<longleftrightarrow> f absolutely_integrable_on (g ` S) \<and> integral (g ` S) f = b" |
3725 proof - |
3518 proof%unimportant - |
3726 obtain C N where "fsigma C" "negligible N" and CNS: "C \<union> N = S" and "disjnt C N" |
3519 obtain C N where "fsigma C" "negligible N" and CNS: "C \<union> N = S" and "disjnt C N" |
3727 using lebesgue_set_almost_fsigma [OF S] . |
3520 using lebesgue_set_almost_fsigma [OF S] . |
3728 then obtain F :: "nat \<Rightarrow> (real^'m::_) set" |
3521 then obtain F :: "nat \<Rightarrow> (real^'m::_) set" |
3729 where F: "range F \<subseteq> Collect compact" and Ceq: "C = Union(range F)" |
3522 where F: "range F \<subseteq> Collect compact" and Ceq: "C = Union(range F)" |
3730 using fsigma_Union_compact by metis |
3523 using fsigma_Union_compact by metis |
3774 ultimately show ?thesis |
3567 ultimately show ?thesis |
3775 by simp |
3568 by simp |
3776 qed |
3569 qed |
3777 |
3570 |
3778 |
3571 |
3779 corollary absolutely_integrable_change_of_variables: |
3572 corollary%important absolutely_integrable_change_of_variables: |
3780 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3573 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3781 assumes "S \<in> sets lebesgue" |
3574 assumes "S \<in> sets lebesgue" |
3782 and "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3575 and "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3783 and "inj_on g S" |
3576 and "inj_on g S" |
3784 shows "f absolutely_integrable_on (g ` S) |
3577 shows "f absolutely_integrable_on (g ` S) |
3785 \<longleftrightarrow> (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S" |
3578 \<longleftrightarrow> (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S" |
3786 using assms has_absolute_integral_change_of_variables by blast |
3579 using%unimportant assms has_absolute_integral_change_of_variables by%unimportant blast |
3787 |
3580 |
3788 corollary integral_change_of_variables: |
3581 corollary%important integral_change_of_variables: |
3789 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3582 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3790 assumes S: "S \<in> sets lebesgue" |
3583 assumes S: "S \<in> sets lebesgue" |
3791 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3584 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)" |
3792 and inj: "inj_on g S" |
3585 and inj: "inj_on g S" |
3793 and disj: "(f absolutely_integrable_on (g ` S) \<or> |
3586 and disj: "(f absolutely_integrable_on (g ` S) \<or> |
3794 (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S)" |
3587 (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S)" |
3795 shows "integral (g ` S) f = integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x))" |
3588 shows "integral (g ` S) f = integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x))" |
3796 using has_absolute_integral_change_of_variables [OF S der_g inj] disj |
3589 using%unimportant has_absolute_integral_change_of_variables [OF S der_g inj] disj |
3797 by blast |
3590 by%unimportant blast |
3798 |
3591 |
3799 lemma has_absolute_integral_change_of_variables_1: |
3592 lemma%unimportant has_absolute_integral_change_of_variables_1: |
3800 fixes f :: "real \<Rightarrow> real^'n::{finite,wellorder}" and g :: "real \<Rightarrow> real" |
3593 fixes f :: "real \<Rightarrow> real^'n::{finite,wellorder}" and g :: "real \<Rightarrow> real" |
3801 assumes S: "S \<in> sets lebesgue" |
3594 assumes S: "S \<in> sets lebesgue" |
3802 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_vector_derivative g' x) (at x within S)" |
3595 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_vector_derivative g' x) (at x within S)" |
3803 and inj: "inj_on g S" |
3596 and inj: "inj_on g S" |
3804 shows "(\<lambda>x. \<bar>g' x\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and> |
3597 shows "(\<lambda>x. \<bar>g' x\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and> |
3833 then show ?thesis |
3626 then show ?thesis |
3834 using absolutely_integrable_on_def by blast |
3627 using absolutely_integrable_on_def by blast |
3835 qed |
3628 qed |
3836 |
3629 |
3837 |
3630 |
3838 corollary absolutely_integrable_change_of_variables_1: |
3631 corollary%important absolutely_integrable_change_of_variables_1: |
3839 fixes f :: "real \<Rightarrow> real^'n::{finite,wellorder}" and g :: "real \<Rightarrow> real" |
3632 fixes f :: "real \<Rightarrow> real^'n::{finite,wellorder}" and g :: "real \<Rightarrow> real" |
3840 assumes S: "S \<in> sets lebesgue" |
3633 assumes S: "S \<in> sets lebesgue" |
3841 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_vector_derivative g' x) (at x within S)" |
3634 and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_vector_derivative g' x) (at x within S)" |
3842 and inj: "inj_on g S" |
3635 and inj: "inj_on g S" |
3843 shows "(f absolutely_integrable_on g ` S \<longleftrightarrow> |
3636 shows "(f absolutely_integrable_on g ` S \<longleftrightarrow> |
3844 (\<lambda>x. \<bar>g' x\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S)" |
3637 (\<lambda>x. \<bar>g' x\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S)" |
3845 using has_absolute_integral_change_of_variables_1 [OF assms] by auto |
3638 using%unimportant has_absolute_integral_change_of_variables_1 [OF assms] by%unimportant auto |
3846 |
3639 |
3847 |
3640 |
3848 subsection%important\<open>Change of variables for integrals: special case of linear function\<close> |
3641 subsection%important\<open>Change of variables for integrals: special case of linear function\<close> |
3849 |
3642 |
3850 lemma has_absolute_integral_change_of_variables_linear: |
3643 lemma%unimportant has_absolute_integral_change_of_variables_linear: |
3851 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3644 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3852 assumes "linear g" |
3645 assumes "linear g" |
3853 shows "(\<lambda>x. \<bar>det (matrix g)\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and> |
3646 shows "(\<lambda>x. \<bar>det (matrix g)\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and> |
3854 integral S (\<lambda>x. \<bar>det (matrix g)\<bar> *\<^sub>R f(g x)) = b |
3647 integral S (\<lambda>x. \<bar>det (matrix g)\<bar> *\<^sub>R f(g x)) = b |
3855 \<longleftrightarrow> f absolutely_integrable_on (g ` S) \<and> integral (g ` S) f = b" |
3648 \<longleftrightarrow> f absolutely_integrable_on (g ` S) \<and> integral (g ` S) f = b" |
3870 show "continuous_on (g ` S) h" |
3663 show "continuous_on (g ` S) h" |
3871 using continuous_on_eq_continuous_within has_derivative_continuous linear_imp_has_derivative h by blast |
3664 using continuous_on_eq_continuous_within has_derivative_continuous linear_imp_has_derivative h by blast |
3872 qed (use h in auto) |
3665 qed (use h in auto) |
3873 qed |
3666 qed |
3874 |
3667 |
3875 lemma absolutely_integrable_change_of_variables_linear: |
3668 lemma%unimportant absolutely_integrable_change_of_variables_linear: |
3876 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3669 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3877 assumes "linear g" |
3670 assumes "linear g" |
3878 shows "(\<lambda>x. \<bar>det (matrix g)\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S |
3671 shows "(\<lambda>x. \<bar>det (matrix g)\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S |
3879 \<longleftrightarrow> f absolutely_integrable_on (g ` S)" |
3672 \<longleftrightarrow> f absolutely_integrable_on (g ` S)" |
3880 using assms has_absolute_integral_change_of_variables_linear by blast |
3673 using assms has_absolute_integral_change_of_variables_linear by blast |
3881 |
3674 |
3882 lemma absolutely_integrable_on_linear_image: |
3675 lemma%unimportant absolutely_integrable_on_linear_image: |
3883 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3676 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3884 assumes "linear g" |
3677 assumes "linear g" |
3885 shows "f absolutely_integrable_on (g ` S) |
3678 shows "f absolutely_integrable_on (g ` S) |
3886 \<longleftrightarrow> (f \<circ> g) absolutely_integrable_on S \<or> det(matrix g) = 0" |
3679 \<longleftrightarrow> (f \<circ> g) absolutely_integrable_on S \<or> det(matrix g) = 0" |
3887 unfolding assms absolutely_integrable_change_of_variables_linear [OF assms, symmetric] absolutely_integrable_on_scaleR_iff |
3680 unfolding assms absolutely_integrable_change_of_variables_linear [OF assms, symmetric] absolutely_integrable_on_scaleR_iff |
3888 by (auto simp: set_integrable_def) |
3681 by (auto simp: set_integrable_def) |
3889 |
3682 |
3890 lemma integral_change_of_variables_linear: |
3683 lemma%important integral_change_of_variables_linear: |
3891 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3684 fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n" and g :: "real^'m::_ \<Rightarrow> real^'m::_" |
3892 assumes "linear g" |
3685 assumes "linear g" |
3893 and "f absolutely_integrable_on (g ` S) \<or> (f \<circ> g) absolutely_integrable_on S" |
3686 and "f absolutely_integrable_on (g ` S) \<or> (f \<circ> g) absolutely_integrable_on S" |
3894 shows "integral (g ` S) f = \<bar>det (matrix g)\<bar> *\<^sub>R integral S (f \<circ> g)" |
3687 shows "integral (g ` S) f = \<bar>det (matrix g)\<bar> *\<^sub>R integral S (f \<circ> g)" |
3895 proof - |
3688 proof%unimportant - |
3896 have "((\<lambda>x. \<bar>det (matrix g)\<bar> *\<^sub>R f (g x)) absolutely_integrable_on S) \<or> (f absolutely_integrable_on g ` S)" |
3689 have "((\<lambda>x. \<bar>det (matrix g)\<bar> *\<^sub>R f (g x)) absolutely_integrable_on S) \<or> (f absolutely_integrable_on g ` S)" |
3897 using absolutely_integrable_on_linear_image assms by blast |
3690 using absolutely_integrable_on_linear_image assms by blast |
3898 moreover |
3691 moreover |
3899 have ?thesis if "((\<lambda>x. \<bar>det (matrix g)\<bar> *\<^sub>R f (g x)) absolutely_integrable_on S)" "(f absolutely_integrable_on g ` S)" |
3692 have ?thesis if "((\<lambda>x. \<bar>det (matrix g)\<bar> *\<^sub>R f (g x)) absolutely_integrable_on S)" "(f absolutely_integrable_on g ` S)" |
3900 using has_absolute_integral_change_of_variables_linear [OF \<open>linear g\<close>] that |
3693 using has_absolute_integral_change_of_variables_linear [OF \<open>linear g\<close>] that |
3904 by blast |
3697 by blast |
3905 qed |
3698 qed |
3906 |
3699 |
3907 subsection%important\<open>Change of variable for measure\<close> |
3700 subsection%important\<open>Change of variable for measure\<close> |
3908 |
3701 |
3909 lemma has_measure_differentiable_image: |
3702 lemma%unimportant has_measure_differentiable_image: |
3910 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
3703 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
3911 assumes "S \<in> sets lebesgue" |
3704 assumes "S \<in> sets lebesgue" |
3912 and "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
3705 and "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
3913 and "inj_on f S" |
3706 and "inj_on f S" |
3914 shows "f ` S \<in> lmeasurable \<and> measure lebesgue (f ` S) = m |
3707 shows "f ` S \<in> lmeasurable \<and> measure lebesgue (f ` S) = m |
3915 \<longleftrightarrow> ((\<lambda>x. \<bar>det (matrix (f' x))\<bar>) has_integral m) S" |
3708 \<longleftrightarrow> ((\<lambda>x. \<bar>det (matrix (f' x))\<bar>) has_integral m) S" |
3916 using has_absolute_integral_change_of_variables [OF assms, of "\<lambda>x. (1::real^1)" "vec m"] |
3709 using%unimportant has_absolute_integral_change_of_variables [OF assms, of "\<lambda>x. (1::real^1)" "vec m"] |
3917 unfolding absolutely_integrable_on_1_iff integral_on_1_eq integrable_on_1_iff absolutely_integrable_on_def |
3710 unfolding%unimportant absolutely_integrable_on_1_iff integral_on_1_eq integrable_on_1_iff absolutely_integrable_on_def |
3918 by (auto simp: has_integral_iff lmeasurable_iff_integrable_on lmeasure_integral) |
3711 by%unimportant (auto simp: has_integral_iff lmeasurable_iff_integrable_on lmeasure_integral) |
3919 |
3712 |
3920 lemma measurable_differentiable_image_eq: |
3713 lemma%unimportant measurable_differentiable_image_eq: |
3921 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
3714 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
3922 assumes "S \<in> sets lebesgue" |
3715 assumes "S \<in> sets lebesgue" |
3923 and "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
3716 and "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
3924 and "inj_on f S" |
3717 and "inj_on f S" |
3925 shows "f ` S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S" |
3718 shows "f ` S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S" |
3926 using has_measure_differentiable_image [OF assms] |
3719 using has_measure_differentiable_image [OF assms] |
3927 by blast |
3720 by blast |
3928 |
3721 |
3929 lemma measurable_differentiable_image_alt: |
3722 lemma%important measurable_differentiable_image_alt: |
3930 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
3723 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
3931 assumes "S \<in> sets lebesgue" |
3724 assumes "S \<in> sets lebesgue" |
3932 and "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
3725 and "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
3933 and "inj_on f S" |
3726 and "inj_on f S" |
3934 shows "f ` S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. \<bar>det (matrix (f' x))\<bar>) absolutely_integrable_on S" |
3727 shows "f ` S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. \<bar>det (matrix (f' x))\<bar>) absolutely_integrable_on S" |
3935 using measurable_differentiable_image_eq [OF assms] |
3728 using%unimportant measurable_differentiable_image_eq [OF assms] |
3936 by (simp only: absolutely_integrable_on_iff_nonneg) |
3729 by%unimportant (simp only: absolutely_integrable_on_iff_nonneg) |
3937 |
3730 |
3938 lemma measure_differentiable_image_eq: |
3731 lemma%important measure_differentiable_image_eq: |
3939 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
3732 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_" |
3940 assumes S: "S \<in> sets lebesgue" |
3733 assumes S: "S \<in> sets lebesgue" |
3941 and der_f: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
3734 and der_f: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)" |
3942 and inj: "inj_on f S" |
3735 and inj: "inj_on f S" |
3943 and intS: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S" |
3736 and intS: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S" |
3944 shows "measure lebesgue (f ` S) = integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" |
3737 shows "measure lebesgue (f ` S) = integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" |
3945 using measurable_differentiable_image_eq [OF S der_f inj] |
3738 using%unimportant measurable_differentiable_image_eq [OF S der_f inj] |
3946 assms has_measure_differentiable_image by%unimportant blast |
3739 assms has_measure_differentiable_image by%unimportant blast |
3947 |
3740 |
3948 end |
3741 end |