diff -r 749aaeb40788 -r be6634e99e09 src/HOL/Analysis/Change_Of_Vars.thy --- a/src/HOL/Analysis/Change_Of_Vars.thy Fri Dec 14 14:33:26 2018 +0100 +++ b/src/HOL/Analysis/Change_Of_Vars.thy Tue Jan 22 21:13:23 2019 +0000 @@ -9,9 +9,9 @@ begin -subsection%unimportant \Orthogonal Transformation of Balls\ +subsection \Orthogonal Transformation of Balls\ -lemma%unimportant image_orthogonal_transformation_ball: +lemma image_orthogonal_transformation_ball: fixes f :: "'a::euclidean_space \ 'a" assumes "orthogonal_transformation f" shows "f ` ball x r = ball (f x) r" @@ -27,7 +27,7 @@ by (auto simp: orthogonal_transformation_isometry) qed -lemma%unimportant image_orthogonal_transformation_cball: +lemma image_orthogonal_transformation_cball: fixes f :: "'a::euclidean_space \ 'a" assumes "orthogonal_transformation f" shows "f ` cball x r = cball (f x) r" @@ -46,14 +46,14 @@ subsection \Measurable Shear and Stretch\ -proposition%important +proposition fixes a :: "real^'n" assumes "m \ n" and ab_ne: "cbox a b \ {}" and an: "0 \ a$n" shows measurable_shear_interval: "(\x. \ i. if i = m then x$m + x$n else x$i) ` (cbox a b) \ lmeasurable" (is "?f ` _ \ _") and measure_shear_interval: "measure lebesgue ((\x. \ i. if i = m then x$m + x$n else x$i) ` cbox a b) = measure lebesgue (cbox a b)" (is "?Q") -proof%unimportant - +proof - have lin: "linear ?f" by (rule linearI) (auto simp: plus_vec_def scaleR_vec_def algebra_simps) show fab: "?f ` cbox a b \ lmeasurable" @@ -155,13 +155,13 @@ qed -proposition%important +proposition fixes S :: "(real^'n) set" assumes "S \ lmeasurable" shows measurable_stretch: "((\x. \ k. m k * x$k) ` S) \ lmeasurable" (is "?f ` S \ _") and measure_stretch: "measure lebesgue ((\x. \ k. m k * x$k) ` S) = \prod m UNIV\ * measure lebesgue S" (is "?MEQ") -proof%unimportant - +proof - have "(?f ` S) \ lmeasurable \ ?MEQ" proof (cases "\k. m k \ 0") case True @@ -259,12 +259,12 @@ qed -proposition%important +proposition fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes "linear f" "S \ lmeasurable" shows measurable_linear_image: "(f ` S) \ lmeasurable" and measure_linear_image: "measure lebesgue (f ` S) = \det (matrix f)\ * measure lebesgue S" (is "?Q f S") -proof%unimportant - +proof - have "\S \ lmeasurable. (f ` S) \ lmeasurable \ ?Q f S" proof (rule induct_linear_elementary [OF \linear f\]; intro ballI) fix f g and S :: "(real,'n) vec set" @@ -407,7 +407,7 @@ qed -lemma%unimportant +lemma fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes f: "orthogonal_transformation f" and S: "S \ lmeasurable" shows measurable_orthogonal_image: "f ` S \ lmeasurable" @@ -430,10 +430,10 @@ inductive%important gdelta :: "'a::topological_space set \ bool" where "(\n::nat. open (F n)) \ gdelta (\(F ` UNIV))" -lemma%important fsigma_Union_compact: +lemma fsigma_Union_compact: fixes S :: "'a::{real_normed_vector,heine_borel} set" shows "fsigma S \ (\F::nat \ 'a set. range F \ Collect compact \ S = \(F ` UNIV))" -proof%unimportant safe +proof safe assume "fsigma S" then obtain F :: "nat \ 'a set" where F: "range F \ Collect closed" "S = \(F ` UNIV)" by (meson fsigma.cases image_subsetI mem_Collect_eq) @@ -464,7 +464,7 @@ by (simp add: compact_imp_closed fsigma.intros image_subset_iff) qed -lemma%unimportant gdelta_imp_fsigma: "gdelta S \ fsigma (- S)" +lemma gdelta_imp_fsigma: "gdelta S \ fsigma (- S)" proof (induction rule: gdelta.induct) case (1 F) have "- \(F ` UNIV) = (\i. -(F i))" @@ -473,7 +473,7 @@ by (simp add: fsigma.intros closed_Compl 1) qed -lemma%unimportant fsigma_imp_gdelta: "fsigma S \ gdelta (- S)" +lemma fsigma_imp_gdelta: "fsigma S \ gdelta (- S)" proof (induction rule: fsigma.induct) case (1 F) have "- \(F ` UNIV) = (\i. -(F i))" @@ -482,11 +482,11 @@ by (simp add: 1 gdelta.intros open_closed) qed -lemma%unimportant gdelta_complement: "gdelta(- S) \ fsigma S" +lemma gdelta_complement: "gdelta(- S) \ fsigma S" using fsigma_imp_gdelta gdelta_imp_fsigma by force text\A Lebesgue set is almost an \F_sigma\ or \G_delta\.\ -lemma%unimportant lebesgue_set_almost_fsigma: +lemma lebesgue_set_almost_fsigma: assumes "S \ sets lebesgue" obtains C T where "fsigma C" "negligible T" "C \ T = S" "disjnt C T" proof - @@ -521,7 +521,7 @@ qed qed -lemma%unimportant lebesgue_set_almost_gdelta: +lemma lebesgue_set_almost_gdelta: assumes "S \ sets lebesgue" obtains C T where "gdelta C" "negligible T" "S \ T = C" "disjnt S T" proof - @@ -539,12 +539,12 @@ qed -proposition%important measure_semicontinuous_with_hausdist_explicit: +proposition measure_semicontinuous_with_hausdist_explicit: assumes "bounded S" and neg: "negligible(frontier S)" and "e > 0" obtains d where "d > 0" "\T. \T \ lmeasurable; \y. y \ T \ \x. x \ S \ dist x y < d\ \ measure lebesgue T < measure lebesgue S + e" -proof%unimportant (cases "S = {}") +proof (cases "S = {}") case True with that \e > 0\ show ?thesis by force next @@ -608,10 +608,10 @@ qed qed -proposition%important lebesgue_regular_inner: +proposition lebesgue_regular_inner: assumes "S \ sets lebesgue" obtains K C where "negligible K" "\n::nat. compact(C n)" "S = (\n. C n) \ K" -proof%unimportant - +proof - have "\T. closed T \ T \ S \ (S - T) \ lmeasurable \ measure lebesgue (S - T) < (1/2)^n" for n using sets_lebesgue_inner_closed assms by (metis sets_lebesgue_inner_closed zero_less_divide_1_iff zero_less_numeral zero_less_power) @@ -661,7 +661,7 @@ qed -lemma%unimportant sets_lebesgue_continuous_image: +lemma sets_lebesgue_continuous_image: assumes T: "T \ sets lebesgue" and contf: "continuous_on S f" and negim: "\T. \negligible T; T \ S\ \ negligible(f ` T)" and "T \ S" shows "f ` T \ sets lebesgue" @@ -686,7 +686,7 @@ by (simp add: Teq image_Un image_Union) qed -lemma%unimportant differentiable_image_in_sets_lebesgue: +lemma differentiable_image_in_sets_lebesgue: fixes f :: "'m::euclidean_space \ 'n::euclidean_space" assumes S: "S \ sets lebesgue" and dim: "DIM('m) \ DIM('n)" and f: "f differentiable_on S" shows "f`S \ sets lebesgue" @@ -698,7 +698,7 @@ by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim]) qed auto -lemma%unimportant sets_lebesgue_on_continuous_image: +lemma sets_lebesgue_on_continuous_image: assumes S: "S \ sets lebesgue" and X: "X \ sets (lebesgue_on S)" and contf: "continuous_on S f" and negim: "\T. \negligible T; T \ S\ \ negligible(f ` T)" shows "f ` X \ sets (lebesgue_on (f ` S))" @@ -713,7 +713,7 @@ by (auto simp: sets_restrict_space_iff) qed -lemma%unimportant differentiable_image_in_sets_lebesgue_on: +lemma differentiable_image_in_sets_lebesgue_on: fixes f :: "'m::euclidean_space \ 'n::euclidean_space" assumes S: "S \ sets lebesgue" and X: "X \ sets (lebesgue_on S)" and dim: "DIM('m) \ DIM('n)" and f: "f differentiable_on S" @@ -727,7 +727,7 @@ qed -proposition%important +proposition fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes S: "S \ lmeasurable" and deriv: "\x. x \ S \ (f has_derivative f' x) (at x within S)" @@ -737,7 +737,7 @@ "f ` S \ lmeasurable" and measure_bounded_differentiable_image: "measure lebesgue (f ` S) \ B * measure lebesgue S" (is "?M") -proof%unimportant - +proof - have "f ` S \ lmeasurable \ measure lebesgue (f ` S) \ B * measure lebesgue S" proof (cases "B < 0") case True @@ -963,13 +963,13 @@ then show "f ` S \ lmeasurable" ?M by blast+ qed -lemma%important +lemma (*FIXME needs name? *) fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes S: "S \ lmeasurable" and deriv: "\x. x \ S \ (f has_derivative f' x) (at x within S)" and int: "(\x. \det (matrix (f' x))\) integrable_on S" shows m_diff_image_weak: "f ` S \ lmeasurable \ measure lebesgue (f ` S) \ integral S (\x. \det (matrix (f' x))\)" -proof%unimportant - +proof - let ?\ = "measure lebesgue" have aint_S: "(\x. \det (matrix (f' x))\) absolutely_integrable_on S" using int unfolding absolutely_integrable_on_def by auto @@ -1161,7 +1161,7 @@ qed -theorem%important +theorem(* FIXME needs name? *) fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes S: "S \ sets lebesgue" and deriv: "\x. x \ S \ (f has_derivative f' x) (at x within S)" @@ -1169,7 +1169,7 @@ shows measurable_differentiable_image: "f ` S \ lmeasurable" and measure_differentiable_image: "measure lebesgue (f ` S) \ integral S (\x. \det (matrix (f' x))\)" (is "?M") -proof%unimportant - +proof - let ?I = "\n::nat. cbox (vec (-n)) (vec n) \ S" let ?\ = "measure lebesgue" have "x \ cbox (vec (- real (nat \norm x\))) (vec (real (nat \norm x\)))" for x :: "real^'n::_" @@ -1214,7 +1214,7 @@ qed -lemma%unimportant borel_measurable_simple_function_limit_increasing: +lemma borel_measurable_simple_function_limit_increasing: fixes f :: "'a::euclidean_space \ real" shows "(f \ borel_measurable lebesgue \ (\x. 0 \ f x)) \ (\g. (\n x. 0 \ g n x \ g n x \ f x) \ (\n x. g n x \ (g(Suc n) x)) \ @@ -1413,7 +1413,7 @@ subsection\Borel measurable Jacobian determinant\ -lemma%unimportant lemma_partial_derivatives0: +lemma lemma_partial_derivatives0: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "linear f" and lim0: "((\x. f x /\<^sub>R norm x) \ 0) (at 0 within S)" and lb: "\v. v \ 0 \ (\k>0. \e>0. \x. x \ S - {0} \ norm x < e \ k * norm x \ \v \ x\)" @@ -1486,7 +1486,7 @@ mem_Collect_eq module_hom_zero span_base span_raw_def) qed -lemma%unimportant lemma_partial_derivatives: +lemma lemma_partial_derivatives: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "linear f" and lim: "((\x. f (x - a) /\<^sub>R norm (x - a)) \ 0) (at a within S)" and lb: "\v. v \ 0 \ (\k>0. \e>0. \x \ S - {a}. norm(a - x) < e \ k * norm(a - x) \ \v \ (x - a)\)" @@ -1504,12 +1504,12 @@ qed -proposition%important borel_measurable_partial_derivatives: +proposition borel_measurable_partial_derivatives: fixes f :: "real^'m::{finite,wellorder} \ real^'n" assumes S: "S \ sets lebesgue" and f: "\x. x \ S \ (f has_derivative f' x) (at x within S)" shows "(\x. (matrix(f' x)$m$n)) \ borel_measurable (lebesgue_on S)" -proof%unimportant - +proof - have contf: "continuous_on S f" using continuous_on_eq_continuous_within f has_derivative_continuous by blast have "{x \ S. (matrix (f' x)$m$n) \ b} \ sets lebesgue" for b @@ -2095,7 +2095,7 @@ qed -theorem%important borel_measurable_det_Jacobian: +theorem borel_measurable_det_Jacobian: fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes S: "S \ sets lebesgue" and f: "\x. x \ S \ (f has_derivative f' x) (at x within S)" shows "(\x. det(matrix(f' x))) \ borel_measurable (lebesgue_on S)" @@ -2104,12 +2104,12 @@ text\The localisation wrt S uses the same argument for many similar results.\ (*See HOL Light's MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_BOREL, etc.*) -lemma%important borel_measurable_lebesgue_on_preimage_borel: +theorem borel_measurable_lebesgue_on_preimage_borel: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "S \ sets lebesgue" shows "f \ borel_measurable (lebesgue_on S) \ (\T. T \ sets borel \ {x \ S. f x \ T} \ sets lebesgue)" -proof%unimportant - +proof - have "{x. (if x \ S then f x else 0) \ T} \ sets lebesgue \ {x \ S. f x \ T} \ sets lebesgue" if "T \ sets borel" for T proof (cases "0 \ T") @@ -2131,7 +2131,7 @@ by blast qed -lemma%unimportant sets_lebesgue_almost_borel: +lemma sets_lebesgue_almost_borel: assumes "S \ sets lebesgue" obtains B N where "B \ sets borel" "negligible N" "B \ N = S" proof - @@ -2141,7 +2141,7 @@ by (metis negligible_iff_null_sets negligible_subset null_sets_completionI that) qed -lemma%unimportant double_lebesgue_sets: +lemma double_lebesgue_sets: assumes S: "S \ sets lebesgue" and T: "T \ sets lebesgue" and fim: "f ` S \ T" shows "(\U. U \ sets lebesgue \ U \ T \ {x \ S. f x \ U} \ sets lebesgue) \ f \ borel_measurable (lebesgue_on S) \ @@ -2186,7 +2186,7 @@ subsection\Simplest case of Sard's theorem (we don't need continuity of derivative)\ -lemma%important Sard_lemma00: +lemma Sard_lemma00: fixes P :: "'b::euclidean_space set" assumes "a \ 0" and a: "a *\<^sub>R i \ 0" and i: "i \ Basis" and P: "P \ {x. a *\<^sub>R i \ x = 0}" @@ -2194,7 +2194,7 @@ obtains S where "S \ lmeasurable" and "{z. norm z \ m \ (\t \ P. norm(z - t) \ e)} \ S" and "measure lebesgue S \ (2 * e) * (2 * m) ^ (DIM('b) - 1)" -proof%unimportant - +proof - have "a > 0" using assms by simp let ?v = "(\j\Basis. (if j = i then e else m) *\<^sub>R j)" @@ -2222,7 +2222,7 @@ qed text\As above, but reorienting the vector (HOL Light's @text{GEOM\_BASIS\_MULTIPLE\_TAC})\ -lemma%unimportant Sard_lemma0: +lemma Sard_lemma0: fixes P :: "(real^'n::{finite,wellorder}) set" assumes "a \ 0" and P: "P \ {x. a \ x = 0}" and "0 \ m" "0 \ e" @@ -2282,13 +2282,13 @@ qed text\As above, but translating the sets (HOL Light's @text{GEN\_GEOM\_ORIGIN\_TAC})\ -lemma%important Sard_lemma1: +lemma Sard_lemma1: fixes P :: "(real^'n::{finite,wellorder}) set" assumes P: "dim P < CARD('n)" and "0 \ m" "0 \ e" obtains S where "S \ lmeasurable" and "{z. norm(z - w) \ m \ (\t \ P. norm(z - w - t) \ e)} \ S" and "measure lebesgue S \ (2 * e) * (2 * m) ^ (CARD('n) - 1)" -proof%unimportant - +proof - obtain a where "a \ 0" "P \ {x. a \ x = 0}" using lowdim_subset_hyperplane [of P] P span_base by auto then obtain S where S: "S \ lmeasurable" @@ -2306,7 +2306,7 @@ qed qed -lemma%important Sard_lemma2: +lemma Sard_lemma2: fixes f :: "real^'m::{finite,wellorder} \ real^'n::{finite,wellorder}" assumes mlen: "CARD('m) \ CARD('n)" (is "?m \ ?n") and "B > 0" "bounded S" @@ -2314,7 +2314,7 @@ and rank: "\x. x \ S \ rank(matrix(f' x)) < CARD('n)" and B: "\x. x \ S \ onorm(f' x) \ B" shows "negligible(f ` S)" -proof%unimportant - +proof - have lin_f': "\x. x \ S \ linear(f' x)" using derS has_derivative_linear by blast show ?thesis @@ -2521,13 +2521,13 @@ qed -theorem%important baby_Sard: +theorem baby_Sard: fixes f :: "real^'m::{finite,wellorder} \ real^'n::{finite,wellorder}" assumes mlen: "CARD('m) \ CARD('n)" and der: "\x. x \ S \ (f has_derivative f' x) (at x within S)" and rank: "\x. x \ S \ rank(matrix(f' x)) < CARD('n)" shows "negligible(f ` S)" -proof%unimportant - +proof - let ?U = "\n. {x \ S. norm(x) \ n \ onorm(f' x) \ real n}" have "\x. x \ S \ \n. norm x \ real n \ onorm (f' x) \ real n" by (meson linear order_trans real_arch_simple) @@ -2549,7 +2549,7 @@ subsection\A one-way version of change-of-variables not assuming injectivity. \ -lemma%important integral_on_image_ubound_weak: +lemma integral_on_image_ubound_weak: fixes f :: "real^'n::{finite,wellorder} \ real" assumes S: "S \ sets lebesgue" and f: "f \ borel_measurable (lebesgue_on (g ` S))" @@ -2560,7 +2560,7 @@ shows "f integrable_on (g ` S) \ integral (g ` S) f \ integral S (\x. \det (matrix (g' x))\ * f(g x))" (is "_ \ _ \ ?b") -proof%unimportant - +proof - let ?D = "\x. \det (matrix (g' x))\" have cont_g: "continuous_on S g" using der_g has_derivative_continuous_on by blast @@ -2738,14 +2738,14 @@ qed -lemma%important integral_on_image_ubound_nonneg: +lemma integral_on_image_ubound_nonneg: fixes f :: "real^'n::{finite,wellorder} \ real" assumes nonneg_fg: "\x. x \ S \ 0 \ f(g x)" and der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" and intS: "(\x. \det (matrix (g' x))\ * f(g x)) integrable_on S" shows "f integrable_on (g ` S) \ integral (g ` S) f \ integral S (\x. \det (matrix (g' x))\ * f(g x))" (is "_ \ _ \ ?b") -proof%unimportant - +proof - let ?D = "\x. det (matrix (g' x))" define S' where "S' \ {x \ S. ?D x * f(g x) \ 0}" then have der_gS': "\x. x \ S' \ (g has_derivative g' x) (at x within S')" @@ -2868,7 +2868,7 @@ qed -lemma%unimportant absolutely_integrable_on_image_real: +lemma absolutely_integrable_on_image_real: fixes f :: "real^'n::{finite,wellorder} \ real" and g :: "real^'n::_ \ real^'n::_" assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" and intS: "(\x. \det (matrix (g' x))\ * f(g x)) absolutely_integrable_on S" @@ -2943,7 +2943,7 @@ qed -proposition%important absolutely_integrable_on_image: +proposition absolutely_integrable_on_image: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes der_g: "\x. x \ S \