src/HOL/Analysis/Change_Of_Vars.thy
 author paulson Tue Apr 17 22:35:48 2018 +0100 (16 months ago) changeset 67998 73a5a33486ee child 67999 1b05f74f2e5f permissions -rw-r--r--
Change of variables proof
 lp15@67998 ` 1` ```theory Change_Of_Vars ``` lp15@67998 ` 2` ``` imports "HOL-Analysis.Vitali_Covering_Theorem" "HOL-Analysis.Determinants" ``` lp15@67998 ` 3` lp15@67998 ` 4` ```begin ``` lp15@67998 ` 5` lp15@67998 ` 6` ```subsection\Induction on matrix row operations\ ``` lp15@67998 ` 7` lp15@67998 ` 8` ```lemma induct_matrix_row_operations: ``` lp15@67998 ` 9` ``` fixes P :: "(real^'n, 'n::finite) vec \ bool" ``` lp15@67998 ` 10` ``` assumes zero_row: "\A i. row i A = 0 \ P A" ``` lp15@67998 ` 11` ``` and diagonal: "\A. (\i j. i \ j \ A\$i\$j = 0) \ P A" ``` lp15@67998 ` 12` ``` and swap_cols: "\A m n. \P A; m \ n\ \ P(\ i j. A \$ i \$ Fun.swap m n id j)" ``` lp15@67998 ` 13` ``` and row_op: "\A m n c. \P A; m \ n\ ``` lp15@67998 ` 14` ``` \ P(\ i. if i = m then row m A + c *\<^sub>R row n A else row i A)" ``` lp15@67998 ` 15` ``` shows "P A" ``` lp15@67998 ` 16` ```proof - ``` lp15@67998 ` 17` ``` have "P A" if "(\i j. \j \ -K; i \ j\ \ A\$i\$j = 0)" for A K ``` lp15@67998 ` 18` ``` proof - ``` lp15@67998 ` 19` ``` have "finite K" ``` lp15@67998 ` 20` ``` by simp ``` lp15@67998 ` 21` ``` then show ?thesis using that ``` lp15@67998 ` 22` ``` proof (induction arbitrary: A rule: finite_induct) ``` lp15@67998 ` 23` ``` case empty ``` lp15@67998 ` 24` ``` with diagonal show ?case ``` lp15@67998 ` 25` ``` by simp ``` lp15@67998 ` 26` ``` next ``` lp15@67998 ` 27` ``` case (insert k K) ``` lp15@67998 ` 28` ``` note insertK = insert ``` lp15@67998 ` 29` ``` have "P A" if kk: "A\$k\$k \ 0" ``` lp15@67998 ` 30` ``` and 0: "\i j. \j \ - insert k K; i \ j\ \ A\$i\$j = 0" ``` lp15@67998 ` 31` ``` "\i. \i \ -L; i \ k\ \ A\$i\$k = 0" for A L ``` lp15@67998 ` 32` ``` proof - ``` lp15@67998 ` 33` ``` have "finite L" ``` lp15@67998 ` 34` ``` by simp ``` lp15@67998 ` 35` ``` then show ?thesis using 0 kk ``` lp15@67998 ` 36` ``` proof (induction arbitrary: A rule: finite_induct) ``` lp15@67998 ` 37` ``` case (empty B) ``` lp15@67998 ` 38` ``` show ?case ``` lp15@67998 ` 39` ``` proof (rule insertK) ``` lp15@67998 ` 40` ``` fix i j ``` lp15@67998 ` 41` ``` assume "i \ - K" "j \ i" ``` lp15@67998 ` 42` ``` show "B \$ j \$ i = 0" ``` lp15@67998 ` 43` ``` using \j \ i\ \i \ - K\ empty ``` lp15@67998 ` 44` ``` by (metis ComplD ComplI Compl_eq_Diff_UNIV Diff_empty UNIV_I insert_iff) ``` lp15@67998 ` 45` ``` qed ``` lp15@67998 ` 46` ``` next ``` lp15@67998 ` 47` ``` case (insert l L B) ``` lp15@67998 ` 48` ``` show ?case ``` lp15@67998 ` 49` ``` proof (cases "k = l") ``` lp15@67998 ` 50` ``` case True ``` lp15@67998 ` 51` ``` with insert show ?thesis ``` lp15@67998 ` 52` ``` by auto ``` lp15@67998 ` 53` ``` next ``` lp15@67998 ` 54` ``` case False ``` lp15@67998 ` 55` ``` let ?C = "\ i. if i = l then row l B - (B \$ l \$ k / B \$ k \$ k) *\<^sub>R row k B else row i B" ``` lp15@67998 ` 56` ``` have 1: "\j \ - insert k K; i \ j\ \ ?C \$ i \$ j = 0" for j i ``` lp15@67998 ` 57` ``` by (auto simp: insert.prems(1) row_def) ``` lp15@67998 ` 58` ``` have 2: "?C \$ i \$ k = 0" ``` lp15@67998 ` 59` ``` if "i \ - L" "i \ k" for i ``` lp15@67998 ` 60` ``` proof (cases "i=l") ``` lp15@67998 ` 61` ``` case True ``` lp15@67998 ` 62` ``` with that insert.prems show ?thesis ``` lp15@67998 ` 63` ``` by (simp add: row_def) ``` lp15@67998 ` 64` ``` next ``` lp15@67998 ` 65` ``` case False ``` lp15@67998 ` 66` ``` with that show ?thesis ``` lp15@67998 ` 67` ``` by (simp add: insert.prems(2) row_def) ``` lp15@67998 ` 68` ``` qed ``` lp15@67998 ` 69` ``` have 3: "?C \$ k \$ k \ 0" ``` lp15@67998 ` 70` ``` by (auto simp: insert.prems row_def \k \ l\) ``` lp15@67998 ` 71` ``` have PC: "P ?C" ``` lp15@67998 ` 72` ``` using insert.IH [OF 1 2 3] by auto ``` lp15@67998 ` 73` ``` have eqB: "(\ i. if i = l then row l ?C + (B \$ l \$ k / B \$ k \$ k) *\<^sub>R row k ?C else row i ?C) = B" ``` lp15@67998 ` 74` ``` using \k \ l\ by (simp add: vec_eq_iff row_def) ``` lp15@67998 ` 75` ``` show ?thesis ``` lp15@67998 ` 76` ``` using row_op [OF PC, of l k, where c = "B\$l\$k / B\$k\$k"] eqB \k \ l\ ``` lp15@67998 ` 77` ``` by (simp add: cong: if_cong) ``` lp15@67998 ` 78` ``` qed ``` lp15@67998 ` 79` ``` qed ``` lp15@67998 ` 80` ``` qed ``` lp15@67998 ` 81` ``` then have nonzero_hyp: "P A" ``` lp15@67998 ` 82` ``` if kk: "A\$k\$k \ 0" and zeroes: "\i j. j \ - insert k K \ i\j \ A\$i\$j = 0" for A ``` lp15@67998 ` 83` ``` by (auto simp: intro!: kk zeroes) ``` lp15@67998 ` 84` ``` show ?case ``` lp15@67998 ` 85` ``` proof (cases "row k A = 0") ``` lp15@67998 ` 86` ``` case True ``` lp15@67998 ` 87` ``` with zero_row show ?thesis by auto ``` lp15@67998 ` 88` ``` next ``` lp15@67998 ` 89` ``` case False ``` lp15@67998 ` 90` ``` then obtain l where l: "A\$k\$l \ 0" ``` lp15@67998 ` 91` ``` by (auto simp: row_def zero_vec_def vec_eq_iff) ``` lp15@67998 ` 92` ``` show ?thesis ``` lp15@67998 ` 93` ``` proof (cases "k = l") ``` lp15@67998 ` 94` ``` case True ``` lp15@67998 ` 95` ``` with l nonzero_hyp insert.prems show ?thesis ``` lp15@67998 ` 96` ``` by blast ``` lp15@67998 ` 97` ``` next ``` lp15@67998 ` 98` ``` case False ``` lp15@67998 ` 99` ``` have *: "A \$ i \$ Fun.swap k l id j = 0" if "j \ k" "j \ K" "i \ j" for i j ``` lp15@67998 ` 100` ``` using False l insert.prems that ``` lp15@67998 ` 101` ``` by (auto simp: swap_def insert split: if_split_asm) ``` lp15@67998 ` 102` ``` have "P (\ i j. (\ i j. A \$ i \$ Fun.swap k l id j) \$ i \$ Fun.swap k l id j)" ``` lp15@67998 ` 103` ``` by (rule swap_cols [OF nonzero_hyp False]) (auto simp: l *) ``` lp15@67998 ` 104` ``` moreover ``` lp15@67998 ` 105` ``` have "(\ i j. (\ i j. A \$ i \$ Fun.swap k l id j) \$ i \$ Fun.swap k l id j) = A" ``` lp15@67998 ` 106` ``` by (metis (no_types, lifting) id_apply o_apply swap_id_idempotent vec_lambda_unique vec_lambda_unique) ``` lp15@67998 ` 107` ``` ultimately show ?thesis ``` lp15@67998 ` 108` ``` by simp ``` lp15@67998 ` 109` ``` qed ``` lp15@67998 ` 110` ``` qed ``` lp15@67998 ` 111` ``` qed ``` lp15@67998 ` 112` ``` qed ``` lp15@67998 ` 113` ``` then show ?thesis ``` lp15@67998 ` 114` ``` by blast ``` lp15@67998 ` 115` ```qed ``` lp15@67998 ` 116` lp15@67998 ` 117` ```lemma induct_matrix_elementary: ``` lp15@67998 ` 118` ``` fixes P :: "(real^'n, 'n::finite) vec \ bool" ``` lp15@67998 ` 119` ``` assumes mult: "\A B. \P A; P B\ \ P(A ** B)" ``` lp15@67998 ` 120` ``` and zero_row: "\A i. row i A = 0 \ P A" ``` lp15@67998 ` 121` ``` and diagonal: "\A. (\i j. i \ j \ A\$i\$j = 0) \ P A" ``` lp15@67998 ` 122` ``` and swap1: "\m n. m \ n \ P(\ i j. mat 1 \$ i \$ Fun.swap m n id j)" ``` lp15@67998 ` 123` ``` and idplus: "\m n c. m \ n \ P(\ i j. if i = m \ j = n then c else of_bool (i = j))" ``` lp15@67998 ` 124` ``` shows "P A" ``` lp15@67998 ` 125` ```proof - ``` lp15@67998 ` 126` ``` have swap: "P (\ i j. A \$ i \$ Fun.swap m n id j)" (is "P ?C") ``` lp15@67998 ` 127` ``` if "P A" "m \ n" for A m n ``` lp15@67998 ` 128` ``` proof - ``` lp15@67998 ` 129` ``` have "A ** (\ i j. mat 1 \$ i \$ Fun.swap m n id j) = ?C" ``` lp15@67998 ` 130` ``` by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff if_distrib sum.delta_remove) ``` lp15@67998 ` 131` ``` then show ?thesis ``` lp15@67998 ` 132` ``` using mult swap1 that by metis ``` lp15@67998 ` 133` ``` qed ``` lp15@67998 ` 134` ``` have row: "P (\ i. if i = m then row m A + c *\<^sub>R row n A else row i A)" (is "P ?C") ``` lp15@67998 ` 135` ``` if "P A" "m \ n" for A m n c ``` lp15@67998 ` 136` ``` proof - ``` lp15@67998 ` 137` ``` let ?B = "\ i j. if i = m \ j = n then c else of_bool (i = j)" ``` lp15@67998 ` 138` ``` have "?B ** A = ?C" ``` lp15@67998 ` 139` ``` using \m \ n\ unfolding matrix_matrix_mult_def row_def of_bool_def ``` lp15@67998 ` 140` ``` by (auto simp: vec_eq_iff if_distrib [of "\x. x * y" for y] sum.remove cong: if_cong) ``` lp15@67998 ` 141` ``` then show ?thesis ``` lp15@67998 ` 142` ``` by (rule subst) (auto simp: that mult idplus) ``` lp15@67998 ` 143` ``` qed ``` lp15@67998 ` 144` ``` show ?thesis ``` lp15@67998 ` 145` ``` by (rule induct_matrix_row_operations [OF zero_row diagonal swap row]) ``` lp15@67998 ` 146` ```qed ``` lp15@67998 ` 147` lp15@67998 ` 148` ```lemma induct_matrix_elementary_alt: ``` lp15@67998 ` 149` ``` fixes P :: "(real^'n, 'n::finite) vec \ bool" ``` lp15@67998 ` 150` ``` assumes mult: "\A B. \P A; P B\ \ P(A ** B)" ``` lp15@67998 ` 151` ``` and zero_row: "\A i. row i A = 0 \ P A" ``` lp15@67998 ` 152` ``` and diagonal: "\A. (\i j. i \ j \ A\$i\$j = 0) \ P A" ``` lp15@67998 ` 153` ``` and swap1: "\m n. m \ n \ P(\ i j. mat 1 \$ i \$ Fun.swap m n id j)" ``` lp15@67998 ` 154` ``` and idplus: "\m n. m \ n \ P(\ i j. of_bool (i = m \ j = n \ i = j))" ``` lp15@67998 ` 155` ``` shows "P A" ``` lp15@67998 ` 156` ```proof - ``` lp15@67998 ` 157` ``` have *: "P (\ i j. if i = m \ j = n then c else of_bool (i = j))" ``` lp15@67998 ` 158` ``` if "m \ n" for m n c ``` lp15@67998 ` 159` ``` proof (cases "c = 0") ``` lp15@67998 ` 160` ``` case True ``` lp15@67998 ` 161` ``` with diagonal show ?thesis by auto ``` lp15@67998 ` 162` ``` next ``` lp15@67998 ` 163` ``` case False ``` lp15@67998 ` 164` ``` then have eq: "(\ i j. if i = m \ j = n then c else of_bool (i = j)) = ``` lp15@67998 ` 165` ``` (\ i j. if i = j then (if j = n then inverse c else 1) else 0) ** ``` lp15@67998 ` 166` ``` (\ i j. of_bool (i = m \ j = n \ i = j)) ** ``` lp15@67998 ` 167` ``` (\ i j. if i = j then if j = n then c else 1 else 0)" ``` lp15@67998 ` 168` ``` using \m \ n\ ``` lp15@67998 ` 169` ``` apply (simp add: matrix_matrix_mult_def vec_eq_iff of_bool_def if_distrib [of "\x. y * x" for y] cong: if_cong) ``` lp15@67998 ` 170` ``` apply (simp add: if_if_eq_conj sum.neutral conj_commute cong: conj_cong) ``` lp15@67998 ` 171` ``` done ``` lp15@67998 ` 172` ``` show ?thesis ``` lp15@67998 ` 173` ``` apply (subst eq) ``` lp15@67998 ` 174` ``` apply (intro mult idplus that) ``` lp15@67998 ` 175` ``` apply (auto intro: diagonal) ``` lp15@67998 ` 176` ``` done ``` lp15@67998 ` 177` ``` qed ``` lp15@67998 ` 178` ``` show ?thesis ``` lp15@67998 ` 179` ``` by (rule induct_matrix_elementary) (auto intro: assms *) ``` lp15@67998 ` 180` ```qed ``` lp15@67998 ` 181` lp15@67998 ` 182` ```lemma induct_linear_elementary: ``` lp15@67998 ` 183` ``` fixes f :: "real^'n \ real^'n" ``` lp15@67998 ` 184` ``` assumes "linear f" ``` lp15@67998 ` 185` ``` and comp: "\f g. \linear f; linear g; P f; P g\ \ P(f \ g)" ``` lp15@67998 ` 186` ``` and zeroes: "\f i. \linear f; \x. (f x) \$ i = 0\ \ P f" ``` lp15@67998 ` 187` ``` and const: "\c. P(\x. \ i. c i * x\$i)" ``` lp15@67998 ` 188` ``` and swap: "\m n::'n. m \ n \ P(\x. \ i. x \$ Fun.swap m n id i)" ``` lp15@67998 ` 189` ``` and idplus: "\m n::'n. m \ n \ P(\x. \ i. if i = m then x\$m + x\$n else x\$i)" ``` lp15@67998 ` 190` ``` shows "P f" ``` lp15@67998 ` 191` ```proof - ``` lp15@67998 ` 192` ``` have "P (( *v) A)" for A ``` lp15@67998 ` 193` ``` proof (rule induct_matrix_elementary_alt) ``` lp15@67998 ` 194` ``` fix A B ``` lp15@67998 ` 195` ``` assume "P (( *v) A)" and "P (( *v) B)" ``` lp15@67998 ` 196` ``` then show "P (( *v) (A ** B))" ``` lp15@67998 ` 197` ``` by (metis (no_types, lifting) comp linear_compose matrix_compose matrix_eq matrix_vector_mul matrix_vector_mul_linear) ``` lp15@67998 ` 198` ``` next ``` lp15@67998 ` 199` ``` fix A :: "((real, 'n) vec, 'n) vec" and i ``` lp15@67998 ` 200` ``` assume "row i A = 0" ``` lp15@67998 ` 201` ``` then show "P (( *v) A)" ``` lp15@67998 ` 202` ``` by (metis inner_zero_left matrix_vector_mul_component matrix_vector_mul_linear row_def vec_eq_iff vec_lambda_beta zeroes) ``` lp15@67998 ` 203` ``` next ``` lp15@67998 ` 204` ``` fix A :: "((real, 'n) vec, 'n) vec" ``` lp15@67998 ` 205` ``` assume 0: "\i j. i \ j \ A \$ i \$ j = 0" ``` lp15@67998 ` 206` ``` have "A \$ i \$ i * x \$ i = (\j\UNIV. A \$ i \$ j * x \$ j)" for x :: "(real, 'n) vec" and i :: "'n" ``` lp15@67998 ` 207` ``` by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i]) ``` lp15@67998 ` 208` ``` then have "(\x. \ i. A \$ i \$ i * x \$ i) = (( *v) A)" ``` lp15@67998 ` 209` ``` by (auto simp: 0 matrix_vector_mult_def) ``` lp15@67998 ` 210` ``` then show "P (( *v) A)" ``` lp15@67998 ` 211` ``` using const [of "\i. A \$ i \$ i"] by simp ``` lp15@67998 ` 212` ``` next ``` lp15@67998 ` 213` ``` fix m n :: "'n" ``` lp15@67998 ` 214` ``` assume "m \ n" ``` lp15@67998 ` 215` ``` have eq: "(\j\UNIV. if i = Fun.swap m n id j then x \$ j else 0) = ``` lp15@67998 ` 216` ``` (\j\UNIV. if j = Fun.swap m n id i then x \$ j else 0)" ``` lp15@67998 ` 217` ``` for i and x :: "(real, 'n) vec" ``` lp15@67998 ` 218` ``` unfolding swap_def by (rule sum.cong) auto ``` lp15@67998 ` 219` ``` have "(\x::real^'n. \ i. x \$ Fun.swap m n id i) = (( *v) (\ i j. if i = Fun.swap m n id j then 1 else 0))" ``` lp15@67998 ` 220` ``` by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\x. x * y" for y] cong: if_cong) ``` lp15@67998 ` 221` ``` with swap [OF \m \ n\] show "P (( *v) (\ i j. mat 1 \$ i \$ Fun.swap m n id j))" ``` lp15@67998 ` 222` ``` by (simp add: mat_def matrix_vector_mult_def) ``` lp15@67998 ` 223` ``` next ``` lp15@67998 ` 224` ``` fix m n :: "'n" ``` lp15@67998 ` 225` ``` assume "m \ n" ``` lp15@67998 ` 226` ``` then have "x \$ m + x \$ n = (\j\UNIV. of_bool (j = n \ m = j) * x \$ j)" for x :: "(real, 'n) vec" ``` lp15@67998 ` 227` ``` by (auto simp: of_bool_def if_distrib [of "\x. x * y" for y] sum.remove cong: if_cong) ``` lp15@67998 ` 228` ``` then have "(\x::real^'n. \ i. if i = m then x \$ m + x \$ n else x \$ i) = ``` lp15@67998 ` 229` ``` (( *v) (\ i j. of_bool (i = m \ j = n \ i = j)))" ``` lp15@67998 ` 230` ``` unfolding matrix_vector_mult_def of_bool_def ``` lp15@67998 ` 231` ``` by (auto simp: vec_eq_iff if_distrib [of "\x. x * y" for y] cong: if_cong) ``` lp15@67998 ` 232` ``` then show "P (( *v) (\ i j. of_bool (i = m \ j = n \ i = j)))" ``` lp15@67998 ` 233` ``` using idplus [OF \m \ n\] by simp ``` lp15@67998 ` 234` ``` qed ``` lp15@67998 ` 235` ``` then show ?thesis ``` lp15@67998 ` 236` ``` by (metis \linear f\ matrix_vector_mul) ``` lp15@67998 ` 237` ```qed ``` lp15@67998 ` 238` lp15@67998 ` 239` lp15@67998 ` 240` ```proposition ``` lp15@67998 ` 241` ``` fixes a :: "real^'n" ``` lp15@67998 ` 242` ``` assumes "m \ n" and ab_ne: "cbox a b \ {}" and an: "0 \ a\$n" ``` lp15@67998 ` 243` ``` shows measurable_shear_interval: "(\x. \ i. if i = m then x\$m + x\$n else x\$i) ` (cbox a b) \ lmeasurable" ``` lp15@67998 ` 244` ``` (is "?f ` _ \ _") ``` lp15@67998 ` 245` ``` and measure_shear_interval: "measure lebesgue ((\x. \ i. if i = m then x\$m + x\$n else x\$i) ` cbox a b) ``` lp15@67998 ` 246` ``` = measure lebesgue (cbox a b)" (is "?Q") ``` lp15@67998 ` 247` ```proof - ``` lp15@67998 ` 248` ``` have lin: "linear ?f" ``` lp15@67998 ` 249` ``` by (force simp: plus_vec_def scaleR_vec_def algebra_simps intro: linearI) ``` lp15@67998 ` 250` ``` show fab: "?f ` cbox a b \ lmeasurable" ``` lp15@67998 ` 251` ``` by (simp add: lin measurable_linear_image_interval) ``` lp15@67998 ` 252` ``` let ?c = "\ i. if i = m then b\$m + b\$n else b\$i" ``` lp15@67998 ` 253` ``` let ?mn = "axis m 1 - axis n (1::real)" ``` lp15@67998 ` 254` ``` have eq1: "measure lebesgue (cbox a ?c) ``` lp15@67998 ` 255` ``` = measure lebesgue (?f ` cbox a b) ``` lp15@67998 ` 256` ``` + measure lebesgue (cbox a ?c \ {x. ?mn \ x \ a\$m}) ``` lp15@67998 ` 257` ``` + measure lebesgue (cbox a ?c \ {x. ?mn \ x \ b\$m})" ``` lp15@67998 ` 258` ``` proof (rule measure_Un3_negligible) ``` lp15@67998 ` 259` ``` show "cbox a ?c \ {x. ?mn \ x \ a\$m} \ lmeasurable" "cbox a ?c \ {x. ?mn \ x \ b\$m} \ lmeasurable" ``` lp15@67998 ` 260` ``` by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurable_convex) ``` lp15@67998 ` 261` ``` have "negligible {x. ?mn \ x = a\$m}" ``` lp15@67998 ` 262` ``` by (metis \m \ n\ axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane) ``` lp15@67998 ` 263` ``` moreover have "?f ` cbox a b \ (cbox a ?c \ {x. ?mn \ x \ a \$ m}) \ {x. ?mn \ x = a\$m}" ``` lp15@67998 ` 264` ``` using \m \ n\ antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis') ``` lp15@67998 ` 265` ``` ultimately show "negligible ((?f ` cbox a b) \ (cbox a ?c \ {x. ?mn \ x \ a \$ m}))" ``` lp15@67998 ` 266` ``` by (rule negligible_subset) ``` lp15@67998 ` 267` ``` have "negligible {x. ?mn \ x = b\$m}" ``` lp15@67998 ` 268` ``` by (metis \m \ n\ axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane) ``` lp15@67998 ` 269` ``` moreover have "(?f ` cbox a b) \ (cbox a ?c \ {x. ?mn \ x \ b\$m}) \ {x. ?mn \ x = b\$m}" ``` lp15@67998 ` 270` ``` using \m \ n\ antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis') ``` lp15@67998 ` 271` ``` ultimately show "negligible (?f ` cbox a b \ (cbox a ?c \ {x. ?mn \ x \ b\$m}))" ``` lp15@67998 ` 272` ``` by (rule negligible_subset) ``` lp15@67998 ` 273` ``` have "negligible {x. ?mn \ x = b\$m}" ``` lp15@67998 ` 274` ``` by (metis \m \ n\ axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane) ``` lp15@67998 ` 275` ``` moreover have "(cbox a ?c \ {x. ?mn \ x \ a \$ m} \ (cbox a ?c \ {x. ?mn \ x \ b\$m})) \ {x. ?mn \ x = b\$m}" ``` lp15@67998 ` 276` ``` using \m \ n\ ab_ne ``` lp15@67998 ` 277` ``` apply (auto simp: algebra_simps mem_box_cart inner_axis') ``` lp15@67998 ` 278` ``` apply (drule_tac x=m in spec)+ ``` lp15@67998 ` 279` ``` apply simp ``` lp15@67998 ` 280` ``` done ``` lp15@67998 ` 281` ``` ultimately show "negligible (cbox a ?c \ {x. ?mn \ x \ a \$ m} \ (cbox a ?c \ {x. ?mn \ x \ b\$m}))" ``` lp15@67998 ` 282` ``` by (rule negligible_subset) ``` lp15@67998 ` 283` ``` show "?f ` cbox a b \ cbox a ?c \ {x. ?mn \ x \ a \$ m} \ cbox a ?c \ {x. ?mn \ x \ b\$m} = cbox a ?c" (is "?lhs = _") ``` lp15@67998 ` 284` ``` proof ``` lp15@67998 ` 285` ``` show "?lhs \ cbox a ?c" ``` lp15@67998 ` 286` ``` by (auto simp: mem_box_cart add_mono) (meson add_increasing2 an order_trans) ``` lp15@67998 ` 287` ``` show "cbox a ?c \ ?lhs" ``` lp15@67998 ` 288` ``` apply (auto simp: algebra_simps image_iff inner_axis' lambda_add_Galois [OF \m \ n\]) ``` lp15@67998 ` 289` ``` apply (auto simp: mem_box_cart split: if_split_asm) ``` lp15@67998 ` 290` ``` done ``` lp15@67998 ` 291` ``` qed ``` lp15@67998 ` 292` ``` qed (fact fab) ``` lp15@67998 ` 293` ``` let ?d = "\ i. if i = m then a \$ m - b \$ m else 0" ``` lp15@67998 ` 294` ``` have eq2: "measure lebesgue (cbox a ?c \ {x. ?mn \ x \ a \$ m}) + measure lebesgue (cbox a ?c \ {x. ?mn \ x \ b\$m}) ``` lp15@67998 ` 295` ``` = measure lebesgue (cbox a (\ i. if i = m then a \$ m + b \$ n else b \$ i))" ``` lp15@67998 ` 296` ``` proof (rule measure_translate_add[of "cbox a ?c \ {x. ?mn \ x \ a\$m}" "cbox a ?c \ {x. ?mn \ x \ b\$m}" ``` lp15@67998 ` 297` ``` "(\ i. if i = m then a\$m - b\$m else 0)" "cbox a (\ i. if i = m then a\$m + b\$n else b\$i)"]) ``` lp15@67998 ` 298` ``` show "(cbox a ?c \ {x. ?mn \ x \ a\$m}) \ lmeasurable" ``` lp15@67998 ` 299` ``` "cbox a ?c \ {x. ?mn \ x \ b\$m} \ lmeasurable" ``` lp15@67998 ` 300` ``` by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurable_convex) ``` lp15@67998 ` 301` ``` have "\x. \x \$ n + a \$ m \ x \$ m\ ``` lp15@67998 ` 302` ``` \ x \ (+) (\ i. if i = m then a \$ m - b \$ m else 0) ` {x. x \$ n + b \$ m \ x \$ m}" ``` lp15@67998 ` 303` ``` using \m \ n\ ``` lp15@67998 ` 304` ``` by (rule_tac x="x - (\ i. if i = m then a\$m - b\$m else 0)" in image_eqI) ``` lp15@67998 ` 305` ``` (simp_all add: mem_box_cart) ``` lp15@67998 ` 306` ``` then have imeq: "(+) ?d ` {x. b \$ m \ ?mn \ x} = {x. a \$ m \ ?mn \ x}" ``` lp15@67998 ` 307` ``` using \m \ n\ by (auto simp: mem_box_cart inner_axis' algebra_simps) ``` lp15@67998 ` 308` ``` have "\x. \0 \ a \$ n; x \$ n + a \$ m \ x \$ m; ``` lp15@67998 ` 309` ``` \i. i \ m \ a \$ i \ x \$ i \ x \$ i \ b \$ i\ ``` lp15@67998 ` 310` ``` \ a \$ m \ x \$ m" ``` lp15@67998 ` 311` ``` using \m \ n\ by force ``` lp15@67998 ` 312` ``` then have "(+) ?d ` (cbox a ?c \ {x. b \$ m \ ?mn \ x}) ``` lp15@67998 ` 313` ``` = cbox a (\ i. if i = m then a \$ m + b \$ n else b \$ i) \ {x. a \$ m \ ?mn \ x}" ``` lp15@67998 ` 314` ``` using an ab_ne ``` lp15@67998 ` 315` ``` apply (simp add: cbox_translation [symmetric] translation_Int interval_ne_empty_cart imeq) ``` lp15@67998 ` 316` ``` apply (auto simp: mem_box_cart inner_axis' algebra_simps if_distrib all_if_distrib) ``` lp15@67998 ` 317` ``` by (metis (full_types) add_mono mult_2_right) ``` lp15@67998 ` 318` ``` then show "cbox a ?c \ {x. ?mn \ x \ a \$ m} \ ``` lp15@67998 ` 319` ``` (+) ?d ` (cbox a ?c \ {x. b \$ m \ ?mn \ x}) = ``` lp15@67998 ` 320` ``` cbox a (\ i. if i = m then a \$ m + b \$ n else b \$ i)" (is "?lhs = ?rhs") ``` lp15@67998 ` 321` ``` using an \m \ n\ ``` lp15@67998 ` 322` ``` apply (auto simp: mem_box_cart inner_axis' algebra_simps if_distrib all_if_distrib, force) ``` lp15@67998 ` 323` ``` apply (drule_tac x=n in spec)+ ``` lp15@67998 ` 324` ``` by (meson ab_ne add_mono_thms_linordered_semiring(3) dual_order.trans interval_ne_empty_cart(1)) ``` lp15@67998 ` 325` ``` have "negligible{x. ?mn \ x = a\$m}" ``` lp15@67998 ` 326` ``` by (metis \m \ n\ axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane) ``` lp15@67998 ` 327` ``` moreover have "(cbox a ?c \ {x. ?mn \ x \ a \$ m} \ ``` lp15@67998 ` 328` ``` (+) ?d ` (cbox a ?c \ {x. b \$ m \ ?mn \ x})) \ {x. ?mn \ x = a\$m}" ``` lp15@67998 ` 329` ``` using \m \ n\ antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis') ``` lp15@67998 ` 330` ``` ultimately show "negligible (cbox a ?c \ {x. ?mn \ x \ a \$ m} \ ``` lp15@67998 ` 331` ``` (+) ?d ` (cbox a ?c \ {x. b \$ m \ ?mn \ x}))" ``` lp15@67998 ` 332` ``` by (rule negligible_subset) ``` lp15@67998 ` 333` ``` qed ``` lp15@67998 ` 334` ``` have ac_ne: "cbox a ?c \ {}" ``` lp15@67998 ` 335` ``` using ab_ne an ``` lp15@67998 ` 336` ``` by (clarsimp simp: interval_eq_empty_cart) (meson add_less_same_cancel1 le_less_linear less_le_trans) ``` lp15@67998 ` 337` ``` have ax_ne: "cbox a (\ i. if i = m then a \$ m + b \$ n else b \$ i) \ {}" ``` lp15@67998 ` 338` ``` using ab_ne an ``` lp15@67998 ` 339` ``` by (clarsimp simp: interval_eq_empty_cart) (meson add_less_same_cancel1 le_less_linear less_le_trans) ``` lp15@67998 ` 340` ``` have eq3: "measure lebesgue (cbox a ?c) = measure lebesgue (cbox a (\ i. if i = m then a\$m + b\$n else b\$i)) + measure lebesgue (cbox a b)" ``` lp15@67998 ` 341` ``` by (simp add: content_cbox_if_cart ab_ne ac_ne ax_ne algebra_simps prod.delta_remove ``` lp15@67998 ` 342` ``` if_distrib [of "\u. u - z" for z] prod.remove) ``` lp15@67998 ` 343` ``` show ?Q ``` lp15@67998 ` 344` ``` using eq1 eq2 eq3 ``` lp15@67998 ` 345` ``` by (simp add: algebra_simps) ``` lp15@67998 ` 346` ```qed ``` lp15@67998 ` 347` lp15@67998 ` 348` lp15@67998 ` 349` lp15@67998 ` 350` ```proposition ``` lp15@67998 ` 351` ``` fixes S :: "(real^'n) set" ``` lp15@67998 ` 352` ``` assumes "S \ lmeasurable" ``` lp15@67998 ` 353` ``` shows measurable_stretch: "((\x. \ k. m k * x\$k) ` S) \ lmeasurable" (is "?f ` S \ _") ``` lp15@67998 ` 354` ``` and measure_stretch: "measure lebesgue ((\x. \ k. m k * x\$k) ` S) = \prod m UNIV\ * measure lebesgue S" ``` lp15@67998 ` 355` ``` (is "?MEQ") ``` lp15@67998 ` 356` ```proof - ``` lp15@67998 ` 357` ``` have "(?f ` S) \ lmeasurable \ ?MEQ" ``` lp15@67998 ` 358` ``` proof (cases "\k. m k \ 0") ``` lp15@67998 ` 359` ``` case True ``` lp15@67998 ` 360` ``` have m0: "0 < \prod m UNIV\" ``` lp15@67998 ` 361` ``` using True by simp ``` lp15@67998 ` 362` ``` have "(indicat_real (?f ` S) has_integral \prod m UNIV\ * measure lebesgue S) UNIV" ``` lp15@67998 ` 363` ``` proof (clarsimp simp add: has_integral_alt [where i=UNIV]) ``` lp15@67998 ` 364` ``` fix e :: "real" ``` lp15@67998 ` 365` ``` assume "e > 0" ``` lp15@67998 ` 366` ``` have "(indicat_real S has_integral (measure lebesgue S)) UNIV" ``` lp15@67998 ` 367` ``` using assms lmeasurable_iff_has_integral by blast ``` lp15@67998 ` 368` ``` then obtain B where "B>0" ``` lp15@67998 ` 369` ``` and B: "\a b. ball 0 B \ cbox a b \ ``` lp15@67998 ` 370` ``` \z. (indicat_real S has_integral z) (cbox a b) \ ``` lp15@67998 ` 371` ``` \z - measure lebesgue S\ < e / \prod m UNIV\" ``` lp15@67998 ` 372` ``` by (simp add: has_integral_alt [where i=UNIV]) (metis (full_types) divide_pos_pos m0 m0 \e > 0\) ``` lp15@67998 ` 373` ``` show "\B>0. \a b. ball 0 B \ cbox a b \ ``` lp15@67998 ` 374` ``` (\z. (indicat_real (?f ` S) has_integral z) (cbox a b) \ ``` lp15@67998 ` 375` ``` \z - \prod m UNIV\ * measure lebesgue S\ < e)" ``` lp15@67998 ` 376` ``` proof (intro exI conjI allI) ``` lp15@67998 ` 377` ``` let ?C = "Max (range (\k. \m k\)) * B" ``` lp15@67998 ` 378` ``` show "?C > 0" ``` lp15@67998 ` 379` ``` using True \B > 0\ by (simp add: Max_gr_iff) ``` lp15@67998 ` 380` ``` show "ball 0 ?C \ cbox u v \ ``` lp15@67998 ` 381` ``` (\z. (indicat_real (?f ` S) has_integral z) (cbox u v) \ ``` lp15@67998 ` 382` ``` \z - \prod m UNIV\ * measure lebesgue S\ < e)" for u v ``` lp15@67998 ` 383` ``` proof ``` lp15@67998 ` 384` ``` assume uv: "ball 0 ?C \ cbox u v" ``` lp15@67998 ` 385` ``` with \?C > 0\ have cbox_ne: "cbox u v \ {}" ``` lp15@67998 ` 386` ``` using centre_in_ball by blast ``` lp15@67998 ` 387` ``` let ?\ = "\k. u\$k / m k" ``` lp15@67998 ` 388` ``` let ?\ = "\k. v\$k / m k" ``` lp15@67998 ` 389` ``` have invm0: "\k. inverse (m k) \ 0" ``` lp15@67998 ` 390` ``` using True by auto ``` lp15@67998 ` 391` ``` have "ball 0 B \ (\x. \ k. x \$ k / m k) ` ball 0 ?C" ``` lp15@67998 ` 392` ``` proof clarsimp ``` lp15@67998 ` 393` ``` fix x :: "(real, 'n) vec" ``` lp15@67998 ` 394` ``` assume x: "norm x < B" ``` lp15@67998 ` 395` ``` have [simp]: "\Max (range (\k. \m k\))\ = Max (range (\k. \m k\))" ``` lp15@67998 ` 396` ``` by (meson Max_ge abs_ge_zero abs_of_nonneg finite finite_imageI order_trans rangeI) ``` lp15@67998 ` 397` ``` have "norm (\ k. m k * x \$ k) \ norm (Max (range (\k. \m k\)) *\<^sub>R x)" ``` lp15@67998 ` 398` ``` by (rule norm_le_componentwise_cart) (auto simp: abs_mult intro: mult_right_mono) ``` lp15@67998 ` 399` ``` also have "\ < ?C" ``` lp15@67998 ` 400` ``` using x by simp (metis \B > 0\ \?C > 0\ mult.commute real_mult_less_iff1 zero_less_mult_pos) ``` lp15@67998 ` 401` ``` finally have "norm (\ k. m k * x \$ k) < ?C" . ``` lp15@67998 ` 402` ``` then show "x \ (\x. \ k. x \$ k / m k) ` ball 0 ?C" ``` lp15@67998 ` 403` ``` using stretch_Galois [of "inverse \ m"] True by (auto simp: image_iff field_simps) ``` lp15@67998 ` 404` ``` qed ``` lp15@67998 ` 405` ``` then have Bsub: "ball 0 B \ cbox (\ k. min (?\ k) (?\ k)) (\ k. max (?\ k) (?\ k))" ``` lp15@67998 ` 406` ``` using cbox_ne uv image_stretch_interval_cart [of "inverse \ m" u v, symmetric] ``` lp15@67998 ` 407` ``` by (force simp: field_simps) ``` lp15@67998 ` 408` ``` obtain z where zint: "(indicat_real S has_integral z) (cbox (\ k. min (?\ k) (?\ k)) (\ k. max (?\ k) (?\ k)))" ``` lp15@67998 ` 409` ``` and zless: "\z - measure lebesgue S\ < e / \prod m UNIV\" ``` lp15@67998 ` 410` ``` using B [OF Bsub] by blast ``` lp15@67998 ` 411` ``` have ind: "indicat_real (?f ` S) = (\x. indicator S (\ k. x\$k / m k))" ``` lp15@67998 ` 412` ``` using True stretch_Galois [of m] by (force simp: indicator_def) ``` lp15@67998 ` 413` ``` show "\z. (indicat_real (?f ` S) has_integral z) (cbox u v) \ ``` lp15@67998 ` 414` ``` \z - \prod m UNIV\ * measure lebesgue S\ < e" ``` lp15@67998 ` 415` ``` proof (simp add: ind, intro conjI exI) ``` lp15@67998 ` 416` ``` have "((\x. indicat_real S (\ k. x \$ k/ m k)) has_integral z *\<^sub>R \prod m UNIV\) ``` lp15@67998 ` 417` ``` ((\x. \ k. x \$ k * m k) ` cbox (\ k. min (?\ k) (?\ k)) (\ k. max (?\ k) (?\ k)))" ``` lp15@67998 ` 418` ``` using True has_integral_stretch_cart [OF zint, of "inverse \ m"] ``` lp15@67998 ` 419` ``` by (simp add: field_simps prod_dividef) ``` lp15@67998 ` 420` ``` moreover have "((\x. \ k. x \$ k * m k) ` cbox (\ k. min (?\ k) (?\ k)) (\ k. max (?\ k) (?\ k))) = cbox u v" ``` lp15@67998 ` 421` ``` using True image_stretch_interval_cart [of "inverse \ m" u v, symmetric] ``` lp15@67998 ` 422` ``` image_stretch_interval_cart [of "\k. 1" u v, symmetric] \cbox u v \ {}\ ``` lp15@67998 ` 423` ``` by (simp add: field_simps image_comp o_def) ``` lp15@67998 ` 424` ``` ultimately show "((\x. indicat_real S (\ k. x \$ k/ m k)) has_integral z *\<^sub>R \prod m UNIV\) (cbox u v)" ``` lp15@67998 ` 425` ``` by simp ``` lp15@67998 ` 426` ``` have "\z *\<^sub>R \prod m UNIV\ - \prod m UNIV\ * measure lebesgue S\ ``` lp15@67998 ` 427` ``` = \prod m UNIV\ * \z - measure lebesgue S\" ``` lp15@67998 ` 428` ``` by (metis (no_types, hide_lams) abs_abs abs_scaleR mult.commute real_scaleR_def right_diff_distrib') ``` lp15@67998 ` 429` ``` also have "\ < e" ``` lp15@67998 ` 430` ``` using zless True by (simp add: field_simps) ``` lp15@67998 ` 431` ``` finally show "\z *\<^sub>R \prod m UNIV\ - \prod m UNIV\ * measure lebesgue S\ < e" . ``` lp15@67998 ` 432` ``` qed ``` lp15@67998 ` 433` ``` qed ``` lp15@67998 ` 434` ``` qed ``` lp15@67998 ` 435` ``` qed ``` lp15@67998 ` 436` ``` then show ?thesis ``` lp15@67998 ` 437` ``` by (auto simp: has_integral_integrable integral_unique lmeasure_integral_UNIV measurable_integrable) ``` lp15@67998 ` 438` ``` next ``` lp15@67998 ` 439` ``` case False ``` lp15@67998 ` 440` ``` then obtain k where "m k = 0" and prm: "prod m UNIV = 0" ``` lp15@67998 ` 441` ``` by auto ``` lp15@67998 ` 442` ``` have nfS: "negligible (?f ` S)" ``` lp15@67998 ` 443` ``` by (rule negligible_subset [OF negligible_standard_hyperplane_cart]) (use \m k = 0\ in auto) ``` lp15@67998 ` 444` ``` then have "(?f ` S) \ lmeasurable" ``` lp15@67998 ` 445` ``` by (simp add: negligible_iff_measure) ``` lp15@67998 ` 446` ``` with nfS show ?thesis ``` lp15@67998 ` 447` ``` by (simp add: prm negligible_iff_measure0) ``` lp15@67998 ` 448` ``` qed ``` lp15@67998 ` 449` ``` then show "(?f ` S) \ lmeasurable" ?MEQ ``` lp15@67998 ` 450` ``` by metis+ ``` lp15@67998 ` 451` ```qed ``` lp15@67998 ` 452` lp15@67998 ` 453` lp15@67998 ` 454` lp15@67998 ` 455` lp15@67998 ` 456` lp15@67998 ` 457` ```proposition ``` lp15@67998 ` 458` ``` fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" ``` lp15@67998 ` 459` ``` assumes "linear f" "S \ lmeasurable" ``` lp15@67998 ` 460` ``` shows measurable_linear_image: "(f ` S) \ lmeasurable" ``` lp15@67998 ` 461` ``` and measure_linear_image: "measure lebesgue (f ` S) = \det (matrix f)\ * measure lebesgue S" (is "?Q f S") ``` lp15@67998 ` 462` ```proof - ``` lp15@67998 ` 463` ``` have "\S \ lmeasurable. (f ` S) \ lmeasurable \ ?Q f S" ``` lp15@67998 ` 464` ``` proof (rule induct_linear_elementary [OF \linear f\]; intro ballI) ``` lp15@67998 ` 465` ``` fix f g and S :: "(real,'n) vec set" ``` lp15@67998 ` 466` ``` assume "linear f" and "linear g" ``` lp15@67998 ` 467` ``` and f [rule_format]: "\S \ lmeasurable. f ` S \ lmeasurable \ ?Q f S" ``` lp15@67998 ` 468` ``` and g [rule_format]: "\S \ lmeasurable. g ` S \ lmeasurable \ ?Q g S" ``` lp15@67998 ` 469` ``` and S: "S \ lmeasurable" ``` lp15@67998 ` 470` ``` then have gS: "g ` S \ lmeasurable" ``` lp15@67998 ` 471` ``` by blast ``` lp15@67998 ` 472` ``` show "(f \ g) ` S \ lmeasurable \ ?Q (f \ g) S" ``` lp15@67998 ` 473` ``` using f [OF gS] g [OF S] matrix_compose [OF \linear g\ \linear f\] ``` lp15@67998 ` 474` ``` by (simp add: o_def image_comp abs_mult det_mul) ``` lp15@67998 ` 475` ``` next ``` lp15@67998 ` 476` ``` fix f :: "(real, 'n) vec \ (real, 'n) vec" and i and S :: "(real, 'n) vec set" ``` lp15@67998 ` 477` ``` assume "linear f" and 0: "\x. f x \$ i = 0" and "S \ lmeasurable" ``` lp15@67998 ` 478` ``` then have "\ inj f" ``` lp15@67998 ` 479` ``` by (metis (full_types) linear_injective_imp_surjective one_neq_zero surjE vec_component) ``` lp15@67998 ` 480` ``` have detf: "det (matrix f) = 0" ``` lp15@67998 ` 481` ``` by (metis "0" \linear f\ invertible_det_nz invertible_right_inverse matrix_right_invertible_surjective matrix_vector_mul surjE vec_component) ``` lp15@67998 ` 482` ``` show "f ` S \ lmeasurable \ ?Q f S" ``` lp15@67998 ` 483` ``` proof ``` lp15@67998 ` 484` ``` show "f ` S \ lmeasurable" ``` lp15@67998 ` 485` ``` using lmeasurable_iff_indicator_has_integral \linear f\ \\ inj f\ negligible_UNIV negligible_linear_singular_image by blast ``` lp15@67998 ` 486` ``` have "measure lebesgue (f ` S) = 0" ``` lp15@67998 ` 487` ``` by (meson \\ inj f\ \linear f\ negligible_imp_measure0 negligible_linear_singular_image) ``` lp15@67998 ` 488` ``` also have "\ = \det (matrix f)\ * measure lebesgue S" ``` lp15@67998 ` 489` ``` by (simp add: detf) ``` lp15@67998 ` 490` ``` finally show "?Q f S" . ``` lp15@67998 ` 491` ``` qed ``` lp15@67998 ` 492` ``` next ``` lp15@67998 ` 493` ``` fix c and S :: "(real, 'n) vec set" ``` lp15@67998 ` 494` ``` assume "S \ lmeasurable" ``` lp15@67998 ` 495` ``` show "(\a. \ i. c i * a \$ i) ` S \ lmeasurable \ ?Q (\a. \ i. c i * a \$ i) S" ``` lp15@67998 ` 496` ``` proof ``` lp15@67998 ` 497` ``` show "(\a. \ i. c i * a \$ i) ` S \ lmeasurable" ``` lp15@67998 ` 498` ``` by (simp add: \S \ lmeasurable\ measurable_stretch) ``` lp15@67998 ` 499` ``` show "?Q (\a. \ i. c i * a \$ i) S" ``` lp15@67998 ` 500` ``` by (simp add: measure_stretch [OF \S \ lmeasurable\, of c] axis_def matrix_def det_diagonal) ``` lp15@67998 ` 501` ``` qed ``` lp15@67998 ` 502` ``` next ``` lp15@67998 ` 503` ``` fix m :: "'n" and n :: "'n" and S :: "(real, 'n) vec set" ``` lp15@67998 ` 504` ``` assume "m \ n" and "S \ lmeasurable" ``` lp15@67998 ` 505` ``` let ?h = "\v::(real, 'n) vec. \ i. v \$ Fun.swap m n id i" ``` lp15@67998 ` 506` ``` have lin: "linear ?h" ``` lp15@67998 ` 507` ``` by (simp add: plus_vec_def scaleR_vec_def linearI) ``` lp15@67998 ` 508` ``` have meq: "measure lebesgue ((\v::(real, 'n) vec. \ i. v \$ Fun.swap m n id i) ` cbox a b) ``` lp15@67998 ` 509` ``` = measure lebesgue (cbox a b)" for a b ``` lp15@67998 ` 510` ``` proof (cases "cbox a b = {}") ``` lp15@67998 ` 511` ``` case True then show ?thesis ``` lp15@67998 ` 512` ``` by simp ``` lp15@67998 ` 513` ``` next ``` lp15@67998 ` 514` ``` case False ``` lp15@67998 ` 515` ``` then have him: "?h ` (cbox a b) \ {}" ``` lp15@67998 ` 516` ``` by blast ``` lp15@67998 ` 517` ``` have eq: "?h ` (cbox a b) = cbox (?h a) (?h b)" ``` lp15@67998 ` 518` ``` by (auto simp: image_iff lambda_swap_Galois mem_box_cart) (metis swap_id_eq)+ ``` lp15@67998 ` 519` ``` show ?thesis ``` lp15@67998 ` 520` ``` using him prod.permute [OF permutes_swap_id, where S=UNIV and g="\i. (b - a)\$i", symmetric] ``` lp15@67998 ` 521` ``` by (simp add: eq content_cbox_cart False) ``` lp15@67998 ` 522` ``` qed ``` lp15@67998 ` 523` ``` have "(\ i j. if Fun.swap m n id i = j then 1 else 0) = (\ i j. if j = Fun.swap m n id i then 1 else (0::real))" ``` lp15@67998 ` 524` ``` by (auto intro!: Cart_lambda_cong) ``` lp15@67998 ` 525` ``` then have "matrix ?h = transpose(\ i j. mat 1 \$ i \$ Fun.swap m n id j)" ``` lp15@67998 ` 526` ``` by (auto simp: matrix_eq transpose_def axis_def mat_def matrix_def) ``` lp15@67998 ` 527` ``` then have 1: "\det (matrix ?h)\ = 1" ``` lp15@67998 ` 528` ``` by (simp add: det_permute_columns permutes_swap_id sign_swap_id abs_mult) ``` lp15@67998 ` 529` ``` show "?h ` S \ lmeasurable \ ?Q ?h S" ``` lp15@67998 ` 530` ``` proof ``` lp15@67998 ` 531` ``` show "?h ` S \ lmeasurable" "?Q ?h S" ``` lp15@67998 ` 532` ``` using measure_linear_sufficient [OF lin \S \ lmeasurable\] meq 1 by force+ ``` lp15@67998 ` 533` ``` qed ``` lp15@67998 ` 534` ``` next ``` lp15@67998 ` 535` ``` fix m :: "'n" and n :: "'n" and S :: "(real, 'n) vec set" ``` lp15@67998 ` 536` ``` assume "m \ n" and "S \ lmeasurable" ``` lp15@67998 ` 537` ``` let ?h = "\v::(real, 'n) vec. \ i. if i = m then v \$ m + v \$ n else v \$ i" ``` lp15@67998 ` 538` ``` have lin: "linear ?h" ``` lp15@67998 ` 539` ``` by (auto simp: algebra_simps plus_vec_def scaleR_vec_def vec_eq_iff intro: linearI) ``` lp15@67998 ` 540` ``` consider "m < n" | " n < m" ``` lp15@67998 ` 541` ``` using \m \ n\ less_linear by blast ``` lp15@67998 ` 542` ``` then have 1: "det(matrix ?h) = 1" ``` lp15@67998 ` 543` ``` proof cases ``` lp15@67998 ` 544` ``` assume "m < n" ``` lp15@67998 ` 545` ``` have *: "matrix ?h \$ i \$ j = (0::real)" if "j < i" for i j :: 'n ``` lp15@67998 ` 546` ``` proof - ``` lp15@67998 ` 547` ``` have "axis j 1 = (\ n. if n = j then 1 else (0::real))" ``` lp15@67998 ` 548` ``` using axis_def by blast ``` lp15@67998 ` 549` ``` then have "(\ p q. if p = m then axis q 1 \$ m + axis q 1 \$ n else axis q 1 \$ p) \$ i \$ j = (0::real)" ``` lp15@67998 ` 550` ``` using \j < i\ axis_def \m < n\ by auto ``` lp15@67998 ` 551` ``` with \m < n\ show ?thesis ``` lp15@67998 ` 552` ``` by (auto simp: matrix_def axis_def cong: if_cong) ``` lp15@67998 ` 553` ``` qed ``` lp15@67998 ` 554` ``` show ?thesis ``` lp15@67998 ` 555` ``` using \m \ n\ by (subst det_upperdiagonal [OF *]) (auto simp: matrix_def axis_def cong: if_cong) ``` lp15@67998 ` 556` ``` next ``` lp15@67998 ` 557` ``` assume "n < m" ``` lp15@67998 ` 558` ``` have *: "matrix ?h \$ i \$ j = (0::real)" if "j > i" for i j :: 'n ``` lp15@67998 ` 559` ``` proof - ``` lp15@67998 ` 560` ``` have "axis j 1 = (\ n. if n = j then 1 else (0::real))" ``` lp15@67998 ` 561` ``` using axis_def by blast ``` lp15@67998 ` 562` ``` then have "(\ p q. if p = m then axis q 1 \$ m + axis q 1 \$ n else axis q 1 \$ p) \$ i \$ j = (0::real)" ``` lp15@67998 ` 563` ``` using \j > i\ axis_def \m > n\ by auto ``` lp15@67998 ` 564` ``` with \m > n\ show ?thesis ``` lp15@67998 ` 565` ``` by (auto simp: matrix_def axis_def cong: if_cong) ``` lp15@67998 ` 566` ``` qed ``` lp15@67998 ` 567` ``` show ?thesis ``` lp15@67998 ` 568` ``` using \m \ n\ ``` lp15@67998 ` 569` ``` by (subst det_lowerdiagonal [OF *]) (auto simp: matrix_def axis_def cong: if_cong) ``` lp15@67998 ` 570` ``` qed ``` lp15@67998 ` 571` ``` have meq: "measure lebesgue (?h ` (cbox a b)) = measure lebesgue (cbox a b)" for a b ``` lp15@67998 ` 572` ``` proof (cases "cbox a b = {}") ``` lp15@67998 ` 573` ``` case True then show ?thesis by simp ``` lp15@67998 ` 574` ``` next ``` lp15@67998 ` 575` ``` case False ``` lp15@67998 ` 576` ``` then have ne: "(+) (\ i. if i = n then - a \$ n else 0) ` cbox a b \ {}" ``` lp15@67998 ` 577` ``` by auto ``` lp15@67998 ` 578` ``` let ?v = "\ i. if i = n then - a \$ n else 0" ``` lp15@67998 ` 579` ``` have "?h ` cbox a b ``` lp15@67998 ` 580` ``` = (+) (\ i. if i = m \ i = n then a \$ n else 0) ` ?h ` (+) ?v ` (cbox a b)" ``` lp15@67998 ` 581` ``` using \m \ n\ unfolding image_comp o_def by (force simp: vec_eq_iff) ``` lp15@67998 ` 582` ``` then have "measure lebesgue (?h ` (cbox a b)) ``` lp15@67998 ` 583` ``` = measure lebesgue ((\v. \ i. if i = m then v \$ m + v \$ n else v \$ i) ` ``` lp15@67998 ` 584` ``` (+) ?v ` cbox a b)" ``` lp15@67998 ` 585` ``` by (rule ssubst) (rule measure_translation) ``` lp15@67998 ` 586` ``` also have "\ = measure lebesgue ((\v. \ i. if i = m then v \$ m + v \$ n else v \$ i) ` cbox (?v +a) (?v + b))" ``` lp15@67998 ` 587` ``` by (metis (no_types, lifting) cbox_translation) ``` lp15@67998 ` 588` ``` also have "\ = measure lebesgue ((+) (\ i. if i = n then - a \$ n else 0) ` cbox a b)" ``` lp15@67998 ` 589` ``` apply (subst measure_shear_interval) ``` lp15@67998 ` 590` ``` using \m \ n\ ne apply auto ``` lp15@67998 ` 591` ``` apply (simp add: cbox_translation) ``` lp15@67998 ` 592` ``` by (metis cbox_borel cbox_translation measure_completion sets_lborel) ``` lp15@67998 ` 593` ``` also have "\ = measure lebesgue (cbox a b)" ``` lp15@67998 ` 594` ``` by (rule measure_translation) ``` lp15@67998 ` 595` ``` finally show ?thesis . ``` lp15@67998 ` 596` ``` qed ``` lp15@67998 ` 597` ``` show "?h ` S \ lmeasurable \ ?Q ?h S" ``` lp15@67998 ` 598` ``` using measure_linear_sufficient [OF lin \S \ lmeasurable\] meq 1 by force ``` lp15@67998 ` 599` ``` qed ``` lp15@67998 ` 600` ``` with assms show "(f ` S) \ lmeasurable" "?Q f S" ``` lp15@67998 ` 601` ``` by metis+ ``` lp15@67998 ` 602` ```qed ``` lp15@67998 ` 603` lp15@67998 ` 604` lp15@67998 ` 605` ```lemma ``` lp15@67998 ` 606` ``` fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" ``` lp15@67998 ` 607` ``` assumes f: "orthogonal_transformation f" and S: "S \ lmeasurable" ``` lp15@67998 ` 608` ``` shows measurable_orthogonal_image: "f ` S \ lmeasurable" ``` lp15@67998 ` 609` ``` and measure_orthogonal_image: "measure lebesgue (f ` S) = measure lebesgue S" ``` lp15@67998 ` 610` ```proof - ``` lp15@67998 ` 611` ``` have "linear f" ``` lp15@67998 ` 612` ``` by (simp add: f orthogonal_transformation_linear) ``` lp15@67998 ` 613` ``` then show "f ` S \ lmeasurable" ``` lp15@67998 ` 614` ``` by (metis S measurable_linear_image) ``` lp15@67998 ` 615` ``` show "measure lebesgue (f ` S) = measure lebesgue S" ``` lp15@67998 ` 616` ``` by (simp add: measure_linear_image \linear f\ S f) ``` lp15@67998 ` 617` ```qed ``` lp15@67998 ` 618` lp15@67998 ` 619` ```lemma sets_lebesgue_inner_closed: ``` lp15@67998 ` 620` ``` assumes "S \ sets lebesgue" "e > 0" ``` lp15@67998 ` 621` ``` obtains T where "closed T" "T \ S" "S-T \ lmeasurable" "measure lebesgue (S - T) < e" ``` lp15@67998 ` 622` ```proof - ``` lp15@67998 ` 623` ``` have "-S \ sets lebesgue" ``` lp15@67998 ` 624` ``` using assms by (simp add: Compl_in_sets_lebesgue) ``` lp15@67998 ` 625` ``` then obtain T where "open T" "-S \ T" ``` lp15@67998 ` 626` ``` and T: "(T - -S) \ lmeasurable" "measure lebesgue (T - -S) < e" ``` lp15@67998 ` 627` ``` using lmeasurable_outer_open assms by blast ``` lp15@67998 ` 628` ``` show thesis ``` lp15@67998 ` 629` ``` proof ``` lp15@67998 ` 630` ``` show "closed (-T)" ``` lp15@67998 ` 631` ``` using \open T\ by blast ``` lp15@67998 ` 632` ``` show "-T \ S" ``` lp15@67998 ` 633` ``` using \- S \ T\ by auto ``` lp15@67998 ` 634` ``` show "S - ( -T) \ lmeasurable" "measure lebesgue (S - (- T)) < e" ``` lp15@67998 ` 635` ``` using T by (auto simp: Int_commute) ``` lp15@67998 ` 636` ``` qed ``` lp15@67998 ` 637` ```qed ``` lp15@67998 ` 638` lp15@67998 ` 639` ```subsection\@{text F_sigma} and @{text G_delta} sets.\ ``` lp15@67998 ` 640` lp15@67998 ` 641` ```(*https://en.wikipedia.org/wiki/F\_set*) ``` lp15@67998 ` 642` ```inductive fsigma :: "'a::topological_space set \ bool" where ``` lp15@67998 ` 643` ``` "(\n::nat. closed (F n)) \ fsigma (UNION UNIV F)" ``` lp15@67998 ` 644` lp15@67998 ` 645` ```inductive gdelta :: "'a::topological_space set \ bool" where ``` lp15@67998 ` 646` ``` "(\n::nat. open (F n)) \ gdelta (INTER UNIV F)" ``` lp15@67998 ` 647` lp15@67998 ` 648` lp15@67998 ` 649` ```lemma fsigma_Union_compact: ``` lp15@67998 ` 650` ``` fixes S :: "'a::{real_normed_vector,heine_borel} set" ``` lp15@67998 ` 651` ``` shows "fsigma S \ (\F::nat \ 'a set. range F \ Collect compact \ S = UNION UNIV F)" ``` lp15@67998 ` 652` ```proof safe ``` lp15@67998 ` 653` ``` assume "fsigma S" ``` lp15@67998 ` 654` ``` then obtain F :: "nat \ 'a set" where F: "range F \ Collect closed" "S = UNION UNIV F" ``` lp15@67998 ` 655` ``` by (meson fsigma.cases image_subsetI mem_Collect_eq) ``` lp15@67998 ` 656` ``` then have "\D::nat \ 'a set. range D \ Collect compact \ UNION UNIV D = F i" for i ``` lp15@67998 ` 657` ``` using closed_Union_compact_subsets [of "F i"] ``` lp15@67998 ` 658` ``` by (metis image_subsetI mem_Collect_eq range_subsetD) ``` lp15@67998 ` 659` ``` then obtain D :: "nat \ nat \ 'a set" ``` lp15@67998 ` 660` ``` where D: "\i. range (D i) \ Collect compact \ UNION UNIV (D i) = F i" ``` lp15@67998 ` 661` ``` by metis ``` lp15@67998 ` 662` ``` let ?DD = "\n. (\(i,j). D i j) (prod_decode n)" ``` lp15@67998 ` 663` ``` show "\F::nat \ 'a set. range F \ Collect compact \ S = UNION UNIV F" ``` lp15@67998 ` 664` ``` proof (intro exI conjI) ``` lp15@67998 ` 665` ``` show "range ?DD \ Collect compact" ``` lp15@67998 ` 666` ``` using D by clarsimp (metis mem_Collect_eq rangeI split_conv subsetCE surj_pair) ``` lp15@67998 ` 667` ``` show "S = UNION UNIV ?DD" ``` lp15@67998 ` 668` ``` proof ``` lp15@67998 ` 669` ``` show "S \ UNION UNIV ?DD" ``` lp15@67998 ` 670` ``` using D F ``` lp15@67998 ` 671` ``` by clarsimp (metis UN_iff old.prod.case prod_decode_inverse prod_encode_eq) ``` lp15@67998 ` 672` ``` show "UNION UNIV ?DD \ S" ``` lp15@67998 ` 673` ``` using D F by fastforce ``` lp15@67998 ` 674` ``` qed ``` lp15@67998 ` 675` ``` qed ``` lp15@67998 ` 676` ```next ``` lp15@67998 ` 677` ``` fix F :: "nat \ 'a set" ``` lp15@67998 ` 678` ``` assume "range F \ Collect compact" and "S = UNION UNIV F" ``` lp15@67998 ` 679` ``` then show "fsigma (UNION UNIV F)" ``` lp15@67998 ` 680` ``` by (simp add: compact_imp_closed fsigma.intros image_subset_iff) ``` lp15@67998 ` 681` ```qed ``` lp15@67998 ` 682` lp15@67998 ` 683` ```lemma gdelta_imp_fsigma: "gdelta S \ fsigma (- S)" ``` lp15@67998 ` 684` ```proof (induction rule: gdelta.induct) ``` lp15@67998 ` 685` ``` case (1 F) ``` lp15@67998 ` 686` ``` have "- INTER UNIV F = (\i. -(F i))" ``` lp15@67998 ` 687` ``` by auto ``` lp15@67998 ` 688` ``` then show ?case ``` lp15@67998 ` 689` ``` by (simp add: fsigma.intros closed_Compl 1) ``` lp15@67998 ` 690` ```qed ``` lp15@67998 ` 691` lp15@67998 ` 692` ```lemma fsigma_imp_gdelta: "fsigma S \ gdelta (- S)" ``` lp15@67998 ` 693` ```proof (induction rule: fsigma.induct) ``` lp15@67998 ` 694` ``` case (1 F) ``` lp15@67998 ` 695` ``` have "- UNION UNIV F = (\i. -(F i))" ``` lp15@67998 ` 696` ``` by auto ``` lp15@67998 ` 697` ``` then show ?case ``` lp15@67998 ` 698` ``` by (simp add: 1 gdelta.intros open_closed) ``` lp15@67998 ` 699` ```qed ``` lp15@67998 ` 700` lp15@67998 ` 701` lp15@67998 ` 702` lp15@67998 ` 703` ```lemma gdelta_complement: "gdelta(- S) \ fsigma S" ``` lp15@67998 ` 704` ``` using fsigma_imp_gdelta gdelta_imp_fsigma by force ``` lp15@67998 ` 705` lp15@67998 ` 706` lp15@67998 ` 707` ```text\A Lebesgue set is almost an @{text F_sigma} or @{text G_delta}.\ ``` lp15@67998 ` 708` ```lemma lebesgue_set_almost_fsigma: ``` lp15@67998 ` 709` ``` assumes "S \ sets lebesgue" ``` lp15@67998 ` 710` ``` obtains C T where "fsigma C" "negligible T" "C \ T = S" "disjnt C T" ``` lp15@67998 ` 711` ```proof - ``` lp15@67998 ` 712` ``` { fix n::nat ``` lp15@67998 ` 713` ``` have "\T. closed T \ T \ S \ S - T \ lmeasurable \ measure lebesgue (S-T) < 1 / Suc n" ``` lp15@67998 ` 714` ``` using sets_lebesgue_inner_closed [OF assms] ``` lp15@67998 ` 715` ``` by (metis divide_pos_pos less_numeral_extra(1) of_nat_0_less_iff zero_less_Suc) ``` lp15@67998 ` 716` ``` } ``` lp15@67998 ` 717` ``` then obtain F where F: "\n::nat. closed (F n) \ F n \ S \ S - F n \ lmeasurable \ measure lebesgue (S - F n) < 1 / Suc n" ``` lp15@67998 ` 718` ``` by metis ``` lp15@67998 ` 719` ``` let ?C = "UNION UNIV F" ``` lp15@67998 ` 720` ``` show thesis ``` lp15@67998 ` 721` ``` proof ``` lp15@67998 ` 722` ``` show "fsigma ?C" ``` lp15@67998 ` 723` ``` using F by (simp add: fsigma.intros) ``` lp15@67998 ` 724` ``` show "negligible (S - ?C)" ``` lp15@67998 ` 725` ``` proof (clarsimp simp add: negligible_outer_le) ``` lp15@67998 ` 726` ``` fix e :: "real" ``` lp15@67998 ` 727` ``` assume "0 < e" ``` lp15@67998 ` 728` ``` then obtain n where n: "1 / Suc n < e" ``` lp15@67998 ` 729` ``` using nat_approx_posE by metis ``` lp15@67998 ` 730` ``` show "\T. S - (\x. F x) \ T \ T \ lmeasurable \ measure lebesgue T \ e" ``` lp15@67998 ` 731` ``` proof (intro exI conjI) ``` lp15@67998 ` 732` ``` show "measure lebesgue (S - F n) \ e" ``` lp15@67998 ` 733` ``` by (meson F n less_trans not_le order.asym) ``` lp15@67998 ` 734` ``` qed (use F in auto) ``` lp15@67998 ` 735` ``` qed ``` lp15@67998 ` 736` ``` show "?C \ (S - ?C) = S" ``` lp15@67998 ` 737` ``` using F by blast ``` lp15@67998 ` 738` ``` show "disjnt ?C (S - ?C)" ``` lp15@67998 ` 739` ``` by (auto simp: disjnt_def) ``` lp15@67998 ` 740` ``` qed ``` lp15@67998 ` 741` ```qed ``` lp15@67998 ` 742` lp15@67998 ` 743` ```lemma lebesgue_set_almost_gdelta: ``` lp15@67998 ` 744` ``` assumes "S \ sets lebesgue" ``` lp15@67998 ` 745` ``` obtains C T where "gdelta C" "negligible T" "S \ T = C" "disjnt S T" ``` lp15@67998 ` 746` ```proof - ``` lp15@67998 ` 747` ``` have "-S \ sets lebesgue" ``` lp15@67998 ` 748` ``` using assms Compl_in_sets_lebesgue by blast ``` lp15@67998 ` 749` ``` then obtain C T where C: "fsigma C" "negligible T" "C \ T = -S" "disjnt C T" ``` lp15@67998 ` 750` ``` using lebesgue_set_almost_fsigma by metis ``` lp15@67998 ` 751` ``` show thesis ``` lp15@67998 ` 752` ``` proof ``` lp15@67998 ` 753` ``` show "gdelta (-C)" ``` lp15@67998 ` 754` ``` by (simp add: \fsigma C\ fsigma_imp_gdelta) ``` lp15@67998 ` 755` ``` show "S \ T = -C" "disjnt S T" ``` lp15@67998 ` 756` ``` using C by (auto simp: disjnt_def) ``` lp15@67998 ` 757` ``` qed (use C in auto) ``` lp15@67998 ` 758` ```qed ``` lp15@67998 ` 759` lp15@67998 ` 760` lp15@67998 ` 761` ```proposition measure_semicontinuous_with_hausdist_explicit: ``` lp15@67998 ` 762` ``` assumes "bounded S" and neg: "negligible(frontier S)" and "e > 0" ``` lp15@67998 ` 763` ``` obtains d where "d > 0" ``` lp15@67998 ` 764` ``` "\T. \T \ lmeasurable; \y. y \ T \ \x. x \ S \ dist x y < d\ ``` lp15@67998 ` 765` ``` \ measure lebesgue T < measure lebesgue S + e" ``` lp15@67998 ` 766` ```proof (cases "S = {}") ``` lp15@67998 ` 767` ``` case True ``` lp15@67998 ` 768` ``` with that \e > 0\ show ?thesis by force ``` lp15@67998 ` 769` ```next ``` lp15@67998 ` 770` ``` case False ``` lp15@67998 ` 771` ``` then have frS: "frontier S \ {}" ``` lp15@67998 ` 772` ``` using \bounded S\ frontier_eq_empty not_bounded_UNIV by blast ``` lp15@67998 ` 773` ``` have "S \ lmeasurable" ``` lp15@67998 ` 774` ``` by (simp add: \bounded S\ measurable_Jordan neg) ``` lp15@67998 ` 775` ``` have null: "(frontier S) \ null_sets lebesgue" ``` lp15@67998 ` 776` ``` by (metis neg negligible_iff_null_sets) ``` lp15@67998 ` 777` ``` have "frontier S \ lmeasurable" and mS0: "measure lebesgue (frontier S) = 0" ``` lp15@67998 ` 778` ``` using neg negligible_imp_measurable negligible_iff_measure by blast+ ``` lp15@67998 ` 779` ``` with \e > 0\ lmeasurable_outer_open ``` lp15@67998 ` 780` ``` obtain U where "open U" ``` lp15@67998 ` 781` ``` and U: "frontier S \ U" "U - frontier S \ lmeasurable" "measure lebesgue (U - frontier S) < e" ``` lp15@67998 ` 782` ``` by (metis fmeasurableD) ``` lp15@67998 ` 783` ``` with null have "U \ lmeasurable" ``` lp15@67998 ` 784` ``` by (metis borel_open measurable_Diff_null_set sets_completionI_sets sets_lborel) ``` lp15@67998 ` 785` ``` have "measure lebesgue (U - frontier S) = measure lebesgue U" ``` lp15@67998 ` 786` ``` using mS0 by (simp add: \U \ lmeasurable\ fmeasurableD measure_Diff_null_set null) ``` lp15@67998 ` 787` ``` with U have mU: "measure lebesgue U < e" ``` lp15@67998 ` 788` ``` by simp ``` lp15@67998 ` 789` ``` show ?thesis ``` lp15@67998 ` 790` ``` proof ``` lp15@67998 ` 791` ``` have "U \ UNIV" ``` lp15@67998 ` 792` ``` using \U \ lmeasurable\ by auto ``` lp15@67998 ` 793` ``` then have "- U \ {}" ``` lp15@67998 ` 794` ``` by blast ``` lp15@67998 ` 795` ``` with \open U\ \frontier S \ U\ show "setdist (frontier S) (- U) > 0" ``` lp15@67998 ` 796` ``` by (auto simp: \bounded S\ open_closed compact_frontier_bounded setdist_gt_0_compact_closed frS) ``` lp15@67998 ` 797` ``` fix T ``` lp15@67998 ` 798` ``` assume "T \ lmeasurable" ``` lp15@67998 ` 799` ``` and T: "\t. t \ T \ \y. y \ S \ dist y t < setdist (frontier S) (- U)" ``` lp15@67998 ` 800` ``` then have "measure lebesgue T - measure lebesgue S \ measure lebesgue (T - S)" ``` lp15@67998 ` 801` ``` by (simp add: \S \ lmeasurable\ measure_diff_le_measure_setdiff) ``` lp15@67998 ` 802` ``` also have "\ \ measure lebesgue U" ``` lp15@67998 ` 803` ``` proof - ``` lp15@67998 ` 804` ``` have "T - S \ U" ``` lp15@67998 ` 805` ``` proof clarify ``` lp15@67998 ` 806` ``` fix x ``` lp15@67998 ` 807` ``` assume "x \ T" and "x \ S" ``` lp15@67998 ` 808` ``` then obtain y where "y \ S" and y: "dist y x < setdist (frontier S) (- U)" ``` lp15@67998 ` 809` ``` using T by blast ``` lp15@67998 ` 810` ``` have "closed_segment x y \ frontier S \ {}" ``` lp15@67998 ` 811` ``` using connected_Int_frontier \x \ S\ \y \ S\ by blast ``` lp15@67998 ` 812` ``` then obtain z where z: "z \ closed_segment x y" "z \ frontier S" ``` lp15@67998 ` 813` ``` by auto ``` lp15@67998 ` 814` ``` with y have "dist z x < setdist(frontier S) (- U)" ``` lp15@67998 ` 815` ``` by (auto simp: dist_commute dest!: dist_in_closed_segment) ``` lp15@67998 ` 816` ``` with z have False if "x \ -U" ``` lp15@67998 ` 817` ``` using setdist_le_dist [OF \z \ frontier S\ that] by auto ``` lp15@67998 ` 818` ``` then show "x \ U" ``` lp15@67998 ` 819` ``` by blast ``` lp15@67998 ` 820` ``` qed ``` lp15@67998 ` 821` ``` then show ?thesis ``` lp15@67998 ` 822` ``` by (simp add: \S \ lmeasurable\ \T \ lmeasurable\ \U \ lmeasurable\ fmeasurableD measure_mono_fmeasurable sets.Diff) ``` lp15@67998 ` 823` ``` qed ``` lp15@67998 ` 824` ``` finally have "measure lebesgue T - measure lebesgue S \ measure lebesgue U" . ``` lp15@67998 ` 825` ``` with mU show "measure lebesgue T < measure lebesgue S + e" ``` lp15@67998 ` 826` ``` by linarith ``` lp15@67998 ` 827` ``` qed ``` lp15@67998 ` 828` ```qed ``` lp15@67998 ` 829` lp15@67998 ` 830` ```proposition lebesgue_regular_inner: ``` lp15@67998 ` 831` ``` assumes "S \ sets lebesgue" ``` lp15@67998 ` 832` ``` obtains K C where "negligible K" "\n::nat. compact(C n)" "S = (\n. C n) \ K" ``` lp15@67998 ` 833` ```proof - ``` lp15@67998 ` 834` ``` have "\T. closed T \ T \ S \ (S - T) \ lmeasurable \ measure lebesgue (S - T) < (1/2)^n" for n ``` lp15@67998 ` 835` ``` using sets_lebesgue_inner_closed assms ``` lp15@67998 ` 836` ``` by (metis sets_lebesgue_inner_closed zero_less_divide_1_iff zero_less_numeral zero_less_power) ``` lp15@67998 ` 837` ``` then obtain C where clo: "\n. closed (C n)" and subS: "\n. C n \ S" ``` lp15@67998 ` 838` ``` and mea: "\n. (S - C n) \ lmeasurable" ``` lp15@67998 ` 839` ``` and less: "\n. measure lebesgue (S - C n) < (1/2)^n" ``` lp15@67998 ` 840` ``` by metis ``` lp15@67998 ` 841` ``` have "\F. (\n::nat. compact(F n)) \ (\n. F n) = C m" for m::nat ``` lp15@67998 ` 842` ``` by (metis clo closed_Union_compact_subsets) ``` lp15@67998 ` 843` ``` then obtain D :: "[nat,nat] \ 'a set" where D: "\m n. compact(D m n)" "\m. (\n. D m n) = C m" ``` lp15@67998 ` 844` ``` by metis ``` lp15@67998 ` 845` ``` let ?C = "from_nat_into (\m. range (D m))" ``` lp15@67998 ` 846` ``` have "countable (\m. range (D m))" ``` lp15@67998 ` 847` ``` by blast ``` lp15@67998 ` 848` ``` have "range (from_nat_into (\m. range (D m))) = (\m. range (D m))" ``` lp15@67998 ` 849` ``` using range_from_nat_into by simp ``` lp15@67998 ` 850` ``` then have CD: "\m n. ?C k = D m n" for k ``` lp15@67998 ` 851` ``` by (metis (mono_tags, lifting) UN_iff rangeE range_eqI) ``` lp15@67998 ` 852` ``` show thesis ``` lp15@67998 ` 853` ``` proof ``` lp15@67998 ` 854` ``` show "negligible (S - (\n. C n))" ``` lp15@67998 ` 855` ``` proof (clarsimp simp: negligible_outer_le) ``` lp15@67998 ` 856` ``` fix e :: "real" ``` lp15@67998 ` 857` ``` assume "e > 0" ``` lp15@67998 ` 858` ``` then obtain n where n: "(1/2)^n < e" ``` lp15@67998 ` 859` ``` using real_arch_pow_inv [of e "1/2"] by auto ``` lp15@67998 ` 860` ``` show "\T. S - (\n. C n) \ T \ T \ lmeasurable \ measure lebesgue T \ e" ``` lp15@67998 ` 861` ``` proof (intro exI conjI) ``` lp15@67998 ` 862` ``` show "S - (\n. C n) \ S - C n" ``` lp15@67998 ` 863` ``` by blast ``` lp15@67998 ` 864` ``` show "S - C n \ lmeasurable" ``` lp15@67998 ` 865` ``` by (simp add: mea) ``` lp15@67998 ` 866` ``` show "measure lebesgue (S - C n) \ e" ``` lp15@67998 ` 867` ``` using less [of n] n by simp ``` lp15@67998 ` 868` ``` qed ``` lp15@67998 ` 869` ``` qed ``` lp15@67998 ` 870` ``` show "compact (?C n)" for n ``` lp15@67998 ` 871` ``` using CD D by metis ``` lp15@67998 ` 872` ``` show "S = (\n. ?C n) \ (S - (\n. C n))" (is "_ = ?rhs") ``` lp15@67998 ` 873` ``` proof ``` lp15@67998 ` 874` ``` show "S \ ?rhs" ``` lp15@67998 ` 875` ``` using D by fastforce ``` lp15@67998 ` 876` ``` show "?rhs \ S" ``` lp15@67998 ` 877` ``` using subS D CD by auto (metis Sup_upper range_eqI subsetCE) ``` lp15@67998 ` 878` ``` qed ``` lp15@67998 ` 879` ``` qed ``` lp15@67998 ` 880` ```qed ``` lp15@67998 ` 881` lp15@67998 ` 882` lp15@67998 ` 883` ```lemma sets_lebesgue_continuous_image: ``` lp15@67998 ` 884` ``` assumes T: "T \ sets lebesgue" and contf: "continuous_on S f" ``` lp15@67998 ` 885` ``` and negim: "\T. \negligible T; T \ S\ \ negligible(f ` T)" and "T \ S" ``` lp15@67998 ` 886` ``` shows "f ` T \ sets lebesgue" ``` lp15@67998 ` 887` ```proof - ``` lp15@67998 ` 888` ``` obtain K C where "negligible K" and com: "\n::nat. compact(C n)" and Teq: "T = (\n. C n) \ K" ``` lp15@67998 ` 889` ``` using lebesgue_regular_inner [OF T] by metis ``` lp15@67998 ` 890` ``` then have comf: "\n::nat. compact(f ` C n)" ``` lp15@67998 ` 891` ``` by (metis Un_subset_iff Union_upper \T \ S\ compact_continuous_image contf continuous_on_subset rangeI) ``` lp15@67998 ` 892` ``` have "((\n. f ` C n) \ f ` K) \ sets lebesgue" ``` lp15@67998 ` 893` ``` proof (rule sets.Un) ``` lp15@67998 ` 894` ``` have "K \ S" ``` lp15@67998 ` 895` ``` using Teq \T \ S\ by blast ``` lp15@67998 ` 896` ``` show "(\n. f ` C n) \ sets lebesgue" ``` lp15@67998 ` 897` ``` proof (rule sets.countable_Union) ``` lp15@67998 ` 898` ``` show "range (\n. f ` C n) \ sets lebesgue" ``` lp15@67998 ` 899` ``` using borel_compact comf by (auto simp: borel_compact) ``` lp15@67998 ` 900` ``` qed auto ``` lp15@67998 ` 901` ``` show "f ` K \ sets lebesgue" ``` lp15@67998 ` 902` ``` by (simp add: \K \ S\ \negligible K\ negim negligible_imp_sets) ``` lp15@67998 ` 903` ``` qed ``` lp15@67998 ` 904` ``` then show ?thesis ``` lp15@67998 ` 905` ``` by (simp add: Teq image_Un image_Union) ``` lp15@67998 ` 906` ```qed ``` lp15@67998 ` 907` lp15@67998 ` 908` ```lemma differentiable_image_in_sets_lebesgue: ``` lp15@67998 ` 909` ``` fixes f :: "'m::euclidean_space \ 'n::euclidean_space" ``` lp15@67998 ` 910` ``` assumes S: "S \ sets lebesgue" and dim: "DIM('m) \ DIM('n)" and f: "f differentiable_on S" ``` lp15@67998 ` 911` ``` shows "f`S \ sets lebesgue" ``` lp15@67998 ` 912` ```proof (rule sets_lebesgue_continuous_image [OF S]) ``` lp15@67998 ` 913` ``` show "continuous_on S f" ``` lp15@67998 ` 914` ``` by (meson differentiable_imp_continuous_on f) ``` lp15@67998 ` 915` ``` show "\T. \negligible T; T \ S\ \ negligible (f ` T)" ``` lp15@67998 ` 916` ``` using differentiable_on_subset f ``` lp15@67998 ` 917` ``` by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim]) ``` lp15@67998 ` 918` ```qed auto ``` lp15@67998 ` 919` lp15@67998 ` 920` ```lemma sets_lebesgue_on_continuous_image: ``` lp15@67998 ` 921` ``` assumes S: "S \ sets lebesgue" and X: "X \ sets (lebesgue_on S)" and contf: "continuous_on S f" ``` lp15@67998 ` 922` ``` and negim: "\T. \negligible T; T \ S\ \ negligible(f ` T)" ``` lp15@67998 ` 923` ``` shows "f ` X \ sets (lebesgue_on (f ` S))" ``` lp15@67998 ` 924` ```proof - ``` lp15@67998 ` 925` ``` have "X \ S" ``` lp15@67998 ` 926` ``` by (metis S X sets.Int_space_eq2 sets_restrict_space_iff) ``` lp15@67998 ` 927` ``` moreover have "f ` S \ sets lebesgue" ``` lp15@67998 ` 928` ``` using S contf negim sets_lebesgue_continuous_image by blast ``` lp15@67998 ` 929` ``` moreover have "f ` X \ sets lebesgue" ``` lp15@67998 ` 930` ``` by (metis S X contf negim sets_lebesgue_continuous_image sets_restrict_space_iff space_restrict_space space_restrict_space2) ``` lp15@67998 ` 931` ``` ultimately show ?thesis ``` lp15@67998 ` 932` ``` by (auto simp: sets_restrict_space_iff) ``` lp15@67998 ` 933` ```qed ``` lp15@67998 ` 934` lp15@67998 ` 935` ```lemma differentiable_image_in_sets_lebesgue_on: ``` lp15@67998 ` 936` ``` fixes f :: "'m::euclidean_space \ 'n::euclidean_space" ``` lp15@67998 ` 937` ``` assumes S: "S \ sets lebesgue" and X: "X \ sets (lebesgue_on S)" and dim: "DIM('m) \ DIM('n)" ``` lp15@67998 ` 938` ``` and f: "f differentiable_on S" ``` lp15@67998 ` 939` ``` shows "f ` X \ sets (lebesgue_on (f`S))" ``` lp15@67998 ` 940` ```proof (rule sets_lebesgue_on_continuous_image [OF S X]) ``` lp15@67998 ` 941` ``` show "continuous_on S f" ``` lp15@67998 ` 942` ``` by (meson differentiable_imp_continuous_on f) ``` lp15@67998 ` 943` ``` show "\T. \negligible T; T \ S\ \ negligible (f ` T)" ``` lp15@67998 ` 944` ``` using differentiable_on_subset f ``` lp15@67998 ` 945` ``` by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim]) ``` lp15@67998 ` 946` ```qed ``` lp15@67998 ` 947` lp15@67998 ` 948` lp15@67998 ` 949` ```proposition ``` lp15@67998 ` 950` ``` fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" ``` lp15@67998 ` 951` ``` assumes S: "S \ lmeasurable" ``` lp15@67998 ` 952` ``` and deriv: "\x. x \ S \ (f has_derivative f' x) (at x within S)" ``` lp15@67998 ` 953` ``` and int: "(\x. \det (matrix (f' x))\) integrable_on S" ``` lp15@67998 ` 954` ``` and bounded: "\x. x \ S \ \det (matrix (f' x))\ \ B" ``` lp15@67998 ` 955` ``` shows measurable_bounded_differentiable_image: ``` lp15@67998 ` 956` ``` "f ` S \ lmeasurable" ``` lp15@67998 ` 957` ``` and measure_bounded_differentiable_image: ``` lp15@67998 ` 958` ``` "measure lebesgue (f ` S) \ B * measure lebesgue S" (is "?M") ``` lp15@67998 ` 959` ```proof - ``` lp15@67998 ` 960` ``` have "f ` S \ lmeasurable \ measure lebesgue (f ` S) \ B * measure lebesgue S" ``` lp15@67998 ` 961` ``` proof (cases "B < 0") ``` lp15@67998 ` 962` ``` case True ``` lp15@67998 ` 963` ``` then have "S = {}" ``` lp15@67998 ` 964` ``` by (meson abs_ge_zero bounded empty_iff equalityI less_le_trans linorder_not_less subsetI) ``` lp15@67998 ` 965` ``` then show ?thesis ``` lp15@67998 ` 966` ``` by auto ``` lp15@67998 ` 967` ``` next ``` lp15@67998 ` 968` ``` case False ``` lp15@67998 ` 969` ``` then have "B \ 0" ``` lp15@67998 ` 970` ``` by arith ``` lp15@67998 ` 971` ``` let ?\ = "measure lebesgue" ``` lp15@67998 ` 972` ``` have f_diff: "f differentiable_on S" ``` lp15@67998 ` 973` ``` using deriv by (auto simp: differentiable_on_def differentiable_def) ``` lp15@67998 ` 974` ``` have eps: "f ` S \ lmeasurable" "?\ (f ` S) \ (B+e) * ?\ S" (is "?ME") ``` lp15@67998 ` 975` ``` if "e > 0" for e ``` lp15@67998 ` 976` ``` proof - ``` lp15@67998 ` 977` ``` have eps_d: "f ` S \ lmeasurable" "?\ (f ` S) \ (B+e) * (?\ S + d)" (is "?MD") ``` lp15@67998 ` 978` ``` if "d > 0" for d ``` lp15@67998 ` 979` ``` proof - ``` lp15@67998 ` 980` ``` obtain T where "open T" "S \ T" and TS: "(T-S) \ lmeasurable" and "?\ (T-S) < d" ``` lp15@67998 ` 981` ``` using S \d > 0\ lmeasurable_outer_open by blast ``` lp15@67998 ` 982` ``` with S have "T \ lmeasurable" and Tless: "?\ T < ?\ S + d" ``` lp15@67998 ` 983` ``` by (auto simp: measurable_measure_Diff dest!: fmeasurable_Diff_D) ``` lp15@67998 ` 984` ``` have "\r. 0 < r \ r < d \ ball x r \ T \ f ` (S \ ball x r) \ lmeasurable \ ``` lp15@67998 ` 985` ``` ?\ (f ` (S \ ball x r)) \ (B + e) * ?\ (ball x r)" ``` lp15@67998 ` 986` ``` if "x \ S" "d > 0" for x d ``` lp15@67998 ` 987` ``` proof - ``` lp15@67998 ` 988` ``` have lin: "linear (f' x)" ``` lp15@67998 ` 989` ``` and lim0: "((\y. (f y - (f x + f' x (y - x))) /\<^sub>R norm(y - x)) \ 0) (at x within S)" ``` lp15@67998 ` 990` ``` using deriv \x \ S\ by (auto simp: has_derivative_within bounded_linear.linear field_simps) ``` lp15@67998 ` 991` ``` have bo: "bounded (f' x ` ball 0 1)" ``` lp15@67998 ` 992` ``` by (simp add: bounded_linear_image linear_linear lin) ``` lp15@67998 ` 993` ``` have neg: "negligible (frontier (f' x ` ball 0 1))" ``` lp15@67998 ` 994` ``` using deriv has_derivative_linear \x \ S\ ``` lp15@67998 ` 995` ``` by (auto intro!: negligible_convex_frontier [OF convex_linear_image]) ``` lp15@67998 ` 996` ``` have 0: "0 < e * unit_ball_vol (real CARD('n))" ``` lp15@67998 ` 997` ``` using \e > 0\ by simp ``` lp15@67998 ` 998` ``` obtain k where "k > 0" and k: ``` lp15@67998 ` 999` ``` "\U. \U \ lmeasurable; \y. y \ U \ \z. z \ f' x ` ball 0 1 \ dist z y < k\ ``` lp15@67998 ` 1000` ``` \ ?\ U < ?\ (f' x ` ball 0 1) + e * unit_ball_vol (CARD('n))" ``` lp15@67998 ` 1001` ``` using measure_semicontinuous_with_hausdist_explicit [OF bo neg 0] by blast ``` lp15@67998 ` 1002` ``` obtain l where "l > 0" and l: "ball x l \ T" ``` lp15@67998 ` 1003` ``` using \x \ S\ \open T\ \S \ T\ openE by blast ``` lp15@67998 ` 1004` ``` obtain \ where "0 < \" ``` lp15@67998 ` 1005` ``` and \: "\y. \y \ S; y \ x; dist y x < \\ ``` lp15@67998 ` 1006` ``` \ norm (f y - (f x + f' x (y - x))) / norm (y - x) < k" ``` lp15@67998 ` 1007` ``` using lim0 \k > 0\ by (force simp: Lim_within field_simps) ``` lp15@67998 ` 1008` ``` define r where "r \ min (min l (\/2)) (min 1 (d/2))" ``` lp15@67998 ` 1009` ``` show ?thesis ``` lp15@67998 ` 1010` ``` proof (intro exI conjI) ``` lp15@67998 ` 1011` ``` show "r > 0" "r < d" ``` lp15@67998 ` 1012` ``` using \l > 0\ \\ > 0\ \d > 0\ by (auto simp: r_def) ``` lp15@67998 ` 1013` ``` have "r \ l" ``` lp15@67998 ` 1014` ``` by (auto simp: r_def) ``` lp15@67998 ` 1015` ``` with l show "ball x r \ T" ``` lp15@67998 ` 1016` ``` by auto ``` lp15@67998 ` 1017` ``` have ex_lessK: "\x' \ ball 0 1. dist (f' x x') ((f y - f x) /\<^sub>R r) < k" ``` lp15@67998 ` 1018` ``` if "y \ S" and "dist x y < r" for y ``` lp15@67998 ` 1019` ``` proof (cases "y = x") ``` lp15@67998 ` 1020` ``` case True ``` lp15@67998 ` 1021` ``` with lin linear_0 \k > 0\ that show ?thesis ``` lp15@67998 ` 1022` ``` by (rule_tac x=0 in bexI) (auto simp: linear_0) ``` lp15@67998 ` 1023` ``` next ``` lp15@67998 ` 1024` ``` case False ``` lp15@67998 ` 1025` ``` then show ?thesis ``` lp15@67998 ` 1026` ``` proof (rule_tac x="(y - x) /\<^sub>R r" in bexI) ``` lp15@67998 ` 1027` ``` have "f' x ((y - x) /\<^sub>R r) = f' x (y - x) /\<^sub>R r" ``` lp15@67998 ` 1028` ``` by (simp add: lin linear_cmul) ``` lp15@67998 ` 1029` ``` then have "dist (f' x ((y - x) /\<^sub>R r)) ((f y - f x) /\<^sub>R r) = norm (f' x (y - x) /\<^sub>R r - (f y - f x) /\<^sub>R r)" ``` lp15@67998 ` 1030` ``` by (simp add: dist_norm) ``` lp15@67998 ` 1031` ``` also have "\ = norm (f' x (y - x) - (f y - f x)) / r" ``` lp15@67998 ` 1032` ``` using \r > 0\ by (simp add: real_vector.scale_right_diff_distrib [symmetric] divide_simps) ``` lp15@67998 ` 1033` ``` also have "\ \ norm (f y - (f x + f' x (y - x))) / norm (y - x)" ``` lp15@67998 ` 1034` ``` using that \r > 0\ False by (simp add: algebra_simps divide_simps dist_norm norm_minus_commute mult_right_mono) ``` lp15@67998 ` 1035` ``` also have "\ < k" ``` lp15@67998 ` 1036` ``` using that \0 < \\ by (simp add: dist_commute r_def \ [OF \y \ S\ False]) ``` lp15@67998 ` 1037` ``` finally show "dist (f' x ((y - x) /\<^sub>R r)) ((f y - f x) /\<^sub>R r) < k" . ``` lp15@67998 ` 1038` ``` show "(y - x) /\<^sub>R r \ ball 0 1" ``` lp15@67998 ` 1039` ``` using that \r > 0\ by (simp add: dist_norm divide_simps norm_minus_commute) ``` lp15@67998 ` 1040` ``` qed ``` lp15@67998 ` 1041` ``` qed ``` lp15@67998 ` 1042` ``` let ?rfs = "(\x. x /\<^sub>R r) ` (+) (- f x) ` f ` (S \ ball x r)" ``` lp15@67998 ` 1043` ``` have rfs_mble: "?rfs \ lmeasurable" ``` lp15@67998 ` 1044` ``` proof (rule bounded_set_imp_lmeasurable) ``` lp15@67998 ` 1045` ``` have "f differentiable_on S \ ball x r" ``` lp15@67998 ` 1046` ``` using f_diff by (auto simp: fmeasurableD differentiable_on_subset) ``` lp15@67998 ` 1047` ``` with S show "?rfs \ sets lebesgue" ``` lp15@67998 ` 1048` ``` by (auto simp: sets.Int intro!: lebesgue_sets_translation differentiable_image_in_sets_lebesgue) ``` lp15@67998 ` 1049` ``` let ?B = "(\(x, y). x + y) ` (f' x ` ball 0 1 \ ball 0 k)" ``` lp15@67998 ` 1050` ``` have "bounded ?B" ``` lp15@67998 ` 1051` ``` by (simp add: bounded_plus [OF bo]) ``` lp15@67998 ` 1052` ``` moreover have "?rfs \ ?B" ``` lp15@67998 ` 1053` ``` apply (auto simp: dist_norm image_iff dest!: ex_lessK) ``` lp15@67998 ` 1054` ``` by (metis (no_types, hide_lams) add.commute diff_add_cancel dist_0_norm dist_commute dist_norm mem_ball) ``` lp15@67998 ` 1055` ``` ultimately show "bounded (?rfs)" ``` lp15@67998 ` 1056` ``` by (rule bounded_subset) ``` lp15@67998 ` 1057` ``` qed ``` lp15@67998 ` 1058` ``` then have "(\x. r *\<^sub>R x) ` ?rfs \ lmeasurable" ``` lp15@67998 ` 1059` ``` by (simp add: measurable_linear_image) ``` lp15@67998 ` 1060` ``` with \r > 0\ have "(+) (- f x) ` f ` (S \ ball x r) \ lmeasurable" ``` lp15@67998 ` 1061` ``` by (simp add: image_comp o_def) ``` lp15@67998 ` 1062` ``` then have "(+) (f x) ` (+) (- f x) ` f ` (S \ ball x r) \ lmeasurable" ``` lp15@67998 ` 1063` ``` using measurable_translation by blast ``` lp15@67998 ` 1064` ``` then show fsb: "f ` (S \ ball x r) \ lmeasurable" ``` lp15@67998 ` 1065` ``` by (simp add: image_comp o_def) ``` lp15@67998 ` 1066` ``` have "?\ (f ` (S \ ball x r)) = ?\ (?rfs) * r ^ CARD('n)" ``` lp15@67998 ` 1067` ``` using \r > 0\ by (simp add: measure_translation measure_linear_image measurable_translation fsb field_simps) ``` lp15@67998 ` 1068` ``` also have "\ \ (\det (matrix (f' x))\ * unit_ball_vol (CARD('n)) + e * unit_ball_vol (CARD('n))) * r ^ CARD('n)" ``` lp15@67998 ` 1069` ``` proof - ``` lp15@67998 ` 1070` ``` have "?\ (?rfs) < ?\ (f' x ` ball 0 1) + e * unit_ball_vol (CARD('n))" ``` lp15@67998 ` 1071` ``` using rfs_mble by (force intro: k dest!: ex_lessK) ``` lp15@67998 ` 1072` ``` then have "?\ (?rfs) < \det (matrix (f' x))\ * unit_ball_vol (CARD('n)) + e * unit_ball_vol (CARD('n))" ``` lp15@67998 ` 1073` ``` by (simp add: lin measure_linear_image [of "f' x"] content_ball) ``` lp15@67998 ` 1074` ``` with \r > 0\ show ?thesis ``` lp15@67998 ` 1075` ``` by auto ``` lp15@67998 ` 1076` ``` qed ``` lp15@67998 ` 1077` ``` also have "\ \ (B + e) * ?\ (ball x r)" ``` lp15@67998 ` 1078` ``` using bounded [OF \x \ S\] \r > 0\ by (simp add: content_ball algebra_simps) ``` lp15@67998 ` 1079` ``` finally show "?\ (f ` (S \ ball x r)) \ (B + e) * ?\ (ball x r)" . ``` lp15@67998 ` 1080` ``` qed ``` lp15@67998 ` 1081` ``` qed ``` lp15@67998 ` 1082` ``` then obtain r where ``` lp15@67998 ` 1083` ``` r0d: "\x d. \x \ S; d > 0\ \ 0 < r x d \ r x d < d" ``` lp15@67998 ` 1084` ``` and rT: "\x d. \x \ S; d > 0\ \ ball x (r x d) \ T" ``` lp15@67998 ` 1085` ``` and r: "\x d. \x \ S; d > 0\ \ ``` lp15@67998 ` 1086` ``` (f ` (S \ ball x (r x d))) \ lmeasurable \ ``` lp15@67998 ` 1087` ``` ?\ (f ` (S \ ball x (r x d))) \ (B + e) * ?\ (ball x (r x d))" ``` lp15@67998 ` 1088` ``` by metis ``` lp15@67998 ` 1089` ``` obtain C where "countable C" and Csub: "C \ {(x,r x t) |x t. x \ S \ 0 < t}" ``` lp15@67998 ` 1090` ``` and pwC: "pairwise (\i j. disjnt (ball (fst i) (snd i)) (ball (fst j) (snd j))) C" ``` lp15@67998 ` 1091` ``` and negC: "negligible(S - (\i \ C. ball (fst i) (snd i)))" ``` lp15@67998 ` 1092` ``` apply (rule Vitali_covering_theorem_balls [of S "{(x,r x t) |x t. x \ S \ 0 < t}" fst snd]) ``` lp15@67998 ` 1093` ``` apply auto ``` lp15@67998 ` 1094` ``` by (metis dist_eq_0_iff r0d) ``` lp15@67998 ` 1095` ``` let ?UB = "(\(x,s) \ C. ball x s)" ``` lp15@67998 ` 1096` ``` have eq: "f ` (S \ ?UB) = (\(x,s) \ C. f ` (S \ ball x s))" ``` lp15@67998 ` 1097` ``` by auto ``` lp15@67998 ` 1098` ``` have mle: "?\ (\(x,s) \ K. f ` (S \ ball x s)) \ (B + e) * (?\ S + d)" (is "?l \ ?r") ``` lp15@67998 ` 1099` ``` if "K \ C" and "finite K" for K ``` lp15@67998 ` 1100` ``` proof - ``` lp15@67998 ` 1101` ``` have gt0: "b > 0" if "(a, b) \ K" for a b ``` lp15@67998 ` 1102` ``` using Csub that \K \ C\ r0d by auto ``` lp15@67998 ` 1103` ``` have inj: "inj_on (\(x, y). ball x y) K" ``` lp15@67998 ` 1104` ``` by (force simp: inj_on_def ball_eq_ball_iff dest: gt0) ``` lp15@67998 ` 1105` ``` have disjnt: "disjoint ((\(x, y). ball x y) ` K)" ``` lp15@67998 ` 1106` ``` using pwC that ``` lp15@67998 ` 1107` ``` apply (clarsimp simp: pairwise_def case_prod_unfold ball_eq_ball_iff) ``` lp15@67998 ` 1108` ``` by (metis subsetD fst_conv snd_conv) ``` lp15@67998 ` 1109` ``` have "?l \ (\i\K. ?\ (case i of (x, s) \ f ` (S \ ball x s)))" ``` lp15@67998 ` 1110` ``` proof (rule measure_UNION_le [OF \finite K\], clarify) ``` lp15@67998 ` 1111` ``` fix x r ``` lp15@67998 ` 1112` ``` assume "(x,r) \ K" ``` lp15@67998 ` 1113` ``` then have "x \ S" ``` lp15@67998 ` 1114` ``` using Csub \K \ C\ by auto ``` lp15@67998 ` 1115` ``` show "f ` (S \ ball x r) \ sets lebesgue" ``` lp15@67998 ` 1116` ``` by (meson Int_lower1 S differentiable_on_subset f_diff fmeasurableD lmeasurable_ball order_refl sets.Int differentiable_image_in_sets_lebesgue) ``` lp15@67998 ` 1117` ``` qed ``` lp15@67998 ` 1118` ``` also have "\ \ (\(x,s) \ K. (B + e) * ?\ (ball x s))" ``` lp15@67998 ` 1119` ``` apply (rule sum_mono) ``` lp15@67998 ` 1120` ``` using Csub r \K \ C\ by auto ``` lp15@67998 ` 1121` ``` also have "\ = (B + e) * (\(x,s) \ K. ?\ (ball x s))" ``` lp15@67998 ` 1122` ``` by (simp add: prod.case_distrib sum_distrib_left) ``` lp15@67998 ` 1123` ``` also have "\ = (B + e) * sum ?\ ((\(x, y). ball x y) ` K)" ``` lp15@67998 ` 1124` ``` using \B \ 0\ \e > 0\ by (simp add: inj sum.reindex prod.case_distrib) ``` lp15@67998 ` 1125` ``` also have "\ = (B + e) * ?\ (\(x,s) \ K. ball x s)" ``` lp15@67998 ` 1126` ``` using \B \ 0\ \e > 0\ that ``` lp15@67998 ` 1127` ``` by (subst measure_Union') (auto simp: disjnt measure_Union') ``` lp15@67998 ` 1128` ``` also have "\ \ (B + e) * ?\ T" ``` lp15@67998 ` 1129` ``` using \B \ 0\ \e > 0\ that apply simp ``` lp15@67998 ` 1130` ``` apply (rule measure_mono_fmeasurable [OF _ _ \T \ lmeasurable\]) ``` lp15@67998 ` 1131` ``` using Csub rT by force+ ``` lp15@67998 ` 1132` ``` also have "\ \ (B + e) * (?\ S + d)" ``` lp15@67998 ` 1133` ``` using \B \ 0\ \e > 0\ Tless by simp ``` lp15@67998 ` 1134` ``` finally show ?thesis . ``` lp15@67998 ` 1135` ``` qed ``` lp15@67998 ` 1136` ``` have fSUB_mble: "(f ` (S \ ?UB)) \ lmeasurable" ``` lp15@67998 ` 1137` ``` unfolding eq using Csub r False \e > 0\ that ``` lp15@67998 ` 1138` ``` by (auto simp: intro!: fmeasurable_UN_bound [OF \countable C\ _ mle]) ``` lp15@67998 ` 1139` ``` have fSUB_meas: "?\ (f ` (S \ ?UB)) \ (B + e) * (?\ S + d)" (is "?MUB") ``` lp15@67998 ` 1140` ``` unfolding eq using Csub r False \e > 0\ that ``` lp15@67998 ` 1141` ``` by (auto simp: intro!: measure_UN_bound [OF \countable C\ _ mle]) ``` lp15@67998 ` 1142` ``` have neg: "negligible ((f ` (S \ ?UB) - f ` S) \ (f ` S - f ` (S \ ?UB)))" ``` lp15@67998 ` 1143` ``` proof (rule negligible_subset [OF negligible_differentiable_image_negligible [OF order_refl negC, where f=f]]) ``` lp15@67998 ` 1144` ``` show "f differentiable_on S - (\i\C. ball (fst i) (snd i))" ``` lp15@67998 ` 1145` ``` by (meson DiffE differentiable_on_subset subsetI f_diff) ``` lp15@67998 ` 1146` ``` qed force ``` lp15@67998 ` 1147` ``` show "f ` S \ lmeasurable" ``` lp15@67998 ` 1148` ``` by (rule lmeasurable_negligible_symdiff [OF fSUB_mble neg]) ``` lp15@67998 ` 1149` ``` show ?MD ``` lp15@67998 ` 1150` ``` using fSUB_meas measure_negligible_symdiff [OF fSUB_mble neg] by simp ``` lp15@67998 ` 1151` ``` qed ``` lp15@67998 ` 1152` ``` show "f ` S \ lmeasurable" ``` lp15@67998 ` 1153` ``` using eps_d [of 1] by simp ``` lp15@67998 ` 1154` ``` show ?ME ``` lp15@67998 ` 1155` ``` proof (rule field_le_epsilon) ``` lp15@67998 ` 1156` ``` fix \ :: real ``` lp15@67998 ` 1157` ``` assume "0 < \" ``` lp15@67998 ` 1158` ``` then show "?\ (f ` S) \ (B + e) * ?\ S + \" ``` lp15@67998 ` 1159` ``` using eps_d [of "\ / (B+e)"] \e > 0\ \B \ 0\ by (auto simp: divide_simps mult_ac) ``` lp15@67998 ` 1160` ``` qed ``` lp15@67998 ` 1161` ``` qed ``` lp15@67998 ` 1162` ``` show ?thesis ``` lp15@67998 ` 1163` ``` proof (cases "?\ S = 0") ``` lp15@67998 ` 1164` ``` case True ``` lp15@67998 ` 1165` ``` with eps have "?\ (f ` S) = 0" ``` lp15@67998 ` 1166` ``` by (metis mult_zero_right not_le zero_less_measure_iff) ``` lp15@67998 ` 1167` ``` then show ?thesis ``` lp15@67998 ` 1168` ``` using eps [of 1] by (simp add: True) ``` lp15@67998 ` 1169` ``` next ``` lp15@67998 ` 1170` ``` case False ``` lp15@67998 ` 1171` ``` have "?\ (f ` S) \ B * ?\ S" ``` lp15@67998 ` 1172` ``` proof (rule field_le_epsilon) ``` lp15@67998 ` 1173` ``` fix e :: real ``` lp15@67998 ` 1174` ``` assume "e > 0" ``` lp15@67998 ` 1175` ``` then show "?\ (f ` S) \ B * ?\ S + e" ``` lp15@67998 ` 1176` ``` using eps [of "e / ?\ S"] False by (auto simp: algebra_simps zero_less_measure_iff) ``` lp15@67998 ` 1177` ``` qed ``` lp15@67998 ` 1178` ``` with eps [of 1] show ?thesis by auto ``` lp15@67998 ` 1179` ``` qed ``` lp15@67998 ` 1180` ``` qed ``` lp15@67998 ` 1181` ``` then show "f ` S \ lmeasurable" ?M by blast+ ``` lp15@67998 ` 1182` ```qed ``` lp15@67998 ` 1183` lp15@67998 ` 1184` ```lemma ``` lp15@67998 ` 1185` ``` fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" ``` lp15@67998 ` 1186` ``` assumes S: "S \ lmeasurable" ``` lp15@67998 ` 1187` ``` and deriv: "\x. x \ S \ (f has_derivative f' x) (at x within S)" ``` lp15@67998 ` 1188` ``` and int: "(\x. \det (matrix (f' x))\) integrable_on S" ``` lp15@67998 ` 1189` ``` shows m_diff_image_weak: "f ` S \ lmeasurable \ measure lebesgue (f ` S) \ integral S (\x. \det (matrix (f' x))\)" ``` lp15@67998 ` 1190` ```proof - ``` lp15@67998 ` 1191` ``` let ?\ = "measure lebesgue" ``` lp15@67998 ` 1192` ``` have aint_S: "(\x. \det (matrix (f' x))\) absolutely_integrable_on S" ``` lp15@67998 ` 1193` ``` using int unfolding absolutely_integrable_on_def by auto ``` lp15@67998 ` 1194` ``` define m where "m \ integral S (\x. \det (matrix (f' x))\)" ``` lp15@67998 ` 1195` ``` have *: "f ` S \ lmeasurable" "?\ (f ` S) \ m + e * ?\ S" ``` lp15@67998 ` 1196` ``` if "e > 0" for e ``` lp15@67998 ` 1197` ``` proof - ``` lp15@67998 ` 1198` ``` define T where "T \ \n. {x \ S. n * e \ \det (matrix (f' x))\ \ ``` lp15@67998 ` 1199` ``` \det (matrix (f' x))\ < (Suc n) * e}" ``` lp15@67998 ` 1200` ``` have meas_t: "T n \ lmeasurable" for n ``` lp15@67998 ` 1201` ``` proof - ``` lp15@67998 ` 1202` ``` have *: "(\x. \det (matrix (f' x))\) \ borel_measurable (lebesgue_on S)" ``` lp15@67998 ` 1203` ``` using aint_S by (simp add: S borel_measurable_restrict_space_iff fmeasurableD set_integrable_def) ``` lp15@67998 ` 1204` ``` have [intro]: "x \ sets (lebesgue_on S) \ x \ sets lebesgue" for x ``` lp15@67998 ` 1205` ``` using S sets_restrict_space_subset by blast ``` lp15@67998 ` 1206` ``` have "{x \ S. real n * e \ \det (matrix (f' x))\} \ sets lebesgue" ``` lp15@67998 ` 1207` ``` using * by (auto simp: borel_measurable_iff_halfspace_ge space_restrict_space) ``` lp15@67998 ` 1208` ``` then have 1: "{x \ S. real n * e \ \det (matrix (f' x))\} \ lmeasurable" ``` lp15@67998 ` 1209` ``` using S by (simp add: fmeasurableI2) ``` lp15@67998 ` 1210` ``` have "{x \ S. \det (matrix (f' x))\ < (1 + real n) * e} \ sets lebesgue" ``` lp15@67998 ` 1211` ``` using * by (auto simp: borel_measurable_iff_halfspace_less space_restrict_space) ``` lp15@67998 ` 1212` ``` then have 2: "{x \ S. \det (matrix (f' x))\ < (1 + real n) * e} \ lmeasurable" ``` lp15@67998 ` 1213` ``` using S by (simp add: fmeasurableI2) ``` lp15@67998 ` 1214` ``` show ?thesis ``` lp15@67998 ` 1215` ``` using fmeasurable.Int [OF 1 2] by (simp add: T_def Int_def cong: conj_cong) ``` lp15@67998 ` 1216` ``` qed ``` lp15@67998 ` 1217` ``` have aint_T: "\k. (\x. \det (matrix (f' x))\) absolutely_integrable_on T k" ``` lp15@67998 ` 1218` ``` using set_integrable_subset [OF aint_S] meas_t T_def by blast ``` lp15@67998 ` 1219` ``` have Seq: "S = (\n. T n)" ``` lp15@67998 ` 1220` ``` apply (auto simp: T_def) ``` lp15@67998 ` 1221` ``` apply (rule_tac x="nat(floor(abs(det(matrix(f' x))) / e))" in exI) ``` lp15@67998 ` 1222` ``` using that apply auto ``` lp15@67998 ` 1223` ``` using of_int_floor_le pos_le_divide_eq apply blast ``` lp15@67998 ` 1224` ``` by (metis add.commute pos_divide_less_eq real_of_int_floor_add_one_gt) ``` lp15@67998 ` 1225` ``` have meas_ft: "f ` T n \ lmeasurable" for n ``` lp15@67998 ` 1226` ``` proof (rule measurable_bounded_differentiable_image) ``` lp15@67998 ` 1227` ``` show "T n \ lmeasurable" ``` lp15@67998 ` 1228` ``` by (simp add: meas_t) ``` lp15@67998 ` 1229` ``` next ``` lp15@67998 ` 1230` ``` fix x :: "(real,'n) vec" ``` lp15@67998 ` 1231` ``` assume "x \ T n" ``` lp15@67998 ` 1232` ``` show "(f has_derivative f' x) (at x within T n)" ``` lp15@67998 ` 1233` ``` by (metis (no_types, lifting) \x \ T n\ deriv has_derivative_within_subset mem_Collect_eq subsetI T_def) ``` lp15@67998 ` 1234` ``` show "\det (matrix (f' x))\ \ (Suc n) * e" ``` lp15@67998 ` 1235` ``` using \x \ T n\ T_def by auto ``` lp15@67998 ` 1236` ``` next ``` lp15@67998 ` 1237` ``` show "(\x. \det (matrix (f' x))\) integrable_on T n" ``` lp15@67998 ` 1238` ``` using aint_T absolutely_integrable_on_def by blast ``` lp15@67998 ` 1239` ``` qed ``` lp15@67998 ` 1240` ``` have disT: "disjoint (range T)" ``` lp15@67998 ` 1241` ``` unfolding disjoint_def ``` lp15@67998 ` 1242` ``` proof clarsimp ``` lp15@67998 ` 1243` ``` show "T m \ T n = {}" if "T m \ T n" for m n ``` lp15@67998 ` 1244` ``` using that ``` lp15@67998 ` 1245` ``` proof (induction m n rule: linorder_less_wlog) ``` lp15@67998 ` 1246` ``` case (less m n) ``` lp15@67998 ` 1247` ``` with \e > 0\ show ?case ``` lp15@67998 ` 1248` ``` unfolding T_def ``` lp15@67998 ` 1249` ``` proof (clarsimp simp add: Collect_conj_eq [symmetric]) ``` lp15@67998 ` 1250` ``` fix x ``` lp15@67998 ` 1251` ``` assume "e > 0" "m < n" "n * e \ \det (matrix (f' x))\" "\det (matrix (f' x))\ < (1 + real m) * e" ``` lp15@67998 ` 1252` ``` then have "n < 1 + real m" ``` lp15@67998 ` 1253` ``` by (metis (no_types, hide_lams) less_le_trans mult.commute not_le real_mult_le_cancel_iff2) ``` lp15@67998 ` 1254` ``` then show "False" ``` lp15@67998 ` 1255` ``` using less.hyps by linarith ``` lp15@67998 ` 1256` ``` qed ``` lp15@67998 ` 1257` ``` qed auto ``` lp15@67998 ` 1258` ``` qed ``` lp15@67998 ` 1259` ``` have injT: "inj_on T ({n. T n \ {}})" ``` lp15@67998 ` 1260` ``` unfolding inj_on_def ``` lp15@67998 ` 1261` ``` proof clarsimp ``` lp15@67998 ` 1262` ``` show "m = n" if "T m = T n" "T n \ {}" for m n ``` lp15@67998 ` 1263` ``` using that ``` lp15@67998 ` 1264` ``` proof (induction m n rule: linorder_less_wlog) ``` lp15@67998 ` 1265` ``` case (less m n) ``` lp15@67998 ` 1266` ``` have False if "T n \ T m" "x \ T n" for x ``` lp15@67998 ` 1267` ``` using \e > 0\ \m < n\ that ``` lp15@67998 ` 1268` ``` apply (auto simp: T_def mult.commute intro: less_le_trans dest!: subsetD) ``` lp15@67998 ` 1269` ``` by (metis add.commute less_le_trans nat_less_real_le not_le real_mult_le_cancel_iff2) ``` lp15@67998 ` 1270` ``` then show ?case ``` lp15@67998 ` 1271` ``` using less.prems by blast ``` lp15@67998 ` 1272` ``` qed auto ``` lp15@67998 ` 1273` ``` qed ``` lp15@67998 ` 1274` ``` have sum_eq_Tim: "(\k\n. f (T k)) = sum f (T ` {..n})" if "f {} = 0" for f :: "_ \ real" and n ``` lp15@67998 ` 1275` ``` proof (subst sum.reindex_nontrivial) ``` lp15@67998 ` 1276` ``` fix i j assume "i \ {..n}" "j \ {..n}" "i \ j" "T i = T j" ``` lp15@67998 ` 1277` ``` with that injT [unfolded inj_on_def] show "f (T i) = 0" ``` lp15@67998 ` 1278` ``` by simp metis ``` lp15@67998 ` 1279` ``` qed (use atMost_atLeast0 in auto) ``` lp15@67998 ` 1280` ``` let ?B = "m + e * ?\ S" ``` lp15@67998 ` 1281` ``` have "(\k\n. ?\ (f ` T k)) \ ?B" for n ``` lp15@67998 ` 1282` ``` proof - ``` lp15@67998 ` 1283` ``` have "(\k\n. ?\ (f ` T k)) \ (\k\n. ((k+1) * e) * ?\(T k))" ``` lp15@67998 ` 1284` ``` proof (rule sum_mono [OF measure_bounded_differentiable_image]) ``` lp15@67998 ` 1285` ``` show "(f has_derivative f' x) (at x within T k)" if "x \ T k" for k x ``` lp15@67998 ` 1286` ``` using that unfolding T_def by (blast intro: deriv has_derivative_within_subset) ``` lp15@67998 ` 1287` ``` show "(\x. \det (matrix (f' x))\) integrable_on T k" for k ``` lp15@67998 ` 1288` ``` using absolutely_integrable_on_def aint_T by blast ``` lp15@67998 ` 1289` ``` show "\det (matrix (f' x))\ \ real (k + 1) * e" if "x \ T k" for k x ``` lp15@67998 ` 1290` ``` using T_def that by auto ``` lp15@67998 ` 1291` ``` qed (use meas_t in auto) ``` lp15@67998 ` 1292` ``` also have "\ \ (\k\n. (k * e) * ?\(T k)) + (\k\n. e * ?\(T k))" ``` lp15@67998 ` 1293` ``` by (simp add: algebra_simps sum.distrib) ``` lp15@67998 ` 1294` ``` also have "\ \ ?B" ``` lp15@67998 ` 1295` ``` proof (rule add_mono) ``` lp15@67998 ` 1296` ``` have "(\k\n. real k * e * ?\ (T k)) = (\k\n. integral (T k) (\x. k * e))" ``` lp15@67998 ` 1297` ``` by (simp add: lmeasure_integral [OF meas_t] ``` lp15@67998 ` 1298` ``` integral_mult_right [symmetric] integral_mult_left [symmetric] ``` lp15@67998 ` 1299` ``` del: integral_mult_right integral_mult_left) ``` lp15@67998 ` 1300` ``` also have "\ \ (\k\n. integral (T k) (\x. (abs (det (matrix (f' x))))))" ``` lp15@67998 ` 1301` ``` proof (rule sum_mono) ``` lp15@67998 ` 1302` ``` fix k ``` lp15@67998 ` 1303` ``` assume "k \ {..n}" ``` lp15@67998 ` 1304` ``` show "integral (T k) (\x. k * e) \ integral (T k) (\x. \det (matrix (f' x))\)" ``` lp15@67998 ` 1305` ``` proof (rule integral_le [OF integrable_on_const [OF meas_t]]) ``` lp15@67998 ` 1306` ``` show "(\x. \det (matrix (f' x))\) integrable_on T k" ``` lp15@67998 ` 1307` ``` using absolutely_integrable_on_def aint_T by blast ``` lp15@67998 ` 1308` ``` next ``` lp15@67998 ` 1309` ``` fix x assume "x \ T k" ``` lp15@67998 ` 1310` ``` show "k * e \ \det (matrix (f' x))\" ``` lp15@67998 ` 1311` ``` using \x \ T k\ T_def by blast ``` lp15@67998 ` 1312` ``` qed ``` lp15@67998 ` 1313` ``` qed ``` lp15@67998 ` 1314` ``` also have "\ = sum (\T. integral T (\x. \det (matrix (f' x))\)) (T ` {..n})" ``` lp15@67998 ` 1315` ``` by (auto intro: sum_eq_Tim) ``` lp15@67998 ` 1316` ``` also have "\ = integral (\k\n. T k) (\x. \det (matrix (f' x))\)" ``` lp15@67998 ` 1317` ``` proof (rule integral_unique [OF has_integral_Union, symmetric]) ``` lp15@67998 ` 1318` ``` fix S assume "S \ T ` {..n}" ``` lp15@67998 ` 1319` ``` then show "((\x. \det (matrix (f' x))\) has_integral integral S (\x. \det (matrix (f' x))\)) S" ``` lp15@67998 ` 1320` ``` using absolutely_integrable_on_def aint_T by blast ``` lp15@67998 ` 1321` ``` next ``` lp15@67998 ` 1322` ``` show "pairwise (\S S'. negligible (S \ S')) (T ` {..n})" ``` lp15@67998 ` 1323` ``` using disT unfolding disjnt_iff by (auto simp: pairwise_def intro!: empty_imp_negligible) ``` lp15@67998 ` 1324` ``` qed auto ``` lp15@67998 ` 1325` ``` also have "\ \ m" ``` lp15@67998 ` 1326` ``` unfolding m_def ``` lp15@67998 ` 1327` ``` proof (rule integral_subset_le) ``` lp15@67998 ` 1328` ``` have "(\x. \det (matrix (f' x))\) absolutely_integrable_on (\k\n. T k)" ``` lp15@67998 ` 1329` ``` apply (rule set_integrable_subset [OF aint_S]) ``` lp15@67998 ` 1330` ``` apply (intro measurable meas_t fmeasurableD) ``` lp15@67998 ` 1331` ``` apply (force simp: Seq) ``` lp15@67998 ` 1332` ``` done ``` lp15@67998 ` 1333` ``` then show "(\x. \det (matrix (f' x))\) integrable_on (\k\n. T k)" ``` lp15@67998 ` 1334` ``` using absolutely_integrable_on_def by blast ``` lp15@67998 ` 1335` ``` qed (use Seq int in auto) ``` lp15@67998 ` 1336` ``` finally show "(\k\n. real k * e * ?\ (T k)) \ m" . ``` lp15@67998 ` 1337` ``` next ``` lp15@67998 ` 1338` ``` have "(\k\n. ?\ (T k)) = sum ?\ (T ` {..n})" ``` lp15@67998 ` 1339` ``` by (auto intro: sum_eq_Tim) ``` lp15@67998 ` 1340` ``` also have "\ = ?\ (\k\n. T k)" ``` lp15@67998 ` 1341` ``` using S disT by (auto simp: pairwise_def meas_t intro: measure_Union' [symmetric]) ``` lp15@67998 ` 1342` ``` also have "\ \ ?\ S" ``` lp15@67998 ` 1343` ``` using S by (auto simp: Seq intro: meas_t fmeasurableD measure_mono_fmeasurable) ``` lp15@67998 ` 1344` ``` finally have "(\k\n. ?\ (T k)) \ ?\ S" . ``` lp15@67998 ` 1345` ``` then show "(\k\n. e * ?\ (T k)) \ e * ?\ S" ``` lp15@67998 ` 1346` ``` by (metis less_eq_real_def ordered_comm_semiring_class.comm_mult_left_mono sum_distrib_left that) ``` lp15@67998 ` 1347` ``` qed ``` lp15@67998 ` 1348` ``` finally show "(\k\n. ?\ (f ` T k)) \ ?B" . ``` lp15@67998 ` 1349` ``` qed ``` lp15@67998 ` 1350` ``` moreover have "measure lebesgue (\k\n. f ` T k) \ (\k\n. ?\ (f ` T k))" for n ``` lp15@67998 ` 1351` ``` by (simp add: fmeasurableD meas_ft measure_UNION_le) ``` lp15@67998 ` 1352` ``` ultimately have B_ge_m: "?\ (\k\n. (f ` T k)) \ ?B" for n ``` lp15@67998 ` 1353` ``` by (meson order_trans) ``` lp15@67998 ` 1354` ``` have "(\n. f ` T n) \ lmeasurable" ``` lp15@67998 ` 1355` ``` by (rule fmeasurable_countable_Union [OF meas_ft B_ge_m]) ``` lp15@67998 ` 1356` ``` moreover have "?\ (\n. f ` T n) \ m + e * ?\ S" ``` lp15@67998 ` 1357` ``` by (rule measure_countable_Union_le [OF meas_ft B_ge_m]) ``` lp15@67998 ` 1358` ``` ultimately show "f ` S \ lmeasurable" "?\ (f ` S) \ m + e * ?\ S" ``` lp15@67998 ` 1359` ``` by (auto simp: Seq image_Union) ``` lp15@67998 ` 1360` ``` qed ``` lp15@67998 ` 1361` ``` show ?thesis ``` lp15@67998 ` 1362` ``` proof ``` lp15@67998 ` 1363` ``` show "f ` S \ lmeasurable" ``` lp15@67998 ` 1364` ``` using * linordered_field_no_ub by blast ``` lp15@67998 ` 1365` ``` let ?x = "m - ?\ (f ` S)" ``` lp15@67998 ` 1366` ``` have False if "?\ (f ` S) > integral S (\x. \det (matrix (f' x))\)" ``` lp15@67998 ` 1367` ``` proof - ``` lp15@67998 ` 1368` ``` have ml: "m < ?\ (f ` S)" ``` lp15@67998 ` 1369` ``` using m_def that by blast ``` lp15@67998 ` 1370` ``` then have "?\ S \ 0" ``` lp15@67998 ` 1371` ``` using "*"(2) bgauge_existence_lemma by fastforce ``` lp15@67998 ` 1372` ``` with ml have 0: "0 < - (m - ?\ (f ` S))/2 / ?\ S" ``` lp15@67998 ` 1373` ``` using that zero_less_measure_iff by force ``` lp15@67998 ` 1374` ``` then show ?thesis ``` lp15@67998 ` 1375` ``` using * [OF 0] that by (auto simp: divide_simps m_def split: if_split_asm) ``` lp15@67998 ` 1376` ``` qed ``` lp15@67998 ` 1377` ``` then show "?\ (f ` S) \ integral S (\x. \det (matrix (f' x))\)" ``` lp15@67998 ` 1378` ``` by fastforce ``` lp15@67998 ` 1379` ``` qed ``` lp15@67998 ` 1380` ```qed ``` lp15@67998 ` 1381` lp15@67998 ` 1382` lp15@67998 ` 1383` ```theorem ``` lp15@67998 ` 1384` ``` fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" ``` lp15@67998 ` 1385` ``` assumes S: "S \ sets lebesgue" ``` lp15@67998 ` 1386` ``` and deriv: "\x. x \ S \ (f has_derivative f' x) (at x within S)" ``` lp15@67998 ` 1387` ``` and int: "(\x. \det (matrix (f' x))\) integrable_on S" ``` lp15@67998 ` 1388` ``` shows measurable_differentiable_image: "f ` S \ lmeasurable" ``` lp15@67998 ` 1389` ``` and measure_differentiable_image: ``` lp15@67998 ` 1390` ``` "measure lebesgue (f ` S) \ integral S (\x. \det (matrix (f' x))\)" (is "?M") ``` lp15@67998 ` 1391` ```proof - ``` lp15@67998 ` 1392` ``` let ?I = "\n::nat. cbox (vec (-n)) (vec n) \ S" ``` lp15@67998 ` 1393` ``` let ?\ = "measure lebesgue" ``` lp15@67998 ` 1394` ``` have "x \ cbox (vec (- real (nat \norm x\))) (vec (real (nat \norm x\)))" for x :: "real^'n::_" ``` lp15@67998 ` 1395` ``` apply (auto simp: mem_box_cart) ``` lp15@67998 ` 1396` ``` apply (metis abs_le_iff component_le_norm_cart minus_le_iff of_nat_ceiling order.trans) ``` lp15@67998 ` 1397` ``` by (meson abs_le_D1 norm_bound_component_le_cart real_nat_ceiling_ge) ``` lp15@67998 ` 1398` ``` then have Seq: "S = (\n. ?I n)" ``` lp15@67998 ` 1399` ``` by auto ``` lp15@67998 ` 1400` ``` have fIn: "f ` ?I n \ lmeasurable" ``` lp15@67998 ` 1401` ``` and mfIn: "?\ (f ` ?I n) \ integral S (\x. \det (matrix (f' x))\)" (is ?MN) for n ``` lp15@67998 ` 1402` ``` proof - ``` lp15@67998 ` 1403` ``` have In: "?I n \ lmeasurable" ``` lp15@67998 ` 1404` ``` by (simp add: S bounded_Int bounded_set_imp_lmeasurable sets.Int) ``` lp15@67998 ` 1405` ``` moreover have "\x. x \ ?I n \ (f has_derivative f' x) (at x within ?I n)" ``` lp15@67998 ` 1406` ``` by (meson Int_iff deriv has_derivative_within_subset subsetI) ``` lp15@67998 ` 1407` ``` moreover have int_In: "(\x. \det (matrix (f' x))\) integrable_on ?I n" ``` lp15@67998 ` 1408` ``` proof - ``` lp15@67998 ` 1409` ``` have "(\x. \det (matrix (f' x))\) absolutely_integrable_on S" ``` lp15@67998 ` 1410` ``` using int absolutely_integrable_integrable_bound by force ``` lp15@67998 ` 1411` ``` then have "(\x. \det (matrix (f' x))\) absolutely_integrable_on ?I n" ``` lp15@67998 ` 1412` ``` by (metis (no_types) Int_lower1 In fmeasurableD inf_commute set_integrable_subset) ``` lp15@67998 ` 1413` ``` then show ?thesis ``` lp15@67998 ` 1414` ``` using absolutely_integrable_on_def by blast ``` lp15@67998 ` 1415` ``` qed ``` lp15@67998 ` 1416` ``` ultimately have "f ` ?I n \ lmeasurable" "?\ (f ` ?I n) \ integral (?I n) (\x. \det (matrix (f' x))\)" ``` lp15@67998 ` 1417` ``` using m_diff_image_weak by metis+ ``` lp15@67998 ` 1418` ``` moreover have "integral (?I n) (\x. \det (matrix (f' x))\) \ integral S (\x. \det (matrix (f' x))\)" ``` lp15@67998 ` 1419` ``` by (simp add: int_In int integral_subset_le) ``` lp15@67998 ` 1420` ``` ultimately show "f ` ?I n \ lmeasurable" ?MN ``` lp15@67998 ` 1421` ``` by auto ``` lp15@67998 ` 1422` ``` qed ``` lp15@67998 ` 1423` ``` have "?I k \ ?I n" if "k \ n" for k n ``` lp15@67998 ` 1424` ``` by (rule Int_mono) (use that in \auto simp: subset_interval_imp_cart\) ``` lp15@67998 ` 1425` ``` then have "(\k\n. f ` ?I k) = f ` ?I n" for n ``` lp15@67998 ` 1426` ``` by (fastforce simp add:) ``` lp15@67998 ` 1427` ``` with mfIn have "?\ (\k\n. f ` ?I k) \ integral S (\x. \det (matrix (f' x))\)" for n ``` lp15@67998 ` 1428` ``` by simp ``` lp15@67998 ` 1429` ``` then have "(\n. f ` ?I n) \ lmeasurable" "?\ (\n. f ` ?I n) \ integral S (\x. \det (matrix (f' x))\)" ``` lp15@67998 ` 1430` ``` by (rule fmeasurable_countable_Union [OF fIn] measure_countable_Union_le [OF fIn])+ ``` lp15@67998 ` 1431` ``` then show "f ` S \ lmeasurable" ?M ``` lp15@67998 ` 1432` ``` by (metis Seq image_UN)+ ``` lp15@67998 ` 1433` ```qed ``` lp15@67998 ` 1434` lp15@67998 ` 1435` lp15@67998 ` 1436` ```lemma borel_measurable_simple_function_limit_increasing: ``` lp15@67998 ` 1437` ``` fixes f :: "'a::euclidean_space \ real" ``` lp15@67998 ` 1438` ``` shows "(f \ borel_measurable lebesgue \ (\x. 0 \ f x)) \ ``` lp15@67998 ` 1439` ``` (\g. (\n x. 0 \ g n x \ g n x \ f x) \ (\n x. g n x \ (g(Suc n) x)) \ ``` lp15@67998 ` 1440` ``` (\n. g n \ borel_measurable lebesgue) \ (\n. finite(range (g n))) \ ``` lp15@67998 ` 1441` ``` (\x. (\n. g n x) \ f x))" ``` lp15@67998 ` 1442` ``` (is "?lhs = ?rhs") ``` lp15@67998 ` 1443` ```proof ``` lp15@67998 ` 1444` ``` assume f: ?lhs ``` lp15@67998 ` 1445` ``` have leb_f: "{x. a \ f x \ f x < b} \ sets lebesgue" for a b ``` lp15@67998 ` 1446` ``` proof - ``` lp15@67998 ` 1447` ``` have "{x. a \ f x \ f x < b} = {x. f x < b} - {x. f x < a}" ``` lp15@67998 ` 1448` ``` by auto ``` lp15@67998 ` 1449` ``` also have "\ \ sets lebesgue" ``` lp15@67998 ` 1450` ``` using borel_measurable_vimage_halfspace_component_lt [of f UNIV] f by auto ``` lp15@67998 ` 1451` ``` finally show ?thesis . ``` lp15@67998 ` 1452` ``` qed ``` lp15@67998 ` 1453` ``` have "g n x \ f x" ``` lp15@67998 ` 1454` ``` if inc_g: "\n x. 0 \ g n x \ g n x \ g (Suc n) x" ``` lp15@67998 ` 1455` ``` and meas_g: "\n. g n \ borel_measurable lebesgue" ``` lp15@67998 ` 1456` ``` and fin: "\n. finite(range (g n))" and lim: "\x. (\n. g n x) \ f x" for g n x ``` lp15@67998 ` 1457` ``` proof - ``` lp15@67998 ` 1458` ``` have "\r>0. \N. \n\N. dist (g n x) (f x) \ r" if "g n x > f x" ``` lp15@67998 ` 1459` ``` proof - ``` lp15@67998 ` 1460` ``` have g: "g n x \ g (N + n) x" for N ``` lp15@67998 ` 1461` ``` by (rule transitive_stepwise_le) (use inc_g in auto) ``` lp15@67998 ` 1462` ``` have "\na\N. g n x - f x \ dist (g na x) (f x)" for N ``` lp15@67998 ` 1463` ``` apply (rule_tac x="N+n" in exI) ``` lp15@67998 ` 1464` ``` using g [of N] by (auto simp: dist_norm) ``` lp15@67998 ` 1465` ``` with that show ?thesis ``` lp15@67998 ` 1466` ``` using diff_gt_0_iff_gt by blast ``` lp15@67998 ` 1467` ``` qed ``` lp15@67998 ` 1468` ``` with lim show ?thesis ``` lp15@67998 ` 1469` ``` apply (auto simp: lim_sequentially) ``` lp15@67998 ` 1470` ``` by (meson less_le_not_le not_le_imp_less) ``` lp15@67998 ` 1471` ``` qed ``` lp15@67998 ` 1472` ``` moreover ``` lp15@67998 ` 1473` ``` let ?\ = "\n k. indicator {y. k/2^n \ f y \ f y < (k+1)/2^n}" ``` lp15@67998 ` 1474` ``` let ?g = "\n x. (\k::real | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * ?\ n k x)" ``` lp15@67998 ` 1475` ``` have "\g. (\n x. 0 \ g n x \ g n x \ (g(Suc n) x)) \ ``` lp15@67998 ` 1476` ``` (\n. g n \ borel_measurable lebesgue) \ (\n. finite(range (g n))) \(\x. (\n. g n x) \ f x)" ``` lp15@67998 ` 1477` ``` proof (intro exI allI conjI) ``` lp15@67998 ` 1478` ``` show "0 \ ?g n x" for n x ``` lp15@67998 ` 1479` ``` proof (clarify intro!: ordered_comm_monoid_add_class.sum_nonneg) ``` lp15@67998 ` 1480` ``` fix k::real ``` lp15@67998 ` 1481` ``` assume "k \ \" and k: "\k\ \ 2 ^ (2*n)" ``` lp15@67998 ` 1482` ``` show "0 \ k/2^n * ?\ n k x" ``` lp15@67998 ` 1483` ``` using f \k \ \\ apply (auto simp: indicator_def divide_simps Ints_def) ``` lp15@67998 ` 1484` ``` apply (drule spec [where x=x]) ``` lp15@67998 ` 1485` ``` using zero_le_power [of "2::real" n] mult_nonneg_nonneg [of "f x" "2^n"] ``` lp15@67998 ` 1486` ``` by linarith ``` lp15@67998 ` 1487` ``` qed ``` lp15@67998 ` 1488` ``` show "?g n x \ ?g (Suc n) x" for n x ``` lp15@67998 ` 1489` ``` proof - ``` lp15@67998 ` 1490` ``` have "?g n x = ``` lp15@67998 ` 1491` ``` (\k | k \ \ \ \k\ \ 2 ^ (2*n). ``` lp15@67998 ` 1492` ``` k/2^n * (indicator {y. k/2^n \ f y \ f y < (k+1/2)/2^n} x + ``` lp15@67998 ` 1493` ``` indicator {y. (k+1/2)/2^n \ f y \ f y < (k+1)/2^n} x))" ``` lp15@67998 ` 1494` ``` by (rule sum.cong [OF refl]) (simp add: indicator_def divide_simps) ``` lp15@67998 ` 1495` ``` also have "\ = (\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * indicator {y. k/2^n \ f y \ f y < (k+1/2)/2^n} x) + ``` lp15@67998 ` 1496` ``` (\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * indicator {y. (k+1/2)/2^n \ f y \ f y < (k+1)/2^n} x)" ``` lp15@67998 ` 1497` ``` by (simp add: comm_monoid_add_class.sum.distrib algebra_simps) ``` lp15@67998 ` 1498` ``` also have "\ = (\k | k \ \ \ \k\ \ 2 ^ (2*n). (2 * k)/2 ^ Suc n * indicator {y. (2 * k)/2 ^ Suc n \ f y \ f y < (2 * k+1)/2 ^ Suc n} x) + ``` lp15@67998 ` 1499` ``` (\k | k \ \ \ \k\ \ 2 ^ (2*n). (2 * k)/2 ^ Suc n * indicator {y. (2 * k+1)/2 ^ Suc n \ f y \ f y < ((2 * k+1) + 1)/2 ^ Suc n} x)" ``` lp15@67998 ` 1500` ``` by (force simp: field_simps indicator_def intro: sum.cong) ``` lp15@67998 ` 1501` ``` also have "\ \ (\k | k \ \ \ \k\ \ 2 ^ (2 * Suc n). k/2 ^ Suc n * (indicator {y. k/2 ^ Suc n \ f y \ f y < (k+1)/2 ^ Suc n} x))" ``` lp15@67998 ` 1502` ``` (is "?a + _ \ ?b") ``` lp15@67998 ` 1503` ``` proof - ``` lp15@67998 ` 1504` ``` have *: "\sum f I \ sum h I; a + sum h I \ b\ \ a + sum f I \ b" for I a b f and h :: "real\real" ``` lp15@67998 ` 1505` ``` by linarith ``` lp15@67998 ` 1506` ``` let ?h = "\k. (2*k+1)/2 ^ Suc n * ``` lp15@67998 ` 1507` ``` (indicator {y. (2 * k+1)/2 ^ Suc n \ f y \ f y < ((2*k+1) + 1)/2 ^ Suc n} x)" ``` lp15@67998 ` 1508` ``` show ?thesis ``` lp15@67998 ` 1509` ``` proof (rule *) ``` lp15@67998 ` 1510` ``` show "(\k | k \ \ \ \k\ \ 2 ^ (2*n). ``` lp15@67998 ` 1511` ``` 2 * k/2 ^ Suc n * indicator {y. (2 * k+1)/2 ^ Suc n \ f y \ f y < (2 * k+1 + 1)/2 ^ Suc n} x) ``` lp15@67998 ` 1512` ``` \ sum ?h {k \ \. \k\ \ 2 ^ (2*n)}" ``` lp15@67998 ` 1513` ``` by (rule sum_mono) (simp add: indicator_def divide_simps) ``` lp15@67998 ` 1514` ``` next ``` lp15@67998 ` 1515` ``` have \: "?a = (\k \ ( *)2 ` {k \ \. \k\ \ 2 ^ (2*n)}. ``` lp15@67998 ` 1516` ``` k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \ f y \ f y < (k+1)/2 ^ Suc n} x)" ``` lp15@67998 ` 1517` ``` by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex) ``` lp15@67998 ` 1518` ``` have \: "sum ?h {k \ \. \k\ \ 2 ^ (2*n)} ``` lp15@67998 ` 1519` ``` = (\k \ (\x. 2*x + 1) ` {k \ \. \k\ \ 2 ^ (2*n)}. ``` lp15@67998 ` 1520` ``` k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \ f y \ f y < (k+1)/2 ^ Suc n} x)" ``` lp15@67998 ` 1521` ``` by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex) ``` lp15@67998 ` 1522` ``` have 0: "( *) 2 ` {k \ \. P k} \ (\x. 2 * x + 1) ` {k \ \. P k} = {}" for P :: "real \ bool" ``` lp15@67998 ` 1523` ``` proof - ``` lp15@67998 ` 1524` ``` have "2 * i \ 2 * j + 1" for i j :: int by arith ``` lp15@67998 ` 1525` ``` thus ?thesis ``` lp15@67998 ` 1526` ``` unfolding Ints_def by auto (use of_int_eq_iff in fastforce) ``` lp15@67998 ` 1527` ``` qed ``` lp15@67998 ` 1528` ``` have "?a + sum ?h {k \ \. \k\ \ 2 ^ (2*n)} ``` lp15@67998 ` 1529` ``` = (\k \ ( *)2 ` {k \ \. \k\ \ 2 ^ (2*n)} \ (\x. 2*x + 1) ` {k \ \. \k\ \ 2 ^ (2*n)}. ``` lp15@67998 ` 1530` ``` k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \ f y \ f y < (k+1)/2 ^ Suc n} x)" ``` lp15@67998 ` 1531` ``` unfolding \ \ ``` lp15@67998 ` 1532` ``` using finite_abs_int_segment [of "2 ^ (2*n)"] ``` lp15@67998 ` 1533` ``` by (subst sum_Un) (auto simp: 0) ``` lp15@67998 ` 1534` ``` also have "\ \ ?b" ``` lp15@67998 ` 1535` ``` proof (rule sum_mono2) ``` lp15@67998 ` 1536` ``` show "finite {k::real. k \ \ \ \k\ \ 2 ^ (2 * Suc n)}" ``` lp15@67998 ` 1537` ``` by (rule finite_abs_int_segment) ``` lp15@67998 ` 1538` ``` show "( *) 2 ` {k::real. k \ \ \ \k\ \ 2^(2*n)} \ (\x. 2*x + 1) ` {k \ \. \k\ \ 2^(2*n)} \ {k \ \. \k\ \ 2 ^ (2 * Suc n)}" ``` lp15@67998 ` 1539` ``` apply auto ``` lp15@67998 ` 1540` ``` using one_le_power [of "2::real" "2*n"] by linarith ``` lp15@67998 ` 1541` ``` have *: "\x \ (S \ T) - U; \x. x \ S \ x \ U; \x. x \ T \ x \ U\ \ P x" for S T U P ``` lp15@67998 ` 1542` ``` by blast ``` lp15@67998 ` 1543` ``` have "0 \ b" if "b \ \" "f x * (2 * 2^n) < b + 1" for b ``` lp15@67998 ` 1544` ``` proof - ``` lp15@67998 ` 1545` ``` have "0 \ f x * (2 * 2^n)" ``` lp15@67998 ` 1546` ``` by (simp add: f) ``` lp15@67998 ` 1547` ``` also have "\ < b+1" ``` lp15@67998 ` 1548` ``` by (simp add: that) ``` lp15@67998 ` 1549` ``` finally show "0 \ b" ``` lp15@67998 ` 1550` ``` using \b \ \\ by (auto simp: elim!: Ints_cases) ``` lp15@67998 ` 1551` ``` qed ``` lp15@67998 ` 1552` ``` then show "0 \ b/2 ^ Suc n * indicator {y. b/2 ^ Suc n \ f y \ f y < (b + 1)/2 ^ Suc n} x" ``` lp15@67998 ` 1553` ``` if "b \ {k \ \. \k\ \ 2 ^ (2 * Suc n)} - ``` lp15@67998 ` 1554` ``` (( *) 2 ` {k \ \. \k\ \ 2 ^ (2*n)} \ (\x. 2*x + 1) ` {k \ \. \k\ \ 2 ^ (2*n)})" for b ``` lp15@67998 ` 1555` ``` using that by (simp add: indicator_def divide_simps) ``` lp15@67998 ` 1556` ``` qed ``` lp15@67998 ` 1557` ``` finally show "?a + sum ?h {k \ \. \k\ \ 2 ^ (2*n)} \ ?b" . ``` lp15@67998 ` 1558` ``` qed ``` lp15@67998 ` 1559` ``` qed ``` lp15@67998 ` 1560` ``` finally show ?thesis . ``` lp15@67998 ` 1561` ``` qed ``` lp15@67998 ` 1562` ``` show "?g n \ borel_measurable lebesgue" for n ``` lp15@67998 ` 1563` ``` apply (intro borel_measurable_indicator borel_measurable_times borel_measurable_sum) ``` lp15@67998 ` 1564` ``` using leb_f sets_restrict_UNIV by auto ``` lp15@67998 ` 1565` ``` show "finite (range (?g n))" for n ``` lp15@67998 ` 1566` ``` proof - ``` lp15@67998 ` 1567` ``` have "(\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * ?\ n k x) ``` lp15@67998 ` 1568` ``` \ (\k. k/2^n) ` {k \ \. \k\ \ 2 ^ (2*n)}" for x ``` lp15@67998 ` 1569` ``` proof (cases "\k. k \ \ \ \k\ \ 2 ^ (2*n) \ k/2^n \ f x \ f x < (k+1)/2^n") ``` lp15@67998 ` 1570` ``` case True ``` lp15@67998 ` 1571` ``` then show ?thesis ``` lp15@67998 ` 1572` ``` by (blast intro: indicator_sum_eq) ``` lp15@67998 ` 1573` ``` next ``` lp15@67998 ` 1574` ``` case False ``` lp15@67998 ` 1575` ``` then have "(\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * ?\ n k x) = 0" ``` lp15@67998 ` 1576` ``` by auto ``` lp15@67998 ` 1577` ``` then show ?thesis by force ``` lp15@67998 ` 1578` ``` qed ``` lp15@67998 ` 1579` ``` then have "range (?g n) \ ((\k. (k/2^n)) ` {k. k \ \ \ \k\ \ 2 ^ (2*n)})" ``` lp15@67998 ` 1580` ``` by auto ``` lp15@67998 ` 1581` ``` moreover have "finite ((\k::real. (k/2^n)) ` {k \ \. \k\ \ 2 ^ (2*n)})" ``` lp15@67998 ` 1582` ``` by (intro finite_imageI finite_abs_int_segment) ``` lp15@67998 ` 1583` ``` ultimately show ?thesis ``` lp15@67998 ` 1584` ``` by (rule finite_subset) ``` lp15@67998 ` 1585` ``` qed ``` lp15@67998 ` 1586` ``` show "(\n. ?g n x) \ f x" for x ``` lp15@67998 ` 1587` ``` proof (clarsimp simp add: lim_sequentially) ``` lp15@67998 ` 1588` ``` fix e::real ``` lp15@67998 ` 1589` ``` assume "e > 0" ``` lp15@67998 ` 1590` ``` obtain N1 where N1: "2 ^ N1 > abs(f x)" ``` lp15@67998 ` 1591` ``` using real_arch_pow by fastforce ``` lp15@67998 ` 1592` ``` obtain N2 where N2: "(1/2) ^ N2 < e" ``` lp15@67998 ` 1593` ``` using real_arch_pow_inv \e > 0\ by fastforce ``` lp15@67998 ` 1594` ``` have "dist (\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * ?\ n k x) (f x) < e" if "N1 + N2 \ n" for n ``` lp15@67998 ` 1595` ``` proof - ``` lp15@67998 ` 1596` ``` let ?m = "real_of_int \2^n * f x\" ``` lp15@67998 ` 1597` ``` have "\?m\ \ 2^n * 2^N1" ``` lp15@67998 ` 1598` ``` using N1 apply (simp add: f) ``` lp15@67998 ` 1599` ``` by (meson floor_mono le_floor_iff less_le_not_le mult_le_cancel_left_pos zero_less_numeral zero_less_power) ``` lp15@67998 ` 1600` ``` also have "\ \ 2 ^ (2*n)" ``` lp15@67998 ` 1601` ``` by (metis that add_leD1 add_le_cancel_left mult.commute mult_2_right one_less_numeral_iff ``` lp15@67998 ` 1602` ``` power_add power_increasing_iff semiring_norm(76)) ``` lp15@67998 ` 1603` ``` finally have m_le: "\?m\ \ 2 ^ (2*n)" . ``` lp15@67998 ` 1604` ``` have "?m/2^n \ f x" "f x < (?m + 1)/2^n" ``` lp15@67998 ` 1605` ``` by (auto simp: mult.commute pos_divide_le_eq mult_imp_less_div_pos) ``` lp15@67998 ` 1606` ``` then have eq: "dist (\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * ?\ n k x) (f x) ``` lp15@67998 ` 1607` ``` = dist (?m/2^n) (f x)" ``` lp15@67998 ` 1608` ``` by (subst indicator_sum_eq [of ?m]) (auto simp: m_le) ``` lp15@67998 ` 1609` ``` have "\2^n\ * \?m/2^n - f x\ = \2^n * (?m/2^n - f x)\" ``` lp15@67998 ` 1610` ``` by (simp add: abs_mult) ``` lp15@67998 ` 1611` ``` also have "\ < 2 ^ N2 * e" ``` lp15@67998 ` 1612` ``` using N2 by (simp add: divide_simps mult.commute) linarith ``` lp15@67998 ` 1613` ``` also have "\ \ \2^n\ * e" ``` lp15@67998 ` 1614` ``` using that \e > 0\ by auto ``` lp15@67998 ` 1615` ``` finally have "dist (?m/2^n) (f x) < e" ``` lp15@67998 ` 1616` ``` by (simp add: dist_norm) ``` lp15@67998 ` 1617` ``` then show ?thesis ``` lp15@67998 ` 1618` ``` using eq by linarith ``` lp15@67998 ` 1619` ``` qed ``` lp15@67998 ` 1620` ``` then show "\no. \n\no. dist (\k | k \ \ \ \k\ \ 2 ^ (2*n). k * ?\ n k x/2^n) (f x) < e" ``` lp15@67998 ` 1621` ``` by force ``` lp15@67998 ` 1622` ``` qed ``` lp15@67998 ` 1623` ``` qed ``` lp15@67998 ` 1624` ``` ultimately show ?rhs ``` lp15@67998 ` 1625` ``` by metis ``` lp15@67998 ` 1626` ```next ``` lp15@67998 ` 1627` ``` assume RHS: ?rhs ``` lp15@67998 ` 1628` ``` with borel_measurable_simple_function_limit [of f UNIV, unfolded borel_measurable_UNIV_eq] ``` lp15@67998 ` 1629` ``` show ?lhs ``` lp15@67998 ` 1630` ``` by (blast intro: order_trans) ``` lp15@67998 ` 1631` ```qed ``` lp15@67998 ` 1632` lp15@67998 ` 1633` ```subsection\Borel measurable Jacobian determinant\ ``` lp15@67998 ` 1634` lp15@67998 ` 1635` ```lemma lemma_partial_derivatives0: ``` lp15@67998 ` 1636` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@67998 ` 1637` ``` assumes "linear f" and lim0: "((\x. f x /\<^sub>R norm x) \ 0) (at 0 within S)" ``` lp15@67998 ` 1638` ``` and lb: "\v. v \ 0 \ (\k>0. \e>0. \x. x \ S - {0} \ norm x < e \ k * norm x \ \v \ x\)" ``` lp15@67998 ` 1639` ``` shows "f x = 0" ``` lp15@67998 ` 1640` ```proof - ``` lp15@67998 ` 1641` ``` have "dim {x. f x = 0} \ DIM('a)" ``` lp15@67998 ` 1642` ``` using dim_subset_UNIV by blast ``` lp15@67998 ` 1643` ``` moreover have False if less: "dim {x. f x = 0} < DIM('a)" ``` lp15@67998 ` 1644` ``` proof - ``` lp15@67998 ` 1645` ``` obtain d where "d \ 0" and d: "\y. f y = 0 \ d \ y = 0" ``` lp15@67998 ` 1646` ``` using orthogonal_to_subspace_exists [OF less] orthogonal_def ``` lp15@67998 ` 1647` ``` by (metis (mono_tags, lifting) mem_Collect_eq span_clauses(1)) ``` lp15@67998 ` 1648` ``` then obtain k where "k > 0" ``` lp15@67998 ` 1649` ``` and k: "\e. e > 0 \ \y. y \ S - {0} \ norm y < e \ k * norm y \ \d \ y\" ``` lp15@67998 ` 1650` ``` using lb by blast ``` lp15@67998 ` 1651` ``` have "\h. \n. ((h n \ S \ h n \ 0 \ k * norm (h n) \ \d \ h n\) \ norm (h n) < 1 / real (Suc n)) \ ``` lp15@67998 ` 1652` ``` norm (h (Suc n)) < norm (h n)" ``` lp15@67998 ` 1653` ``` proof (rule dependent_nat_choice) ``` lp15@67998 ` 1654` ``` show "\y. (y \ S \ y \ 0 \ k * norm y \ \d \ y\) \ norm y < 1 / real (Suc 0)" ``` lp15@67998 ` 1655` ``` by simp (metis DiffE insertCI k not_less not_one_le_zero) ``` lp15@67998 ` 1656` ``` qed (use k [of "min (norm x) (1/(Suc n + 1))" for x n] in auto) ``` lp15@67998 ` 1657` ``` then obtain \ where \: "\n. \ n \ S - {0}" and kd: "\n. k * norm(\ n) \ \d \ \ n\" ``` lp15@67998 ` 1658` ``` and norm_lt: "\n. norm(\ n) < 1/(Suc n)" ``` lp15@67998 ` 1659` ``` by force ``` lp15@67998 ` 1660` ``` let ?\ = "\n. \ n /\<^sub>R norm (\ n)" ``` lp15@67998 ` 1661` ``` have com: "\g. (\n. g n \ sphere (0::'a) 1) ``` lp15@67998 ` 1662` ``` \ \l \ sphere 0 1. \\::nat\nat. strict_mono \ \ (g \ \) \ l" ``` lp15@67998 ` 1663` ``` using compact_sphere compact_def by metis ``` lp15@67998 ` 1664` ``` moreover have "\n. ?\ n \ sphere 0 1" ``` lp15@67998 ` 1665` ``` using \ by auto ``` lp15@67998 ` 1666` ``` ultimately obtain l::'a and \::"nat\nat" ``` lp15@67998 ` 1667` ``` where l: "l \ sphere 0 1" and "strict_mono \" and to_l: "(?\ \ \) \ l" ``` lp15@67998 ` 1668` ``` by meson ``` lp15@67998 ` 1669` ``` moreover have "continuous (at l) (\x. (\d \ x\ - k))" ``` lp15@67998 ` 1670` ``` by (intro continuous_intros) ``` lp15@67998 ` 1671` ``` ultimately have lim_dl: "((\x. (\d \ x\ - k)) \ (?\ \ \)) \ (\d \ l\ - k)" ``` lp15@67998 ` 1672` ``` by (meson continuous_imp_tendsto) ``` lp15@67998 ` 1673` ``` have "\\<^sub>F i in sequentially. 0 \ ((\x. \d \ x\ - k) \ ((\n. \ n /\<^sub>R norm (\ n)) \ \)) i" ``` lp15@67998 ` 1674` ``` using \ kd by (auto simp: divide_simps) ``` lp15@67998 ` 1675` ``` then have "k \ \d \ l\" ``` lp15@67998 ` 1676` ``` using tendsto_lowerbound [OF lim_dl, of 0] by auto ``` lp15@67998 ` 1677` ``` moreover have "d \ l = 0" ``` lp15@67998 ` 1678` ``` proof (rule d) ``` lp15@67998 ` 1679` ``` show "f l = 0" ``` lp15@67998 ` 1680` ``` proof (rule LIMSEQ_unique [of "f \ ?\ \ \"]) ``` lp15@67998 ` 1681` ``` have "isCont f l" ``` lp15@67998 ` 1682` ``` using \linear f\ linear_continuous_at linear_conv_bounded_linear by blast ``` lp15@67998 ` 1683` ``` then show "(f \ (\n. \ n /\<^sub>R norm (\ n)) \ \) \ f l" ``` lp15@67998 ` 1684` ``` unfolding comp_assoc ``` lp15@67998 ` 1685` ``` using to_l continuous_imp_tendsto by blast ``` lp15@67998 ` 1686` ``` have "\ \ 0" ``` lp15@67998 ` 1687` ``` using norm_lt LIMSEQ_norm_0 by metis ``` lp15@67998 ` 1688` ``` with \strict_mono \\ have "(\ \ \) \ 0" ``` lp15@67998 ` 1689` ``` by (metis LIMSEQ_subseq_LIMSEQ) ``` lp15@67998 ` 1690` ``` with lim0 \ have "((\x. f x /\<^sub>R norm x) \ (\ \ \)) \ 0" ``` lp15@67998 ` 1691` ``` by (force simp: tendsto_at_iff_sequentially) ``` lp15@67998 ` 1692` ``` then show "(f \ (\n. \ n /\<^sub>R norm (\ n)) \ \) \ 0" ``` lp15@67998 ` 1693` ``` by (simp add: o_def linear_cmul \linear f\) ``` lp15@67998 ` 1694` ``` qed ``` lp15@67998 ` 1695` ``` qed ``` lp15@67998 ` 1696` ``` ultimately show False ``` lp15@67998 ` 1697` ``` using \k > 0\ by auto ``` lp15@67998 ` 1698` ``` qed ``` lp15@67998 ` 1699` ``` ultimately have dim: "dim {x. f x = 0} = DIM('a)" ``` lp15@67998 ` 1700` ``` by force ``` lp15@67998 ` 1701` ``` then show ?thesis ``` lp15@67998 ` 1702` ``` by (metis (mono_tags, lifting) UNIV_I assms(1) dim_eq_full linear_eq_0_span mem_Collect_eq) ``` lp15@67998 ` 1703` ```qed ``` lp15@67998 ` 1704` lp15@67998 ` 1705` ```lemma lemma_partial_derivatives: ``` lp15@67998 ` 1706` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@67998 ` 1707` ``` assumes "linear f" and lim: "((\x. f (x - a) /\<^sub>R norm (x - a)) \ 0) (at a within S)" ``` lp15@67998 ` 1708` ``` and lb: "\v. v \ 0 \ (\k>0. \e>0. \x \ S - {a}. norm(a - x) < e \ k * norm(a - x) \ \v \ (x - a)\)" ``` lp15@67998 ` 1709` ``` shows "f x = 0" ``` lp15@67998 ` 1710` ```proof - ``` lp15@67998 ` 1711` ``` have "((\x. f x /\<^sub>R norm x) \ 0) (at 0 within (\x. x-a) ` S)" ``` lp15@67998 ` 1712` ``` using lim by (simp add: Lim_within dist_norm) ``` lp15@67998 ` 1713` ``` then show ?thesis ``` lp15@67998 ` 1714` ``` proof (rule lemma_partial_derivatives0 [OF \linear f\]) ``` lp15@67998 ` 1715` ``` fix v :: "'a" ``` lp15@67998 ` 1716` ``` assume v: "v \ 0" ``` lp15@67998 ` 1717` ``` show "\k>0. \e>0. \x. x \ (\x. x - a) ` S - {0} \ norm x < e \ k * norm x \ \v \ x\" ``` lp15@67998 ` 1718` ``` using lb [OF v] by (force simp: norm_minus_commute) ``` lp15@67998 ` 1719` ``` qed ``` lp15@67998 ` 1720` ```qed ``` lp15@67998 ` 1721` lp15@67998 ` 1722` lp15@67998 ` 1723` ```proposition borel_measurable_partial_derivatives: ``` lp15@67998 ` 1724` ``` fixes f :: "real^'m::{finite,wellorder} \ real^'n" ``` lp15@67998 ` 1725` ``` assumes S: "S \ sets lebesgue" ``` lp15@67998 ` 1726` ``` and f: "\x. x \ S \ (f has_derivative f' x) (at x within S)" ``` lp15@67998 ` 1727` ``` shows "(\x. (matrix(f' x)\$m\$n)) \ borel_measurable (lebesgue_on S)" ``` lp15@67998 ` 1728` ```proof - ``` lp15@67998 ` 1729` ``` have contf: "continuous_on S f" ``` lp15@67998 ` 1730` ``` using continuous_on_eq_continuous_within f has_derivative_continuous by blast ``` lp15@67998 ` 1731` ``` have "{x \ S. (matrix (f' x)\$m\$n) \ b} \ sets lebesgue" for b ``` lp15@67998 ` 1732` ``` proof (rule sets_negligible_symdiff) ``` lp15@67998 ` 1733` ``` let ?T = "{x \ S. \e>0. \d>0. \A. A\$m\$n < b \ (\i j. A\$i\$j \ \) \ ``` lp15@67998 ` 1734` ``` (\y \ S. norm(y - x) < d \ norm(f y - f x - A *v (y - x)) \ e * norm(y - x))}" ``` lp15@67998 ` 1735` ``` let ?U = "S \ ``` lp15@67998 ` 1736` ``` (\e \ {e \ \. e > 0}. ``` lp15@67998 ` 1737` ``` \A \ {A. A\$m\$n < b \ (\i j. A\$i\$j \ \)}. ``` lp15@67998 ` 1738` ``` \d \ {d \ \. 0 < d}. ``` lp15@67998 ` 1739` ``` S \ (\y \ S. {x \ S. norm(y - x) < d \ norm(f y - f x - A *v (y - x)) \ e * norm(y - x)}))" ``` lp15@67998 ` 1740` ``` have "?T = ?U" ``` lp15@67998 ` 1741` ``` proof (intro set_eqI iffI) ``` lp15@67998 ` 1742` ``` fix x ``` lp15@67998 ` 1743` ``` assume xT: "x \ ?T" ``` lp15@67998 ` 1744` ``` then show "x \ ?U" ``` lp15@67998 ` 1745` ``` proof (clarsimp simp add:) ``` lp15@67998 ` 1746` ``` fix q :: real ``` lp15@67998 ` 1747` ``` assume "q \ \" "q > 0" ``` lp15@67998 ` 1748` ``` then obtain d A where "d > 0" and A: "A \$ m \$ n < b" "\i j. A \$ i \$ j \ \" ``` lp15@67998 ` 1749` ``` "\y. \y\S; norm (y - x) < d\ \ norm (f y - f x - A *v (y - x)) \ q * norm (y - x)" ``` lp15@67998 ` 1750` ``` using xT by auto ``` lp15@67998 ` 1751` ``` then obtain \ where "d > \" "\ > 0" "\ \ \" ``` lp15@67998 ` 1752` ``` using Rats_dense_in_real by blast ``` lp15@67998 ` 1753` ``` with A show "\A. A \$ m \$ n < b \ (\i j. A \$ i \$ j \ \) \ ``` lp15@67998 ` 1754` ``` (\s. s \ \ \ 0 < s \ (\y\S. norm (y - x) < s \ norm (f y - f x - A *v (y - x)) \ q * norm (y - x)))" ``` lp15@67998 ` 1755` ``` by force ``` lp15@67998 ` 1756` ``` qed ``` lp15@67998 ` 1757` ``` next ``` lp15@67998 ` 1758` ``` fix x ``` lp15@67998 ` 1759` ``` assume xU: "x \ ?U" ``` lp15@67998 ` 1760` ``` then show "x \ ?T" ``` lp15@67998 ` 1761` ``` proof clarsimp ``` lp15@67998 ` 1762` ``` fix e :: "real" ``` lp15@67998 ` 1763` ``` assume "e > 0" ``` lp15@67998 ` 1764` ``` then obtain \ where \: "e > \" "\ > 0" "\ \ \" ``` lp15@67998 ` 1765` ``` using Rats_dense_in_real by blast ``` lp15@67998 ` 1766` ``` with xU obtain A r where "x \ S" and Ar: "A \$ m \$ n < b" "\i j. A \$ i \$ j \ \" "r \ \" "r > 0" ``` lp15@67998 ` 1767` ``` and "\y\S. norm (y - x) < r \ norm (f y - f x - A *v (y - x)) \ \ * norm (y - x)" ``` lp15@67998 ` 1768` ``` by (auto simp: split: if_split_asm) ``` lp15@67998 ` 1769` ``` then have "\y\S. norm (y - x) < r \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x)" ``` lp15@67998 ` 1770` ``` by (meson \e > \\ less_eq_real_def mult_right_mono norm_ge_zero order_trans) ``` lp15@67998 ` 1771` ``` then show "\d>0. \A. A \$ m \$ n < b \ (\i j. A \$ i \$ j \ \) \ (\y\S. norm (y - x) < d \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x))" ``` lp15@67998 ` 1772` ``` using \x \ S\ Ar by blast ``` lp15@67998 ` 1773` ``` qed ``` lp15@67998 ` 1774` ``` qed ``` lp15@67998 ` 1775` ``` moreover have "?U \ sets lebesgue" ``` lp15@67998 ` 1776` ``` proof - ``` lp15@67998 ` 1777` ``` have coQ: "countable {e \ \. 0 < e}" ``` lp15@67998 ` 1778` ``` using countable_Collect countable_rat by blast ``` lp15@67998 ` 1779` ``` have ne: "{e \ \. (0::real) < e} \ {}" ``` lp15@67998 ` 1780` ``` using zero_less_one Rats_1 by blast ``` lp15@67998 ` 1781` ``` have coA: "countable {A. A \$ m \$ n < b \ (\i j. A \$ i \$ j \ \)}" ``` lp15@67998 ` 1782` ``` proof (rule countable_subset) ``` lp15@67998 ` 1783` ``` show "countable {A. \i j. A \$ i \$ j \ \}" ``` lp15@67998 ` 1784` ``` using countable_vector [OF countable_vector, of "\i j. \"] by (simp add: countable_rat) ``` lp15@67998 ` 1785` ``` qed blast ``` lp15@67998 ` 1786` ``` have *: "\U \ {} \ closedin (subtopology euclidean S) (S \ \ U)\ ``` lp15@67998 ` 1787` ``` \ closedin (subtopology euclidean S) (S \ \ U)" for U ``` lp15@67998 ` 1788` ``` by fastforce ``` lp15@67998 ` 1789` ``` have eq: "{x::(real,'m)vec. P x \ (Q x \ R x)} = {x. P x \ \ Q x} \ {x. P x \ R x}" for P Q R ``` lp15@67998 ` 1790` ``` by auto ``` lp15@67998 ` 1791` ``` have sets: "S \ (\y\S. {x \ S. norm (y - x) < d \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x)}) ``` lp15@67998 ` 1792` ``` \ sets lebesgue" for e A d ``` lp15@67998 ` 1793` ``` proof - ``` lp15@67998 ` 1794` ``` have clo: "closedin (subtopology euclidean S) ``` lp15@67998 ` 1795` ``` {x \ S. norm (y - x) < d \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x)}" ``` lp15@67998 ` 1796` ``` for y ``` lp15@67998 ` 1797` ``` proof - ``` lp15@67998 ` 1798` ``` have cont1: "continuous_on S (\x. norm (y - x))" ``` lp15@67998 ` 1799` ``` and cont2: "continuous_on S (\x. e * norm (y - x) - norm (f y - f x - (A *v y - A *v x)))" ``` lp15@67998 ` 1800` ``` by (force intro: contf continuous_intros)+ ``` lp15@67998 ` 1801` ``` have clo1: "closedin (subtopology euclidean S) {x \ S. d \ norm (y - x)}" ``` lp15@67998 ` 1802` ``` using continuous_closedin_preimage [OF cont1, of "{d..}"] by (simp add: vimage_def Int_def) ``` lp15@67998 ` 1803` ``` have clo2: "closedin (subtopology euclidean S) ``` lp15@67998 ` 1804` ``` {x \ S. norm (f y - f x - (A *v y - A *v x)) \ e * norm (y - x)}" ``` lp15@67998 ` 1805` ``` using continuous_closedin_preimage [OF cont2, of "{0..}"] by (simp add: vimage_def Int_def) ``` lp15@67998 ` 1806` ``` show ?thesis ``` lp15@67998 ` 1807` ``` by (auto simp: eq not_less matrix_vector_mult_diff_distrib intro: clo1 clo2) ``` lp15@67998 ` 1808` ``` qed ``` lp15@67998 ` 1809` ``` show ?thesis ``` lp15@67998 ` 1810` ``` by (rule lebesgue_closedin [of S]) (force intro: * S clo)+ ``` lp15@67998 ` 1811` ``` qed ``` lp15@67998 ` 1812` ``` show ?thesis ``` lp15@67998 ` 1813` ``` by (intro sets sets.Int S sets.countable_UN'' sets.countable_INT'' coQ coA) auto ``` lp15@67998 ` 1814` ``` qed ``` lp15@67998 ` 1815` ``` ultimately show "?T \ sets lebesgue" ``` lp15@67998 ` 1816` ``` by simp ``` lp15@67998 ` 1817` ``` let ?M = "(?T - {x \ S. matrix (f' x) \$ m \$ n \ b} \ ({x \ S. matrix (f' x) \$ m \$ n \ b} - ?T))" ``` lp15@67998 ` 1818` ``` let ?\ = "\x v. \\>0. \e>0. \y \ S-{x}. norm (x - y) < e \ \v \ (y - x)\ < \ * norm (x - y)" ``` lp15@67998 ` 1819` ``` have nN: "negligible {x \ S. \v\0. ?\ x v}" ``` lp15@67998 ` 1820` ``` unfolding negligible_eq_zero_density ``` lp15@67998 ` 1821` ``` proof clarsimp ``` lp15@67998 ` 1822` ``` fix x v and r e :: "real" ``` lp15@67998 ` 1823` ``` assume "x \ S" "v \ 0" "r > 0" "e > 0" ``` lp15@67998 ` 1824` ``` and Theta [rule_format]: "?\ x v" ``` lp15@67998 ` 1825` ``` moreover have "(norm v * e / 2) / CARD('m) ^ CARD('m) > 0" ``` lp15@67998 ` 1826` ``` by (simp add: \v \ 0\ \e > 0\) ``` lp15@67998 ` 1827` ``` ultimately obtain d where "d > 0" ``` lp15@67998 ` 1828` ``` and dless: "\y. \y \ S - {x}; norm (x - y) < d\ \ ``` lp15@67998 ` 1829` ``` \v \ (y - x)\ < ((norm v * e / 2) / CARD('m) ^ CARD('m)) * norm (x - y)" ``` lp15@67998 ` 1830` ``` by metis ``` lp15@67998 ` 1831` ``` let ?W = "ball x (min d r) \ {y. \v \ (y - x)\ < (norm v * e/2 * min d r) / CARD('m) ^ CARD('m)}" ``` lp15@67998 ` 1832` ``` have "open {x. \v \ (x - a)\ < b}" for a b ``` lp15@67998 ` 1833` ``` by (intro open_Collect_less continuous_intros) ``` lp15@67998 ` 1834` ``` show "\d>0. d \ r \ ``` lp15@67998 ` 1835` ``` (\U. {x' \ S. \v\0. ?\ x' v} \ ball x d \ U \ ``` lp15@67998 ` 1836` ``` U \ lmeasurable \ measure lebesgue U < e * content (ball x d))" ``` lp15@67998 ` 1837` ``` proof (intro exI conjI) ``` lp15@67998 ` 1838` ``` show "0 < min d r" "min d r \ r" ``` lp15@67998 ` 1839` ``` using \r > 0\ \d > 0\ by auto ``` lp15@67998 ` 1840` ``` show "{x' \ S. \v. v \ 0 \ (\\>0. \e>0. \z\S - {x'}. norm (x' - z) < e \ \v \ (z - x')\ < \ * norm (x' - z))} \ ball x (min d r) \ ?W" ``` lp15@67998 ` 1841` ``` proof (clarsimp simp: dist_norm norm_minus_commute) ``` lp15@67998 ` 1842` ``` fix y :: "(real, 'm) vec" and w :: "(real, 'm) vec" ``` lp15@67998 ` 1843` ``` assume "y \ S" "w \ 0" ``` lp15@67998 ` 1844` ``` and less [rule_format]: ``` lp15@67998 ` 1845` ``` "\\>0. \e>0. \z\S - {y}. norm (y - z) < e \ \w \ (z - y)\ < \ * norm (y - z)" ``` lp15@67998 ` 1846` ``` and d: "norm (y - x) < d" and r: "norm (y - x) < r" ``` lp15@67998 ` 1847` ``` show "\v \ (y - x)\ < norm v * e * min d r / (2 * real CARD('m) ^ CARD('m))" ``` lp15@67998 ` 1848` ``` proof (cases "y = x") ``` lp15@67998 ` 1849` ``` case True ``` lp15@67998 ` 1850` ``` with \r > 0\ \d > 0\ \e > 0\ \v \ 0\ show ?thesis ``` lp15@67998 ` 1851` ``` by simp ``` lp15@67998 ` 1852` ``` next ``` lp15@67998 ` 1853` ``` case False ``` lp15@67998 ` 1854` ``` have "\v \ (y - x)\ < norm v * e / 2 / real (CARD('m) ^ CARD('m)) * norm (x - y)" ``` lp15@67998 ` 1855` ``` apply (rule dless) ``` lp15@67998 ` 1856` ``` using False \y \ S\ d by (auto simp: norm_minus_commute) ``` lp15@67998 ` 1857` ``` also have "\ \ norm v * e * min d r / (2 * real CARD('m) ^ CARD('m))" ``` lp15@67998 ` 1858` ``` using d r \e > 0\ by (simp add: field_simps norm_minus_commute mult_left_mono) ``` lp15@67998 ` 1859` ``` finally show ?thesis . ``` lp15@67998 ` 1860` ``` qed ``` lp15@67998 ` 1861` ``` qed ``` lp15@67998 ` 1862` ``` show "?W \ lmeasurable" ``` lp15@67998 ` 1863` ``` by (simp add: fmeasurable_Int_fmeasurable borel_open) ``` lp15@67998 ` 1864` ``` obtain k::'m where True ``` lp15@67998 ` 1865` ``` by metis ``` lp15@67998 ` 1866` ``` obtain T where T: "orthogonal_transformation T" and v: "v = T(norm v *\<^sub>R axis k (1::real))" ``` lp15@67998 ` 1867` ``` using rotation_rightward_line by metis ``` lp15@67998 ` 1868` ``` define b where "b \ norm v" ``` lp15@67998 ` 1869` ``` have "b > 0" ``` lp15@67998 ` 1870` ``` using \v \ 0\ by (auto simp: b_def) ``` lp15@67998 ` 1871` ``` obtain eqb: "inv T v = b *\<^sub>R axis k (1::real)" and "inj T" "bij T" and invT: "orthogonal_transformation (inv T)" ``` lp15@67998 ` 1872` ``` by (metis UNIV_I b_def T v bij_betw_inv_into_left orthogonal_transformation_inj orthogonal_transformation_bij orthogonal_transformation_inv) ``` lp15@67998 ` 1873` ``` let ?v = "\ i. min d r / CARD('m)" ``` lp15@67998 ` 1874` ``` let ?v' = "\ i. if i = k then (e/2 * min d r) / CARD('m) ^ CARD('m) else min d r" ``` lp15@67998 ` 1875` ``` let ?x' = "inv T x" ``` lp15@67998 ` 1876` ``` let ?W' = "(ball ?x' (min d r) \ {y. \(y - ?x')\$k\ < e * min d r / (2 * CARD('m) ^ CARD('m))})" ``` lp15@67998 ` 1877` ``` have abs: "x - e \ y \ y \ x + e \ abs(y - x) \ e" for x y e::real ``` lp15@67998 ` 1878` ``` by auto ``` lp15@67998 ` 1879` ``` have "?W = T ` ?W'" ``` lp15@67998 ` 1880` ``` proof - ``` lp15@67998 ` 1881` ``` have 1: "T ` (ball (inv T x) (min d r)) = ball x (min d r)" ``` lp15@67998 ` 1882` ``` by (simp add: T image_orthogonal_transformation_ball orthogonal_transformation_surj surj_f_inv_f) ``` lp15@67998 ` 1883` ``` have 2: "{y. \v \ (y - x)\ < b * e * min d r / (2 * real CARD('m) ^ CARD('m))} = ``` lp15@67998 ` 1884` ``` T ` {y. \y \$ k - ?x' \$ k\ < e * min d r / (2 * real CARD('m) ^ CARD('m))}" ``` lp15@67998 ` 1885` ``` proof - ``` lp15@67998 ` 1886` ``` have *: "\T (b *\<^sub>R axis k 1) \ (y - x)\ = b * \inv T y \$ k - ?x' \$ k\" for y ``` lp15@67998 ` 1887` ``` proof - ``` lp15@67998 ` 1888` ``` have "\T (b *\<^sub>R axis k 1) \ (y - x)\ = \(b *\<^sub>R axis k 1) \ inv T (y - x)\" ``` lp15@67998 ` 1889` ``` by (metis (no_types, hide_lams) b_def eqb invT orthogonal_transformation_def v) ``` lp15@67998 ` 1890` ``` also have "\ = b * \(axis k 1) \ inv T (y - x)\" ``` lp15@67998 ` 1891` ``` using \b > 0\ by (simp add: abs_mult) ``` lp15@67998 ` 1892` ``` also have "\ = b * \inv T y \$ k - ?x' \$ k\" ``` lp15@67998 ` 1893` ``` using orthogonal_transformation_linear [OF invT] ``` lp15@67998 ` 1894` ``` by (simp add: inner_axis' linear_diff) ``` lp15@67998 ` 1895` ``` finally show ?thesis ``` lp15@67998 ` 1896` ``` by simp ``` lp15@67998 ` 1897` ``` qed ``` lp15@67998 ` 1898` ``` show ?thesis ``` lp15@67998 ` 1899` ``` using v b_def [symmetric] ``` lp15@67998 ` 1900` ``` using \b > 0\ by (simp add: * bij_image_Collect_eq [OF \bij T\] mult_less_cancel_left_pos times_divide_eq_right [symmetric] del: times_divide_eq_right) ``` lp15@67998 ` 1901` ``` qed ``` lp15@67998 ` 1902` ``` show ?thesis ``` lp15@67998 ` 1903` ``` using \b > 0\ by (simp add: image_Int \inj T\ 1 2 b_def [symmetric]) ``` lp15@67998 ` 1904` ``` qed ``` lp15@67998 ` 1905` ``` moreover have "?W' \ lmeasurable" ``` lp15@67998 ` 1906` ``` by (auto intro: fmeasurable_Int_fmeasurable) ``` lp15@67998 ` 1907` ``` ultimately have "measure lebesgue ?W = measure lebesgue ?W'" ``` lp15@67998 ` 1908` ``` by (metis measure_orthogonal_image T) ``` lp15@67998 ` 1909` ``` also have "\ \ measure lebesgue (cbox (?x' - ?v') (?x' + ?v'))" ``` lp15@67998 ` 1910` ``` proof (rule measure_mono_fmeasurable) ``` lp15@67998 ` 1911` ``` show "?W' \ cbox (?x' - ?v') (?x' + ?v')" ``` lp15@67998 ` 1912` ``` apply (clarsimp simp add: mem_box_cart abs dist_norm norm_minus_commute simp del: min_less_iff_conj min.bounded_iff) ``` lp15@67998 ` 1913` ``` by (metis component_le_norm_cart less_eq_real_def le_less_trans vector_minus_component) ``` lp15@67998 ` 1914` ``` qed auto ``` lp15@67998 ` 1915` ``` also have "\ \ e/2 * measure lebesgue (cbox (?x' - ?v) (?x' + ?v))" ``` lp15@67998 ` 1916` ``` proof - ``` lp15@67998 ` 1917` ``` have "cbox (?x' - ?v) (?x' + ?v) \ {}" ``` lp15@67998 ` 1918` ``` using \r > 0\ \d > 0\ by (auto simp: interval_eq_empty_cart divide_less_0_iff) ``` lp15@67998 ` 1919` ``` with \r > 0\ \d > 0\ \e > 0\ show ?thesis ``` lp15@67998 ` 1920` ``` apply (simp add: content_cbox_if_cart mem_box_cart) ``` lp15@67998 ` 1921` ``` apply (auto simp: prod_nonneg) ``` lp15@67998 ` 1922` ``` apply (simp add: abs if_distrib prod.delta_remove prod_constant field_simps power_diff split: if_split_asm) ``` lp15@67998 ` 1923` ``` done ``` lp15@67998 ` 1924` ``` qed ``` lp15@67998 ` 1925` ``` also have "\ \ e/2 * measure lebesgue (cball ?x' (min d r))" ``` lp15@67998 ` 1926` ``` proof (rule mult_left_mono [OF measure_mono_fmeasurable]) ``` lp15@67998 ` 1927` ``` have *: "norm (?x' - y) \ min d r" ``` lp15@67998 ` 1928` ``` if y: "\i. \?x' \$ i - y \$ i\ \ min d r / real CARD('m)" for y ``` lp15@67998 ` 1929` ``` proof - ``` lp15@67998 ` 1930` ``` have "norm (?x' - y) \ (\i\UNIV. \(?x' - y) \$ i\)" ``` lp15@67998 ` 1931` ``` by (rule norm_le_l1_cart) ``` lp15@67998 ` 1932` ``` also have "\ \ real CARD('m) * (min d r / real CARD('m))" ``` lp15@67998 ` 1933` ``` by (rule sum_bounded_above) (use y in auto) ``` lp15@67998 ` 1934` ``` finally show ?thesis ``` lp15@67998 ` 1935` ``` by simp ``` lp15@67998 ` 1936` ``` qed ``` lp15@67998 ` 1937` ``` show "cbox (?x' - ?v) (?x' + ?v) \ cball ?x' (min d r)" ``` lp15@67998 ` 1938` ``` apply (clarsimp simp only: mem_box_cart dist_norm mem_cball intro!: *) ``` lp15@67998 ` 1939` ``` by (simp add: abs_diff_le_iff abs_minus_commute) ``` lp15@67998 ` 1940` ``` qed (use \e > 0\ in auto) ``` lp15@67998 ` 1941` ``` also have "\ < e * content (cball ?x' (min d r))" ``` lp15@67998 ` 1942` ``` using \r > 0\ \d > 0\ \e > 0\ by auto ``` lp15@67998 ` 1943` ``` also have "\ = e * content (ball x (min d r))" ``` lp15@67998 ` 1944` ``` using \r > 0\ \d > 0\ by (simp add: content_cball content_ball) ``` lp15@67998 ` 1945` ``` finally show "measure lebesgue ?W < e * content (ball x (min d r))" . ``` lp15@67998 ` 1946` ``` qed ``` lp15@67998 ` 1947` ``` qed ``` lp15@67998 ` 1948` ``` have *: "(\x. (x \ S) \ (x \ T \ x \ U)) \ (T - U) \ (U - T) \ S" for S T U :: "(real,'m) vec set" ``` lp15@67998 ` 1949` ``` by blast ``` lp15@67998 ` 1950` ``` have MN: "?M \ {x \ S. \v\0. ?\ x v}" ``` lp15@67998 ` 1951` ``` proof (rule *) ``` lp15@67998 ` 1952` ``` fix x ``` lp15@67998 ` 1953` ``` assume x: "x \ {x \ S. \v\0. ?\ x v}" ``` lp15@67998 ` 1954` ``` show "(x \ ?T) \ (x \ {x \ S. matrix (f' x) \$ m \$ n \ b})" ``` lp15@67998 ` 1955` ``` proof (cases "x \ S") ``` lp15@67998 ` 1956` ``` case True ``` lp15@67998 ` 1957` ``` then have x: "\ ?\ x v" if "v \ 0" for v ``` lp15@67998 ` 1958` ``` using x that by force ``` lp15@67998 ` 1959` ``` show ?thesis ``` lp15@67998 ` 1960` ``` proof (rule iffI; clarsimp) ``` lp15@67998 ` 1961` ``` assume b: "\e>0. \d>0. \A. A \$ m \$ n < b \ (\i j. A \$ i \$ j \ \) \ ``` lp15@67998 ` 1962` ``` (\y\S. norm (y - x) < d \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x))" ``` lp15@67998 ` 1963` ``` (is "\e>0. \d>0. \A. ?\ e d A") ``` lp15@67998 ` 1964` ``` then have "\k. \d>0. \A. ?\ (1 / Suc k) d A" ``` lp15@67998 ` 1965` ``` by (metis (no_types, hide_lams) less_Suc_eq_0_disj of_nat_0_less_iff zero_less_divide_1_iff) ``` lp15@67998 ` 1966` ``` then obtain \ A where \: "\k. \ k > 0" ``` lp15@67998 ` 1967` ``` and Ab: "\k. A k \$ m \$ n < b" ``` lp15@67998 ` 1968` ``` and A: "\k y. \y \ S; norm (y - x) < \ k\ \ ``` lp15@67998 ` 1969` ``` norm (f y - f x - A k *v (y - x)) \ 1/(Suc k) * norm (y - x)" ``` lp15@67998 ` 1970` ``` by metis ``` lp15@67998 ` 1971` ``` have "\i j. \a. (\n. A n \$ i \$ j) \ a" ``` lp15@67998 ` 1972` ``` proof (intro allI) ``` lp15@67998 ` 1973` ``` fix i j ``` lp15@67998 ` 1974` ``` have vax: "(A n *v axis j 1) \$ i = A n \$ i \$ j" for n ``` lp15@67998 ` 1975` ``` by (metis cart_eq_inner_axis matrix_vector_mul_component) ``` lp15@67998 ` 1976` ``` let ?CA = "{x. Cauchy (\n. (A n) *v x)}" ``` lp15@67998 ` 1977` ``` have "subspace ?CA" ``` lp15@67998 ` 1978` ``` unfolding subspace_def convergent_eq_Cauchy [symmetric] ``` lp15@67998 ` 1979` ``` by (force simp: algebra_simps intro: tendsto_intros) ``` lp15@67998 ` 1980` ``` then have CA_eq: "?CA = span ?CA" ``` lp15@67998 ` 1981` ``` by (metis span_eq) ``` lp15@67998 ` 1982` ``` also have "\ = UNIV" ``` lp15@67998 ` 1983` ``` proof - ``` lp15@67998 ` 1984` ``` have "dim ?CA \ CARD('m)" ``` lp15@67998 ` 1985` ``` by (rule dim_subset_UNIV_cart) ``` lp15@67998 ` 1986` ``` moreover have "False" if less: "dim ?CA < CARD('m)" ``` lp15@67998 ` 1987` ``` proof - ``` lp15@67998 ` 1988` ``` obtain d where "d \ 0" and d: "\y. y \ span ?CA \ orthogonal d y" ``` lp15@67998 ` 1989` ``` using less by (force intro: orthogonal_to_subspace_exists [of ?CA]) ``` lp15@67998 ` 1990` ``` with x [OF \d \ 0\] obtain \ where "\ > 0" ``` lp15@67998 ` 1991` ``` and \: "\e. e > 0 \ \y \ S - {x}. norm (x - y) < e \ \ * norm (x - y) \ \d \ (y - x)\" ``` lp15@67998 ` 1992` ``` by (fastforce simp: not_le Bex_def) ``` lp15@67998 ` 1993` ``` obtain \ z where \Sx: "\i. \ i \ S - {x}" ``` lp15@67998 ` 1994` ``` and \le: "\i. \ * norm(\ i - x) \ \d \ (\ i - x)\" ``` lp15@67998 ` 1995` ``` and \x: "\ \ x" ``` lp15@67998 ` 1996` ``` and z: "(\n. (\ n - x) /\<^sub>R norm (\ n - x)) \ z" ``` lp15@67998 ` 1997` ``` proof - ``` lp15@67998 ` 1998` ``` have "\\. (\i. (\ i \ S - {x} \ ``` lp15@67998 ` 1999` ``` \ * norm(\ i - x) \ \d \ (\ i - x)\ \ norm(\ i - x) < 1/Suc i) \ ``` lp15@67998 ` 2000` ``` norm(\(Suc i) - x) < norm(\ i - x))" ``` lp15@67998 ` 2001` ``` proof (rule dependent_nat_choice) ``` lp15@67998 ` 2002` ``` show "\y. y \ S - {x} \ \ * norm (y - x) \ \d \ (y - x)\ \ norm (y - x) < 1 / Suc 0" ``` lp15@67998 ` 2003` ``` using \ [of 1] by (auto simp: dist_norm norm_minus_commute) ``` lp15@67998 ` 2004` ``` next ``` lp15@67998 ` 2005` ``` fix y i ``` lp15@67998 ` 2006` ``` assume "y \ S - {x} \ \ * norm (y - x) \ \d \ (y - x)\ \ norm (y - x) < 1/Suc i" ``` lp15@67998 ` 2007` ``` then have "min (norm(y - x)) (1/((Suc i) + 1)) > 0" ``` lp15@67998 ` 2008` ``` by auto ``` lp15@67998 ` 2009` ``` then obtain y' where "y' \ S - {x}" and y': "norm (x - y') < min (norm (y - x)) (1/((Suc i) + 1))" ``` lp15@67998 ` 2010` ``` "\ * norm (x - y') \ \d \ (y' - x)\" ``` lp15@67998 ` 2011` ``` using \ by metis ``` lp15@67998 ` 2012` ``` with \ show "\y'. (y' \ S - {x} \ \ * norm (y' - x) \ \d \ (y' - x)\ \ ``` lp15@67998 ` 2013` ``` norm (y' - x) < 1/(Suc (Suc i))) \ norm (y' - x) < norm (y - x)" ``` lp15@67998 ` 2014` ``` by (auto simp: dist_norm norm_minus_commute) ``` lp15@67998 ` 2015` ``` qed ``` lp15@67998 ` 2016` ``` then obtain \ where ``` lp15@67998 ` 2017` ``` \Sx: "\i. \ i \ S - {x}" ``` lp15@67998 ` 2018` ``` and \le: "\i. \ * norm(\ i - x) \ \d \ (\ i - x)\" ``` lp15@67998 ` 2019` ``` and \conv: "\i. norm(\ i - x) < 1/(Suc i)" ``` lp15@67998 ` 2020` ``` by blast ``` lp15@67998 ` 2021` ``` let ?f = "\i. (\ i - x) /\<^sub>R norm (\ i - x)" ``` lp15@67998 ` 2022` ``` have "?f i \ sphere 0 1" for i ``` lp15@67998 ` 2023` ``` using \Sx by auto ``` lp15@67998 ` 2024` ``` then obtain l \ where "l \ sphere 0 1" "strict_mono \" and l: "(?f \ \) \ l" ``` lp15@67998 ` 2025` ``` using compact_sphere [of "0::(real,'m) vec" 1] unfolding compact_def by meson ``` lp15@67998 ` 2026` ``` show thesis ``` lp15@67998 ` 2027` ``` proof ``` lp15@67998 ` 2028` ``` show "(\ \ \) i \ S - {x}" "\ * norm ((\ \ \) i - x) \ \d \ ((\ \ \) i - x)\" for i ``` lp15@67998 ` 2029` ``` using \Sx \le by auto ``` lp15@67998 ` 2030` ``` have "\ \ x" ``` lp15@67998 ` 2031` ``` proof (clarsimp simp add: LIMSEQ_def dist_norm) ``` lp15@67998 ` 2032` ``` fix r :: "real" ``` lp15@67998 ` 2033` ``` assume "r > 0" ``` lp15@67998 ` 2034` ``` with real_arch_invD obtain no where "no \ 0" "real no > 1/r" ``` lp15@67998 ` 2035` ``` by (metis divide_less_0_1_iff not_less_iff_gr_or_eq of_nat_0_eq_iff reals_Archimedean2) ``` lp15@67998 ` 2036` ``` with \conv show "\no. \n\no. norm (\ n - x) < r" ``` lp15@67998 ` 2037` ``` by (metis \r > 0\ add.commute divide_inverse inverse_inverse_eq inverse_less_imp_less less_trans mult.left_neutral nat_le_real_less of_nat_Suc) ``` lp15@67998 ` 2038` ``` qed ``` lp15@67998 ` 2039` ``` with \strict_mono \\ show "(\ \ \) \ x" ``` lp15@67998 ` 2040` ``` by (metis LIMSEQ_subseq_LIMSEQ) ``` lp15@67998 ` 2041` ``` show "(\n. ((\ \ \) n - x) /\<^sub>R norm ((\ \ \) n - x)) \ l" ``` lp15@67998 ` 2042` ``` using l by (auto simp: o_def) ``` lp15@67998 ` 2043` ``` qed ``` lp15@67998 ` 2044` ``` qed ``` lp15@67998 ` 2045` ``` have "isCont (\x. (\d \ x\ - \)) z" ``` lp15@67998 ` 2046` ``` by (intro continuous_intros) ``` lp15@67998 ` 2047` ``` from isCont_tendsto_compose [OF this z] ``` lp15@67998 ` 2048` ``` have lim: "(\y. \d \ ((\ y - x) /\<^sub>R norm (\ y - x))\ - \) \ \d \ z\ - \" ``` lp15@67998 ` 2049` ``` by auto ``` lp15@67998 ` 2050` ``` moreover have "\\<^sub>F i in sequentially. 0 \ \d \ ((\ i - x) /\<^sub>R norm (\ i - x))\ - \" ``` lp15@67998 ` 2051` ``` proof (rule eventuallyI) ``` lp15@67998 ` 2052` ``` fix n ``` lp15@67998 ` 2053` ``` show "0 \ \d \ ((\ n - x) /\<^sub>R norm (\ n - x))\ - \" ``` lp15@67998 ` 2054` ``` using \le [of n] \Sx by (auto simp: abs_mult divide_simps) ``` lp15@67998 ` 2055` ``` qed ``` lp15@67998 ` 2056` ``` ultimately have "\ \ \d \ z\" ``` lp15@67998 ` 2057` ``` using tendsto_lowerbound [where a=0] by fastforce ``` lp15@67998 ` 2058` ``` have "Cauchy (\n. (A n) *v z)" ``` lp15@67998 ` 2059` ``` proof (clarsimp simp add: Cauchy_def) ``` lp15@67998 ` 2060` ``` fix \ :: "real" ``` lp15@67998 ` 2061` ``` assume "0 < \" ``` lp15@67998 ` 2062` ``` then obtain N::nat where "N > 0" and N: "\/2 > 1/N" ``` lp15@67998 ` 2063` ``` by (metis half_gt_zero inverse_eq_divide neq0_conv real_arch_inverse) ``` lp15@67998 ` 2064` ``` show "\M. \m\M. \n\M. dist (A m *v z) (A n *v z) < \" ``` lp15@67998 ` 2065` ``` proof (intro exI allI impI) ``` lp15@67998 ` 2066` ``` fix i j ``` lp15@67998 ` 2067` ``` assume ij: "N \ i" "N \ j" ``` lp15@67998 ` 2068` ``` let ?V = "\i k. A i *v ((\ k - x) /\<^sub>R norm (\ k - x))" ``` lp15@67998 ` 2069` ``` have "\\<^sub>F k in sequentially. dist (\ k) x < min (\ i) (\ j)" ``` lp15@67998 ` 2070` ``` using \x [unfolded tendsto_iff] by (meson min_less_iff_conj \) ``` lp15@67998 ` 2071` ``` then have even: "\\<^sub>F k in sequentially. norm (?V i k - ?V j k) - 2 / N \ 0" ``` lp15@67998 ` 2072` ``` proof (rule eventually_mono, clarsimp) ``` lp15@67998 ` 2073` ``` fix p ``` lp15@67998 ` 2074` ``` assume p: "dist (\ p) x < \ i" "dist (\ p) x < \ j" ``` lp15@67998 ` 2075` ``` let ?C = "\k. f (\ p) - f x - A k *v (\ p - x)" ``` lp15@67998 ` 2076` ``` have "norm ((A i - A j) *v (\ p - x)) = norm (?C j - ?C i)" ``` lp15@67998 ` 2077` ``` by (simp add: algebra_simps) ``` lp15@67998 ` 2078` ``` also have "\ \ norm (?C j) + norm (?C i)" ``` lp15@67998 ` 2079` ``` using norm_triangle_ineq4 by blast ``` lp15@67998 ` 2080` ``` also have "\ \ 1/(Suc j) * norm (\ p - x) + 1/(Suc i) * norm (\ p - x)" ``` lp15@67998 ` 2081` ``` by (metis A Diff_iff \Sx dist_norm p add_mono) ``` lp15@67998 ` 2082` ``` also have "\ \ 1/N * norm (\ p - x) + 1/N * norm (\ p - x)" ``` lp15@67998 ` 2083` ``` apply (intro add_mono mult_right_mono) ``` lp15@67998 ` 2084` ``` using ij \N > 0\ by (auto simp: field_simps) ``` lp15@67998 ` 2085` ``` also have "\ = 2 / N * norm (\ p - x)" ``` lp15@67998 ` 2086` ``` by simp ``` lp15@67998 ` 2087` ``` finally have no_le: "norm ((A i - A j) *v (\ p - x)) \ 2 / N * norm (\ p - x)" . ``` lp15@67998 ` 2088` ``` have "norm (?V i p - ?V j p) = ``` lp15@67998 ` 2089` ``` norm ((A i - A j) *v ((\ p - x) /\<^sub>R norm (\ p - x)))" ``` lp15@67998 ` 2090` ``` by (simp add: algebra_simps) ``` lp15@67998 ` 2091` ``` also have "\ = norm ((A i - A j) *v (\ p - x)) / norm (\ p - x)" ``` lp15@67998 ` 2092` ``` by (simp add: divide_inverse matrix_vector_mult_scaleR) ``` lp15@67998 ` 2093` ``` also have "\ \ 2 / N" ``` lp15@67998 ` 2094` ``` using no_le by (auto simp: divide_simps) ``` lp15@67998 ` 2095` ``` finally show "norm (?V i p - ?V j p) \ 2 / N" . ``` lp15@67998 ` 2096` ``` qed ``` lp15@67998 ` 2097` ``` have "isCont (\w. (norm(A i *v w - A j *v w) - 2 / N)) z" ``` lp15@67998 ` 2098` ``` by (intro continuous_intros) ``` lp15@67998 ` 2099` ``` from isCont_tendsto_compose [OF this z] ``` lp15@67998 ` 2100` ``` have lim: "(\w. norm (A i *v ((\ w - x) /\<^sub>R norm (\ w - x)) - ``` lp15@67998 ` 2101` ``` A j *v ((\ w - x) /\<^sub>R norm (\ w - x))) - 2 / N) ``` lp15@67998 ` 2102` ``` \ norm (A i *v z - A j *v z) - 2 / N" ``` lp15@67998 ` 2103` ``` by auto ``` lp15@67998 ` 2104` ``` have "dist (A i *v z) (A j *v z) \ 2 / N" ``` lp15@67998 ` 2105` ``` using tendsto_upperbound [OF lim even] by (auto simp: dist_norm) ``` lp15@67998 ` 2106` ``` with N show "dist (A i *v z) (A j *v z) < \" ``` lp15@67998 ` 2107` ``` by linarith ``` lp15@67998 ` 2108` ``` qed ``` lp15@67998 ` 2109` ``` qed ``` lp15@67998 ` 2110` ``` then have "d \ z = 0" ``` lp15@67998 ` 2111` ``` using CA_eq d orthogonal_def by auto ``` lp15@67998 ` 2112` ``` then show False ``` lp15@67998 ` 2113` ``` using \0 < \\ \\ \ \d \ z\\ by auto ``` lp15@67998 ` 2114` ``` qed ``` lp15@67998 ` 2115` ``` ultimately show ?thesis ``` lp15@67998 ` 2116` ``` using dim_eq_full by fastforce ``` lp15@67998 ` 2117` ``` qed ``` lp15@67998 ` 2118` ``` finally have "?CA = UNIV" . ``` lp15@67998 ` 2119` ``` then have "Cauchy (\n. (A n) *v axis j 1)" ``` lp15@67998 ` 2120` ``` by auto ``` lp15@67998 ` 2121` ``` then obtain L where "(\n. A n *v axis j 1) \ L" ``` lp15@67998 ` 2122` ``` by (auto simp: Cauchy_convergent_iff convergent_def) ``` lp15@67998 ` 2123` ``` then have "(\x. (A x *v axis j 1) \$ i) \ L \$ i" ``` lp15@67998 ` 2124` ``` by (rule tendsto_vec_nth) ``` lp15@67998 ` 2125` ``` then show "\a. (\n. A n \$ i \$ j) \ a" ``` lp15@67998 ` 2126` ``` by (force simp: vax) ``` lp15@67998 ` 2127` ``` qed ``` lp15@67998 ` 2128` ``` then obtain B where B: "\i j. (\n. A n \$ i \$ j) \ B \$ i \$ j" ``` lp15@67998 ` 2129` ``` by (auto simp: lambda_skolem) ``` lp15@67998 ` 2130` ``` have lin_df: "linear (f' x)" ``` lp15@67998 ` 2131` ``` and lim_df: "((\y. (1 / norm (y - x)) *\<^sub>R (f y - (f x + f' x (y - x)))) \ 0) (at x within S)" ``` lp15@67998 ` 2132` ``` using \x \ S\ assms by (auto simp: has_derivative_within linear_linear) ``` lp15@67998 ` 2133` ``` moreover have "(matrix (f' x) - B) *v w = 0" for w ``` lp15@67998 ` 2134` ``` proof (rule lemma_partial_derivatives [of "( *v) (matrix (f' x) - B)"]) ``` lp15@67998 ` 2135` ``` show "linear (( *v) (matrix (f' x) - B))" ``` lp15@67998 ` 2136` ``` by (rule matrix_vector_mul_linear) ``` lp15@67998 ` 2137` ``` have "((\y. ((f x + f' x (y - x)) - f y) /\<^sub>R norm (y - x)) \ 0) (at x within S)" ``` lp15@67998 ` 2138` ``` using tendsto_minus [OF lim_df] by (simp add: algebra_simps divide_simps) ``` lp15@67998 ` 2139` ``` then show "((\y. (matrix (f' x) - B) *v (y - x) /\<^sub>R norm (y - x)) \ 0) (at x within S)" ``` lp15@67998 ` 2140` ``` proof (rule Lim_transform) ``` lp15@67998 ` 2141` ``` have "((\y. ((f y + B *v x - (f x + B *v y)) /\<^sub>R norm (y - x))) \ 0) (at x within S)" ``` lp15@67998 ` 2142` ``` proof (clarsimp simp add: Lim_within dist_norm) ``` lp15@67998 ` 2143` ``` fix e :: "real" ``` lp15@67998 ` 2144` ``` assume "e > 0" ``` lp15@67998 ` 2145` ``` then obtain q::nat where "q \ 0" and qe2: "1/q < e/2" ``` lp15@67998 ` 2146` ``` by (metis divide_pos_pos inverse_eq_divide real_arch_inverse zero_less_numeral) ``` lp15@67998 ` 2147` ``` let ?g = "\p. sum (\i. sum (\j. abs((A p - B)\$i\$j)) UNIV) UNIV" ``` lp15@67998 ` 2148` ``` have "(\k. onorm (\y. (A k - B) *v y)) \ 0" ``` lp15@67998 ` 2149` ``` proof (rule Lim_null_comparison) ``` lp15@67998 ` 2150` ``` show "\\<^sub>F k in sequentially. norm (onorm (\y. (A k - B) *v y)) \ ?g k" ``` lp15@67998 ` 2151` ``` proof (rule eventually_sequentiallyI) ``` lp15@67998 ` 2152` ``` fix k :: "nat" ``` lp15@67998 ` 2153` ``` assume "0 \ k" ``` lp15@67998 ` 2154` ``` have "0 \ onorm (( *v) (A k - B))" ``` lp15@67998 ` 2155` ``` by (simp add: linear_linear onorm_pos_le matrix_vector_mul_linear) ``` lp15@67998 ` 2156` ``` then show "norm (onorm (( *v) (A k - B))) \ (\i\UNIV. \j\UNIV. \(A k - B) \$ i \$ j\)" ``` lp15@67998 ` 2157` ``` by (simp add: onorm_le_matrix_component_sum del: vector_minus_component) ``` lp15@67998 ` 2158` ``` qed ``` lp15@67998 ` 2159` ``` next ``` lp15@67998 ` 2160` ``` show "?g \ 0" ``` lp15@67998 ` 2161` ``` using B Lim_null tendsto_rabs_zero_iff by (fastforce intro!: tendsto_null_sum) ``` lp15@67998 ` 2162` ``` qed ``` lp15@67998 ` 2163` ``` with \e > 0\ obtain p where "\n. n \ p \ \onorm (( *v) (A n - B))\ < e/2" ``` lp15@67998 ` 2164` ``` unfolding lim_sequentially by (metis diff_zero dist_real_def divide_pos_pos zero_less_numeral) ``` lp15@67998 ` 2165` ``` then have pqe2: "\onorm (( *v) (A (p + q) - B))\ < e/2" (*17 [`abs (onorm (\y. A (p + q) ** y - B ** y)) < e / &2`]*) ``` lp15@67998 ` 2166` ``` using le_add1 by blast ``` lp15@67998 ` 2167` ``` show "\d>0. \y\S. y \ x \ norm (y - x) < d \ ``` lp15@67998 ` 2168` ``` inverse (norm (y - x)) * norm (f y + B *v x - (f x + B *v y)) < e" ``` lp15@67998 ` 2169` ``` proof (intro exI, safe) ``` lp15@67998 ` 2170` ``` show "0 < \(p + q)" ``` lp15@67998 ` 2171` ``` by (simp add: \) ``` lp15@67998 ` 2172` ``` next ``` lp15@67998 ` 2173` ``` fix y ``` lp15@67998 ` 2174` ``` assume y: "y \ S" "norm (y - x) < \(p + q)" and "y \ x" ``` lp15@67998 ` 2175` ``` have *: "\norm(b - c) < e - d; norm(y - x - b) \ d\ \ norm(y - x - c) < e" ``` lp15@67998 ` 2176` ``` for b c d e x and y:: "real^'n" ``` lp15@67998 ` 2177` ``` using norm_triangle_ineq2 [of "y - x - c" "y - x - b"] by simp ``` lp15@67998 ` 2178` ``` have "norm (f y - f x - B *v (y - x)) < e * norm (y - x)" ``` lp15@67998 ` 2179` ``` proof (rule *) ``` lp15@67998 ` 2180` ``` show "norm (f y - f x - A (p + q) *v (y - x)) \ norm (y - x) / (Suc (p + q))" ``` lp15@67998 ` 2181` ``` using A [OF y] by simp ``` lp15@67998 ` 2182` ``` have "norm (A (p + q) *v (y - x) - B *v (y - x)) \ onorm(\x. (A(p + q) - B) *v x) * norm(y - x)" ``` lp15@67998 ` 2183` ``` by (metis linear_linear matrix_vector_mul_linear matrix_vector_mult_diff_rdistrib onorm) ``` lp15@67998 ` 2184` ``` also have "\ < (e/2) * norm (y - x)" ``` lp15@67998 ` 2185` ``` using \y \ x\ pqe2 by auto ``` lp15@67998 ` 2186` ``` also have "\ \ (e - 1 / (Suc (p + q))) * norm (y - x)" ``` lp15@67998 ` 2187` ``` proof (rule mult_right_mono) ``` lp15@67998 ` 2188` ``` have "1 / Suc (p + q) \ 1 / q" ``` lp15@67998 ` 2189` ``` using \q \ 0\ by (auto simp: divide_simps) ``` lp15@67998 ` 2190` ``` also have "\ < e/2" ``` lp15@67998 ` 2191` ``` using qe2 by auto ``` lp15@67998 ` 2192` ``` finally show "e / 2 \ e - 1 / real (Suc (p + q))" ``` lp15@67998 ` 2193` ``` by linarith ``` lp15@67998 ` 2194` ``` qed auto ``` lp15@67998 ` 2195` ``` finally show "norm (A (p + q) *v (y - x) - B *v (y - x)) < e * norm (y - x) - norm (y - x) / real (Suc (p + q))" ``` lp15@67998 ` 2196` ``` by (simp add: algebra_simps) ``` lp15@67998 ` 2197` ``` qed ``` lp15@67998 ` 2198` ``` then show "inverse (norm (y - x)) * norm (f y + B *v x - (f x + B *v y)) < e" ``` lp15@67998 ` 2199` ``` using \y \ x\ by (simp add: divide_simps algebra_simps) ``` lp15@67998 ` 2200` ``` qed ``` lp15@67998 ` 2201` ``` qed ``` lp15@67998 ` 2202` ``` then show "((\y. (matrix (f' x) - B) *v (y - x) /\<^sub>R ``` lp15@67998 ` 2203` ``` norm (y - x) - (f x + f' x (y - x) - f y) /\<^sub>R norm (y - x)) \ 0) ``` lp15@67998 ` 2204` ``` (at x within S)" ``` lp15@67998 ` 2205` ``` by (simp add: algebra_simps lin_df linear_diff matrix_vector_mul_linear) ``` lp15@67998 ` 2206` ``` qed ``` lp15@67998 ` 2207` ``` qed (use x in \simp; auto simp: not_less\) ``` lp15@67998 ` 2208` ``` ultimately have "f' x = ( *v) B" ``` lp15@67998 ` 2209` ``` by (force simp: algebra_simps) ``` lp15@67998 ` 2210` ``` show "matrix (f' x) \$ m \$ n \ b" ``` lp15@67998 ` 2211` ``` proof (rule tendsto_upperbound [of "\i. (A i \$ m \$ n)" _ sequentially]) ``` lp15@67998 ` 2212` ``` show "(\i. A i \$ m \$ n) \ matrix (f' x) \$ m \$ n" ``` lp15@67998 ` 2213` ``` by (simp add: B \f' x = ( *v) B\) ``` lp15@67998 ` 2214` ``` show "\\<^sub>F i in sequentially. A i \$ m \$ n \ b" ``` lp15@67998 ` 2215` ``` by (simp add: Ab less_eq_real_def) ``` lp15@67998 ` 2216` ``` qed auto ``` lp15@67998 ` 2217` ``` next ``` lp15@67998 ` 2218` ``` fix e :: "real" ``` lp15@67998 ` 2219` ``` assume "x \ S" and b: "matrix (f' x) \$ m \$ n \ b" and "e > 0" ``` lp15@67998 ` 2220` ``` then obtain d where "d>0" ``` lp15@67998 ` 2221` ``` and d: "\y. y\S \ 0 < dist y x \ dist y x < d \ norm (f y - f x - f' x (y - x)) / (norm (y - x)) ``` lp15@67998 ` 2222` ``` < e/2" ``` lp15@67998 ` 2223` ``` using f [OF \x \ S\] unfolding Deriv.has_derivative_at_within Lim_within ``` lp15@67998 ` 2224` ``` by (auto simp: field_simps dest: spec [of _ "e/2"]) ``` lp15@67998 ` 2225` ``` let ?A = "matrix(f' x) - (\ i j. if i = m \ j = n then e / 4 else 0)" ``` lp15@67998 ` 2226` ``` obtain B where BRats: "\i j. B\$i\$j \ \" and Bo_e6: "onorm(( *v) (?A - B)) < e/6" ``` lp15@67998 ` 2227` ``` using matrix_rational_approximation \e > 0\ ``` lp15@67998 ` 2228` ``` by (metis zero_less_divide_iff zero_less_numeral) ``` lp15@67998 ` 2229` ``` show "\d>0. \A. A \$ m \$ n < b \ (\i j. A \$ i \$ j \ \) \ ``` lp15@67998 ` 2230` ``` (\y\S. norm (y - x) < d \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x))" ``` lp15@67998 ` 2231` ``` proof (intro exI conjI ballI allI impI) ``` lp15@67998 ` 2232` ``` show "d>0" ``` lp15@67998 ` 2233` ``` by (rule \d>0\) ``` lp15@67998 ` 2234` ``` show "B \$ m \$ n < b" ``` lp15@67998 ` 2235` ``` proof - ``` lp15@67998 ` 2236` ``` have "\matrix (( *v) (?A - B)) \$ m \$ n\ \ onorm (( *v) (?A - B))" ``` lp15@67998 ` 2237` ``` using component_le_onorm [OF matrix_vector_mul_linear, of _ m n] by metis ``` lp15@67998 ` 2238` ``` then show ?thesis ``` lp15@67998 ` 2239` ``` using b Bo_e6 by simp ``` lp15@67998 ` 2240` ``` qed ``` lp15@67998 ` 2241` ``` show "B \$ i \$ j \ \" for i j ``` lp15@67998 ` 2242` ``` using BRats by auto ``` lp15@67998 ` 2243` ``` show "norm (f y - f x - B *v (y - x)) \ e * norm (y - x)" ``` lp15@67998 ` 2244` ``` if "y \ S" and y: "norm (y - x) < d" for y ``` lp15@67998 ` 2245` ``` proof (cases "y = x") ``` lp15@67998 ` 2246` ``` case True then show ?thesis ``` lp15@67998 ` 2247` ``` by simp ``` lp15@67998 ` 2248` ``` next ``` lp15@67998 ` 2249` ``` case False ``` lp15@67998 ` 2250` ``` have *: "norm(d' - d) \ e/2 \ norm(y - (x + d')) < e/2 \ norm(y - x - d) \ e" for d d' e and x y::"real^'n" ``` lp15@67998 ` 2251` ``` using norm_triangle_le [of "d' - d" "y - (x + d')"] by simp ``` lp15@67998 ` 2252` ``` show ?thesis ``` lp15@67998 ` 2253` ``` proof (rule *) ``` lp15@67998 ` 2254` ``` have split246: "\norm y \ e / 6; norm(x - y) \ e / 4\ \ norm x \ e/2" if "e > 0" for e and x y :: "real^'n" ``` lp15@67998 ` 2255` ``` using norm_triangle_le [of y "x-y" "e/2"] \e > 0\ by simp ``` lp15@67998 ` 2256` ``` have "linear (f' x)" ``` lp15@67998 ` 2257` ``` using True f has_derivative_linear by blast ``` lp15@67998 ` 2258` ``` then have "norm (f' x (y - x) - B *v (y - x)) = norm ((matrix (f' x) - B) *v (y - x))" ``` lp15@67998 ` 2259` ``` by (metis matrix_vector_mul matrix_vector_mult_diff_rdistrib) ``` lp15@67998 ` 2260` ``` also have "\ \ (e * norm (y - x)) / 2" ``` lp15@67998 ` 2261` ``` proof (rule split246) ``` lp15@67998 ` 2262` ``` have "norm ((?A - B) *v (y - x)) / norm (y - x) \ onorm(\x. (?A - B) *v x)" ``` lp15@67998 ` 2263` ``` by (simp add: le_onorm linear_linear matrix_vector_mul_linear) ``` lp15@67998 ` 2264` ``` also have "\ < e/6" ``` lp15@67998 ` 2265` ``` by (rule Bo_e6) ``` lp15@67998 ` 2266` ``` finally have "norm ((?A - B) *v (y - x)) / norm (y - x) < e / 6" . ``` lp15@67998 ` 2267` ``` then show "norm ((?A - B) *v (y - x)) \ e * norm (y - x) / 6" ``` lp15@67998 ` 2268` ``` by (simp add: divide_simps False) ``` lp15@67998 ` 2269` ``` have "norm ((matrix (f' x) - B) *v (y - x) - ((?A - B) *v (y - x))) = norm ((\ i j. if i = m \ j = n then e / 4 else 0) *v (y - x))" ``` lp15@67998 ` 2270` ``` by (simp add: algebra_simps) ``` lp15@67998 ` 2271` ``` also have "\ = norm((e/4) *\<^sub>R (y - x)\$n *\<^sub>R axis m (1::real))" ``` lp15@67998 ` 2272` ``` proof - ``` lp15@67998 ` 2273` ``` have "(\j\UNIV. (if i = m \ j = n then e / 4 else 0) * (y \$ j - x \$ j)) * 4 = e * (y \$ n - x \$ n) * axis m 1 \$ i" for i ``` lp15@67998 ` 2274` ``` proof (cases "i=m") ``` lp15@67998 ` 2275` ``` case True then show ?thesis ``` lp15@67998 ` 2276` ``` by (auto simp: if_distrib [of "\z. z * _"] cong: if_cong) ``` lp15@67998 ` 2277` ``` next ``` lp15@67998 ` 2278` ``` case False then show ?thesis ``` lp15@67998 ` 2279` ``` by (simp add: axis_def) ``` lp15@67998 ` 2280` ``` qed ``` lp15@67998 ` 2281` ``` then have "(\ i j. if i = m \ j = n then e / 4 else 0) *v (y - x) = (e/4) *\<^sub>R (y - x)\$n *\<^sub>R axis m (1::real)" ``` lp15@67998 ` 2282` ``` by (auto simp: vec_eq_iff matrix_vector_mult_def) ``` lp15@67998 ` 2283` ``` then show ?thesis ``` lp15@67998 ` 2284` ``` by metis ``` lp15@67998 ` 2285` ``` qed ``` lp15@67998 ` 2286` ``` also have "\ \ e * norm (y - x) / 4" ``` lp15@67998 ` 2287` ``` using \e > 0\ apply (simp add: norm_mult abs_mult) ``` lp15@67998 ` 2288` ``` by (metis component_le_norm_cart vector_minus_component) ``` lp15@67998 ` 2289` ``` finally show "norm ((matrix (f' x) - B) *v (y - x) - ((?A - B) *v (y - x))) \ e * norm (y - x) / 4" . ``` lp15@67998 ` 2290` ``` show "0 < e * norm (y - x)" ``` lp15@67998 ` 2291` ``` by (simp add: False \e > 0\) ``` lp15@67998 ` 2292` ``` qed ``` lp15@67998 ` 2293` ``` finally show "norm (f' x (y - x) - B *v (y - x)) \ (e * norm (y - x)) / 2" . ``` lp15@67998 ` 2294` ``` show "norm (f y - (f x + f' x (y - x))) < (e * norm (y - x)) / 2" ``` lp15@67998 ` 2295` ``` using False d [OF \y \ S\] y by (simp add: dist_norm field_simps) ``` lp15@67998 ` 2296` ``` qed ``` lp15@67998 ` 2297` ``` qed ``` lp15@67998 ` 2298` ``` qed ``` lp15@67998 ` 2299` ``` qed ``` lp15@67998 ` 2300` ``` qed auto ``` lp15@67998 ` 2301` ``` qed ``` lp15@67998 ` 2302` ``` show "negligible ?M" ``` lp15@67998 ` 2303` ``` using negligible_subset [OF nN MN] . ``` lp15@67998 ` 2304` ``` qed ``` lp15@67998 ` 2305` ``` then show ?thesis ``` lp15@67998 ` 2306` ``` by (simp add: borel_measurable_vimage_halfspace_component_le sets_restrict_space_iff assms) ``` lp15@67998 ` 2307` ```qed ``` lp15@67998 ` 2308` lp15@67998 ` 2309` lp15@67998 ` 2310` ```theorem borel_measurable_det_Jacobian: ``` lp15@67998 ` 2311` ``` fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" ``` lp15@67998 ` 2312` ``` assumes S: "S \ sets lebesgue" and f: "\x. x \ S \ (f has_derivative f' x) (at x within S)" ``` lp15@67998 ` 2313` ``` shows "(\x. det(matrix(f' x))) \ borel_measurable (lebesgue_on S)" ``` lp15@67998 ` 2314` ``` unfolding det_def ``` lp15@67998 ` 2315` ``` by (intro measurable) (auto intro: f borel_measurable_partial_derivatives [OF S]) ``` lp15@67998 ` 2316` lp15@67998 ` 2317` ```text\The localisation wrt S uses the same argument for many similar results. ``` lp15@67998 ` 2318` ```See HOL Light's MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_BOREL, etc.\ ``` lp15@67998 ` 2319` ```lemma borel_measurable_lebesgue_on_preimage_borel: ``` lp15@67998 ` 2320` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@67998 ` 2321` ``` assumes "S \ sets lebesgue" ``` lp15@67998 ` 2322` ``` shows "f \ borel_measurable (lebesgue_on S) \ ``` lp15@67998 ` 2323` ``` (\T. T \ sets borel \ {x \ S. f x \ T} \ sets lebesgue)" ``` lp15@67998 ` 2324` ```proof - ``` lp15@67998 ` 2325` ``` have "{x. (if x \ S then f x else 0) \ T} \ sets lebesgue \ {x \ S. f x \ T} \ sets lebesgue" ``` lp15@67998 ` 2326` ``` if "T \ sets borel" for T ``` lp15@67998 ` 2327` ``` proof (cases "0 \ T") ``` lp15@67998 ` 2328` ``` case True ``` lp15@67998 ` 2329` ``` then have "{x \ S. f x \ T} = {x. (if x \ S then f x else 0) \ T} \ S" ``` lp15@67998 ` 2330` ``` "{x. (if x \ S then f x else 0) \ T} = {x \ S. f x \ T} \ -S" ``` lp15@67998 ` 2331` ``` by auto ``` lp15@67998 ` 2332` ``` then show ?thesis ``` lp15@67998 ` 2333` ``` by (metis (no_types, lifting) Compl_in_sets_lebesgue assms sets.Int sets.Un) ``` lp15@67998 ` 2334` ``` next ``` lp15@67998 ` 2335` ``` case False ``` lp15@67998 ` 2336` ``` then have "{x. (if x \ S then f x else 0) \ T} = {x \ S. f x \ T}" ``` lp15@67998 ` 2337` ``` by auto ``` lp15@67998 ` 2338` ``` then show ?thesis ``` lp15@67998 ` 2339` ``` by auto ``` lp15@67998 ` 2340` ``` qed ``` lp15@67998 ` 2341` ``` then show ?thesis ``` lp15@67998 ` 2342` ``` unfolding borel_measurable_lebesgue_preimage_borel borel_measurable_UNIV [OF assms, symmetric] ``` lp15@67998 ` 2343` ``` by blast ``` lp15@67998 ` 2344` ```qed ``` lp15@67998 ` 2345` lp15@67998 ` 2346` ```lemma sets_lebesgue_almost_borel: ``` lp15@67998 ` 2347` ``` assumes "S \ sets lebesgue" ``` lp15@67998 ` 2348` ``` obtains B N where "B \ sets borel" "negligible N" "B \ N = S" ``` lp15@67998 ` 2349` ```proof - ``` lp15@67998 ` 2350` ``` obtain T N N' where "S = T \ N" "N \ N'" "N' \ null_sets lborel" "T \ sets borel" ``` lp15@67998 ` 2351` ``` using sets_completionE [OF assms] by auto ``` lp15@67998 ` 2352` ``` then show thesis ``` lp15@67998 ` 2353` ``` by (metis negligible_iff_null_sets negligible_subset null_sets_completionI that) ``` lp15@67998 ` 2354` ```qed ``` lp15@67998 ` 2355` lp15@67998 ` 2356` ```lemma double_lebesgue_sets: ``` lp15@67998 ` 2357` ``` assumes S: "S \ sets lebesgue" and T: "T \ sets lebesgue" and fim: "f ` S \ T" ``` lp15@67998 ` 2358` ``` shows "(\U. U \ sets lebesgue \ U \ T \ {x \ S. f x \ U} \ sets lebesgue) \ ``` lp15@67998 ` 2359` ``` f \ borel_measurable (lebesgue_on S) \ ``` lp15@67998 ` 2360` ``` (\U. negligible U \ U \ T \ {x \ S. f x \ U} \ sets lebesgue)" ``` lp15@67998 ` 2361` ``` (is "?lhs \ _ \ ?rhs") ``` lp15@67998 ` 2362` ``` unfolding borel_measurable_lebesgue_on_preimage_borel [OF S] ``` lp15@67998 ` 2363` ```proof (intro iffI allI conjI impI, safe) ``` lp15@67998 ` 2364` ``` fix V :: "'b set" ``` lp15@67998 ` 2365` ``` assume *: "\U. U \ sets lebesgue \ U \ T \ {x \ S. f x \ U} \ sets lebesgue" ``` lp15@67998 ` 2366` ``` and "V \ sets borel" ``` lp15@67998 ` 2367` ``` then have V: "V \ sets lebesgue" ``` lp15@67998 ` 2368` ``` by simp ``` lp15@67998 ` 2369` ``` have "{x \ S. f x \ V} = {x \ S. f x \ T \ V}" ``` lp15@67998 ` 2370` ``` using fim by blast ``` lp15@67998 ` 2371` ``` also have "{x \ S. f x \ T \ V} \ sets lebesgue" ``` lp15@67998 ` 2372` ``` using T V * le_inf_iff by blast ``` lp15@67998 ` 2373` ``` finally show "{x \ S. f x \ V} \ sets lebesgue" . ``` lp15@67998 ` 2374` ```next ``` lp15@67998 ` 2375` ``` fix U :: "'b set" ``` lp15@67998 ` 2376` ``` assume "\U. U \ sets lebesgue \ U \ T \ {x \ S. f x \ U} \ sets lebesgue" ``` lp15@67998 ` 2377` ``` "negligible U" "U \ T" ``` lp15@67998 ` 2378` ``` then show "{x \ S. f x \ U} \ sets lebesgue" ``` lp15@67998 ` 2379` ``` using negligible_imp_sets by blast ``` lp15@67998 ` 2380` ```next ``` lp15@67998 ` 2381` ``` fix U :: "'b set" ``` lp15@67998 ` 2382` ``` assume 1 [rule_format]: "(\T. T \ sets borel \ {x \ S. f x \ T} \ sets lebesgue)" ``` lp15@67998 ` 2383` ``` and 2 [rule_format]: "\U. negligible U \ U \ T \ {x \ S. f x \ U} \ sets lebesgue" ``` lp15@67998 ` 2384` ``` and "U \ sets lebesgue" "U \ T" ``` lp15@67998 ` 2385` ``` then obtain C N where C: "C \ sets borel \ negligible N \ C \ N = U" ``` lp15@67998 ` 2386` ``` using sets_lebesgue_almost_borel ``` lp15@67998 ` 2387` ``` by metis ``` lp15@67998 ` 2388` ``` then have "{x \ S. f x \ C} \ sets lebesgue" ``` lp15@67998 ` 2389` ``` by (blast intro: 1) ``` lp15@67998 ` 2390` ``` moreover have "{x \ S. f x \ N} \ sets lebesgue" ``` lp15@67998 ` 2391` ``` using C \U \ T\ by (blast intro: 2) ``` lp15@67998 ` 2392` ``` moreover have "{x \ S. f x \ C \ N} = {x \ S. f x \ C} \ {x \ S. f x \ N}" ``` lp15@67998 ` 2393` ``` by auto ``` lp15@67998 ` 2394` ``` ultimately show "{x \ S. f x \ U} \ sets lebesgue" ``` lp15@67998 ` 2395` ``` using C by auto ``` lp15@67998 ` 2396` ```qed ``` lp15@67998 ` 2397` lp15@67998 ` 2398` lp15@67998 ` 2399` lp15@67998 ` 2400` ```thm integrable_on_subcbox ``` lp15@67998 ` 2401` lp15@67998 ` 2402` ```proposition measurable_bounded_by_integrable_imp_integrable: ``` lp15@67998 ` 2403` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@67998 ` 2404` ``` assumes f: "f \ borel_measurable (lebesgue_on S)" and g: "g integrable_on S" ``` lp15@67998 ` 2405` ``` and normf: "\x. x \ S \ norm(f x) \ g x" and S: "S \ sets lebesgue" ``` lp15@67998 ` 2406` ``` shows "f integrable_on S" ``` lp15@67998 ` 2407` ```proof (rule integrable_on_all_intervals_integrable_bound [OF _ normf g]) ``` lp15@67998 ` 2408` ``` show "(\x. if x \ S then f x else 0) integrable_on cbox a b" for a b ``` lp15@67998 ` 2409` ``` proof (rule measurable_bounded_lemma) ``` lp15@67998 ` 2410` ``` show "(\x. if x \ S then f x else 0) \ borel_measurable lebesgue" ``` lp15@67998 ` 2411` ``` by (simp add: S borel_measurable_UNIV f) ``` lp15@67998 ` 2412` ``` show "(\x. if x \ S then g x else 0) integrable_on cbox a b" ``` lp15@67998 ` 2413` ``` by (simp add: g integrable_altD(1)) ``` lp15@67998 ` 2414` ``` show "norm (if x \ S then f x else 0) \ (if x \ S then g x else 0)" for x ``` lp15@67998 ` 2415` ``` using normf by simp ``` lp15@67998 ` 2416` ``` qed ``` lp15@67998 ` 2417` ```qed ``` lp15@67998 ` 2418` lp15@67998 ` 2419` lp15@67998 ` 2420` ```subsection\Simplest case of Sard's theorem (we don't need continuity of derivative)\ ``` lp15@67998 ` 2421` lp15@67998 ` 2422` ```lemma Sard_lemma00: ``` lp15@67998 ` 2423` ``` fixes P :: "'b::euclidean_space set" ``` lp15@67998 ` 2424` ``` assumes "a \ 0" and a: "a *\<^sub>R i \ 0" and i: "i \ Basis" ``` lp15@67998 ` 2425` ``` and P: "P \ {x. a *\<^sub>R i \ x = 0}" ``` lp15@67998 ` 2426` ``` and "0 \ m" "0 \ e" ``` lp15@67998 ` 2427` ``` obtains S where "S \ lmeasurable" ``` lp15@67998 ` 2428` ``` and "{z. norm z \ m \ (\t \ P. norm(z - t) \ e)} \ S" ``` lp15@67998 ` 2429` ``` and "measure lebesgue S \ (2 * e) * (2 * m) ^ (DIM('b) - 1)" ``` lp15@67998 ` 2430` ```proof - ``` lp15@67998 ` 2431` ``` have "a > 0" ``` lp15@67998 ` 2432` ``` using assms by simp ``` lp15@67998 ` 2433` ``` let ?v = "(\j\Basis. (if j = i then e else m) *\<^sub>R j)" ``` lp15@67998 ` 2434` ``` show thesis ``` lp15@67998 ` 2435` ``` proof ``` lp15@67998 ` 2436` ``` have "- e \ x \ i" "x \ i \ e" ``` lp15@67998 ` 2437` ``` if "t \ P" "norm (x - t) \ e" for x t ``` lp15@67998 ` 2438` ``` using \a > 0\ that Basis_le_norm [of i "x-t"] P i ``` lp15@67998 ` 2439` ``` by (auto simp: inner_commute algebra_simps) ``` lp15@67998 ` 2440` ``` moreover have "- m \ x \ j" "x \ j \ m" ``` lp15@67998 ` 2441` ``` if "norm x \ m" "t \ P" "norm (x - t) \ e" "j \ Basis" and "j \ i" ``` lp15@67998 ` 2442` ``` for x t j ``` lp15@67998 ` 2443` ``` using that Basis_le_norm [of j x] by auto ``` lp15@67998 ` 2444` ``` ultimately ``` lp15@67998 ` 2445` ``` show "{z. norm z \ m \ (\t\P. norm (z - t) \ e)} \ cbox (-?v) ?v" ```