# HG changeset patch # User immler # Date 1547760141 18000 # Node ID 96a43caa49027cabf27f30ed1dcd133d72a70a02 # Parent a8faf6f15da7a6cff61c47595bbe4c0a9f0cf9b1 revert to 56acd449da41 diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Cross3.thy --- a/src/HOL/Analysis/Cross3.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Cross3.thy Thu Jan 17 16:22:21 2019 -0500 @@ -79,14 +79,14 @@ hide_fact (open) left_diff_distrib right_diff_distrib -proposition Jacobi: "x \ (y \ z) + y \ (z \ x) + z \ (x \ y) = 0" for x::"real^3" +lemma%important Jacobi: "x \ (y \ z) + y \ (z \ x) + z \ (x \ y) = 0" for x::"real^3" by%unimportant (simp add: cross3_simps) -proposition Lagrange: "x \ (y \ z) = (x \ z) *\<^sub>R y - (x \ y) *\<^sub>R z" +lemma%important Lagrange: "x \ (y \ z) = (x \ z) *\<^sub>R y - (x \ y) *\<^sub>R z" by%unimportant (simp add: cross3_simps) (metis (full_types) exhaust_3) -proposition cross_triple: "(x \ y) \ z = (y \ z) \ x" - by%unimportant (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps) +lemma cross_triple: "(x \ y) \ z = (y \ z) \ x" + by (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps) lemma cross_components: "(x \ y)$1 = x$2 * y$3 - y$2 * x$3" "(x \ y)$2 = x$3 * y$1 - y$3 * x$1" "(x \ y)$3 = x$1 * y$2 - y$1 * x$2" @@ -126,15 +126,15 @@ lemma cross_cross_det: "(w \ x) \ (y \ z) = det(vector[w,x,z]) *\<^sub>R y - det(vector[w,x,y]) *\<^sub>R z" using exhaust_3 by (force simp add: cross3_simps) -proposition dot_cross: "(w \ x) \ (y \ z) = (w \ y) * (x \ z) - (w \ z) * (x \ y)" +lemma%important dot_cross: "(w \ x) \ (y \ z) = (w \ y) * (x \ z) - (w \ z) * (x \ y)" by%unimportant (force simp add: cross3_simps) -proposition norm_cross: "(norm (x \ y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \ y)\<^sup>2" +lemma norm_cross: "(norm (x \ y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \ y)\<^sup>2" unfolding power2_norm_eq_inner power_mult_distrib by (simp add: cross3_simps power2_eq_square) -lemma cross_eq_0: "x \ y = 0 \ collinear{0,x,y}" -proof - +lemma%important cross_eq_0: "x \ y = 0 \ collinear{0,x,y}" +proof%unimportant - have "x \ y = 0 \ norm (x \ y) = 0" by simp also have "... \ (norm x * norm y)\<^sup>2 = (x \ y)\<^sup>2" @@ -175,10 +175,10 @@ apply (simp add: vector_matrix_mult_def matrix_vector_mult_def forall_3 cross3_simps) done -lemma cross_orthogonal_matrix: +lemma%important cross_orthogonal_matrix: assumes "orthogonal_matrix A" shows "(A *v x) \ (A *v y) = det A *\<^sub>R (A *v (x \ y))" -proof - +proof%unimportant - have "mat 1 = transpose (A ** transpose A)" by (metis (no_types) assms orthogonal_matrix_def transpose_mat) then show ?thesis @@ -191,10 +191,10 @@ lemma cross_rotoinversion_matrix: "rotoinversion_matrix A \ (A *v x) \ (A *v y) = - A *v (x \ y)" by (simp add: rotoinversion_matrix_def cross_orthogonal_matrix scaleR_matrix_vector_assoc) -lemma cross_orthogonal_transformation: +lemma%important cross_orthogonal_transformation: assumes "orthogonal_transformation f" shows "(f x) \ (f y) = det(matrix f) *\<^sub>R f(x \ y)" -proof - +proof%unimportant - have orth: "orthogonal_matrix (matrix f)" using assms orthogonal_transformation_matrix by blast have "matrix f *v z = f z" for z @@ -208,7 +208,7 @@ \ (f x) \ (f y) = f(x \ y)" by (simp add: cross_orthogonal_transformation orthogonal_transformation) -subsection%important \Continuity\ +subsection%unimportant \Continuity\ lemma continuous_cross: "\continuous F f; continuous F g\ \ continuous F (\x. (f x) \ (g x))" apply (subst continuous_componentwise) diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Determinants.thy --- a/src/HOL/Analysis/Determinants.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Determinants.thy Thu Jan 17 16:22:21 2019 -0500 @@ -6,7 +6,7 @@ theory Determinants imports - Cartesian_Euclidean_Space + Cartesian_Space "HOL-Library.Permutations" begin @@ -976,6 +976,36 @@ by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq) qed +lemma%important det_orthogonal_matrix: + fixes Q:: "'a::linordered_idom^'n^'n" + assumes oQ: "orthogonal_matrix Q" + shows "det Q = 1 \ det Q = - 1" +proof%unimportant - + have "Q ** transpose Q = mat 1" + by (metis oQ orthogonal_matrix_def) + then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)" + by simp + then have "det Q * det Q = 1" + by (simp add: det_mul) + then show ?thesis + by (simp add: square_eq_1_iff) +qed + +lemma%important orthogonal_transformation_det [simp]: + fixes f :: "real^'n \ real^'n" + shows "orthogonal_transformation f \ \det (matrix f)\ = 1" + using%unimportant det_orthogonal_matrix orthogonal_transformation_matrix by fastforce + +subsection%important \Rotation, reflection, rotoinversion\ + +definition%important "rotation_matrix Q \ orthogonal_matrix Q \ det Q = 1" +definition%important "rotoinversion_matrix Q \ orthogonal_matrix Q \ det Q = - 1" + +lemma%important orthogonal_rotation_or_rotoinversion: + fixes Q :: "'a::linordered_idom^'n^'n" + shows " orthogonal_matrix Q \ rotation_matrix Q \ rotoinversion_matrix Q" + by%unimportant (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) + text\ Slightly stronger results giving rotation, but only in two or more dimensions\ lemma%unimportant rotation_matrix_exists_basis: @@ -994,8 +1024,10 @@ then show ?thesis using \A *v axis k 1 = a\ that by auto next - obtain j where "j \ k" - by (metis (full_types) 2 card_2_exists ex_card) + from ex_card[OF 2] obtain h i::'n where "h \ i" + by (auto simp add: eval_nat_numeral card_Suc_eq) + then obtain j where "j \ k" + by (metis (full_types)) let ?TA = "transpose A" let ?A = "\ i. if i = j then - 1 *\<^sub>R (?TA $ i) else ?TA $i" assume "rotoinversion_matrix A" diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Extended_Real_Limits.thy --- a/src/HOL/Analysis/Extended_Real_Limits.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Extended_Real_Limits.thy Thu Jan 17 16:22:21 2019 -0500 @@ -16,23 +16,23 @@ "HOL-Library.Indicator_Function" begin -lemma compact_UNIV: +lemma%important compact_UNIV: "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)" - using compact_complete_linorder + using%unimportant compact_complete_linorder by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def) -lemma compact_eq_closed: +lemma%important compact_eq_closed: fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" shows "compact S \ closed S" using%unimportant closed_Int_compact[of S, OF _ compact_UNIV] compact_imp_closed by auto -lemma closed_contains_Sup_cl: +lemma%important closed_contains_Sup_cl: fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" assumes "closed S" and "S \ {}" shows "Sup S \ S" -proof - +proof%unimportant - from compact_eq_closed[of S] compact_attains_sup[of S] assms obtain s where S: "s \ S" "\t\S. t \ s" by auto @@ -42,12 +42,12 @@ by simp qed -lemma closed_contains_Inf_cl: +lemma%important closed_contains_Inf_cl: fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" assumes "closed S" and "S \ {}" shows "Inf S \ S" -proof - +proof%unimportant - from compact_eq_closed[of S] compact_attains_inf[of S] assms obtain s where S: "s \ S" "\t\S. s \ t" by auto @@ -57,7 +57,7 @@ by simp qed -instance%unimportant enat :: second_countable_topology +instance enat :: second_countable_topology proof show "\B::enat set set. countable B \ open = generate_topology B" proof (intro exI conjI) @@ -66,8 +66,8 @@ qed (simp add: open_enat_def) qed -instance%unimportant ereal :: second_countable_topology -proof (standard, intro exI conjI) +instance%important ereal :: second_countable_topology +proof%unimportant (standard, intro exI conjI) let ?B = "(\r\\. {{..< r}, {r <..}} :: ereal set set)" show "countable ?B" by (auto intro: countable_rat) @@ -98,8 +98,8 @@ text \This is a copy from \ereal :: second_countable_topology\. Maybe find a common super class of topological spaces where the rational numbers are densely embedded ?\ -instance ennreal :: second_countable_topology -proof (standard, intro exI conjI) +instance%important ennreal :: second_countable_topology +proof%unimportant (standard, intro exI conjI) let ?B = "(\r\\. {{..< r}, {r <..}} :: ennreal set set)" show "countable ?B" by (auto intro: countable_rat) @@ -128,13 +128,13 @@ qed qed -lemma ereal_open_closed_aux: +lemma%important ereal_open_closed_aux: fixes S :: "ereal set" assumes "open S" and "closed S" and S: "(-\) \ S" shows "S = {}" -proof (rule ccontr) +proof%unimportant (rule ccontr) assume "\ ?thesis" then have *: "Inf S \ S" @@ -172,10 +172,10 @@ by auto qed -lemma ereal_open_closed: +lemma%important ereal_open_closed: fixes S :: "ereal set" shows "open S \ closed S \ S = {} \ S = UNIV" -proof - +proof%unimportant - { assume lhs: "open S \ closed S" { @@ -196,10 +196,10 @@ by auto qed -lemma ereal_open_atLeast: +lemma%important ereal_open_atLeast: fixes x :: ereal shows "open {x..} \ x = -\" -proof +proof%unimportant assume "x = -\" then have "{x..} = UNIV" by auto @@ -215,12 +215,12 @@ by (simp add: bot_ereal_def atLeast_eq_UNIV_iff) qed -lemma mono_closed_real: +lemma%important mono_closed_real: fixes S :: "real set" assumes mono: "\y z. y \ S \ y \ z \ z \ S" and "closed S" shows "S = {} \ S = UNIV \ (\a. S = {a..})" -proof - +proof%unimportant - { assume "S \ {}" { assume ex: "\B. \x\S. B \ x" @@ -261,12 +261,12 @@ by blast qed -lemma mono_closed_ereal: +lemma%important mono_closed_ereal: fixes S :: "real set" assumes mono: "\y z. y \ S \ y \ z \ z \ S" and "closed S" shows "\a. S = {x. a \ ereal x}" -proof - +proof%unimportant - { assume "S = {}" then have ?thesis @@ -296,11 +296,11 @@ using mono_closed_real[of S] assms by auto qed -lemma Liminf_within: +lemma%important Liminf_within: fixes f :: "'a::metric_space \ 'b::complete_lattice" shows "Liminf (at x within S) f = (SUP e\{0<..}. INF y\(S \ ball x e - {x}). f y)" unfolding Liminf_def eventually_at -proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe) +proof%unimportant (rule SUP_eq, simp_all add: Ball_def Bex_def, safe) fix P d assume "0 < d" and "\y. y \ S \ y \ x \ dist y x < d \ P y" then have "S \ ball x d - {x} \ {x. P x}" @@ -316,11 +316,11 @@ (auto intro!: INF_mono exI[of _ d] simp: dist_commute) qed -lemma Limsup_within: +lemma%important Limsup_within: fixes f :: "'a::metric_space \ 'b::complete_lattice" shows "Limsup (at x within S) f = (INF e\{0<..}. SUP y\(S \ ball x e - {x}). f y)" unfolding Limsup_def eventually_at -proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe) +proof%unimportant (rule INF_eq, simp_all add: Ball_def Bex_def, safe) fix P d assume "0 < d" and "\y. y \ S \ y \ x \ dist y x < d \ P y" then have "S \ ball x d - {x} \ {x. P x}" @@ -357,7 +357,7 @@ done -subsection%important \Extended-Real.thy\ (*FIX ME change title *) +subsection%important \Extended-Real.thy\ (*FIX title *) lemma sum_constant_ereal: fixes a::ereal @@ -377,10 +377,10 @@ ultimately show ?thesis by (metis (mono_tags, lifting) eventually_mono) qed -lemma ereal_Inf_cmult: +lemma%important ereal_Inf_cmult: assumes "c>(0::real)" shows "Inf {ereal c * x |x. P x} = ereal c * Inf {x. P x}" -proof - +proof%unimportant - have "(\x::ereal. c * x) (Inf {x::ereal. P x}) = Inf ((\x::ereal. c * x)`{x::ereal. P x})" apply (rule mono_bij_Inf) apply (simp add: assms ereal_mult_left_mono less_imp_le mono_def) @@ -399,12 +399,12 @@ It is much more convenient in many situations, see for instance the proof of \tendsto_sum_ereal\ below.\ -lemma tendsto_add_ereal_PInf: +lemma%important tendsto_add_ereal_PInf: fixes y :: ereal assumes y: "y \ -\" assumes f: "(f \ \) F" and g: "(g \ y) F" shows "((\x. f x + g x) \ \) F" -proof - +proof%unimportant - have "\C. eventually (\x. g x > ereal C) F" proof (cases y) case (real r) @@ -437,12 +437,12 @@ that \- (x + y)\ is in general different from \(- x) + (- y)\ in ereal creates difficulties, so it is more efficient to copy the previous proof.\ -lemma tendsto_add_ereal_MInf: +lemma%important tendsto_add_ereal_MInf: fixes y :: ereal assumes y: "y \ \" assumes f: "(f \ -\) F" and g: "(g \ y) F" shows "((\x. f x + g x) \ -\) F" -proof - +proof%unimportant - have "\C. eventually (\x. g x < ereal C) F" proof (cases y) case (real r) @@ -470,12 +470,12 @@ then show ?thesis by (simp add: tendsto_MInfty) qed -lemma tendsto_add_ereal_general1: +lemma%important tendsto_add_ereal_general1: fixes x y :: ereal assumes y: "\y\ \ \" assumes f: "(f \ x) F" and g: "(g \ y) F" shows "((\x. f x + g x) \ x + y) F" -proof (cases x) +proof%unimportant (cases x) case (real r) have a: "\x\ \ \" by (simp add: real) show ?thesis by (rule tendsto_add_ereal[OF a, OF y, OF f, OF g]) @@ -488,12 +488,12 @@ by (metis abs_ereal.simps(3) ereal_MInfty_eq_plus) qed -lemma tendsto_add_ereal_general2: +lemma%important tendsto_add_ereal_general2: fixes x y :: ereal assumes x: "\x\ \ \" and f: "(f \ x) F" and g: "(g \ y) F" shows "((\x. f x + g x) \ x + y) F" -proof - +proof%unimportant - have "((\x. g x + f x) \ x + y) F" using tendsto_add_ereal_general1[OF x, OF g, OF f] add.commute[of "y", of "x"] by simp moreover have "\x. g x + f x = f x + g x" using add.commute by auto @@ -503,12 +503,12 @@ text \The next lemma says that the addition is continuous on \ereal\, except at the pairs \(-\, \)\ and \(\, -\)\.\ -lemma tendsto_add_ereal_general [tendsto_intros]: +lemma%important tendsto_add_ereal_general [tendsto_intros]: fixes x y :: ereal assumes "\((x=\ \ y=-\) \ (x=-\ \ y=\))" and f: "(f \ x) F" and g: "(g \ y) F" shows "((\x. f x + g x) \ x + y) F" -proof (cases x) +proof%unimportant (cases x) case (real r) show ?thesis apply (rule tendsto_add_ereal_general2) using real assms by auto @@ -528,10 +528,10 @@ ereal times ereal, except at \(\, 0)\ and \(-\, 0)\ and \(0, \)\ and \(0, -\)\, starting with specific situations.\ -lemma tendsto_mult_real_ereal: +lemma%important tendsto_mult_real_ereal: assumes "(u \ ereal l) F" "(v \ ereal m) F" shows "((\n. u n * v n) \ ereal l * ereal m) F" -proof - +proof%unimportant - have ureal: "eventually (\n. u n = ereal(real_of_ereal(u n))) F" by (rule real_lim_then_eventually_real[OF assms(1)]) then have "((\n. ereal(real_of_ereal(u n))) \ ereal l) F" using assms by auto then have limu: "((\n. real_of_ereal(u n)) \ l) F" by auto @@ -551,11 +551,11 @@ then show ?thesis using * filterlim_cong by fastforce qed -lemma tendsto_mult_ereal_PInf: +lemma%important tendsto_mult_ereal_PInf: fixes f g::"_ \ ereal" assumes "(f \ l) F" "l>0" "(g \ \) F" shows "((\x. f x * g x) \ \) F" -proof - +proof%unimportant - obtain a::real where "0 < ereal a" "a < l" using assms(2) using ereal_dense2 by blast have *: "eventually (\x. f x > a) F" using \a < l\ assms(1) by (simp add: order_tendsto_iff) { @@ -579,11 +579,11 @@ then show ?thesis by (auto simp add: tendsto_PInfty) qed -lemma tendsto_mult_ereal_pos: +lemma%important tendsto_mult_ereal_pos: fixes f g::"_ \ ereal" assumes "(f \ l) F" "(g \ m) F" "l>0" "m>0" shows "((\x. f x * g x) \ l * m) F" -proof (cases) +proof%unimportant (cases) assume *: "l = \ \ m = \" then show ?thesis proof (cases) @@ -618,11 +618,11 @@ shows "sgn(l) * sgn(l) = 1" apply (cases l) using assms by (auto simp add: one_ereal_def sgn_if) -lemma tendsto_mult_ereal [tendsto_intros]: +lemma%important tendsto_mult_ereal [tendsto_intros]: fixes f g::"_ \ ereal" assumes "(f \ l) F" "(g \ m) F" "\((l=0 \ abs(m) = \) \ (m=0 \ abs(l) = \))" shows "((\x. f x * g x) \ l * m) F" -proof (cases) +proof%unimportant (cases) assume "l=0 \ m=0" then have "abs(l) \ \" "abs(m) \ \" using assms(3) by auto then obtain lr mr where "l = ereal lr" "m = ereal mr" by auto @@ -661,11 +661,11 @@ subsubsection%important \Continuity of division\ -lemma tendsto_inverse_ereal_PInf: +lemma%important tendsto_inverse_ereal_PInf: fixes u::"_ \ ereal" assumes "(u \ \) F" shows "((\x. 1/ u x) \ 0) F" -proof - +proof%unimportant - { fix e::real assume "e>0" have "1/e < \" by auto @@ -702,11 +702,11 @@ shows "(u \ l) F \ l \ 0 \ ((\x. 1/ u x) \ 1/l) F" using tendsto_inverse unfolding inverse_eq_divide . -lemma tendsto_inverse_ereal [tendsto_intros]: +lemma%important tendsto_inverse_ereal [tendsto_intros]: fixes u::"_ \ ereal" assumes "(u \ l) F" "l \ 0" shows "((\x. 1/ u x) \ 1/l) F" -proof (cases l) +proof%unimportant (cases l) case (real r) then have "r \ 0" using assms(2) by auto then have "1/l = ereal(1/r)" using real by (simp add: one_ereal_def) @@ -747,11 +747,11 @@ then show ?thesis unfolding v_def using Lim_transform_eventually[OF *] \ 1/l = 0 \ by auto qed -lemma tendsto_divide_ereal [tendsto_intros]: +lemma%important tendsto_divide_ereal [tendsto_intros]: fixes f g::"_ \ ereal" assumes "(f \ l) F" "(g \ m) F" "m \ 0" "\(abs(l) = \ \ abs(m) = \)" shows "((\x. f x / g x) \ l / m) F" -proof - +proof%unimportant - define h where "h = (\x. 1/ g x)" have *: "(h \ 1/m) F" unfolding h_def using assms(2) assms(3) tendsto_inverse_ereal by auto have "((\x. f x * h x) \ l * (1/m)) F" @@ -766,11 +766,11 @@ text \The assumptions of @{thm tendsto_diff_ereal} are too strong, we weaken them here.\ -lemma tendsto_diff_ereal_general [tendsto_intros]: +lemma%important tendsto_diff_ereal_general [tendsto_intros]: fixes u v::"'a \ ereal" assumes "(u \ l) F" "(v \ m) F" "\((l = \ \ m = \) \ (l = -\ \ m = -\))" shows "((\n. u n - v n) \ l - m) F" -proof - +proof%unimportant - have "((\n. u n + (-v n)) \ l + (-m)) F" apply (intro tendsto_intros assms) using assms by (auto simp add: ereal_uminus_eq_reorder) then show ?thesis by (simp add: minus_ereal_def) @@ -780,11 +780,11 @@ "(\ n::nat. real n) \ \" by (simp add: filterlim_real_sequentially tendsto_PInfty_eq_at_top) -lemma tendsto_at_top_pseudo_inverse [tendsto_intros]: +lemma%important tendsto_at_top_pseudo_inverse [tendsto_intros]: fixes u::"nat \ nat" assumes "LIM n sequentially. u n :> at_top" shows "LIM n sequentially. Inf {N. u N \ n} :> at_top" -proof - +proof%unimportant - { fix C::nat define M where "M = Max {u n| n. n \ C}+1" @@ -811,11 +811,11 @@ then show ?thesis using filterlim_at_top by auto qed -lemma pseudo_inverse_finite_set: +lemma%important pseudo_inverse_finite_set: fixes u::"nat \ nat" assumes "LIM n sequentially. u n :> at_top" shows "finite {N. u N \ n}" -proof - +proof%unimportant - fix n have "eventually (\N. u N \ n+1) sequentially" using assms by (simp add: filterlim_at_top) @@ -860,11 +860,11 @@ then show ?thesis by auto qed -lemma ereal_truncation_real_top [tendsto_intros]: +lemma%important ereal_truncation_real_top [tendsto_intros]: fixes x::ereal assumes "x \ - \" shows "(\n::nat. real_of_ereal(min x n)) \ x" -proof (cases x) +proof%unimportant (cases x) case (real r) then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto then have "min x n = x" if "n \ K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce @@ -878,10 +878,10 @@ then show ?thesis using id_nat_ereal_tendsto_PInf PInf by auto qed (simp add: assms) -lemma ereal_truncation_bottom [tendsto_intros]: +lemma%important ereal_truncation_bottom [tendsto_intros]: fixes x::ereal shows "(\n::nat. max x (- real n)) \ x" -proof (cases x) +proof%unimportant (cases x) case (real r) then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto then have "max x (-real n) = x" if "n \ K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce @@ -899,11 +899,11 @@ then show ?thesis by auto qed -lemma ereal_truncation_real_bottom [tendsto_intros]: +lemma%important ereal_truncation_real_bottom [tendsto_intros]: fixes x::ereal assumes "x \ \" shows "(\n::nat. real_of_ereal(max x (- real n))) \ x" -proof (cases x) +proof%unimportant (cases x) case (real r) then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto then have "max x (-real n) = x" if "n \ K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce @@ -931,9 +931,9 @@ qed(simp) -lemma continuous_ereal_abs: +lemma%important continuous_ereal_abs: "continuous_on (UNIV::ereal set) abs" -proof - +proof%unimportant - have "continuous_on ({..0} \ {(0::ereal)..}) abs" apply (rule continuous_on_closed_Un, auto) apply (rule iffD1[OF continuous_on_cong, of "{..0}" _ "\x. -x"]) @@ -970,11 +970,11 @@ then show ?thesis by auto qed -lemma tendsto_mult_ennreal [tendsto_intros]: +lemma%important tendsto_mult_ennreal [tendsto_intros]: fixes l m::ennreal assumes "(u \ l) F" "(v \ m) F" "\((l = 0 \ m = \) \ (l = \ \ m = 0))" shows "((\n. u n * v n) \ l * m) F" -proof - +proof%unimportant - have "((\n. e2ennreal(enn2ereal (u n) * enn2ereal (v n))) \ e2ennreal(enn2ereal l * enn2ereal m)) F" apply (intro tendsto_intros) using assms apply auto using enn2ereal_inject zero_ennreal.rep_eq by fastforce+ @@ -987,9 +987,9 @@ qed -subsection%important \monoset\ (*FIX ME title *) +subsection%important \monoset\ -definition (in order) mono_set: +definition%important (in order) mono_set: "mono_set S \ (\x y. x \ y \ x \ S \ y \ S)" lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto @@ -997,11 +997,11 @@ lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto -lemma (in complete_linorder) mono_set_iff: +lemma%important (in complete_linorder) mono_set_iff: fixes S :: "'a set" defines "a \ Inf S" shows "mono_set S \ S = {a <..} \ S = {a..}" (is "_ = ?c") -proof +proof%unimportant assume "mono_set S" then have mono: "\x y. x \ y \ x \ S \ y \ S" by (auto simp: mono_set) @@ -1043,12 +1043,12 @@ by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan) -lemma ereal_Liminf_Sup_monoset: +lemma%important ereal_Liminf_Sup_monoset: fixes f :: "'a \ ereal" shows "Liminf net f = Sup {l. \S. open S \ mono_set S \ l \ S \ eventually (\x. f x \ S) net}" (is "_ = Sup ?A") -proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least) +proof%unimportant (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least) fix P assume P: "eventually P net" fix S @@ -1082,12 +1082,12 @@ qed qed -lemma ereal_Limsup_Inf_monoset: +lemma%important ereal_Limsup_Inf_monoset: fixes f :: "'a \ ereal" shows "Limsup net f = Inf {l. \S. open S \ mono_set (uminus ` S) \ l \ S \ eventually (\x. f x \ S) net}" (is "_ = Inf ?A") -proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest) +proof%unimportant (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest) fix P assume P: "eventually P net" fix S @@ -1121,11 +1121,11 @@ qed qed -lemma liminf_bounded_open: +lemma%important liminf_bounded_open: fixes x :: "nat \ ereal" shows "x0 \ liminf x \ (\S. open S \ mono_set S \ x0 \ S \ (\N. \n\N. x n \ S))" (is "_ \ ?P x0") -proof +proof%unimportant assume "?P x0" then show "x0 \ liminf x" unfolding ereal_Liminf_Sup_monoset eventually_sequentially @@ -1159,11 +1159,11 @@ by auto qed -lemma limsup_finite_then_bounded: +lemma%important limsup_finite_then_bounded: fixes u::"nat \ real" assumes "limsup u < \" shows "\C. \n. u n \ C" -proof - +proof%unimportant - obtain C where C: "limsup u < C" "C < \" using assms ereal_dense2 by blast then have "C = ereal(real_of_ereal C)" using ereal_real by force have "eventually (\n. u n < C) sequentially" using C(1) unfolding Limsup_def @@ -1273,11 +1273,11 @@ then show ?case using Suc.IH by simp qed (auto) -lemma Limsup_obtain: +lemma%important Limsup_obtain: fixes u::"_ \ 'a :: complete_linorder" assumes "Limsup F u > c" shows "\i. u i > c" -proof - +proof%unimportant - have "(INF P\{P. eventually P F}. SUP x\{x. P x}. u x) > c" using assms by (simp add: Limsup_def) then show ?thesis by (metis eventually_True mem_Collect_eq less_INF_D less_SUP_iff) qed @@ -1285,10 +1285,10 @@ text \The next lemma is extremely useful, as it often makes it possible to reduce statements about limsups to statements about limits.\ -lemma limsup_subseq_lim: +lemma%important limsup_subseq_lim: fixes u::"nat \ 'a :: {complete_linorder, linorder_topology}" shows "\r::nat\nat. strict_mono r \ (u o r) \ limsup u" -proof (cases) +proof%unimportant (cases) assume "\n. \p>n. \m\p. u m \ u p" then have "\r. \n. (\m\r n. u m \ u (r n)) \ r n < r (Suc n)" by (intro dependent_nat_choice) (auto simp: conj_commute) @@ -1378,10 +1378,10 @@ then show ?thesis using \strict_mono r\ by auto qed -lemma liminf_subseq_lim: +lemma%important liminf_subseq_lim: fixes u::"nat \ 'a :: {complete_linorder, linorder_topology}" shows "\r::nat\nat. strict_mono r \ (u o r) \ liminf u" -proof (cases) +proof%unimportant (cases) assume "\n. \p>n. \m\p. u m \ u p" then have "\r. \n. (\m\r n. u m \ u (r n)) \ r n < r (Suc n)" by (intro dependent_nat_choice) (auto simp: conj_commute) @@ -1476,10 +1476,10 @@ subsequences thanks to \limsup_subseq_lim\. The statement for limits follows for instance from \tendsto_add_ereal_general\.\ -lemma ereal_limsup_add_mono: +lemma%important ereal_limsup_add_mono: fixes u v::"nat \ ereal" shows "limsup (\n. u n + v n) \ limsup u + limsup v" -proof (cases) +proof%unimportant (cases) assume "(limsup u = \) \ (limsup v = \)" then have "limsup u + limsup v = \" by simp then show ?thesis by auto @@ -1522,11 +1522,11 @@ This explains why there are more assumptions in the next lemma dealing with liminfs that in the previous one about limsups.\ -lemma ereal_liminf_add_mono: +lemma%important ereal_liminf_add_mono: fixes u v::"nat \ ereal" assumes "\((liminf u = \ \ liminf v = -\) \ (liminf u = -\ \ liminf v = \))" shows "liminf (\n. u n + v n) \ liminf u + liminf v" -proof (cases) +proof%unimportant (cases) assume "(liminf u = -\) \ (liminf v = -\)" then have *: "liminf u + liminf v = -\" using assms by auto show ?thesis by (simp add: *) @@ -1565,11 +1565,11 @@ then show ?thesis unfolding w_def by simp qed -lemma ereal_limsup_lim_add: +lemma%important ereal_limsup_lim_add: fixes u v::"nat \ ereal" assumes "u \ a" "abs(a) \ \" shows "limsup (\n. u n + v n) = a + limsup v" -proof - +proof%unimportant - have "limsup u = a" using assms(1) using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast have "(\n. -u n) \ -a" using assms(1) by auto then have "limsup (\n. -u n) = -a" using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast @@ -1596,11 +1596,11 @@ then show ?thesis using up by simp qed -lemma ereal_limsup_lim_mult: +lemma%important ereal_limsup_lim_mult: fixes u v::"nat \ ereal" assumes "u \ a" "a>0" "a \ \" shows "limsup (\n. u n * v n) = a * limsup v" -proof - +proof%unimportant - define w where "w = (\n. u n * v n)" obtain r where r: "strict_mono r" "(v o r) \ limsup v" using limsup_subseq_lim by auto have "(u o r) \ a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto @@ -1626,11 +1626,11 @@ then show ?thesis using I unfolding w_def by auto qed -lemma ereal_liminf_lim_mult: +lemma%important ereal_liminf_lim_mult: fixes u v::"nat \ ereal" assumes "u \ a" "a>0" "a \ \" shows "liminf (\n. u n * v n) = a * liminf v" -proof - +proof%unimportant - define w where "w = (\n. u n * v n)" obtain r where r: "strict_mono r" "(v o r) \ liminf v" using liminf_subseq_lim by auto have "(u o r) \ a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto @@ -1656,11 +1656,11 @@ then show ?thesis using I unfolding w_def by auto qed -lemma ereal_liminf_lim_add: +lemma%important ereal_liminf_lim_add: fixes u v::"nat \ ereal" assumes "u \ a" "abs(a) \ \" shows "liminf (\n. u n + v n) = a + liminf v" -proof - +proof%unimportant - have "liminf u = a" using assms(1) tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast then have *: "abs(liminf u) \ \" using assms(2) by auto have "(\n. -u n) \ -a" using assms(1) by auto @@ -1689,10 +1689,10 @@ then show ?thesis using up by simp qed -lemma ereal_liminf_limsup_add: +lemma%important ereal_liminf_limsup_add: fixes u v::"nat \ ereal" shows "liminf (\n. u n + v n) \ liminf u + limsup v" -proof (cases) +proof%unimportant (cases) assume "limsup v = \ \ liminf u = \" then show ?thesis by auto next @@ -1741,12 +1741,12 @@ done -lemma liminf_minus_ennreal: +lemma%important liminf_minus_ennreal: fixes u v::"nat \ ennreal" shows "(\n. v n \ u n) \ liminf (\n. u n - v n) \ limsup u - limsup v" unfolding liminf_SUP_INF limsup_INF_SUP including ennreal.lifting -proof (transfer, clarsimp) +proof%unimportant (transfer, clarsimp) fix v u :: "nat \ ereal" assume *: "\x. 0 \ v x" "\x. 0 \ u x" "\n. v n \ u n" moreover have "0 \ limsup u - limsup v" using * by (intro ereal_diff_positive Limsup_mono always_eventually) simp @@ -1759,7 +1759,7 @@ by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus) qed -subsection%important "Relate extended reals and the indicator function" +subsection%unimportant "Relate extended reals and the indicator function" lemma ereal_indicator_le_0: "(indicator S x::ereal) \ 0 \ x \ S" by (auto split: split_indicator simp: one_ereal_def) diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Fashoda_Theorem.thy --- a/src/HOL/Analysis/Fashoda_Theorem.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Fashoda_Theorem.thy Thu Jan 17 16:22:21 2019 -0500 @@ -30,14 +30,14 @@ apply (rule, rule continuous_interval_bij) done -lemma in_interval_interval_bij: +lemma%important in_interval_interval_bij: fixes a b u v x :: "'a::euclidean_space" assumes "x \ cbox a b" and "cbox u v \ {}" shows "interval_bij (a, b) (u, v) x \ cbox u v" apply (simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis cong: ball_cong) apply safe -proof - +proof%unimportant - fix i :: 'a assume i: "i \ Basis" have "cbox a b \ {}" @@ -89,7 +89,7 @@ shows "\x$1\ \ 1" and "\x$2\ \ 1" using assms unfolding infnorm_eq_1_2 by auto -proposition fashoda_unit: +lemma%important fashoda_unit: fixes f g :: "real \ real^2" assumes "f ` {-1 .. 1} \ cbox (-1) 1" and "g ` {-1 .. 1} \ cbox (-1) 1" @@ -99,7 +99,7 @@ and "f 1$1 = 1" "g (- 1) $2 = -1" and "g 1 $2 = 1" shows "\s\{-1 .. 1}. \t\{-1 .. 1}. f s = g t" -proof (rule ccontr) +proof%unimportant (rule ccontr) assume "\ ?thesis" note as = this[unfolded bex_simps,rule_format] define sqprojection @@ -256,7 +256,7 @@ qed qed -proposition fashoda_unit_path: +lemma%important fashoda_unit_path: fixes f g :: "real \ real^2" assumes "path f" and "path g" @@ -267,7 +267,7 @@ and "(pathstart g)$2 = -1" and "(pathfinish g)$2 = 1" obtains z where "z \ path_image f" and "z \ path_image g" -proof - +proof%unimportant - note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def] define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real have isc: "iscale ` {- 1..1} \ {0..1}" @@ -312,7 +312,7 @@ done qed -theorem fashoda: +lemma%important fashoda: fixes b :: "real^2" assumes "path f" and "path g" @@ -323,7 +323,7 @@ and "(pathstart g)$2 = a$2" and "(pathfinish g)$2 = b$2" obtains z where "z \ path_image f" and "z \ path_image g" -proof - +proof%unimportant - fix P Q S presume "P \ Q \ S" "P \ thesis" and "Q \ thesis" and "S \ thesis" then show thesis @@ -632,7 +632,7 @@ subsection%important \Useful Fashoda corollary pointed out to me by Tom Hales\(*FIXME change title? *) -corollary fashoda_interlace: +lemma%important fashoda_interlace: fixes a :: "real^2" assumes "path f" and "path g" @@ -646,7 +646,7 @@ and "(pathstart g)$1 < (pathfinish f)$1" and "(pathfinish f)$1 < (pathfinish g)$1" obtains z where "z \ path_image f" and "z \ path_image g" -proof - +proof%unimportant - have "cbox a b \ {}" using path_image_nonempty[of f] using assms(3) by auto note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less] diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Jan 17 16:22:21 2019 -0500 @@ -259,32 +259,20 @@ text\The ordering on one-dimensional vectors is linear.\ -class cart_one = - assumes UNIV_one: "card (UNIV :: 'a set) = Suc 0" -begin - -subclass finite -proof - from UNIV_one show "finite (UNIV :: 'a set)" - by (auto intro!: card_ge_0_finite) -qed - -end - instance vec:: (order, finite) order by standard (auto simp: less_eq_vec_def less_vec_def vec_eq_iff intro: order.trans order.antisym order.strict_implies_order) -instance vec :: (linorder, cart_one) linorder +instance vec :: (linorder, CARD_1) linorder proof obtain a :: 'b where all: "\P. (\i. P i) \ P a" proof - - have "card (UNIV :: 'b set) = Suc 0" by (rule UNIV_one) + have "CARD ('b) = 1" by (rule CARD_1) then obtain b :: 'b where "UNIV = {b}" by (auto iff: card_Suc_eq) then have "\P. (\i\UNIV. P i) \ P b" by auto then show thesis by (auto intro: that) qed - fix x y :: "'a^'b::cart_one" + fix x y :: "'a^'b::CARD_1" note [simp] = less_eq_vec_def less_vec_def all vec_eq_iff field_simps show "x \ y \ y \ x" by auto qed @@ -638,7 +626,7 @@ lemma%unimportant norm_le_l1_cart: "norm x \ sum(\i. \x$i\) UNIV" by (simp add: norm_vec_def L2_set_le_sum) -lemma%unimportant bounded_linear_vec_nth: "bounded_linear (\x. x $ i)" +lemma%unimportant bounded_linear_vec_nth[intro]: "bounded_linear (\x. x $ i)" apply standard apply (rule vector_add_component) apply (rule vector_scaleR_component) diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Finite_Product_Measure.thy --- a/src/HOL/Analysis/Finite_Product_Measure.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy Thu Jan 17 16:22:21 2019 -0500 @@ -8,14 +8,14 @@ imports Binary_Product_Measure begin -lemma PiE_choice: "(\f\Pi\<^sub>E I F. \i\I. P i (f i)) \ (\i\I. \x\F i. P i x)" +lemma%unimportant PiE_choice: "(\f\Pi\<^sub>E I F. \i\I. P i (f i)) \ (\i\I. \x\F i. P i x)" by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1]) (force intro: exI[of _ "restrict f I" for f]) -lemma case_prod_const: "(\(i, j). c) = (\_. c)" +lemma%unimportant case_prod_const: "(\(i, j). c) = (\_. c)" by auto -subsubsection \More about Function restricted by \<^const>\extensional\\ +subsubsection%unimportant \More about Function restricted by \<^const>\extensional\\ definition "merge I J = (\(x, y) i. if i \ I then x i else if i \ J then y i else undefined)" @@ -116,42 +116,42 @@ definition%important prod_emb where "prod_emb I M K X = (\x. restrict x K) -` X \ (\\<^sub>E i\I. space (M i))" -lemma prod_emb_iff: +lemma%important prod_emb_iff: "f \ prod_emb I M K X \ f \ extensional I \ (restrict f K \ X) \ (\i\I. f i \ space (M i))" unfolding%unimportant prod_emb_def PiE_def by auto -lemma +lemma%unimportant shows prod_emb_empty[simp]: "prod_emb M L K {} = {}" and prod_emb_Un[simp]: "prod_emb M L K (A \ B) = prod_emb M L K A \ prod_emb M L K B" and prod_emb_Int: "prod_emb M L K (A \ B) = prod_emb M L K A \ prod_emb M L K B" and prod_emb_UN[simp]: "prod_emb M L K (\i\I. F i) = (\i\I. prod_emb M L K (F i))" and prod_emb_INT[simp]: "I \ {} \ prod_emb M L K (\i\I. F i) = (\i\I. prod_emb M L K (F i))" and prod_emb_Diff[simp]: "prod_emb M L K (A - B) = prod_emb M L K A - prod_emb M L K B" - by (auto simp: prod_emb_def) + by%unimportant (auto simp: prod_emb_def) -lemma prod_emb_PiE: "J \ I \ (\i. i \ J \ E i \ space (M i)) \ +lemma%unimportant prod_emb_PiE: "J \ I \ (\i. i \ J \ E i \ space (M i)) \ prod_emb I M J (\\<^sub>E i\J. E i) = (\\<^sub>E i\I. if i \ J then E i else space (M i))" by (force simp: prod_emb_def PiE_iff if_split_mem2) -lemma prod_emb_PiE_same_index[simp]: +lemma%unimportant prod_emb_PiE_same_index[simp]: "(\i. i \ I \ E i \ space (M i)) \ prod_emb I M I (Pi\<^sub>E I E) = Pi\<^sub>E I E" by (auto simp: prod_emb_def PiE_iff) -lemma prod_emb_trans[simp]: +lemma%unimportant prod_emb_trans[simp]: "J \ K \ K \ L \ prod_emb L M K (prod_emb K M J X) = prod_emb L M J X" by (auto simp add: Int_absorb1 prod_emb_def PiE_def) -lemma prod_emb_Pi: +lemma%unimportant prod_emb_Pi: assumes "X \ (\ j\J. sets (M j))" "J \ K" shows "prod_emb K M J (Pi\<^sub>E J X) = (\\<^sub>E i\K. if i \ J then X i else space (M i))" using assms sets.space_closed by (auto simp: prod_emb_def PiE_iff split: if_split_asm) blast+ -lemma prod_emb_id: +lemma%unimportant prod_emb_id: "B \ (\\<^sub>E i\L. space (M i)) \ prod_emb L M L B = B" by (auto simp: prod_emb_def subset_eq extensional_restrict) -lemma prod_emb_mono: +lemma%unimportant prod_emb_mono: "F \ G \ prod_emb A M B F \ prod_emb A M B G" by (auto simp: prod_emb_def) @@ -173,20 +173,20 @@ translations "\\<^sub>M x\I. M" == "CONST PiM I (%x. M)" -lemma extend_measure_cong: +lemma%important extend_measure_cong: assumes "\ = \'" "I = I'" "G = G'" "\i. i \ I' \ \ i = \' i" shows "extend_measure \ I G \ = extend_measure \' I' G' \'" - unfolding extend_measure_def by (auto simp add: assms) + unfolding%unimportant extend_measure_def by (auto simp add: assms) -lemma Pi_cong_sets: +lemma%unimportant Pi_cong_sets: "\I = J; \x. x \ I \ M x = N x\ \ Pi I M = Pi J N" unfolding Pi_def by auto -lemma PiM_cong: +lemma%important PiM_cong: assumes "I = J" "\x. x \ I \ M x = N x" shows "PiM I M = PiM J N" unfolding PiM_def -proof (rule extend_measure_cong, goal_cases) +proof%unimportant (rule extend_measure_cong, goal_cases) case 1 show ?case using assms by (subst assms(1), intro PiE_cong[of J "\i. space (M i)" "\i. space (N i)"]) simp_all @@ -206,14 +206,14 @@ qed -lemma prod_algebra_sets_into_space: +lemma%unimportant prod_algebra_sets_into_space: "prod_algebra I M \ Pow (\\<^sub>E i\I. space (M i))" by (auto simp: prod_emb_def prod_algebra_def) -lemma prod_algebra_eq_finite: +lemma%important prod_algebra_eq_finite: assumes I: "finite I" shows "prod_algebra I M = {(\\<^sub>E i\I. X i) |X. X \ (\ j\I. sets (M j))}" (is "?L = ?R") -proof (intro iffI set_eqI) +proof%unimportant (intro iffI set_eqI) fix A assume "A \ ?L" then obtain J E where J: "J \ {} \ I = {}" "finite J" "J \ I" "\i\J. E i \ sets (M i)" and A: "A = prod_emb I M J (\\<^sub>E j\J. E j)" @@ -232,32 +232,32 @@ by (auto simp: prod_algebra_def) qed -lemma prod_algebraI: +lemma%unimportant prod_algebraI: "finite J \ (J \ {} \ I = {}) \ J \ I \ (\i. i \ J \ E i \ sets (M i)) \ prod_emb I M J (\\<^sub>E j\J. E j) \ prod_algebra I M" by (auto simp: prod_algebra_def) -lemma prod_algebraI_finite: +lemma%unimportant prod_algebraI_finite: "finite I \ (\i\I. E i \ sets (M i)) \ (Pi\<^sub>E I E) \ prod_algebra I M" using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets.sets_into_space] by simp -lemma Int_stable_PiE: "Int_stable {Pi\<^sub>E J E | E. \i\I. E i \ sets (M i)}" +lemma%unimportant Int_stable_PiE: "Int_stable {Pi\<^sub>E J E | E. \i\I. E i \ sets (M i)}" proof (safe intro!: Int_stableI) fix E F assume "\i\I. E i \ sets (M i)" "\i\I. F i \ sets (M i)" then show "\G. Pi\<^sub>E J E \ Pi\<^sub>E J F = Pi\<^sub>E J G \ (\i\I. G i \ sets (M i))" by (auto intro!: exI[of _ "\i. E i \ F i"] simp: PiE_Int) qed -lemma prod_algebraE: +lemma%unimportant prod_algebraE: assumes A: "A \ prod_algebra I M" obtains J E where "A = prod_emb I M J (\\<^sub>E j\J. E j)" "finite J" "J \ {} \ I = {}" "J \ I" "\i. i \ J \ E i \ sets (M i)" using A by (auto simp: prod_algebra_def) -lemma prod_algebraE_all: +lemma%important prod_algebraE_all: assumes A: "A \ prod_algebra I M" obtains E where "A = Pi\<^sub>E I E" "E \ (\ i\I. sets (M i))" -proof - +proof%unimportant - from A obtain E J where A: "A = prod_emb I M J (Pi\<^sub>E J E)" and J: "J \ I" and E: "E \ (\ i\J. sets (M i))" by (auto simp: prod_algebra_def) @@ -270,7 +270,7 @@ ultimately show ?thesis using that by auto qed -lemma Int_stable_prod_algebra: "Int_stable (prod_algebra I M)" +lemma%unimportant Int_stable_prod_algebra: "Int_stable (prod_algebra I M)" proof (unfold Int_stable_def, safe) fix A assume "A \ prod_algebra I M" from prod_algebraE[OF this] guess J E . note A = this @@ -291,11 +291,11 @@ finally show "A \ B \ prod_algebra I M" . qed -proposition prod_algebra_mono: +lemma%unimportant prod_algebra_mono: assumes space: "\i. i \ I \ space (E i) = space (F i)" assumes sets: "\i. i \ I \ sets (E i) \ sets (F i)" shows "prod_algebra I E \ prod_algebra I F" -proof +proof%unimportant fix A assume "A \ prod_algebra I E" then obtain J G where J: "J \ {} \ I = {}" "finite J" "J \ I" and A: "A = prod_emb I E J (\\<^sub>E i\J. G i)" @@ -315,17 +315,18 @@ apply auto done qed -proposition prod_algebra_cong: + +lemma%unimportant prod_algebra_cong: assumes "I = J" and sets: "(\i. i \ I \ sets (M i) = sets (N i))" shows "prod_algebra I M = prod_algebra J N" -proof - +proof%unimportant - have space: "\i. i \ I \ space (M i) = space (N i)" using sets_eq_imp_space_eq[OF sets] by auto with sets show ?thesis unfolding \I = J\ by (intro antisym prod_algebra_mono) auto qed -lemma space_in_prod_algebra: +lemma%unimportant space_in_prod_algebra: "(\\<^sub>E i\I. space (M i)) \ prod_algebra I M" proof cases assume "I = {}" then show ?thesis @@ -340,26 +341,26 @@ finally show ?thesis . qed -lemma space_PiM: "space (\\<^sub>M i\I. M i) = (\\<^sub>E i\I. space (M i))" +lemma%unimportant space_PiM: "space (\\<^sub>M i\I. M i) = (\\<^sub>E i\I. space (M i))" using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp -lemma prod_emb_subset_PiM[simp]: "prod_emb I M K X \ space (PiM I M)" +lemma%unimportant prod_emb_subset_PiM[simp]: "prod_emb I M K X \ space (PiM I M)" by (auto simp: prod_emb_def space_PiM) -lemma space_PiM_empty_iff[simp]: "space (PiM I M) = {} \ (\i\I. space (M i) = {})" +lemma%unimportant space_PiM_empty_iff[simp]: "space (PiM I M) = {} \ (\i\I. space (M i) = {})" by (auto simp: space_PiM PiE_eq_empty_iff) -lemma undefined_in_PiM_empty[simp]: "(\x. undefined) \ space (PiM {} M)" +lemma%unimportant undefined_in_PiM_empty[simp]: "(\x. undefined) \ space (PiM {} M)" by (auto simp: space_PiM) -lemma sets_PiM: "sets (\\<^sub>M i\I. M i) = sigma_sets (\\<^sub>E i\I. space (M i)) (prod_algebra I M)" +lemma%unimportant sets_PiM: "sets (\\<^sub>M i\I. M i) = sigma_sets (\\<^sub>E i\I. space (M i)) (prod_algebra I M)" using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp -proposition sets_PiM_single: "sets (PiM I M) = +lemma%important sets_PiM_single: "sets (PiM I M) = sigma_sets (\\<^sub>E i\I. space (M i)) {{f\\\<^sub>E i\I. space (M i). f i \ A} | i A. i \ I \ A \ sets (M i)}" (is "_ = sigma_sets ?\ ?R") unfolding sets_PiM -proof (rule sigma_sets_eqI) +proof%unimportant (rule sigma_sets_eqI) interpret R: sigma_algebra ?\ "sigma_sets ?\ ?R" by (rule sigma_algebra_sigma_sets) auto fix A assume "A \ prod_algebra I M" from prod_algebraE[OF this] guess J X . note X = this @@ -387,7 +388,7 @@ finally show "A \ sigma_sets ?\ (prod_algebra I M)" . qed -lemma sets_PiM_eq_proj: +lemma%unimportant sets_PiM_eq_proj: "I \ {} \ sets (PiM I M) = sets (SUP i\I. vimage_algebra (\\<^sub>E i\I. space (M i)) (\x. x i) (M i))" apply (simp add: sets_PiM_single) apply (subst sets_Sup_eq[where X="\\<^sub>E i\I. space (M i)"]) @@ -399,18 +400,18 @@ apply (auto intro!: arg_cong2[where f=sigma_sets]) done -lemma (*FIX ME needs name *) +lemma%unimportant (*FIX ME needs name *) shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\k. undefined}" and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\k. undefined} }" by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq) -proposition sets_PiM_sigma: +lemma%important sets_PiM_sigma: assumes \_cover: "\i. i \ I \ \S\E i. countable S \ \ i = \S" assumes E: "\i. i \ I \ E i \ Pow (\ i)" assumes J: "\j. j \ J \ finite j" "\J = I" defines "P \ {{f\(\\<^sub>E i\I. \ i). \i\j. f i \ A i} | A j. j \ J \ A \ Pi j E}" shows "sets (\\<^sub>M i\I. sigma (\ i) (E i)) = sets (sigma (\\<^sub>E i\I. \ i) P)" -proof cases +proof%unimportant cases assume "I = {}" with \\J = I\ have "P = {{\_. undefined}} \ P = {}" by (auto simp: P_def) @@ -494,21 +495,21 @@ finally show "?thesis" . qed -lemma sets_PiM_in_sets: +lemma%unimportant sets_PiM_in_sets: assumes space: "space N = (\\<^sub>E i\I. space (M i))" assumes sets: "\i A. i \ I \ A \ sets (M i) \ {x\space N. x i \ A} \ sets N" shows "sets (\\<^sub>M i \ I. M i) \ sets N" unfolding sets_PiM_single space[symmetric] by (intro sets.sigma_sets_subset subsetI) (auto intro: sets) -lemma sets_PiM_cong[measurable_cong]: +lemma%unimportant sets_PiM_cong[measurable_cong]: assumes "I = J" "\i. i \ J \ sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)" using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong) -lemma sets_PiM_I: +lemma%important sets_PiM_I: assumes "finite J" "J \ I" "\i\J. E i \ sets (M i)" shows "prod_emb I M J (\\<^sub>E j\J. E j) \ sets (\\<^sub>M i\I. M i)" -proof cases +proof%unimportant cases assume "J = {}" then have "prod_emb I M J (\\<^sub>E j\J. E j) = (\\<^sub>E j\I. space (M j))" by (auto simp: prod_emb_def) @@ -519,7 +520,7 @@ by (force simp add: sets_PiM prod_algebra_def) qed -proposition measurable_PiM: +lemma%unimportant measurable_PiM: assumes space: "f \ space N \ (\\<^sub>E i\I. space (M i))" assumes sets: "\X J. J \ {} \ I = {} \ finite J \ J \ I \ (\i. i \ J \ X i \ sets (M i)) \ f -` prod_emb I M J (Pi\<^sub>E J X) \ space N \ sets N" @@ -531,13 +532,13 @@ with sets[of J X] show "f -` A \ space N \ sets N" by auto qed -lemma measurable_PiM_Collect: +lemma%important measurable_PiM_Collect: assumes space: "f \ space N \ (\\<^sub>E i\I. space (M i))" assumes sets: "\X J. J \ {} \ I = {} \ finite J \ J \ I \ (\i. i \ J \ X i \ sets (M i)) \ {\\space N. \i\J. f \ i \ X i} \ sets N" shows "f \ measurable N (PiM I M)" using sets_PiM prod_algebra_sets_into_space space -proof (rule measurable_sigma_sets) +proof%unimportant (rule measurable_sigma_sets) fix A assume "A \ prod_algebra I M" from prod_algebraE[OF this] guess J X . note X = this then have "f -` A \ space N = {\ \ space N. \i\J. f \ i \ X i}" @@ -546,7 +547,7 @@ finally show "f -` A \ space N \ sets N" . qed -lemma measurable_PiM_single: +lemma%unimportant measurable_PiM_single: assumes space: "f \ space N \ (\\<^sub>E i\I. space (M i))" assumes sets: "\A i. i \ I \ A \ sets (M i) \ {\ \ space N. f \ i \ A} \ sets N" shows "f \ measurable N (PiM I M)" @@ -560,11 +561,11 @@ finally show "f -` A \ space N \ sets N" . qed (auto simp: space) -lemma measurable_PiM_single': +lemma%important measurable_PiM_single': assumes f: "\i. i \ I \ f i \ measurable N (M i)" and "(\\ i. f i \) \ space N \ (\\<^sub>E i\I. space (M i))" shows "(\\ i. f i \) \ measurable N (Pi\<^sub>M I M)" -proof (rule measurable_PiM_single) +proof%unimportant (rule measurable_PiM_single) fix A i assume A: "i \ I" "A \ sets (M i)" then have "{\ \ space N. f i \ \ A} = f i -` A \ space N" by auto @@ -572,12 +573,12 @@ using A f by (auto intro!: measurable_sets) qed fact -lemma sets_PiM_I_finite[measurable]: +lemma%unimportant sets_PiM_I_finite[measurable]: assumes "finite I" and sets: "(\i. i \ I \ E i \ sets (M i))" shows "(\\<^sub>E j\I. E j) \ sets (\\<^sub>M i\I. M i)" using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] \finite I\ sets by auto -lemma measurable_component_singleton[measurable (raw)]: +lemma%unimportant measurable_component_singleton[measurable (raw)]: assumes "i \ I" shows "(\x. x i) \ measurable (Pi\<^sub>M I M) (M i)" proof (unfold measurable_def, intro CollectI conjI ballI) fix A assume "A \ sets (M i)" @@ -588,30 +589,30 @@ using \A \ sets (M i)\ \i \ I\ by (auto intro!: sets_PiM_I) qed (insert \i \ I\, auto simp: space_PiM) -lemma measurable_component_singleton'[measurable_dest]: +lemma%unimportant measurable_component_singleton'[measurable_dest]: assumes f: "f \ measurable N (Pi\<^sub>M I M)" assumes g: "g \ measurable L N" assumes i: "i \ I" shows "(\x. (f (g x)) i) \ measurable L (M i)" using measurable_compose[OF measurable_compose[OF g f] measurable_component_singleton, OF i] . -lemma measurable_PiM_component_rev: +lemma%unimportant measurable_PiM_component_rev: "i \ I \ f \ measurable (M i) N \ (\x. f (x i)) \ measurable (PiM I M) N" by simp -lemma measurable_case_nat[measurable (raw)]: +lemma%unimportant measurable_case_nat[measurable (raw)]: assumes [measurable (raw)]: "i = 0 \ f \ measurable M N" "\j. i = Suc j \ (\x. g x j) \ measurable M N" shows "(\x. case_nat (f x) (g x) i) \ measurable M N" by (cases i) simp_all -lemma measurable_case_nat'[measurable (raw)]: +lemma%unimportant measurable_case_nat'[measurable (raw)]: assumes fg[measurable]: "f \ measurable N M" "g \ measurable N (\\<^sub>M i\UNIV. M)" shows "(\x. case_nat (f x) (g x)) \ measurable N (\\<^sub>M i\UNIV. M)" using fg[THEN measurable_space] by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split) -lemma measurable_add_dim[measurable]: +lemma%unimportant measurable_add_dim[measurable]: "(\(f, y). f(i := y)) \ measurable (Pi\<^sub>M I M \\<^sub>M M i) (Pi\<^sub>M (insert i I) M)" (is "?f \ measurable ?P ?I") proof (rule measurable_PiM_single) @@ -625,12 +626,12 @@ finally show "{\ \ space ?P. case_prod (\f. fun_upd f i) \ j \ A} \ sets ?P" . qed (auto simp: space_pair_measure space_PiM PiE_def) -proposition measurable_fun_upd: +lemma%important measurable_fun_upd: assumes I: "I = J \ {i}" assumes f[measurable]: "f \ measurable N (PiM J M)" assumes h[measurable]: "h \ measurable N (M i)" shows "(\x. (f x) (i := h x)) \ measurable N (PiM I M)" -proof (intro measurable_PiM_single') +proof%unimportant (intro measurable_PiM_single') fix j assume "j \ I" then show "(\\. ((f \)(i := h \)) j) \ measurable N (M j)" unfolding I by (cases "j = i") auto next @@ -639,14 +640,14 @@ by (auto simp: space_PiM PiE_iff extensional_def) qed -lemma measurable_component_update: +lemma%unimportant measurable_component_update: "x \ space (Pi\<^sub>M I M) \ i \ I \ (\v. x(i := v)) \ measurable (M i) (Pi\<^sub>M (insert i I) M)" by simp -lemma measurable_merge[measurable]: +lemma%important measurable_merge[measurable]: "merge I J \ measurable (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \ J) M)" (is "?f \ measurable ?P ?U") -proof (rule measurable_PiM_single) +proof%unimportant (rule measurable_PiM_single) fix i A assume A: "A \ sets (M i)" "i \ I \ J" then have "{\ \ space ?P. merge I J \ i \ A} = (if i \ I then ((\x. x i) \ fst) -` A \ space ?P else ((\x. x i) \ snd) -` A \ space ?P)" @@ -657,7 +658,7 @@ finally show "{\ \ space ?P. merge I J \ i \ A} \ sets ?P" . qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def) -lemma measurable_restrict[measurable (raw)]: +lemma%unimportant measurable_restrict[measurable (raw)]: assumes X: "\i. i \ I \ X i \ measurable N (M i)" shows "(\x. \i\I. X i x) \ measurable N (Pi\<^sub>M I M)" proof (rule measurable_PiM_single) @@ -668,14 +669,14 @@ using A X by (auto intro!: measurable_sets) qed (insert X, auto simp add: PiE_def dest: measurable_space) -lemma measurable_abs_UNIV: +lemma%unimportant measurable_abs_UNIV: "(\n. (\\. f n \) \ measurable M (N n)) \ (\\ n. f n \) \ measurable M (PiM UNIV N)" by (intro measurable_PiM_single) (auto dest: measurable_space) -lemma measurable_restrict_subset: "J \ L \ (\f. restrict f J) \ measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)" +lemma%unimportant measurable_restrict_subset: "J \ L \ (\f. restrict f J) \ measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)" by (intro measurable_restrict measurable_component_singleton) auto -lemma measurable_restrict_subset': +lemma%unimportant measurable_restrict_subset': assumes "J \ L" "\x. x \ J \ sets (M x) = sets (N x)" shows "(\f. restrict f J) \ measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)" proof- @@ -686,12 +687,12 @@ finally show ?thesis . qed -lemma measurable_prod_emb[intro, simp]: +lemma%unimportant measurable_prod_emb[intro, simp]: "J \ L \ X \ sets (Pi\<^sub>M J M) \ prod_emb L M J X \ sets (Pi\<^sub>M L M)" unfolding prod_emb_def space_PiM[symmetric] by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton) -lemma merge_in_prod_emb: +lemma%unimportant merge_in_prod_emb: assumes "y \ space (PiM I M)" "x \ X" and X: "X \ sets (Pi\<^sub>M J M)" and "J \ I" shows "merge J I (x, y) \ prod_emb I M J X" using assms sets.sets_into_space[OF X] @@ -699,7 +700,7 @@ cong: if_cong restrict_cong) (simp add: extensional_def) -lemma prod_emb_eq_emptyD: +lemma%unimportant prod_emb_eq_emptyD: assumes J: "J \ I" and ne: "space (PiM I M) \ {}" and X: "X \ sets (Pi\<^sub>M J M)" and *: "prod_emb I M J X = {}" shows "X = {}" @@ -710,19 +711,19 @@ from merge_in_prod_emb[OF this \x\X\ X J] * show "x \ {}" by auto qed -lemma sets_in_Pi_aux: +lemma%unimportant sets_in_Pi_aux: "finite I \ (\j. j \ I \ {x\space (M j). x \ F j} \ sets (M j)) \ {x\space (PiM I M). x \ Pi I F} \ sets (PiM I M)" by (simp add: subset_eq Pi_iff) -lemma sets_in_Pi[measurable (raw)]: +lemma%unimportant sets_in_Pi[measurable (raw)]: "finite I \ f \ measurable N (PiM I M) \ (\j. j \ I \ {x\space (M j). x \ F j} \ sets (M j)) \ Measurable.pred N (\x. f x \ Pi I F)" unfolding pred_def by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto -lemma sets_in_extensional_aux: +lemma%unimportant sets_in_extensional_aux: "{x\space (PiM I M). x \ extensional I} \ sets (PiM I M)" proof - have "{x\space (PiM I M). x \ extensional I} = space (PiM I M)" @@ -730,12 +731,12 @@ then show ?thesis by simp qed -lemma sets_in_extensional[measurable (raw)]: +lemma%unimportant sets_in_extensional[measurable (raw)]: "f \ measurable N (PiM I M) \ Measurable.pred N (\x. f x \ extensional I)" unfolding pred_def by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto -lemma sets_PiM_I_countable: +lemma%unimportant sets_PiM_I_countable: assumes I: "countable I" and E: "\i. i \ I \ E i \ sets (M i)" shows "Pi\<^sub>E I E \ sets (Pi\<^sub>M I M)" proof cases assume "I \ {}" @@ -746,11 +747,11 @@ finally show ?thesis . qed (simp add: sets_PiM_empty) -lemma sets_PiM_D_countable: +lemma%important sets_PiM_D_countable: assumes A: "A \ PiM I M" shows "\J\I. \X\PiM J M. countable J \ A = prod_emb I M J X" using A[unfolded sets_PiM_single] -proof induction +proof%unimportant induction case (Basic A) then obtain i X where *: "i \ I" "X \ sets (M i)" and "A = {f \ \\<^sub>E i\I. space (M i). f i \ X}" by auto @@ -782,12 +783,12 @@ qed(auto intro: X) qed -proposition measure_eqI_PiM_finite: +lemma%important measure_eqI_PiM_finite: assumes [simp]: "finite I" "sets P = PiM I M" "sets Q = PiM I M" assumes eq: "\A. (\i. i \ I \ A i \ sets (M i)) \ P (Pi\<^sub>E I A) = Q (Pi\<^sub>E I A)" assumes A: "range A \ prod_algebra I M" "(\i. A i) = space (PiM I M)" "\i::nat. P (A i) \ \" shows "P = Q" -proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) +proof%unimportant (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) show "range A \ prod_algebra I M" "(\i. A i) = (\\<^sub>E i\I. space (M i))" "\i. P (A i) \ \" unfolding space_PiM[symmetric] by fact+ fix X assume "X \ prod_algebra I M" @@ -798,13 +799,13 @@ unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq) qed (simp_all add: sets_PiM) -proposition measure_eqI_PiM_infinite: +lemma%important measure_eqI_PiM_infinite: assumes [simp]: "sets P = PiM I M" "sets Q = PiM I M" assumes eq: "\A J. finite J \ J \ I \ (\i. i \ J \ A i \ sets (M i)) \ P (prod_emb I M J (Pi\<^sub>E J A)) = Q (prod_emb I M J (Pi\<^sub>E J A))" assumes A: "finite_measure P" shows "P = Q" -proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) +proof%unimportant (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) interpret finite_measure P by fact define i where "i = (SOME i. i \ I)" have i: "I \ {} \ i \ I" @@ -838,12 +839,12 @@ fixes I :: "'i set" assumes finite_index: "finite I" -proposition (in finite_product_sigma_finite) sigma_finite_pairs: +lemma%important (in finite_product_sigma_finite) sigma_finite_pairs: "\F::'i \ nat \ 'a set. (\i\I. range (F i) \ sets (M i)) \ (\k. \i\I. emeasure (M i) (F i k) \ \) \ incseq (\k. \\<^sub>E i\I. F i k) \ (\k. \\<^sub>E i\I. F i k) = space (PiM I M)" -proof - +proof%unimportant - have "\i::'i. \F::nat \ 'a set. range F \ sets (M i) \ incseq F \ (\i. F i) = space (M i) \ (\k. emeasure (M i) (F k) \ \)" using M.sigma_finite_incseq by metis from choice[OF this] guess F :: "'i \ nat \ 'a set" .. @@ -869,7 +870,7 @@ qed qed -lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\_. undefined} = 1" +lemma%unimportant emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\_. undefined} = 1" proof - let ?\ = "\A. if A = {} then 0 else (1::ennreal)" have "emeasure (Pi\<^sub>M {} M) (prod_emb {} M {} (\\<^sub>E i\{}. {})) = 1" @@ -886,12 +887,12 @@ by simp qed -lemma PiM_empty: "PiM {} M = count_space {\_. undefined}" +lemma%unimportant PiM_empty: "PiM {} M = count_space {\_. undefined}" by (rule measure_eqI) (auto simp add: sets_PiM_empty) -lemma (in product_sigma_finite) emeasure_PiM: +lemma%important (in product_sigma_finite) emeasure_PiM: "finite I \ (\i. i\I \ A i \ sets (M i)) \ emeasure (PiM I M) (Pi\<^sub>E I A) = (\i\I. emeasure (M i) (A i))" -proof (induct I arbitrary: A rule: finite_induct) +proof%unimportant (induct I arbitrary: A rule: finite_induct) case (insert i I) interpret finite_product_sigma_finite M I by standard fact have "finite (insert i I)" using \finite I\ by auto @@ -946,7 +947,7 @@ by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space) qed simp -lemma (in product_sigma_finite) PiM_eqI: +lemma%unimportant (in product_sigma_finite) PiM_eqI: assumes I[simp]: "finite I" and P: "sets P = PiM I M" assumes eq: "\A. (\i. i \ I \ A i \ sets (M i)) \ P (Pi\<^sub>E I A) = (\i\I. emeasure (M i) (A i))" shows "P = PiM I M" @@ -964,7 +965,7 @@ qed qed -lemma (in product_sigma_finite) sigma_finite: +lemma%unimportant (in product_sigma_finite) sigma_finite: assumes "finite I" shows "sigma_finite_measure (PiM I M)" proof @@ -985,11 +986,11 @@ sublocale finite_product_sigma_finite \ sigma_finite_measure "Pi\<^sub>M I M" using sigma_finite[OF finite_index] . -lemma (in finite_product_sigma_finite) measure_times: +lemma%unimportant (in finite_product_sigma_finite) measure_times: "(\i. i \ I \ A i \ sets (M i)) \ emeasure (Pi\<^sub>M I M) (Pi\<^sub>E I A) = (\i\I. emeasure (M i) (A i))" using emeasure_PiM[OF finite_index] by auto -lemma (in product_sigma_finite) nn_integral_empty: +lemma%unimportant (in product_sigma_finite) nn_integral_empty: "0 \ f (\k. undefined) \ integral\<^sup>N (Pi\<^sub>M {} M) f = f (\k. undefined)" by (simp add: PiM_empty nn_integral_count_space_finite max.absorb2) @@ -997,7 +998,7 @@ assumes IJ[simp]: "I \ J = {}" and fin: "finite I" "finite J" shows "distr (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \ J) M) (merge I J) = Pi\<^sub>M (I \ J) M" (is "?D = ?P") -proof (rule PiM_eqI) +proof%unimportant (rule PiM_eqI) interpret I: finite_product_sigma_finite M I by standard fact interpret J: finite_product_sigma_finite M J by standard fact fix A assume A: "\i. i \ I \ J \ A i \ sets (M i)" @@ -1009,12 +1010,12 @@ (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times prod.union_disjoint) qed (insert fin, simp_all) -proposition (in product_sigma_finite) product_nn_integral_fold: +lemma%important (in product_sigma_finite) product_nn_integral_fold: assumes IJ: "I \ J = {}" "finite I" "finite J" and f[measurable]: "f \ borel_measurable (Pi\<^sub>M (I \ J) M)" shows "integral\<^sup>N (Pi\<^sub>M (I \ J) M) f = (\\<^sup>+ x. (\\<^sup>+ y. f (merge I J (x, y)) \(Pi\<^sub>M J M)) \(Pi\<^sub>M I M))" -proof - +proof%unimportant - interpret I: finite_product_sigma_finite M I by standard fact interpret J: finite_product_sigma_finite M J by standard fact interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard @@ -1029,7 +1030,7 @@ done qed -lemma (in product_sigma_finite) distr_singleton: +lemma%unimportant (in product_sigma_finite) distr_singleton: "distr (Pi\<^sub>M {i} M) (M i) (\x. x i) = M i" (is "?D = _") proof (intro measure_eqI[symmetric]) interpret I: finite_product_sigma_finite M "{i}" by standard simp @@ -1041,7 +1042,7 @@ by (simp add: emeasure_distr measurable_component_singleton) qed simp -lemma (in product_sigma_finite) product_nn_integral_singleton: +lemma%unimportant (in product_sigma_finite) product_nn_integral_singleton: assumes f: "f \ borel_measurable (M i)" shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\x. f (x i)) = integral\<^sup>N (M i) f" proof - @@ -1053,11 +1054,11 @@ done qed -proposition (in product_sigma_finite) product_nn_integral_insert: +lemma%important (in product_sigma_finite) product_nn_integral_insert: assumes I[simp]: "finite I" "i \ I" and f: "f \ borel_measurable (Pi\<^sub>M (insert i I) M)" shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\\<^sup>+ x. (\\<^sup>+ y. f (x(i := y)) \(M i)) \(Pi\<^sub>M I M))" -proof - +proof%unimportant - interpret I: finite_product_sigma_finite M I by standard auto interpret i: finite_product_sigma_finite M "{i}" by standard auto have IJ: "I \ {i} = {}" and insert: "I \ {i} = insert i I" @@ -1077,7 +1078,7 @@ qed qed -lemma (in product_sigma_finite) product_nn_integral_insert_rev: +lemma%unimportant (in product_sigma_finite) product_nn_integral_insert_rev: assumes I[simp]: "finite I" "i \ I" and [measurable]: "f \ borel_measurable (Pi\<^sub>M (insert i I) M)" shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\\<^sup>+ y. (\\<^sup>+ x. f (x(i := y)) \(Pi\<^sub>M I M)) \(M i))" @@ -1088,7 +1089,7 @@ apply measurable done -lemma (in product_sigma_finite) product_nn_integral_prod: +lemma%unimportant (in product_sigma_finite) product_nn_integral_prod: assumes "finite I" "\i. i \ I \ f i \ borel_measurable (M i)" shows "(\\<^sup>+ x. (\i\I. f i (x i)) \Pi\<^sub>M I M) = (\i\I. integral\<^sup>N (M i) (f i))" using assms proof (induction I) @@ -1111,11 +1112,11 @@ done qed (simp add: space_PiM) -proposition (in product_sigma_finite) product_nn_integral_pair: +lemma%important (in product_sigma_finite) product_nn_integral_pair: assumes [measurable]: "case_prod f \ borel_measurable (M x \\<^sub>M M y)" assumes xy: "x \ y" shows "(\\<^sup>+\. f (\ x) (\ y) \PiM {x, y} M) = (\\<^sup>+z. f (fst z) (snd z) \(M x \\<^sub>M M y))" -proof - +proof%unimportant - interpret psm: pair_sigma_finite "M x" "M y" unfolding pair_sigma_finite_def using sigma_finite_measures by simp_all have "{x, y} = {y, x}" by auto @@ -1128,7 +1129,7 @@ finally show ?thesis . qed -lemma (in product_sigma_finite) distr_component: +lemma%unimportant (in product_sigma_finite) distr_component: "distr (M i) (Pi\<^sub>M {i} M) (\x. \i\{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P") proof (intro PiM_eqI) fix A assume A: "\ia. ia \ {i} \ A ia \ sets (M ia)" @@ -1138,7 +1139,7 @@ by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict) qed simp_all -lemma (in product_sigma_finite) +lemma%unimportant (in product_sigma_finite) assumes IJ: "I \ J = {}" "finite I" "finite J" and A: "A \ sets (Pi\<^sub>M (I \ J) M)" shows emeasure_fold_integral: "emeasure (Pi\<^sub>M (I \ J) M) A = (\\<^sup>+x. emeasure (Pi\<^sub>M J M) ((\y. merge I J (x, y)) -` A \ space (Pi\<^sub>M J M)) \Pi\<^sub>M I M)" (is ?I) @@ -1163,11 +1164,11 @@ by (simp add: vimage_comp comp_def space_pair_measure cong: measurable_cong) qed -lemma sets_Collect_single: +lemma%unimportant sets_Collect_single: "i \ I \ A \ sets (M i) \ { x \ space (Pi\<^sub>M I M). x i \ A } \ sets (Pi\<^sub>M I M)" by simp -lemma pair_measure_eq_distr_PiM: +lemma%unimportant pair_measure_eq_distr_PiM: fixes M1 :: "'a measure" and M2 :: "'a measure" assumes "sigma_finite_measure M1" "sigma_finite_measure M2" shows "(M1 \\<^sub>M M2) = distr (Pi\<^sub>M UNIV (case_bool M1 M2)) (M1 \\<^sub>M M2) (\x. (x True, x False))" @@ -1194,7 +1195,7 @@ by (subst emeasure_distr) (auto simp: measurable_pair_iff) qed simp -lemma infprod_in_sets[intro]: +lemma%unimportant infprod_in_sets[intro]: fixes E :: "nat \ 'a set" assumes E: "\i. E i \ sets (M i)" shows "Pi UNIV E \ sets (\\<^sub>M i\UNIV::nat set. M i)" proof - diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Function_Topology.thy --- a/src/HOL/Analysis/Function_Topology.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Function_Topology.thy Thu Jan 17 16:22:21 2019 -0500 @@ -61,8 +61,6 @@ I realized afterwards that this theory has a lot in common with \<^file>\~~/src/HOL/Library/Finite_Map.thy\. \ - - subsection%important \Topology without type classes\ subsubsection%important \The topology generated by some (open) subsets\ @@ -80,14 +78,14 @@ | UN: "(\k. k \ K \ generate_topology_on S k) \ generate_topology_on S (\K)" | Basis: "s \ S \ generate_topology_on S s" -lemma istopology_generate_topology_on: +lemma%unimportant istopology_generate_topology_on: "istopology (generate_topology_on S)" unfolding istopology_def by (auto intro: generate_topology_on.intros) text \The basic property of the topology generated by a set \S\ is that it is the smallest topology containing all the elements of \S\:\ -lemma generate_topology_on_coarsest: +lemma%unimportant generate_topology_on_coarsest: assumes "istopology T" "\s. s \ S \ T s" "generate_topology_on S s0" @@ -98,17 +96,17 @@ abbreviation%unimportant topology_generated_by::"('a set set) \ ('a topology)" where "topology_generated_by S \ topology (generate_topology_on S)" -lemma openin_topology_generated_by_iff: +lemma%unimportant openin_topology_generated_by_iff: "openin (topology_generated_by S) s \ generate_topology_on S s" using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp -lemma openin_topology_generated_by: +lemma%unimportant openin_topology_generated_by: "openin (topology_generated_by S) s \ generate_topology_on S s" using openin_topology_generated_by_iff by auto -lemma topology_generated_by_topspace: +lemma%important topology_generated_by_topspace: "topspace (topology_generated_by S) = (\S)" -proof +proof%unimportant { fix s assume "openin (topology_generated_by S) s" then have "generate_topology_on S s" by (rule openin_topology_generated_by) @@ -123,9 +121,9 @@ unfolding topspace_def using openin_topology_generated_by_iff by auto qed -lemma topology_generated_by_Basis: +lemma%important topology_generated_by_Basis: "s \ S \ openin (topology_generated_by S) s" - by (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis) +by%unimportant (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis) lemma generate_topology_on_Inter: "\finite \; \K. K \ \ \ generate_topology_on \ K; \ \ {}\ \ generate_topology_on \ (\\)" @@ -268,28 +266,28 @@ where "continuous_on_topo T1 T2 f = ((\ U. openin T2 U \ openin T1 (f-`U \ topspace(T1))) \ (f`(topspace T1) \ (topspace T2)))" -lemma continuous_on_continuous_on_topo: +lemma%important continuous_on_continuous_on_topo: "continuous_on s f \ continuous_on_topo (subtopology euclidean s) euclidean f" - unfolding continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def +unfolding%unimportant continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def topspace_euclidean_subtopology open_openin topspace_euclidean by fast -lemma continuous_on_topo_UNIV: +lemma%unimportant continuous_on_topo_UNIV: "continuous_on UNIV f \ continuous_on_topo euclidean euclidean f" using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto -lemma continuous_on_topo_open [intro]: +lemma%important continuous_on_topo_open [intro]: "continuous_on_topo T1 T2 f \ openin T2 U \ openin T1 (f-`U \ topspace(T1))" - unfolding continuous_on_topo_def by auto +unfolding%unimportant continuous_on_topo_def by auto -lemma continuous_on_topo_topspace [intro]: +lemma%unimportant continuous_on_topo_topspace [intro]: "continuous_on_topo T1 T2 f \ f`(topspace T1) \ (topspace T2)" unfolding continuous_on_topo_def by auto -lemma continuous_on_generated_topo_iff: +lemma%important continuous_on_generated_topo_iff: "continuous_on_topo T1 (topology_generated_by S) f \ ((\U. U \ S \ openin T1 (f-`U \ topspace(T1))) \ (f`(topspace T1) \ (\ S)))" unfolding continuous_on_topo_def topology_generated_by_topspace -proof (auto simp add: topology_generated_by_Basis) +proof%unimportant (auto simp add: topology_generated_by_Basis) assume H: "\U. U \ S \ openin T1 (f -` U \ topspace T1)" fix U assume "openin (topology_generated_by S) U" then have "generate_topology_on S U" by (rule openin_topology_generated_by) @@ -311,17 +309,17 @@ qed (auto simp add: H) qed -lemma continuous_on_generated_topo: +lemma%important continuous_on_generated_topo: assumes "\U. U \S \ openin T1 (f-`U \ topspace(T1))" "f`(topspace T1) \ (\ S)" shows "continuous_on_topo T1 (topology_generated_by S) f" - using assms continuous_on_generated_topo_iff by blast +using%unimportant assms continuous_on_generated_topo_iff by blast -proposition continuous_on_topo_compose: +lemma%important continuous_on_topo_compose: assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g" shows "continuous_on_topo T1 T3 (g o f)" - using assms unfolding continuous_on_topo_def -proof (auto) +using%unimportant assms unfolding continuous_on_topo_def +proof%unimportant (auto) fix U :: "'c set" assume H: "openin T3 U" have "openin T1 (f -` (g -` U \ topspace T2) \ topspace T1)" @@ -332,7 +330,7 @@ by simp qed (blast) -lemma continuous_on_topo_preimage_topspace [intro]: +lemma%unimportant continuous_on_topo_preimage_topspace [intro]: assumes "continuous_on_topo T1 T2 f" shows "f-`(topspace T2) \ topspace T1 = topspace T1" using assms unfolding continuous_on_topo_def by auto @@ -351,9 +349,9 @@ definition%important pullback_topology::"('a set) \ ('a \ 'b) \ ('b topology) \ ('a topology)" where "pullback_topology A f T = topology (\S. \U. openin T U \ S = f-`U \ A)" -lemma istopology_pullback_topology: +lemma%important istopology_pullback_topology: "istopology (\S. \U. openin T U \ S = f-`U \ A)" - unfolding istopology_def proof (auto) +unfolding%unimportant istopology_def proof (auto) fix K assume "\S\K. \U. openin T U \ S = f -` U \ A" then have "\U. \S\K. openin T (U S) \ S = f-`(U S) \ A" by (rule bchoice) @@ -364,19 +362,19 @@ then show "\V. openin T V \ \K = f -` V \ A" by auto qed -lemma openin_pullback_topology: +lemma%unimportant openin_pullback_topology: "openin (pullback_topology A f T) S \ (\U. openin T U \ S = f-`U \ A)" unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto -lemma topspace_pullback_topology: +lemma%unimportant topspace_pullback_topology: "topspace (pullback_topology A f T) = f-`(topspace T) \ A" by (auto simp add: topspace_def openin_pullback_topology) -proposition continuous_on_topo_pullback [intro]: +lemma%important continuous_on_topo_pullback [intro]: assumes "continuous_on_topo T1 T2 g" shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)" unfolding continuous_on_topo_def -proof (auto) +proof%unimportant (auto) fix U::"'b set" assume "openin T2 U" then have "openin T1 (g-`U \ topspace T1)" using assms unfolding continuous_on_topo_def by auto @@ -396,11 +394,11 @@ using assms unfolding continuous_on_topo_def by auto qed -proposition continuous_on_topo_pullback' [intro]: +lemma%important continuous_on_topo_pullback' [intro]: assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \ g-`A" shows "continuous_on_topo T1 (pullback_topology A f T2) g" unfolding continuous_on_topo_def -proof (auto) +proof%unimportant (auto) fix U assume "openin (pullback_topology A f T2) U" then have "\V. openin T2 V \ U = f-`V \ A" unfolding openin_pullback_topology by auto @@ -549,9 +547,9 @@ done qed -lemma topspace_product_topology: +lemma%important topspace_product_topology: "topspace (product_topology T I) = (\\<^sub>E i\I. topspace(T i))" -proof +proof%unimportant show "topspace (product_topology T I) \ (\\<^sub>E i\I. topspace (T i))" unfolding product_topology_def topology_generated_by_topspace unfolding topspace_def by auto @@ -561,16 +559,16 @@ unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace) qed -lemma product_topology_basis: +lemma%unimportant product_topology_basis: assumes "\i. openin (T i) (X i)" "finite {i. X i \ topspace (T i)}" shows "openin (product_topology T I) (\\<^sub>E i\I. X i)" unfolding product_topology_def by (rule topology_generated_by_Basis) (use assms in auto) -proposition product_topology_open_contains_basis: +lemma%important product_topology_open_contains_basis: assumes "openin (product_topology T I) U" "x \ U" shows "\X. x \ (\\<^sub>E i\I. X i) \ (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)} \ (\\<^sub>E i\I. X i) \ U" -proof - +proof%unimportant - have "generate_topology_on {(\\<^sub>E i\I. X i) |X. (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)}} U" using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto then have "\x. x\U \ \X. x \ (\\<^sub>E i\I. X i) \ (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)} \ (\\<^sub>E i\I. X i) \ U" @@ -719,7 +717,7 @@ text \The basic property of the product topology is the continuity of projections:\ -lemma continuous_on_topo_product_coordinates [simp]: +lemma%unimportant continuous_on_topo_product_coordinates [simp]: assumes "i \ I" shows "continuous_on_topo (product_topology T I) (T i) (\x. x i)" proof - @@ -741,12 +739,12 @@ by (auto simp add: assms topspace_product_topology PiE_iff) qed -lemma continuous_on_topo_coordinatewise_then_product [intro]: +lemma%important continuous_on_topo_coordinatewise_then_product [intro]: assumes "\i. i \ I \ continuous_on_topo T1 (T i) (\x. f x i)" "\i x. i \ I \ x \ topspace T1 \ f x i = undefined" shows "continuous_on_topo T1 (product_topology T I) f" unfolding product_topology_def -proof (rule continuous_on_generated_topo) +proof%unimportant (rule continuous_on_generated_topo) fix U assume "U \ {Pi\<^sub>E I X |X. (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)}}" then obtain X where H: "U = Pi\<^sub>E I X" "\i. openin (T i) (X i)" "finite {i. X i \ topspace (T i)}" by blast @@ -774,7 +772,7 @@ using assms unfolding continuous_on_topo_def by auto qed -lemma continuous_on_topo_product_then_coordinatewise [intro]: +lemma%unimportant continuous_on_topo_product_then_coordinatewise [intro]: assumes "continuous_on_topo T1 (product_topology T I) f" shows "\i. i \ I \ continuous_on_topo T1 (T i) (\x. f x i)" "\i x. i \ I \ x \ topspace T1 \ f x i = undefined" @@ -796,7 +794,7 @@ using \i \ I\ by (auto simp add: PiE_iff extensional_def) qed -lemma continuous_on_restrict: +lemma%unimportant continuous_on_restrict: assumes "J \ I" shows "continuous_on_topo (product_topology T I) (product_topology T J) (\x. restrict x J)" proof (rule continuous_on_topo_coordinatewise_then_product) @@ -819,7 +817,7 @@ definition%important open_fun_def: "open U = openin (product_topology (\i. euclidean) UNIV) U" -instance proof +instance proof%unimportant have "topspace (product_topology (\(i::'a). euclidean::('b topology)) UNIV) = UNIV" unfolding topspace_product_topology topspace_euclidean by auto then show "open (UNIV::('a \ 'b) set)" @@ -828,15 +826,15 @@ end -lemma euclidean_product_topology: +lemma%unimportant euclidean_product_topology: "euclidean = product_topology (\i. euclidean::('b::topological_space) topology) UNIV" by (metis open_openin topology_eq open_fun_def) -proposition product_topology_basis': +lemma%important product_topology_basis': fixes x::"'i \ 'a" and U::"'i \ ('b::topological_space) set" assumes "finite I" "\i. i \ I \ open (U i)" shows "open {f. \i\I. f (x i) \ U i}" -proof - +proof%unimportant - define J where "J = x`I" define V where "V = (\y. if y \ J then \{U i|i. i\I \ x i = y} else UNIV)" define X where "X = (\y. if y \ J then V y else UNIV)" @@ -866,24 +864,24 @@ text \The results proved in the general situation of products of possibly different spaces have their counterparts in this simpler setting.\ -lemma continuous_on_product_coordinates [simp]: +lemma%unimportant continuous_on_product_coordinates [simp]: "continuous_on UNIV (\x. x i::('b::topological_space))" unfolding continuous_on_topo_UNIV euclidean_product_topology by (rule continuous_on_topo_product_coordinates, simp) -lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]: +lemma%unimportant continuous_on_coordinatewise_then_product [intro, continuous_intros]: assumes "\i. continuous_on UNIV (\x. f x i)" shows "continuous_on UNIV f" using assms unfolding continuous_on_topo_UNIV euclidean_product_topology by (rule continuous_on_topo_coordinatewise_then_product, simp) -lemma continuous_on_product_then_coordinatewise: +lemma%unimportant continuous_on_product_then_coordinatewise: assumes "continuous_on UNIV f" shows "continuous_on UNIV (\x. f x i)" using assms unfolding continuous_on_topo_UNIV euclidean_product_topology by (rule continuous_on_topo_product_then_coordinatewise(1), simp) -lemma continuous_on_product_coordinatewise_iff: +lemma%unimportant continuous_on_product_coordinatewise_iff: "continuous_on UNIV f \ (\i. continuous_on UNIV (\x. f x i))" by (auto intro: continuous_on_product_then_coordinatewise) @@ -893,7 +891,7 @@ of product spaces, but they have more to do with countability and could be put in the corresponding theory.\ -lemma countable_nat_product_event_const: +lemma%unimportant countable_nat_product_event_const: fixes F::"'a set" and a::'a assumes "a \ F" "countable F" shows "countable {x::(nat \ 'a). (\i. x i \ F) \ finite {i. x i \ a}}" @@ -930,7 +928,7 @@ then show ?thesis using countable_subset[OF *] by auto qed -lemma countable_product_event_const: +lemma%unimportant countable_product_event_const: fixes F::"('a::countable) \ 'b set" and b::'b assumes "\i. countable (F i)" shows "countable {f::('a \ 'b). (\i. f i \ F i) \ (finite {i. f i \ b})}" @@ -963,7 +961,7 @@ qed instance "fun" :: (countable, first_countable_topology) first_countable_topology -proof +proof%unimportant fix x::"'a \ 'b" have "\A::('b \ nat \ 'b set). \x. (\i. x \ A x i \ open (A x i)) \ (\S. open S \ x \ S \ (\i. A x i \ S))" apply (rule choice) using first_countable_basis by auto @@ -1035,11 +1033,11 @@ using \countable K\ \\k. k \ K \ x \ k\ \\k. k \ K \ open k\ Inc by auto qed -proposition product_topology_countable_basis: +lemma%important product_topology_countable_basis: shows "\K::(('a::countable \ 'b::second_countable_topology) set set). topological_basis K \ countable K \ (\k\K. \X. (k = Pi\<^sub>E UNIV X) \ (\i. open (X i)) \ finite {i. X i \ UNIV})" -proof - +proof%unimportant - obtain B::"'b set set" where B: "countable B \ topological_basis B" using ex_countable_basis by auto then have "B \ {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE) @@ -1142,15 +1140,15 @@ definition%important strong_operator_topology::"('a::real_normed_vector \\<^sub>L'b::real_normed_vector) topology" where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean" -lemma strong_operator_topology_topspace: +lemma%unimportant strong_operator_topology_topspace: "topspace strong_operator_topology = UNIV" unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto -lemma strong_operator_topology_basis: +lemma%important strong_operator_topology_basis: fixes f::"('a::real_normed_vector \\<^sub>L'b::real_normed_vector)" and U::"'i \ 'b set" and x::"'i \ 'a" assumes "finite I" "\i. i \ I \ open (U i)" shows "openin strong_operator_topology {f. \i\I. blinfun_apply f (x i) \ U i}" -proof - +proof%unimportant - have "open {g::('a\'b). \i\I. g (x i) \ U i}" by (rule product_topology_basis'[OF assms]) moreover have "{f. \i\I. blinfun_apply f (x i) \ U i} @@ -1160,16 +1158,16 @@ unfolding strong_operator_topology_def open_openin apply (subst openin_pullback_topology) by auto qed -lemma strong_operator_topology_continuous_evaluation: +lemma%important strong_operator_topology_continuous_evaluation: "continuous_on_topo strong_operator_topology euclidean (\f. blinfun_apply f x)" -proof - +proof%unimportant - have "continuous_on_topo strong_operator_topology euclidean ((\f. f x) o blinfun_apply)" unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback) using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce then show ?thesis unfolding comp_def by simp qed -lemma continuous_on_strong_operator_topo_iff_coordinatewise: +lemma%unimportant continuous_on_strong_operator_topo_iff_coordinatewise: "continuous_on_topo T strong_operator_topology f \ (\x. continuous_on_topo T euclidean (\y. blinfun_apply (f y) x))" proof (auto) @@ -1192,9 +1190,9 @@ by (auto simp add: \continuous_on_topo T euclidean (blinfun_apply o f)\) qed -lemma strong_operator_topology_weaker_than_euclidean: +lemma%important strong_operator_topology_weaker_than_euclidean: "continuous_on_topo euclidean strong_operator_topology (\f. f)" - by (subst continuous_on_strong_operator_topo_iff_coordinatewise, +by%unimportant (subst continuous_on_strong_operator_topo_iff_coordinatewise, auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on) @@ -1228,9 +1226,9 @@ spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how to do this.\ -lemma dist_fun_le_dist_first_terms: +lemma%important dist_fun_le_dist_first_terms: "dist x y \ 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \ N} + (1/2)^N" -proof - +proof%unimportant - have "(\n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1) = (\n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))" by (rule suminf_cong, simp add: power_add) @@ -1278,7 +1276,7 @@ finally show ?thesis unfolding M_def by simp qed -lemma open_fun_contains_ball_aux: +lemma%unimportant open_fun_contains_ball_aux: assumes "open (U::(('a \ 'b) set))" "x \ U" shows "\e>0. {y. dist x y < e} \ U" @@ -1341,7 +1339,7 @@ then show "\m>0. {y. dist x y < m} \ U" using * by blast qed -lemma ball_fun_contains_open_aux: +lemma%unimportant ball_fun_contains_open_aux: fixes x::"('a \ 'b)" and e::real assumes "e>0" shows "\U. open U \ x \ U \ U \ {y. dist x y < e}" @@ -1388,7 +1386,7 @@ ultimately show ?thesis by auto qed -lemma fun_open_ball_aux: +lemma%unimportant fun_open_ball_aux: fixes U::"('a \ 'b) set" shows "open U \ (\x\U. \e>0. \y. dist x y < e \ y \ U)" proof (auto) @@ -1577,7 +1575,7 @@ -subsection%important \Measurability\ (*FIX ME move? *) +subsection%important \Measurability\ (*FIX ME mv *) text \There are two natural sigma-algebras on a product space: the borel sigma algebra, generated by open sets in the product, and the product sigma algebra, countably generated by @@ -1595,11 +1593,11 @@ compare it with the product sigma algebra as explained above. \ -lemma measurable_product_coordinates [measurable (raw)]: +lemma%unimportant measurable_product_coordinates [measurable (raw)]: "(\x. x i) \ measurable borel borel" by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates]) -lemma measurable_product_then_coordinatewise: +lemma%unimportant measurable_product_then_coordinatewise: fixes f::"'a \ 'b \ ('c::topological_space)" assumes [measurable]: "f \ borel_measurable M" shows "(\x. f x i) \ borel_measurable M" @@ -1613,10 +1611,10 @@ of the product sigma algebra that is more similar to the one we used above for the product topology.\ -lemma sets_PiM_finite: +lemma%important sets_PiM_finite: "sets (Pi\<^sub>M I M) = sigma_sets (\\<^sub>E i\I. space (M i)) {(\\<^sub>E i\I. X i) |X. (\i. X i \ sets (M i)) \ finite {i. X i \ space (M i)}}" -proof +proof%unimportant have "{(\\<^sub>E i\I. X i) |X. (\i. X i \ sets (M i)) \ finite {i. X i \ space (M i)}} \ sets (Pi\<^sub>M I M)" proof (auto) fix X assume H: "\i. X i \ sets (M i)" "finite {i. X i \ space (M i)}" @@ -1656,9 +1654,9 @@ done qed -lemma sets_PiM_subset_borel: +lemma%important sets_PiM_subset_borel: "sets (Pi\<^sub>M UNIV (\_. borel)) \ sets borel" -proof - +proof%unimportant - have *: "Pi\<^sub>E UNIV X \ sets borel" if [measurable]: "\i. X i \ sets borel" "finite {i. X i \ UNIV}" for X::"'a \ 'b set" proof - define I where "I = {i. X i \ UNIV}" @@ -1675,9 +1673,9 @@ by (simp add: * sets.sigma_sets_subset') qed -proposition sets_PiM_equal_borel: +lemma%important sets_PiM_equal_borel: "sets (Pi\<^sub>M UNIV (\i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel" -proof +proof%unimportant obtain K::"('a \ 'b) set set" where K: "topological_basis K" "countable K" "\k. k \ K \ \X. (k = Pi\<^sub>E UNIV X) \ (\i. open (X i)) \ finite {i. X i \ UNIV}" using product_topology_countable_basis by fast @@ -1702,11 +1700,11 @@ unfolding borel_def by auto qed (simp add: sets_PiM_subset_borel) -lemma measurable_coordinatewise_then_product: +lemma%important measurable_coordinatewise_then_product: fixes f::"'a \ ('b::countable) \ ('c::second_countable_topology)" assumes [measurable]: "\i. (\x. f x i) \ borel_measurable M" shows "f \ borel_measurable M" -proof - +proof%unimportant - have "f \ measurable M (Pi\<^sub>M UNIV (\_. borel))" by (rule measurable_PiM_single', auto simp add: assms) then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Further_Topology.thy --- a/src/HOL/Analysis/Further_Topology.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Further_Topology.thy Thu Jan 17 16:22:21 2019 -0500 @@ -1,4 +1,4 @@ -section%important \Extending Continous Maps, Invariance of Domain, etc\ (*FIX rename? *) +section%important \Extending Continous Maps, Invariance of Domain, etc\ text\Ported from HOL Light (moretop.ml) by L C Paulson\ @@ -8,13 +8,13 @@ subsection%important\A map from a sphere to a higher dimensional sphere is nullhomotopic\ -lemma spheremap_lemma1: +lemma%important spheremap_lemma1: fixes f :: "'a::euclidean_space \ 'a::euclidean_space" assumes "subspace S" "subspace T" and dimST: "dim S < dim T" and "S \ T" and diff_f: "f differentiable_on sphere 0 1 \ S" shows "f ` (sphere 0 1 \ S) \ sphere 0 1 \ T" -proof +proof%unimportant assume fim: "f ` (sphere 0 1 \ S) = sphere 0 1 \ T" have inS: "\x. \x \ S; x \ 0\ \ (x /\<^sub>R norm x) \ S" using subspace_mul \subspace S\ by blast @@ -158,14 +158,14 @@ qed -lemma spheremap_lemma2: +lemma%important spheremap_lemma2: fixes f :: "'a::euclidean_space \ 'a::euclidean_space" assumes ST: "subspace S" "subspace T" "dim S < dim T" and "S \ T" and contf: "continuous_on (sphere 0 1 \ S) f" and fim: "f ` (sphere 0 1 \ S) \ sphere 0 1 \ T" shows "\c. homotopic_with (\x. True) (sphere 0 1 \ S) (sphere 0 1 \ T) f (\x. c)" -proof - +proof%unimportant - have [simp]: "\x. \norm x = 1; x \ S\ \ norm (f x) = 1" using fim by (simp add: image_subset_iff) have "compact (sphere 0 1 \ S)" @@ -252,11 +252,11 @@ qed -lemma spheremap_lemma3: +lemma%important spheremap_lemma3: assumes "bounded S" "convex S" "subspace U" and affSU: "aff_dim S \ dim U" obtains T where "subspace T" "T \ U" "S \ {} \ aff_dim T = aff_dim S" "(rel_frontier S) homeomorphic (sphere 0 1 \ T)" -proof (cases "S = {}") +proof%unimportant (cases "S = {}") case True with \subspace U\ subspace_0 show ?thesis by (rule_tac T = "{0}" in that) auto @@ -300,14 +300,14 @@ qed -proposition inessential_spheremap_lowdim_gen: +proposition%important inessential_spheremap_lowdim_gen: fixes f :: "'M::euclidean_space \ 'a::euclidean_space" assumes "convex S" "bounded S" "convex T" "bounded T" and affST: "aff_dim S < aff_dim T" and contf: "continuous_on (rel_frontier S) f" and fim: "f ` (rel_frontier S) \ rel_frontier T" obtains c where "homotopic_with (\z. True) (rel_frontier S) (rel_frontier T) f (\x. c)" -proof (cases "S = {}") +proof%unimportant (cases "S = {}") case True then show ?thesis by (simp add: that) @@ -350,7 +350,7 @@ qed qed -lemma inessential_spheremap_lowdim: +lemma%unimportant inessential_spheremap_lowdim: fixes f :: "'M::euclidean_space \ 'a::euclidean_space" assumes "DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ` (sphere a r) \ (sphere b s)" @@ -379,7 +379,7 @@ subsection%important\ Some technical lemmas about extending maps from cell complexes\ -lemma extending_maps_Union_aux: +lemma%unimportant extending_maps_Union_aux: assumes fin: "finite \" and "\S. S \ \ \ closed S" and "\S T. \S \ \; T \ \; S \ T\ \ S \ T \ K" @@ -410,7 +410,7 @@ done qed -lemma extending_maps_Union: +lemma%unimportant extending_maps_Union: assumes fin: "finite \" and "\S. S \ \ \ \g. continuous_on S g \ g ` S \ T \ (\x \ S \ K. g x = h x)" and "\S. S \ \ \ closed S" @@ -422,14 +422,14 @@ by (metis K psubsetI) -lemma extend_map_lemma: +lemma%important extend_map_lemma: assumes "finite \" "\ \ \" "convex T" "bounded T" and poly: "\X. X \ \ \ polytope X" and aff: "\X. X \ \ - \ \ aff_dim X < aff_dim T" and face: "\S T. \S \ \; T \ \\ \ (S \ T) face_of S \ (S \ T) face_of T" and contf: "continuous_on (\\) f" and fim: "f ` (\\) \ rel_frontier T" obtains g where "continuous_on (\\) g" "g ` (\\) \ rel_frontier T" "\x. x \ \\ \ g x = f x" -proof (cases "\ - \ = {}") +proof%unimportant (cases "\ - \ = {}") case True then have "\\ \ \\" by (simp add: Union_mono) @@ -608,7 +608,7 @@ using extendf [of i] unfolding eq by (metis that) qed -lemma extend_map_lemma_cofinite0: +lemma%unimportant extend_map_lemma_cofinite0: assumes "finite \" and "pairwise (\S T. S \ T \ K) \" and "\S. S \ \ \ \a g. a \ U \ continuous_on (S - {a}) g \ g ` (S - {a}) \ T \ (\x \ S \ K. g x = h x)" @@ -665,7 +665,7 @@ qed -lemma extend_map_lemma_cofinite1: +lemma%unimportant extend_map_lemma_cofinite1: assumes "finite \" and \: "\X. X \ \ \ \a g. a \ U \ continuous_on (X - {a}) g \ g ` (X - {a}) \ T \ (\x \ X \ K. g x = h x)" and clo: "\X. X \ \ \ closed X" @@ -695,7 +695,7 @@ qed -lemma extend_map_lemma_cofinite: +lemma%important extend_map_lemma_cofinite: assumes "finite \" "\ \ \" and T: "convex T" "bounded T" and poly: "\X. X \ \ \ polytope X" and contf: "continuous_on (\\) f" and fim: "f ` (\\) \ rel_frontier T" @@ -704,7 +704,7 @@ obtains C g where "finite C" "disjnt C (\\)" "card C \ card \" "continuous_on (\\ - C) g" "g ` (\ \ - C) \ rel_frontier T" "\x. x \ \\ \ g x = f x" -proof - +proof%unimportant - define \ where "\ \ \ \ {D. \C \ \ - \. D face_of C \ aff_dim D < aff_dim T}" have "finite \" using assms finite_subset by blast @@ -869,7 +869,7 @@ qed text\The next two proofs are similar\ -theorem extend_map_cell_complex_to_sphere: +theorem%important extend_map_cell_complex_to_sphere: assumes "finite \" and S: "S \ \\" "closed S" and T: "convex T" "bounded T" and poly: "\X. X \ \ \ polytope X" and aff: "\X. X \ \ \ aff_dim X < aff_dim T" @@ -877,7 +877,7 @@ and contf: "continuous_on S f" and fim: "f ` S \ rel_frontier T" obtains g where "continuous_on (\\) g" "g ` (\\) \ rel_frontier T" "\x. x \ S \ g x = f x" -proof - +proof%unimportant - obtain V g where "S \ V" "open V" "continuous_on V g" and gim: "g ` V \ rel_frontier T" and gf: "\x. x \ S \ g x = f x" using neighbourhood_extension_into_ANR [OF contf fim _ \closed S\] ANR_rel_frontier_convex T by blast have "compact S" @@ -924,7 +924,7 @@ qed -theorem extend_map_cell_complex_to_sphere_cofinite: +theorem%important extend_map_cell_complex_to_sphere_cofinite: assumes "finite \" and S: "S \ \\" "closed S" and T: "convex T" "bounded T" and poly: "\X. X \ \ \ polytope X" and aff: "\X. X \ \ \ aff_dim X \ aff_dim T" @@ -932,7 +932,7 @@ and contf: "continuous_on S f" and fim: "f ` S \ rel_frontier T" obtains C g where "finite C" "disjnt C S" "continuous_on (\\ - C) g" "g ` (\\ - C) \ rel_frontier T" "\x. x \ S \ g x = f x" -proof - +proof%unimportant - obtain V g where "S \ V" "open V" "continuous_on V g" and gim: "g ` V \ rel_frontier T" and gf: "\x. x \ S \ g x = f x" using neighbourhood_extension_into_ANR [OF contf fim _ \closed S\] ANR_rel_frontier_convex T by blast have "compact S" @@ -993,10 +993,10 @@ subsection%important\ Special cases and corollaries involving spheres\ -lemma disjnt_Diff1: "X \ Y' \ disjnt (X - Y) (X' - Y')" +lemma%unimportant disjnt_Diff1: "X \ Y' \ disjnt (X - Y) (X' - Y')" by (auto simp: disjnt_def) -proposition extend_map_affine_to_sphere_cofinite_simple: +proposition%important extend_map_affine_to_sphere_cofinite_simple: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "compact S" "convex U" "bounded U" and aff: "aff_dim T \ aff_dim U" @@ -1005,7 +1005,7 @@ obtains K g where "finite K" "K \ T" "disjnt K S" "continuous_on (T - K) g" "g ` (T - K) \ rel_frontier U" "\x. x \ S \ g x = f x" -proof - +proof%unimportant - have "\K g. finite K \ disjnt K S \ continuous_on (T - K) g \ g ` (T - K) \ rel_frontier U \ (\x \ S. g x = f x)" if "affine T" "S \ T" and aff: "aff_dim T \ aff_dim U" for T @@ -1144,14 +1144,14 @@ (*Up to extend_map_affine_to_sphere_cofinite_gen*) -lemma extend_map_affine_to_sphere1: +lemma%important extend_map_affine_to_sphere1: fixes f :: "'a::euclidean_space \ 'b::topological_space" assumes "finite K" "affine U" and contf: "continuous_on (U - K) f" and fim: "f ` (U - K) \ T" and comps: "\C. \C \ components(U - S); C \ K \ {}\ \ C \ L \ {}" and clo: "closedin (subtopology euclidean U) S" and K: "disjnt K S" "K \ U" obtains g where "continuous_on (U - L) g" "g ` (U - L) \ T" "\x. x \ S \ g x = f x" -proof (cases "K = {}") +proof%unimportant (cases "K = {}") case True then show ?thesis by (metis Diff_empty Diff_subset contf fim continuous_on_subset image_subsetI rev_image_eqI subset_iff that) @@ -1436,7 +1436,7 @@ qed -lemma extend_map_affine_to_sphere2: +lemma%important extend_map_affine_to_sphere2: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "compact S" "convex U" "bounded U" "affine T" "S \ T" and affTU: "aff_dim T \ aff_dim U" @@ -1446,7 +1446,7 @@ obtains K g where "finite K" "K \ L" "K \ T" "disjnt K S" "continuous_on (T - K) g" "g ` (T - K) \ rel_frontier U" "\x. x \ S \ g x = f x" -proof - +proof%unimportant - obtain K g where K: "finite K" "K \ T" "disjnt K S" and contg: "continuous_on (T - K) g" and gim: "g ` (T - K) \ rel_frontier U" @@ -1490,7 +1490,7 @@ qed -proposition extend_map_affine_to_sphere_cofinite_gen: +proposition%important extend_map_affine_to_sphere_cofinite_gen: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes SUT: "compact S" "convex U" "bounded U" "affine T" "S \ T" and aff: "aff_dim T \ aff_dim U" @@ -1500,7 +1500,7 @@ obtains K g where "finite K" "K \ L" "K \ T" "disjnt K S" "continuous_on (T - K) g" "g ` (T - K) \ rel_frontier U" "\x. x \ S \ g x = f x" -proof (cases "S = {}") +proof%unimportant (cases "S = {}") case True show ?thesis proof (cases "rel_frontier U = {}") @@ -1645,7 +1645,7 @@ qed -corollary extend_map_affine_to_sphere_cofinite: +corollary%important extend_map_affine_to_sphere_cofinite: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes SUT: "compact S" "affine T" "S \ T" and aff: "aff_dim T \ DIM('b)" and "0 \ r" @@ -1654,7 +1654,7 @@ and dis: "\C. \C \ components(T - S); bounded C\ \ C \ L \ {}" obtains K g where "finite K" "K \ L" "K \ T" "disjnt K S" "continuous_on (T - K) g" "g ` (T - K) \ sphere a r" "\x. x \ S \ g x = f x" -proof (cases "r = 0") +proof%unimportant (cases "r = 0") case True with fim show ?thesis by (rule_tac K="{}" and g = "\x. a" in that) (auto simp: continuous_on_const) @@ -1670,7 +1670,7 @@ done qed -corollary extend_map_UNIV_to_sphere_cofinite: +corollary%important extend_map_UNIV_to_sphere_cofinite: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes aff: "DIM('a) \ DIM('b)" and "0 \ r" and SUT: "compact S" @@ -1684,7 +1684,7 @@ apply (auto simp: assms that Compl_eq_Diff_UNIV [symmetric]) done -corollary extend_map_UNIV_to_sphere_no_bounded_component: +corollary%important extend_map_UNIV_to_sphere_no_bounded_component: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes aff: "DIM('a) \ DIM('b)" and "0 \ r" and SUT: "compact S" @@ -1696,14 +1696,14 @@ apply (auto simp: that dest: dis) done -theorem Borsuk_separation_theorem_gen: +theorem%important Borsuk_separation_theorem_gen: fixes S :: "'a::euclidean_space set" assumes "compact S" shows "(\c \ components(- S). \bounded c) \ (\f. continuous_on S f \ f ` S \ sphere (0::'a) 1 \ (\c. homotopic_with (\x. True) S (sphere 0 1) f (\x. c)))" (is "?lhs = ?rhs") -proof +proof%unimportant assume L [rule_format]: ?lhs show ?rhs proof clarify @@ -1734,14 +1734,14 @@ qed -corollary Borsuk_separation_theorem: +corollary%important Borsuk_separation_theorem: fixes S :: "'a::euclidean_space set" assumes "compact S" and 2: "2 \ DIM('a)" shows "connected(- S) \ (\f. continuous_on S f \ f ` S \ sphere (0::'a) 1 \ (\c. homotopic_with (\x. True) S (sphere 0 1) f (\x. c)))" (is "?lhs = ?rhs") -proof +proof%unimportant assume L: ?lhs show ?rhs proof (cases "S = {}") @@ -1764,7 +1764,7 @@ qed -lemma homotopy_eqv_separation: +lemma%unimportant homotopy_eqv_separation: fixes S :: "'a::euclidean_space set" and T :: "'a set" assumes "S homotopy_eqv T" and "compact S" and "compact T" shows "connected(- S) \ connected(- T)" @@ -1783,11 +1783,11 @@ qed qed -proposition Jordan_Brouwer_separation: +lemma%important Jordan_Brouwer_separation: fixes S :: "'a::euclidean_space set" and a::'a assumes hom: "S homeomorphic sphere a r" and "0 < r" shows "\ connected(- S)" -proof - +proof%unimportant - have "- sphere a r \ ball a r \ {}" using \0 < r\ by (simp add: Int_absorb1 subset_eq) moreover @@ -1817,11 +1817,11 @@ qed -proposition Jordan_Brouwer_frontier: +lemma%important Jordan_Brouwer_frontier: fixes S :: "'a::euclidean_space set" and a::'a assumes S: "S homeomorphic sphere a r" and T: "T \ components(- S)" and 2: "2 \ DIM('a)" shows "frontier T = S" -proof (cases r rule: linorder_cases) +proof%unimportant (cases r rule: linorder_cases) assume "r < 0" with S T show ?thesis by auto next @@ -1866,11 +1866,11 @@ qed (rule T) qed -proposition Jordan_Brouwer_nonseparation: +lemma%important Jordan_Brouwer_nonseparation: fixes S :: "'a::euclidean_space set" and a::'a assumes S: "S homeomorphic sphere a r" and "T \ S" and 2: "2 \ DIM('a)" shows "connected(- T)" -proof - +proof%unimportant - have *: "connected(C \ (S - T))" if "C \ components(- S)" for C proof (rule connected_intermediate_closure) show "connected C" @@ -1894,7 +1894,7 @@ subsection%important\ Invariance of domain and corollaries\ -lemma invariance_of_domain_ball: +lemma%unimportant invariance_of_domain_ball: fixes f :: "'a \ 'a::euclidean_space" assumes contf: "continuous_on (cball a r) f" and "0 < r" and inj: "inj_on f (cball a r)" @@ -1983,12 +1983,12 @@ text\Proved by L. E. J. Brouwer (1912)\ -theorem invariance_of_domain: +theorem%important invariance_of_domain: fixes f :: "'a \ 'a::euclidean_space" assumes "continuous_on S f" "open S" "inj_on f S" shows "open(f ` S)" unfolding open_subopen [of "f`S"] -proof clarify +proof%unimportant clarify fix a assume "a \ S" obtain \ where "\ > 0" and \: "cball a \ \ S" @@ -2004,7 +2004,7 @@ qed qed -lemma inv_of_domain_ss0: +lemma%unimportant inv_of_domain_ss0: fixes f :: "'a \ 'a::euclidean_space" assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \ S" and "subspace S" and dimS: "dim S = DIM('b::euclidean_space)" @@ -2049,7 +2049,7 @@ by (metis (no_types, hide_lams) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV) qed -lemma inv_of_domain_ss1: +lemma%unimportant inv_of_domain_ss1: fixes f :: "'a \ 'a::euclidean_space" assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \ S" and "subspace S" @@ -2090,14 +2090,14 @@ qed -corollary invariance_of_domain_subspaces: +corollary%important invariance_of_domain_subspaces: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes ope: "openin (subtopology euclidean U) S" and "subspace U" "subspace V" and VU: "dim V \ dim U" and contf: "continuous_on S f" and fim: "f ` S \ V" and injf: "inj_on f S" shows "openin (subtopology euclidean V) (f ` S)" -proof - +proof%unimportant - obtain V' where "subspace V'" "V' \ U" "dim V' = dim V" using choose_subspace_of_subspace [OF VU] by (metis span_eq_iff \subspace U\) @@ -2134,14 +2134,14 @@ qed qed -corollary invariance_of_dimension_subspaces: +corollary%important invariance_of_dimension_subspaces: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes ope: "openin (subtopology euclidean U) S" and "subspace U" "subspace V" and contf: "continuous_on S f" and fim: "f ` S \ V" and injf: "inj_on f S" and "S \ {}" shows "dim U \ dim V" -proof - +proof%unimportant - have "False" if "dim V < dim U" proof - obtain T where "subspace T" "T \ U" "dim T = dim V" @@ -2174,14 +2174,14 @@ using not_less by blast qed -corollary invariance_of_domain_affine_sets: +corollary%important invariance_of_domain_affine_sets: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes ope: "openin (subtopology euclidean U) S" and aff: "affine U" "affine V" "aff_dim V \ aff_dim U" and contf: "continuous_on S f" and fim: "f ` S \ V" and injf: "inj_on f S" shows "openin (subtopology euclidean V) (f ` S)" -proof (cases "S = {}") +proof%unimportant (cases "S = {}") case True then show ?thesis by auto next @@ -2209,14 +2209,14 @@ by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois) qed -corollary invariance_of_dimension_affine_sets: +corollary%important invariance_of_dimension_affine_sets: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes ope: "openin (subtopology euclidean U) S" and aff: "affine U" "affine V" and contf: "continuous_on S f" and fim: "f ` S \ V" and injf: "inj_on f S" and "S \ {}" shows "aff_dim U \ aff_dim V" -proof - +proof%unimportant - obtain a b where "a \ S" "a \ U" "b \ V" using \S \ {}\ fim ope openin_contains_cball by fastforce have "dim ((+) (- a) ` U) \ dim ((+) (- b) ` V)" @@ -2238,7 +2238,7 @@ by (metis \a \ U\ \b \ V\ aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff) qed -corollary invariance_of_dimension: +corollary%important invariance_of_dimension: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes contf: "continuous_on S f" and "open S" and injf: "inj_on f S" and "S \ {}" @@ -2247,7 +2247,7 @@ by auto -corollary continuous_injective_image_subspace_dim_le: +corollary%important continuous_injective_image_subspace_dim_le: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "subspace S" "subspace T" and contf: "continuous_on S f" and fim: "f ` S \ T" @@ -2256,7 +2256,7 @@ apply (rule invariance_of_dimension_subspaces [of S S _ f]) using%unimportant assms by (auto simp: subspace_affine) -lemma invariance_of_dimension_convex_domain: +lemma%unimportant invariance_of_dimension_convex_domain: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "convex S" and contf: "continuous_on S f" and fim: "f ` S \ affine hull T" @@ -2285,7 +2285,7 @@ qed -lemma homeomorphic_convex_sets_le: +lemma%unimportant homeomorphic_convex_sets_le: assumes "convex S" "S homeomorphic T" shows "aff_dim S \ aff_dim T" proof - @@ -2302,23 +2302,23 @@ qed qed -lemma homeomorphic_convex_sets: +lemma%unimportant homeomorphic_convex_sets: assumes "convex S" "convex T" "S homeomorphic T" shows "aff_dim S = aff_dim T" by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym) -lemma homeomorphic_convex_compact_sets_eq: +lemma%unimportant homeomorphic_convex_compact_sets_eq: assumes "convex S" "compact S" "convex T" "compact T" shows "S homeomorphic T \ aff_dim S = aff_dim T" by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets) -lemma invariance_of_domain_gen: +lemma%unimportant invariance_of_domain_gen: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "open S" "continuous_on S f" "inj_on f S" "DIM('b) \ DIM('a)" shows "open(f ` S)" using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto -lemma injective_into_1d_imp_open_map_UNIV: +lemma%unimportant injective_into_1d_imp_open_map_UNIV: fixes f :: "'a::euclidean_space \ real" assumes "open T" "continuous_on S f" "inj_on f S" "T \ S" shows "open (f ` T)" @@ -2326,7 +2326,7 @@ using assms apply (auto simp: elim: continuous_on_subset subset_inj_on) done -lemma continuous_on_inverse_open: +lemma%unimportant continuous_on_inverse_open: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "open S" "continuous_on S f" "DIM('b) \ DIM('a)" and gf: "\x. x \ S \ g(f x) = x" shows "continuous_on (f ` S) g" @@ -2345,7 +2345,7 @@ by (metis \open T\ continuous_on_subset inj_onI inj_on_subset invariance_of_domain_gen openin_open openin_open_eq) qed -lemma invariance_of_domain_homeomorphism: +lemma%unimportant invariance_of_domain_homeomorphism: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "open S" "continuous_on S f" "DIM('b) \ DIM('a)" "inj_on f S" obtains g where "homeomorphism S (f ` S) f g" @@ -2354,14 +2354,14 @@ by (simp add: assms continuous_on_inverse_open homeomorphism_def) qed -corollary invariance_of_domain_homeomorphic: +corollary%important invariance_of_domain_homeomorphic: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "open S" "continuous_on S f" "DIM('b) \ DIM('a)" "inj_on f S" shows "S homeomorphic (f ` S)" using%unimportant invariance_of_domain_homeomorphism [OF assms] by%unimportant (meson homeomorphic_def) -lemma continuous_image_subset_interior: +lemma%unimportant continuous_image_subset_interior: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "continuous_on S f" "inj_on f S" "DIM('b) \ DIM('a)" shows "f ` (interior S) \ interior(f ` S)" @@ -2372,13 +2372,13 @@ apply (auto simp: subset_inj_on interior_subset continuous_on_subset) done -lemma homeomorphic_interiors_same_dimension: +lemma%important homeomorphic_interiors_same_dimension: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" and dimeq: "DIM('a) = DIM('b)" shows "(interior S) homeomorphic (interior T)" using assms [unfolded homeomorphic_minimal] unfolding homeomorphic_def -proof (clarify elim!: ex_forward) +proof%unimportant (clarify elim!: ex_forward) fix f g assume S: "\x\S. f x \ T \ g (f x) = x" and T: "\y\T. g y \ S \ f (g y) = y" and contf: "continuous_on S f" and contg: "continuous_on T g" @@ -2422,7 +2422,7 @@ qed qed -lemma homeomorphic_open_imp_same_dimension: +lemma%unimportant homeomorphic_open_imp_same_dimension: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "open S" "S \ {}" "open T" "T \ {}" shows "DIM('a) = DIM('b)" @@ -2431,7 +2431,7 @@ apply (rule order_antisym; metis inj_onI invariance_of_dimension) done -proposition homeomorphic_interiors: +lemma%unimportant homeomorphic_interiors: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "interior S = {} \ interior T = {}" shows "(interior S) homeomorphic (interior T)" @@ -2449,7 +2449,7 @@ by (rule homeomorphic_interiors_same_dimension [OF \S homeomorphic T\]) qed -lemma homeomorphic_frontiers_same_dimension: +lemma%unimportant homeomorphic_frontiers_same_dimension: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "closed S" "closed T" and dimeq: "DIM('a) = DIM('b)" shows "(frontier S) homeomorphic (frontier T)" @@ -2505,7 +2505,7 @@ qed qed -lemma homeomorphic_frontiers: +lemma%unimportant homeomorphic_frontiers: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "closed S" "closed T" "interior S = {} \ interior T = {}" @@ -2522,7 +2522,7 @@ using False assms homeomorphic_interiors homeomorphic_open_imp_same_dimension by blast qed -lemma continuous_image_subset_rel_interior: +lemma%unimportant continuous_image_subset_rel_interior: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \ T" and TS: "aff_dim T \ aff_dim S" @@ -2545,7 +2545,7 @@ qed auto qed -lemma homeomorphic_rel_interiors_same_dimension: +lemma%unimportant homeomorphic_rel_interiors_same_dimension: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T" shows "(rel_interior S) homeomorphic (rel_interior T)" @@ -2597,11 +2597,11 @@ qed qed -lemma homeomorphic_rel_interiors: +lemma%important homeomorphic_rel_interiors: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "rel_interior S = {} \ rel_interior T = {}" shows "(rel_interior S) homeomorphic (rel_interior T)" -proof (cases "rel_interior T = {}") +proof%unimportant (cases "rel_interior T = {}") case True with assms show ?thesis by auto next @@ -2630,7 +2630,7 @@ qed -lemma homeomorphic_rel_boundaries_same_dimension: +lemma%unimportant homeomorphic_rel_boundaries_same_dimension: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T" shows "(S - rel_interior S) homeomorphic (T - rel_interior T)" @@ -2664,7 +2664,7 @@ qed qed -lemma homeomorphic_rel_boundaries: +lemma%unimportant homeomorphic_rel_boundaries: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "rel_interior S = {} \ rel_interior T = {}" shows "(S - rel_interior S) homeomorphic (T - rel_interior T)" @@ -2696,11 +2696,11 @@ by (rule homeomorphic_rel_boundaries_same_dimension [OF \S homeomorphic T\]) qed -proposition uniformly_continuous_homeomorphism_UNIV_trivial: +proposition%important uniformly_continuous_homeomorphism_UNIV_trivial: fixes f :: "'a::euclidean_space \ 'a" assumes contf: "uniformly_continuous_on S f" and hom: "homeomorphism S UNIV f g" shows "S = UNIV" -proof (cases "S = {}") +proof%unimportant (cases "S = {}") case True then show ?thesis by (metis UNIV_I hom empty_iff homeomorphism_def image_eqI) @@ -2744,7 +2744,7 @@ subsection%important\Dimension-based conditions for various homeomorphisms\ -lemma homeomorphic_subspaces_eq: +lemma%unimportant homeomorphic_subspaces_eq: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "subspace S" "subspace T" shows "S homeomorphic T \ dim S = dim T" @@ -2765,7 +2765,7 @@ by (simp add: assms homeomorphic_subspaces) qed -lemma homeomorphic_affine_sets_eq: +lemma%unimportant homeomorphic_affine_sets_eq: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "affine S" "affine T" shows "S homeomorphic T \ aff_dim S = aff_dim T" @@ -2783,19 +2783,19 @@ by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets) qed -lemma homeomorphic_hyperplanes_eq: +lemma%unimportant homeomorphic_hyperplanes_eq: fixes a :: "'a::euclidean_space" and c :: "'b::euclidean_space" assumes "a \ 0" "c \ 0" shows "({x. a \ x = b} homeomorphic {x. c \ x = d} \ DIM('a) = DIM('b))" apply (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms) by (metis DIM_positive Suc_pred) -lemma homeomorphic_UNIV_UNIV: +lemma%unimportant homeomorphic_UNIV_UNIV: shows "(UNIV::'a set) homeomorphic (UNIV::'b set) \ DIM('a::euclidean_space) = DIM('b::euclidean_space)" by (simp add: homeomorphic_subspaces_eq) -lemma simply_connected_sphere_gen: +lemma%unimportant simply_connected_sphere_gen: assumes "convex S" "bounded S" and 3: "3 \ aff_dim S" shows "simply_connected(rel_frontier S)" proof - @@ -2819,16 +2819,16 @@ qed qed -subsection%important\more invariance of domain\(*FIX ME title? *) - -proposition invariance_of_domain_sphere_affine_set_gen: +subsection%important\more invariance of domain\ + +proposition%important invariance_of_domain_sphere_affine_set_gen: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \ T" and U: "bounded U" "convex U" and "affine T" and affTU: "aff_dim T < aff_dim U" and ope: "openin (subtopology euclidean (rel_frontier U)) S" shows "openin (subtopology euclidean T) (f ` S)" -proof (cases "rel_frontier U = {}") +proof%unimportant (cases "rel_frontier U = {}") case True then show ?thesis using ope openin_subset by force @@ -2927,7 +2927,7 @@ qed -lemma invariance_of_domain_sphere_affine_set: +lemma%unimportant invariance_of_domain_sphere_affine_set: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \ T" and "r \ 0" "affine T" and affTU: "aff_dim T < DIM('a)" @@ -2948,7 +2948,7 @@ qed qed -lemma no_embedding_sphere_lowdim: +lemma%unimportant no_embedding_sphere_lowdim: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes contf: "continuous_on (sphere a r) f" and injf: "inj_on f (sphere a r)" and "r > 0" shows "DIM('a) \ DIM('b)" @@ -2969,7 +2969,7 @@ using not_less by blast qed -lemma simply_connected_sphere: +lemma%unimportant simply_connected_sphere: fixes a :: "'a::euclidean_space" assumes "3 \ DIM('a)" shows "simply_connected(sphere a r)" @@ -2986,7 +2986,7 @@ by (simp add: aff_dim_cball) qed -lemma simply_connected_sphere_eq: +lemma%unimportant simply_connected_sphere_eq: fixes a :: "'a::euclidean_space" shows "simply_connected(sphere a r) \ 3 \ DIM('a) \ r \ 0" (is "?lhs = ?rhs") proof (cases "r \ 0") @@ -3029,7 +3029,7 @@ qed -lemma simply_connected_punctured_universe_eq: +lemma%unimportant simply_connected_punctured_universe_eq: fixes a :: "'a::euclidean_space" shows "simply_connected(- {a}) \ 3 \ DIM('a)" proof - @@ -3047,17 +3047,17 @@ finally show ?thesis . qed -lemma not_simply_connected_circle: +lemma%unimportant not_simply_connected_circle: fixes a :: complex shows "0 < r \ \ simply_connected(sphere a r)" by (simp add: simply_connected_sphere_eq) -proposition simply_connected_punctured_convex: +proposition%important simply_connected_punctured_convex: fixes a :: "'a::euclidean_space" assumes "convex S" and 3: "3 \ aff_dim S" shows "simply_connected(S - {a})" -proof (cases "a \ rel_interior S") +proof%unimportant (cases "a \ rel_interior S") case True then obtain e where "a \ S" "0 < e" and e: "cball a e \ affine hull S \ S" by (auto simp: rel_interior_cball) @@ -3096,11 +3096,11 @@ by (meson Diff_subset closure_subset subset_trans) qed -corollary simply_connected_punctured_universe: +corollary%important simply_connected_punctured_universe: fixes a :: "'a::euclidean_space" assumes "3 \ DIM('a)" shows "simply_connected(- {a})" -proof - +proof%unimportant - have [simp]: "affine hull cball a 1 = UNIV" apply auto by (metis UNIV_I aff_dim_cball aff_dim_lt_full zero_less_one not_less_iff_gr_or_eq) @@ -3116,10 +3116,10 @@ subsection%important\The power, squaring and exponential functions as covering maps\ -proposition covering_space_power_punctured_plane: +proposition%important covering_space_power_punctured_plane: assumes "0 < n" shows "covering_space (- {0}) (\z::complex. z^n) (- {0})" -proof - +proof%unimportant - consider "n = 1" | "2 \ n" using assms by linarith then obtain e where "0 < e" and e: "\w z. cmod(w - z) < e * cmod z \ (w^n = z^n \ w = z)" @@ -3367,14 +3367,14 @@ done qed -corollary covering_space_square_punctured_plane: +corollary%important covering_space_square_punctured_plane: "covering_space (- {0}) (\z::complex. z^2) (- {0})" by%unimportant (simp add: covering_space_power_punctured_plane) -proposition covering_space_exp_punctured_plane: +proposition%important covering_space_exp_punctured_plane: "covering_space UNIV (\z::complex. exp z) (- {0})" -proof (simp add: covering_space_def, intro conjI ballI) +proof%unimportant (simp add: covering_space_def, intro conjI ballI) show "continuous_on UNIV (\z::complex. exp z)" by (rule continuous_on_exp [OF continuous_on_id]) show "range exp = - {0::complex}" @@ -3487,9 +3487,9 @@ qed -subsection%important\Hence the Borsukian results about mappings into circles\(*FIX ME title *) - -lemma inessential_eq_continuous_logarithm: +subsection%important\Hence the Borsukian results about mappings into circles\ + +lemma%unimportant inessential_eq_continuous_logarithm: fixes f :: "'a::real_normed_vector \ complex" shows "(\a. homotopic_with (\h. True) S (-{0}) f (\t. a)) \ (\g. continuous_on S g \ (\x \ S. f x = exp(g x)))" @@ -3513,7 +3513,7 @@ by (simp add: f homotopic_with_eq) qed -corollary inessential_imp_continuous_logarithm_circle: +corollary%important inessential_imp_continuous_logarithm_circle: fixes f :: "'a::real_normed_vector \ complex" assumes "homotopic_with (\h. True) S (sphere 0 1) f (\t. a)" obtains g where "continuous_on S g" and "\x. x \ S \ f x = exp(g x)" @@ -3525,7 +3525,7 @@ qed -lemma inessential_eq_continuous_logarithm_circle: +lemma%unimportant inessential_eq_continuous_logarithm_circle: fixes f :: "'a::real_normed_vector \ complex" shows "(\a. homotopic_with (\h. True) S (sphere 0 1) f (\t. a)) \ (\g. continuous_on S g \ (\x \ S. f x = exp(\ * of_real(g x))))" @@ -3565,12 +3565,12 @@ by (simp add: homotopic_with_eq) qed -proposition homotopic_with_sphere_times: +lemma%important homotopic_with_sphere_times: fixes f :: "'a::real_normed_vector \ complex" assumes hom: "homotopic_with (\x. True) S (sphere 0 1) f g" and conth: "continuous_on S h" and hin: "\x. x \ S \ h x \ sphere 0 1" shows "homotopic_with (\x. True) S (sphere 0 1) (\x. f x * h x) (\x. g x * h x)" -proof - +proof%unimportant - obtain k where contk: "continuous_on ({0..1::real} \ S) k" and kim: "k ` ({0..1} \ S) \ sphere 0 1" and k0: "\x. k(0, x) = f x" @@ -3585,13 +3585,14 @@ done qed -proposition homotopic_circlemaps_divide: + +lemma%important homotopic_circlemaps_divide: fixes f :: "'a::real_normed_vector \ complex" shows "homotopic_with (\x. True) S (sphere 0 1) f g \ continuous_on S f \ f ` S \ sphere 0 1 \ continuous_on S g \ g ` S \ sphere 0 1 \ (\c. homotopic_with (\x. True) S (sphere 0 1) (\x. f x / g x) (\x. c))" -proof - +proof%unimportant - have "homotopic_with (\x. True) S (sphere 0 1) (\x. f x / g x) (\x. 1)" if "homotopic_with (\x. True) S (sphere 0 1) (\x. f x / g x) (\x. c)" for c proof - @@ -3645,7 +3646,7 @@ text\Many similar proofs below.\ -lemma upper_hemicontinuous: +lemma%unimportant upper_hemicontinuous: assumes "\x. x \ S \ f x \ T" shows "((\U. openin (subtopology euclidean T) U \ openin (subtopology euclidean S) {x \ S. f x \ U}) \ @@ -3676,7 +3677,7 @@ by (simp add: openin_closedin_eq) qed -lemma lower_hemicontinuous: +lemma%unimportant lower_hemicontinuous: assumes "\x. x \ S \ f x \ T" shows "((\U. closedin (subtopology euclidean T) U \ closedin (subtopology euclidean S) {x \ S. f x \ U}) \ @@ -3707,7 +3708,7 @@ by (simp add: openin_closedin_eq) qed -lemma open_map_iff_lower_hemicontinuous_preimage: +lemma%unimportant open_map_iff_lower_hemicontinuous_preimage: assumes "f ` S \ T" shows "((\U. openin (subtopology euclidean S) U \ openin (subtopology euclidean T) (f ` U)) \ @@ -3738,7 +3739,7 @@ using assms openin_imp_subset [OF opeSU] by (force simp: openin_closedin_eq) qed -lemma closed_map_iff_upper_hemicontinuous_preimage: +lemma%unimportant closed_map_iff_upper_hemicontinuous_preimage: assumes "f ` S \ T" shows "((\U. closedin (subtopology euclidean S) U \ closedin (subtopology euclidean T) (f ` U)) \ @@ -3769,7 +3770,7 @@ by (simp add: openin_closedin_eq) qed -proposition upper_lower_hemicontinuous_explicit: +proposition%important upper_lower_hemicontinuous_explicit: fixes T :: "('b::{real_normed_vector,heine_borel}) set" assumes fST: "\x. x \ S \ f x \ T" and ope: "\U. openin (subtopology euclidean T) U @@ -3781,7 +3782,7 @@ "\x'. \x' \ S; dist x x' < d\ \ (\y \ f x. \y'. y' \ f x' \ dist y y' < e) \ (\y' \ f x'. \y. y \ f x \ dist y' y < e)" -proof - +proof%unimportant - have "openin (subtopology euclidean T) (T \ (\a\f x. \b\ball 0 e. {a + b}))" by (auto simp: open_sums openin_open_Int) with ope have "openin (subtopology euclidean S) @@ -3842,11 +3843,11 @@ subsection%important\Complex logs exist on various "well-behaved" sets\ -lemma continuous_logarithm_on_contractible: +lemma%important continuous_logarithm_on_contractible: fixes f :: "'a::real_normed_vector \ complex" assumes "continuous_on S f" "contractible S" "\z. z \ S \ f z \ 0" obtains g where "continuous_on S g" "\x. x \ S \ f x = exp(g x)" -proof - +proof%unimportant - obtain c where hom: "homotopic_with (\h. True) S (-{0}) f (\x. c)" using nullhomotopic_from_contractible assms by (metis imageE subset_Compl_singleton) @@ -3854,27 +3855,27 @@ by (metis inessential_eq_continuous_logarithm that) qed -lemma continuous_logarithm_on_simply_connected: +lemma%important continuous_logarithm_on_simply_connected: fixes f :: "'a::real_normed_vector \ complex" assumes contf: "continuous_on S f" and S: "simply_connected S" "locally path_connected S" and f: "\z. z \ S \ f z \ 0" obtains g where "continuous_on S g" "\x. x \ S \ f x = exp(g x)" - using covering_space_lift [OF covering_space_exp_punctured_plane S contf] - by (metis (full_types) f imageE subset_Compl_singleton) - -lemma continuous_logarithm_on_cball: + using%unimportant covering_space_lift [OF covering_space_exp_punctured_plane S contf] + by%unimportant (metis (full_types) f imageE subset_Compl_singleton) + +lemma%unimportant continuous_logarithm_on_cball: fixes f :: "'a::real_normed_vector \ complex" assumes "continuous_on (cball a r) f" and "\z. z \ cball a r \ f z \ 0" obtains h where "continuous_on (cball a r) h" "\z. z \ cball a r \ f z = exp(h z)" using assms continuous_logarithm_on_contractible convex_imp_contractible by blast -lemma continuous_logarithm_on_ball: +lemma%unimportant continuous_logarithm_on_ball: fixes f :: "'a::real_normed_vector \ complex" assumes "continuous_on (ball a r) f" and "\z. z \ ball a r \ f z \ 0" obtains h where "continuous_on (ball a r) h" "\z. z \ ball a r \ f z = exp(h z)" using assms continuous_logarithm_on_contractible convex_imp_contractible by blast -lemma continuous_sqrt_on_contractible: +lemma%unimportant continuous_sqrt_on_contractible: fixes f :: "'a::real_normed_vector \ complex" assumes "continuous_on S f" "contractible S" and "\z. z \ S \ f z \ 0" @@ -3891,7 +3892,7 @@ qed qed -lemma continuous_sqrt_on_simply_connected: +lemma%unimportant continuous_sqrt_on_simply_connected: fixes f :: "'a::real_normed_vector \ complex" assumes contf: "continuous_on S f" and S: "simply_connected S" "locally path_connected S" and f: "\z. z \ S \ f z \ 0" @@ -3911,12 +3912,12 @@ subsection%important\Another simple case where sphere maps are nullhomotopic\ -lemma inessential_spheremap_2_aux: +lemma%important inessential_spheremap_2_aux: fixes f :: "'a::euclidean_space \ complex" assumes 2: "2 < DIM('a)" and contf: "continuous_on (sphere a r) f" and fim: "f `(sphere a r) \ (sphere 0 1)" obtains c where "homotopic_with (\z. True) (sphere a r) (sphere 0 1) f (\x. c)" -proof - +proof%unimportant - obtain g where contg: "continuous_on (sphere a r) g" and feq: "\x. x \ sphere a r \ f x = exp(g x)" proof (rule continuous_logarithm_on_simply_connected [OF contf]) @@ -3938,12 +3939,12 @@ by metis qed -lemma inessential_spheremap_2: +lemma%important inessential_spheremap_2: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes a2: "2 < DIM('a)" and b2: "DIM('b) = 2" and contf: "continuous_on (sphere a r) f" and fim: "f `(sphere a r) \ (sphere b s)" obtains c where "homotopic_with (\z. True) (sphere a r) (sphere b s) f (\x. c)" -proof (cases "s \ 0") +proof%unimportant (cases "s \ 0") case True then show ?thesis using contf contractible_sphere fim nullhomotopic_into_contractible that by blast @@ -3977,12 +3978,12 @@ subsection%important\Holomorphic logarithms and square roots\ -lemma contractible_imp_holomorphic_log: +lemma%important contractible_imp_holomorphic_log: assumes holf: "f holomorphic_on S" and S: "contractible S" and fnz: "\z. z \ S \ f z \ 0" obtains g where "g holomorphic_on S" "\z. z \ S \ f z = exp(g z)" -proof - +proof%unimportant - have contf: "continuous_on S f" by (simp add: holf holomorphic_on_imp_continuous_on) obtain g where contg: "continuous_on S g" and feq: "\x. x \ S \ f x = exp (g x)" @@ -4025,12 +4026,12 @@ qed (*Identical proofs*) -lemma simply_connected_imp_holomorphic_log: +lemma%important simply_connected_imp_holomorphic_log: assumes holf: "f holomorphic_on S" and S: "simply_connected S" "locally path_connected S" and fnz: "\z. z \ S \ f z \ 0" obtains g where "g holomorphic_on S" "\z. z \ S \ f z = exp(g z)" -proof - +proof%unimportant - have contf: "continuous_on S f" by (simp add: holf holomorphic_on_imp_continuous_on) obtain g where contg: "continuous_on S g" and feq: "\x. x \ S \ f x = exp (g x)" @@ -4073,7 +4074,7 @@ qed -lemma contractible_imp_holomorphic_sqrt: +lemma%unimportant contractible_imp_holomorphic_sqrt: assumes holf: "f holomorphic_on S" and S: "contractible S" and fnz: "\z. z \ S \ f z \ 0" @@ -4091,7 +4092,7 @@ qed qed -lemma simply_connected_imp_holomorphic_sqrt: +lemma%unimportant simply_connected_imp_holomorphic_sqrt: assumes holf: "f holomorphic_on S" and S: "simply_connected S" "locally path_connected S" and fnz: "\z. z \ S \ f z \ 0" @@ -4111,11 +4112,11 @@ text\ Related theorems about holomorphic inverse cosines.\ -lemma contractible_imp_holomorphic_arccos: +lemma%important contractible_imp_holomorphic_arccos: assumes holf: "f holomorphic_on S" and S: "contractible S" and non1: "\z. z \ S \ f z \ 1 \ f z \ -1" obtains g where "g holomorphic_on S" "\z. z \ S \ f z = cos(g z)" -proof - +proof%unimportant - have hol1f: "(\z. 1 - f z ^ 2) holomorphic_on S" by (intro holomorphic_intros holf) obtain g where holg: "g holomorphic_on S" and eq: "\z. z \ S \ 1 - (f z)\<^sup>2 = (g z)\<^sup>2" @@ -4149,11 +4150,11 @@ qed -lemma contractible_imp_holomorphic_arccos_bounded: +lemma%important contractible_imp_holomorphic_arccos_bounded: assumes holf: "f holomorphic_on S" and S: "contractible S" and "a \ S" and non1: "\z. z \ S \ f z \ 1 \ f z \ -1" obtains g where "g holomorphic_on S" "norm(g a) \ pi + norm(f a)" "\z. z \ S \ f z = cos(g z)" -proof - +proof%unimportant - obtain g where holg: "g holomorphic_on S" and feq: "\z. z \ S \ f z = cos (g z)" using contractible_imp_holomorphic_arccos [OF holf S non1] by blast obtain b where "cos b = f a" "norm b \ pi + norm (f a)" @@ -4199,11 +4200,11 @@ \f. continuous_on S f \ f ` S \ (- {0::complex}) \ (\a. homotopic_with (\h. True) S (- {0}) f (\x. a))" -lemma Borsukian_retraction_gen: +lemma%important Borsukian_retraction_gen: assumes "Borsukian S" "continuous_on S h" "h ` S = T" "continuous_on T k" "k ` T \ S" "\y. y \ T \ h(k y) = y" shows "Borsukian T" -proof - +proof%unimportant - interpret R: Retracts S h T k using assms by (simp add: Retracts.intro) show ?thesis @@ -4213,42 +4214,42 @@ done qed -lemma retract_of_Borsukian: "\Borsukian T; S retract_of T\ \ Borsukian S" +lemma%unimportant retract_of_Borsukian: "\Borsukian T; S retract_of T\ \ Borsukian S" apply (auto simp: retract_of_def retraction_def) apply (erule (1) Borsukian_retraction_gen) apply (meson retraction retraction_def) apply (auto simp: continuous_on_id) done -lemma homeomorphic_Borsukian: "\Borsukian S; S homeomorphic T\ \ Borsukian T" +lemma%unimportant homeomorphic_Borsukian: "\Borsukian S; S homeomorphic T\ \ Borsukian T" using Borsukian_retraction_gen order_refl by (fastforce simp add: homeomorphism_def homeomorphic_def) -lemma homeomorphic_Borsukian_eq: +lemma%unimportant homeomorphic_Borsukian_eq: "S homeomorphic T \ Borsukian S \ Borsukian T" by (meson homeomorphic_Borsukian homeomorphic_sym) -lemma Borsukian_translation: +lemma%unimportant Borsukian_translation: fixes S :: "'a::real_normed_vector set" shows "Borsukian (image (\x. a + x) S) \ Borsukian S" apply (rule homeomorphic_Borsukian_eq) using homeomorphic_translation homeomorphic_sym by blast -lemma Borsukian_injective_linear_image: +lemma%unimportant Borsukian_injective_linear_image: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "linear f" "inj f" shows "Borsukian(f ` S) \ Borsukian S" apply (rule homeomorphic_Borsukian_eq) using assms homeomorphic_sym linear_homeomorphic_image by blast -lemma homotopy_eqv_Borsukianness: +lemma%unimportant homotopy_eqv_Borsukianness: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" assumes "S homotopy_eqv T" shows "(Borsukian S \ Borsukian T)" by (meson Borsukian_def assms homotopy_eqv_cohomotopic_triviality_null) -lemma Borsukian_alt: +lemma%unimportant Borsukian_alt: fixes S :: "'a::real_normed_vector set" shows "Borsukian S \ @@ -4258,20 +4259,20 @@ unfolding Borsukian_def homotopic_triviality by (simp add: path_connected_punctured_universe) -lemma Borsukian_continuous_logarithm: +lemma%unimportant Borsukian_continuous_logarithm: fixes S :: "'a::real_normed_vector set" shows "Borsukian S \ (\f. continuous_on S f \ f ` S \ (- {0::complex}) \ (\g. continuous_on S g \ (\x \ S. f x = exp(g x))))" by (simp add: Borsukian_def inessential_eq_continuous_logarithm) -lemma Borsukian_continuous_logarithm_circle: +lemma%important Borsukian_continuous_logarithm_circle: fixes S :: "'a::real_normed_vector set" shows "Borsukian S \ (\f. continuous_on S f \ f ` S \ sphere (0::complex) 1 \ (\g. continuous_on S g \ (\x \ S. f x = exp(g x))))" (is "?lhs = ?rhs") -proof +proof%unimportant assume ?lhs then show ?rhs by (force simp: Borsukian_continuous_logarithm) next @@ -4301,13 +4302,13 @@ qed -lemma Borsukian_continuous_logarithm_circle_real: +lemma%important Borsukian_continuous_logarithm_circle_real: fixes S :: "'a::real_normed_vector set" shows "Borsukian S \ (\f. continuous_on S f \ f ` S \ sphere (0::complex) 1 \ (\g. continuous_on S (complex_of_real \ g) \ (\x \ S. f x = exp(\ * of_real(g x)))))" (is "?lhs = ?rhs") -proof +proof%unimportant assume LHS: ?lhs show ?rhs proof (clarify) @@ -4334,52 +4335,52 @@ qed qed -lemma Borsukian_circle: +lemma%unimportant Borsukian_circle: fixes S :: "'a::real_normed_vector set" shows "Borsukian S \ (\f. continuous_on S f \ f ` S \ sphere (0::complex) 1 \ (\a. homotopic_with (\h. True) S (sphere (0::complex) 1) f (\x. a)))" by (simp add: inessential_eq_continuous_logarithm_circle Borsukian_continuous_logarithm_circle_real) -lemma contractible_imp_Borsukian: "contractible S \ Borsukian S" +lemma%unimportant contractible_imp_Borsukian: "contractible S \ Borsukian S" by (meson Borsukian_def nullhomotopic_from_contractible) -lemma simply_connected_imp_Borsukian: +lemma%unimportant simply_connected_imp_Borsukian: fixes S :: "'a::real_normed_vector set" shows "\simply_connected S; locally path_connected S\ \ Borsukian S" apply (simp add: Borsukian_continuous_logarithm) by (metis (no_types, lifting) continuous_logarithm_on_simply_connected image_iff) -lemma starlike_imp_Borsukian: +lemma%unimportant starlike_imp_Borsukian: fixes S :: "'a::real_normed_vector set" shows "starlike S \ Borsukian S" by (simp add: contractible_imp_Borsukian starlike_imp_contractible) -lemma Borsukian_empty: "Borsukian {}" +lemma%unimportant Borsukian_empty: "Borsukian {}" by (auto simp: contractible_imp_Borsukian) -lemma Borsukian_UNIV: "Borsukian (UNIV :: 'a::real_normed_vector set)" +lemma%unimportant Borsukian_UNIV: "Borsukian (UNIV :: 'a::real_normed_vector set)" by (auto simp: contractible_imp_Borsukian) -lemma convex_imp_Borsukian: +lemma%unimportant convex_imp_Borsukian: fixes S :: "'a::real_normed_vector set" shows "convex S \ Borsukian S" by (meson Borsukian_def convex_imp_contractible nullhomotopic_from_contractible) -proposition Borsukian_sphere: +lemma%unimportant Borsukian_sphere: fixes a :: "'a::euclidean_space" shows "3 \ DIM('a) \ Borsukian (sphere a r)" apply (rule simply_connected_imp_Borsukian) using simply_connected_sphere apply blast using ENR_imp_locally_path_connected ENR_sphere by blast -proposition Borsukian_open_Un: +lemma%important Borsukian_open_Un: fixes S :: "'a::real_normed_vector set" assumes opeS: "openin (subtopology euclidean (S \ T)) S" and opeT: "openin (subtopology euclidean (S \ T)) T" and BS: "Borsukian S" and BT: "Borsukian T" and ST: "connected(S \ T)" shows "Borsukian(S \ T)" -proof (clarsimp simp add: Borsukian_continuous_logarithm) +proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm) fix f :: "'a \ complex" assume contf: "continuous_on (S \ T) f" and 0: "0 \ f ` (S \ T)" then have contfS: "continuous_on S f" and contfT: "continuous_on T f" @@ -4443,13 +4444,13 @@ qed text\The proof is a duplicate of that of \Borsukian_open_Un\.\ -lemma Borsukian_closed_Un: +lemma%important Borsukian_closed_Un: fixes S :: "'a::real_normed_vector set" assumes cloS: "closedin (subtopology euclidean (S \ T)) S" and cloT: "closedin (subtopology euclidean (S \ T)) T" and BS: "Borsukian S" and BT: "Borsukian T" and ST: "connected(S \ T)" shows "Borsukian(S \ T)" -proof (clarsimp simp add: Borsukian_continuous_logarithm) +proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm) fix f :: "'a \ complex" assume contf: "continuous_on (S \ T) f" and 0: "0 \ f ` (S \ T)" then have contfS: "continuous_on S f" and contfT: "continuous_on T f" @@ -4512,18 +4513,18 @@ qed qed -lemma Borsukian_separation_compact: +lemma%unimportant Borsukian_separation_compact: fixes S :: "complex set" assumes "compact S" shows "Borsukian S \ connected(- S)" by (simp add: Borsuk_separation_theorem Borsukian_circle assms) -lemma Borsukian_monotone_image_compact: +lemma%important Borsukian_monotone_image_compact: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "Borsukian S" and contf: "continuous_on S f" and fim: "f ` S = T" and "compact S" and conn: "\y. y \ T \ connected {x. x \ S \ f x = y}" shows "Borsukian T" -proof (clarsimp simp add: Borsukian_continuous_logarithm) +proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm) fix g :: "'b \ complex" assume contg: "continuous_on T g" and 0: "0 \ g ` T" have "continuous_on S (g \ f)" @@ -4583,13 +4584,13 @@ qed -lemma Borsukian_open_map_image_compact: +lemma%important Borsukian_open_map_image_compact: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "Borsukian S" and contf: "continuous_on S f" and fim: "f ` S = T" and "compact S" and ope: "\U. openin (subtopology euclidean S) U \ openin (subtopology euclidean T) (f ` U)" shows "Borsukian T" -proof (clarsimp simp add: Borsukian_continuous_logarithm_circle_real) +proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm_circle_real) fix g :: "'b \ complex" assume contg: "continuous_on T g" and gim: "g ` T \ sphere 0 1" have "continuous_on S (g \ f)" @@ -4670,12 +4671,12 @@ text\If two points are separated by a closed set, there's a minimal one.\ -proposition closed_irreducible_separator: +proposition%important closed_irreducible_separator: fixes a :: "'a::real_normed_vector" assumes "closed S" and ab: "\ connected_component (- S) a b" obtains T where "T \ S" "closed T" "T \ {}" "\ connected_component (- T) a b" "\U. U \ T \ connected_component (- U) a b" -proof (cases "a \ S \ b \ S") +proof%unimportant (cases "a \ S \ b \ S") case True then show ?thesis proof @@ -4778,7 +4779,7 @@ qed qed -lemma frontier_minimal_separating_closed_pointwise: +lemma%unimportant frontier_minimal_separating_closed_pointwise: fixes S :: "'a::real_normed_vector set" assumes S: "closed S" "a \ S" and nconn: "\ connected_component (- S) a b" and conn: "\T. \closed T; T \ S\ \ connected_component (- T) a b" @@ -4815,21 +4816,21 @@ closedin (subtopology euclidean U) S \ closedin (subtopology euclidean U) T \ connected (S \ T)" -lemma unicoherentI [intro?]: +lemma%unimportant unicoherentI [intro?]: assumes "\S T. \connected S; connected T; U = S \ T; closedin (subtopology euclidean U) S; closedin (subtopology euclidean U) T\ \ connected (S \ T)" shows "unicoherent U" using assms unfolding unicoherent_def by blast -lemma unicoherentD: +lemma%unimportant unicoherentD: assumes "unicoherent U" "connected S" "connected T" "U = S \ T" "closedin (subtopology euclidean U) S" "closedin (subtopology euclidean U) T" shows "connected (S \ T)" using assms unfolding unicoherent_def by blast -proposition homeomorphic_unicoherent: +lemma%important homeomorphic_unicoherent: assumes ST: "S homeomorphic T" and S: "unicoherent S" shows "unicoherent T" -proof - +proof%unimportant - obtain f g where gf: "\x. x \ S \ g (f x) = x" and fim: "T = f ` S" and gfim: "g ` f ` S = S" and contf: "continuous_on S f" and contg: "continuous_on (f ` S) g" using ST by (auto simp: homeomorphic_def homeomorphism_def) @@ -4870,24 +4871,24 @@ qed -lemma homeomorphic_unicoherent_eq: +lemma%unimportant homeomorphic_unicoherent_eq: "S homeomorphic T \ (unicoherent S \ unicoherent T)" by (meson homeomorphic_sym homeomorphic_unicoherent) -lemma unicoherent_translation: +lemma%unimportant unicoherent_translation: fixes S :: "'a::real_normed_vector set" shows "unicoherent (image (\x. a + x) S) \ unicoherent S" using homeomorphic_translation homeomorphic_unicoherent_eq by blast -lemma unicoherent_injective_linear_image: +lemma%unimportant unicoherent_injective_linear_image: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "linear f" "inj f" shows "(unicoherent(f ` S) \ unicoherent S)" using assms homeomorphic_unicoherent_eq linear_homeomorphic_image by blast -lemma Borsukian_imp_unicoherent: +lemma%unimportant Borsukian_imp_unicoherent: fixes U :: "'a::euclidean_space set" assumes "Borsukian U" shows "unicoherent U" unfolding unicoherent_def @@ -4997,27 +4998,27 @@ qed -corollary contractible_imp_unicoherent: +corollary%important contractible_imp_unicoherent: fixes U :: "'a::euclidean_space set" assumes "contractible U" shows "unicoherent U" by%unimportant (simp add: Borsukian_imp_unicoherent assms contractible_imp_Borsukian) -corollary convex_imp_unicoherent: +corollary%important convex_imp_unicoherent: fixes U :: "'a::euclidean_space set" assumes "convex U" shows "unicoherent U" by%unimportant (simp add: Borsukian_imp_unicoherent assms convex_imp_Borsukian) text\If the type class constraint can be relaxed, I don't know how!\ -corollary unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)" +corollary%important unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)" by%unimportant (simp add: convex_imp_unicoherent) -lemma unicoherent_monotone_image_compact: +lemma%important unicoherent_monotone_image_compact: fixes T :: "'b :: t2_space set" assumes S: "unicoherent S" "compact S" and contf: "continuous_on S f" and fim: "f ` S = T" and conn: "\y. y \ T \ connected (S \ f -` {y})" shows "unicoherent T" -proof +proof%unimportant fix U V assume UV: "connected U" "connected V" "T = U \ V" and cloU: "closedin (subtopology euclidean T) U" @@ -5053,7 +5054,7 @@ subsection%important\Several common variants of unicoherence\ -lemma connected_frontier_simple: +lemma%unimportant connected_frontier_simple: fixes S :: "'a :: euclidean_space set" assumes "connected S" "connected(- S)" shows "connected(frontier S)" unfolding frontier_closures @@ -5061,18 +5062,18 @@ apply (simp_all add: assms connected_imp_connected_closure) by (simp add: closure_def) -lemma connected_frontier_component_complement: +lemma%unimportant connected_frontier_component_complement: fixes S :: "'a :: euclidean_space set" assumes "connected S" and C: "C \ components(- S)" shows "connected(frontier C)" apply (rule connected_frontier_simple) using C in_components_connected apply blast by (metis Compl_eq_Diff_UNIV connected_UNIV assms top_greatest component_complement_connected) -lemma connected_frontier_disjoint: +lemma%important connected_frontier_disjoint: fixes S :: "'a :: euclidean_space set" assumes "connected S" "connected T" "disjnt S T" and ST: "frontier S \ frontier T" shows "connected(frontier S)" -proof (cases "S = UNIV") +proof%unimportant (cases "S = UNIV") case True then show ?thesis by simp next @@ -5106,11 +5107,11 @@ subsection%important\Some separation results\ -lemma separation_by_component_closed_pointwise: +lemma%important separation_by_component_closed_pointwise: fixes S :: "'a :: euclidean_space set" assumes "closed S" "\ connected_component (- S) a b" obtains C where "C \ components S" "\ connected_component(- C) a b" -proof (cases "a \ S \ b \ S") +proof%unimportant (cases "a \ S \ b \ S") case True then show ?thesis using connected_component_in componentsI that by fastforce @@ -5143,11 +5144,11 @@ qed -lemma separation_by_component_closed: +lemma%important separation_by_component_closed: fixes S :: "'a :: euclidean_space set" assumes "closed S" "\ connected(- S)" obtains C where "C \ components S" "\ connected(- C)" -proof - +proof%unimportant - obtain x y where "closed S" "x \ S" "y \ S" and "\ connected_component (- S) x y" using assms by (auto simp: connected_iff_connected_component) then obtain C where "C \ components S" "\ connected_component(- C) x y" @@ -5157,12 +5158,12 @@ by (metis Compl_iff \C \ components S\ \x \ S\ \y \ S\ connected_component_eq connected_component_eq_eq connected_iff_connected_component that) qed -lemma separation_by_Un_closed_pointwise: +lemma%important separation_by_Un_closed_pointwise: fixes S :: "'a :: euclidean_space set" assumes ST: "closed S" "closed T" "S \ T = {}" and conS: "connected_component (- S) a b" and conT: "connected_component (- T) a b" shows "connected_component (- (S \ T)) a b" -proof (rule ccontr) +proof%unimportant (rule ccontr) have "a \ S" "b \ S" "a \ T" "b \ T" using conS conT connected_component_in by auto assume "\ connected_component (- (S \ T)) a b" @@ -5181,14 +5182,14 @@ by (meson Compl_anti_mono C conS conT connected_component_of_subset) qed -lemma separation_by_Un_closed: +lemma%unimportant separation_by_Un_closed: fixes S :: "'a :: euclidean_space set" assumes ST: "closed S" "closed T" "S \ T = {}" and conS: "connected(- S)" and conT: "connected(- T)" shows "connected(- (S \ T))" using assms separation_by_Un_closed_pointwise by (fastforce simp add: connected_iff_connected_component) -lemma open_unicoherent_UNIV: +lemma%unimportant open_unicoherent_UNIV: fixes S :: "'a :: euclidean_space set" assumes "open S" "open T" "connected S" "connected T" "S \ T = UNIV" shows "connected(S \ T)" @@ -5199,7 +5200,7 @@ by simp qed -lemma separation_by_component_open_aux: +lemma%unimportant separation_by_component_open_aux: fixes S :: "'a :: euclidean_space set" assumes ST: "closed S" "closed T" "S \ T = {}" and "S \ {}" "T \ {}" @@ -5279,11 +5280,11 @@ qed -proposition separation_by_component_open: +lemma%important separation_by_component_open: fixes S :: "'a :: euclidean_space set" assumes "open S" and non: "\ connected(- S)" obtains C where "C \ components S" "\ connected(- C)" -proof - +proof%unimportant - obtain T U where "closed T" "closed U" and TU: "T \ U = - S" "T \ U = {}" "T \ {}" "U \ {}" using assms by (auto simp: connected_closed_set closed_def) @@ -5306,18 +5307,18 @@ qed qed -lemma separation_by_Un_open: +lemma%unimportant separation_by_Un_open: fixes S :: "'a :: euclidean_space set" assumes "open S" "open T" "S \ T = {}" and cS: "connected(-S)" and cT: "connected(-T)" shows "connected(- (S \ T))" using assms unicoherent_UNIV unfolding unicoherent_def by force -lemma nonseparation_by_component_eq: +lemma%important nonseparation_by_component_eq: fixes S :: "'a :: euclidean_space set" assumes "open S \ closed S" shows "((\C \ components S. connected(-C)) \ connected(- S))" (is "?lhs = ?rhs") -proof +proof%unimportant assume ?lhs with assms show ?rhs by (meson separation_by_component_closed separation_by_component_open) next @@ -5327,13 +5328,13 @@ text\Another interesting equivalent of an inessential mapping into C-{0}\ -proposition inessential_eq_extensible: +proposition%important inessential_eq_extensible: fixes f :: "'a::euclidean_space \ complex" assumes "closed S" shows "(\a. homotopic_with (\h. True) S (-{0}) f (\t. a)) \ (\g. continuous_on UNIV g \ (\x \ S. g x = f x) \ (\x. g x \ 0))" (is "?lhs = ?rhs") -proof +proof%unimportant assume ?lhs then obtain a where a: "homotopic_with (\h. True) S (-{0}) f (\t. a)" .. show ?rhs @@ -5393,14 +5394,14 @@ by (simp add: inessential_eq_continuous_logarithm) qed -lemma inessential_on_clopen_Union: +lemma%important inessential_on_clopen_Union: fixes \ :: "'a::euclidean_space set set" assumes T: "path_connected T" and "\S. S \ \ \ closedin (subtopology euclidean (\\)) S" and "\S. S \ \ \ openin (subtopology euclidean (\\)) S" and hom: "\S. S \ \ \ \a. homotopic_with (\x. True) S T f (\x. a)" obtains a where "homotopic_with (\x. True) (\\) T f (\x. a)" -proof (cases "\\ = {}") +proof%unimportant (cases "\\ = {}") case True with that show ?thesis by force @@ -5441,12 +5442,12 @@ then show ?thesis .. qed -proposition Janiszewski_dual: +lemma%important Janiszewski_dual: fixes S :: "complex set" assumes "compact S" "compact T" "connected S" "connected T" "connected(- (S \ T))" shows "connected(S \ T)" -proof - +proof%unimportant - have ST: "compact (S \ T)" by (simp add: assms compact_Un) with Borsukian_imp_unicoherent [of "S \ T"] ST assms diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Great_Picard.thy --- a/src/HOL/Analysis/Great_Picard.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Great_Picard.thy Thu Jan 17 16:22:21 2019 -0500 @@ -9,13 +9,13 @@ subsection\Schottky's theorem\ -lemma Schottky_lemma0: +lemma%important Schottky_lemma0: assumes holf: "f holomorphic_on S" and cons: "contractible S" and "a \ S" and f: "\z. z \ S \ f z \ 1 \ f z \ -1" obtains g where "g holomorphic_on S" "norm(g a) \ 1 + norm(f a) / 3" "\z. z \ S \ f z = cos(of_real pi * g z)" -proof - +proof%unimportant - obtain g where holg: "g holomorphic_on S" and g: "norm(g a) \ pi + norm(f a)" and f_eq_cos: "\z. z \ S \ f z = cos(g z)" using contractible_imp_holomorphic_arccos_bounded [OF assms] @@ -38,7 +38,7 @@ qed -lemma Schottky_lemma1: +lemma%unimportant Schottky_lemma1: fixes n::nat assumes "0 < n" shows "0 < n + sqrt(real n ^ 2 - 1)" @@ -54,7 +54,7 @@ qed -lemma Schottky_lemma2: +lemma%unimportant Schottky_lemma2: fixes x::real assumes "0 \ x" obtains n where "0 < n" "\x - ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi\ < 1/2" @@ -158,12 +158,12 @@ qed -lemma Schottky_lemma3: +lemma%important Schottky_lemma3: fixes z::complex assumes "z \ (\m \ Ints. \n \ {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)}) \ (\m \ Ints. \n \ {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)})" shows "cos(pi * cos(pi * z)) = 1 \ cos(pi * cos(pi * z)) = -1" -proof - +proof%unimportant - have sqrt2 [simp]: "complex_of_real (sqrt x) * complex_of_real (sqrt x) = x" if "x \ 0" for x::real by (metis abs_of_nonneg of_real_mult real_sqrt_mult_self that) have 1: "\k. exp (\ * (of_int m * complex_of_real pi) - @@ -223,13 +223,13 @@ qed -theorem Schottky: +theorem%important Schottky: assumes holf: "f holomorphic_on cball 0 1" and nof0: "norm(f 0) \ r" and not01: "\z. z \ cball 0 1 \ \(f z = 0 \ f z = 1)" and "0 < t" "t < 1" "norm z \ t" shows "norm(f z) \ exp(pi * exp(pi * (2 + 2 * r + 12 * t / (1 - t))))" -proof - +proof%unimportant - obtain h where holf: "h holomorphic_on cball 0 1" and nh0: "norm (h 0) \ 1 + norm(2 * f 0 - 1) / 3" and h: "\z. z \ cball 0 1 \ 2 * f z - 1 = cos(of_real pi * h z)" @@ -376,12 +376,12 @@ subsection%important\The Little Picard Theorem\ -proposition Landau_Picard: +lemma%important Landau_Picard: obtains R where "\z. 0 < R z" "\f. \f holomorphic_on cball 0 (R(f 0)); \z. norm z \ R(f 0) \ f z \ 0 \ f z \ 1\ \ norm(deriv f 0) < 1" -proof - +proof%unimportant - define R where "R \ \z. 3 * exp(pi * exp(pi*(2 + 2 * cmod z + 12)))" show ?thesis proof @@ -436,10 +436,10 @@ qed qed -lemma little_Picard_01: +lemma%important little_Picard_01: assumes holf: "f holomorphic_on UNIV" and f01: "\z. f z \ 0 \ f z \ 1" obtains c where "f = (\x. c)" -proof - +proof%unimportant - obtain R where Rpos: "\z. 0 < R z" and R: "\h. \h holomorphic_on cball 0 (R(h 0)); @@ -481,11 +481,11 @@ qed -theorem little_Picard: +theorem%important little_Picard: assumes holf: "f holomorphic_on UNIV" and "a \ b" "range f \ {a,b} = {}" obtains c where "f = (\x. c)" -proof - +proof%unimportant - let ?g = "\x. 1/(b - a)*(f x - b) + 1" obtain c where "?g = (\x. c)" proof (rule little_Picard_01) @@ -505,7 +505,7 @@ text\A couple of little applications of Little Picard\ -lemma holomorphic_periodic_fixpoint: +lemma%unimportant holomorphic_periodic_fixpoint: assumes holf: "f holomorphic_on UNIV" and "p \ 0" and per: "\z. f(z + p) = f z" obtains x where "f x = x" @@ -527,7 +527,7 @@ qed -lemma holomorphic_involution_point: +lemma%unimportant holomorphic_involution_point: assumes holfU: "f holomorphic_on UNIV" and non: "\a. f \ (\x. a + x)" obtains x where "f(f x) = x" proof - @@ -616,7 +616,7 @@ subsection%important\The Arzelà--Ascoli theorem\ -lemma subsequence_diagonalization_lemma: +lemma%unimportant subsequence_diagonalization_lemma: fixes P :: "nat \ (nat \ 'a) \ bool" assumes sub: "\i r. \k. strict_mono (k :: nat \ nat) \ P i (r \ k)" and P_P: "\i r::nat \ 'a. \k1 k2 N. @@ -660,7 +660,7 @@ qed qed -lemma function_convergent_subsequence: +lemma%unimportant function_convergent_subsequence: fixes f :: "[nat,'a] \ 'b::{real_normed_vector,heine_borel}" assumes "countable S" and M: "\n::nat. \x. x \ S \ norm(f n x) \ M" obtains k where "strict_mono (k::nat\nat)" "\x. x \ S \ \l. (\n. f (k n) x) \ l" @@ -698,7 +698,7 @@ qed -theorem Arzela_Ascoli: +theorem%important Arzela_Ascoli: fixes \ :: "[nat,'a::euclidean_space] \ 'b::{real_normed_vector,heine_borel}" assumes "compact S" and M: "\n x. x \ S \ norm(\ n x) \ M" @@ -707,7 +707,7 @@ \ \d. 0 < d \ (\n y. y \ S \ norm(x - y) < d \ norm(\ n x - \ n y) < e)" obtains g k where "continuous_on S g" "strict_mono (k :: nat \ nat)" "\e. 0 < e \ \N. \n x. n \ N \ x \ S \ norm(\(k n) x - g x) < e" -proof - +proof%unimportant - have UEQ: "\e. 0 < e \ \d. 0 < d \ (\n. \x \ S. \x' \ S. dist x' x < d \ dist (\ n x') (\ n x) < e)" apply (rule compact_uniformly_equicontinuous [OF \compact S\, of "range \"]) using equicont by (force simp: dist_commute dist_norm)+ @@ -795,7 +795,7 @@ holomorphic function, and converges \emph{uniformly} on compact subsets of S.\ -theorem Montel: +theorem%important Montel: fixes \ :: "[nat,complex] \ complex" assumes "open S" and \: "\h. h \ \ \ h holomorphic_on S" @@ -805,7 +805,7 @@ where "g holomorphic_on S" "strict_mono (r :: nat \ nat)" "\x. x \ S \ ((\n. \ (r n) x) \ g x) sequentially" "\K. \compact K; K \ S\ \ uniform_limit K (\ \ r) g sequentially" -proof - +proof%unimportant - obtain K where comK: "\n. compact(K n)" and KS: "\n::nat. K n \ S" and subK: "\X. \compact X; X \ S\ \ \N. \n\N. X \ K n" using open_Union_compact_subsets [OF \open S\] by metis @@ -995,7 +995,7 @@ subsection%important\Some simple but useful cases of Hurwitz's theorem\ -proposition Hurwitz_no_zeros: +proposition%important Hurwitz_no_zeros: assumes S: "open S" "connected S" and holf: "\n::nat. \ n holomorphic_on S" and holg: "g holomorphic_on S" @@ -1004,7 +1004,7 @@ and nz: "\n z. z \ S \ \ n z \ 0" and "z0 \ S" shows "g z0 \ 0" -proof +proof%unimportant assume g0: "g z0 = 0" obtain h r m where "0 < m" "0 < r" and subS: "ball z0 r \ S" @@ -1159,7 +1159,7 @@ ultimately show False using \0 < m\ by auto qed -corollary Hurwitz_injective: +corollary%important Hurwitz_injective: assumes S: "open S" "connected S" and holf: "\n::nat. \ n holomorphic_on S" and holg: "g holomorphic_on S" @@ -1167,7 +1167,7 @@ and nonconst: "\ g constant_on S" and inj: "\n. inj_on (\ n) S" shows "inj_on g S" -proof - +proof%unimportant - have False if z12: "z1 \ S" "z2 \ S" "z1 \ z2" "g z2 = g z1" for z1 z2 proof - obtain z0 where "z0 \ S" and z0: "g z0 \ g z2" @@ -1231,13 +1231,13 @@ subsection%important\The Great Picard theorem\ -lemma GPicard1: +lemma%important GPicard1: assumes S: "open S" "connected S" and "w \ S" "0 < r" "Y \ X" and holX: "\h. h \ X \ h holomorphic_on S" and X01: "\h z. \h \ X; z \ S\ \ h z \ 0 \ h z \ 1" and r: "\h. h \ Y \ norm(h w) \ r" obtains B Z where "0 < B" "open Z" "w \ Z" "Z \ S" "\h z. \h \ Y; z \ Z\ \ norm(h z) \ B" -proof - +proof%unimportant - obtain e where "e > 0" and e: "cball w e \ S" using assms open_contains_cball_eq by blast show ?thesis @@ -1277,20 +1277,20 @@ qed (use \e > 0\ in auto) qed -lemma GPicard2: +lemma%important GPicard2: assumes "S \ T" "connected T" "S \ {}" "open S" "\x. \x islimpt S; x \ T\ \ x \ S" shows "S = T" - by (metis assms open_subset connected_clopen closedin_limpt) + by%unimportant (metis assms open_subset connected_clopen closedin_limpt) -lemma GPicard3: +lemma%important GPicard3: assumes S: "open S" "connected S" "w \ S" and "Y \ X" and holX: "\h. h \ X \ h holomorphic_on S" and X01: "\h z. \h \ X; z \ S\ \ h z \ 0 \ h z \ 1" and no_hw_le1: "\h. h \ Y \ norm(h w) \ 1" and "compact K" "K \ S" obtains B where "\h z. \h \ Y; z \ K\ \ norm(h z) \ B" -proof - +proof%unimportant - define U where "U \ {z \ S. \B Z. 0 < B \ open Z \ z \ Z \ Z \ S \ (\h z'. h \ Y \ z' \ Z \ norm(h z') \ B)}" then have "U \ S" by blast @@ -1432,11 +1432,11 @@ qed -lemma GPicard4: +lemma%important GPicard4: assumes "0 < k" and holf: "f holomorphic_on (ball 0 k - {0})" and AE: "\e. \0 < e; e < k\ \ \d. 0 < d \ d < e \ (\z \ sphere 0 d. norm(f z) \ B)" obtains \ where "0 < \" "\ < k" "\z. z \ ball 0 \ - {0} \ norm(f z) \ B" -proof - +proof%unimportant - obtain \ where "0 < \" "\ < k/2" and \: "\z. norm z = \ \ norm(f z) \ B" using AE [of "k/2"] \0 < k\ by auto show ?thesis @@ -1471,13 +1471,13 @@ qed -lemma GPicard5: +lemma%important GPicard5: assumes holf: "f holomorphic_on (ball 0 1 - {0})" and f01: "\z. z \ ball 0 1 - {0} \ f z \ 0 \ f z \ 1" obtains e B where "0 < e" "e < 1" "0 < B" "(\z \ ball 0 e - {0}. norm(f z) \ B) \ (\z \ ball 0 e - {0}. norm(f z) \ B)" -proof - +proof%unimportant - have [simp]: "1 + of_nat n \ (0::complex)" for n using of_nat_eq_0_iff by fastforce have [simp]: "cmod (1 + of_nat n) = 1 + of_nat n" for n @@ -1614,13 +1614,13 @@ qed -lemma GPicard6: +lemma%important GPicard6: assumes "open M" "z \ M" "a \ 0" and holf: "f holomorphic_on (M - {z})" and f0a: "\w. w \ M - {z} \ f w \ 0 \ f w \ a" obtains r where "0 < r" "ball z r \ M" "bounded(f ` (ball z r - {z})) \ bounded((inverse \ f) ` (ball z r - {z}))" -proof - +proof%unimportant - obtain r where "0 < r" and r: "ball z r \ M" using assms openE by blast let ?g = "\w. f (z + of_real r * w) / a" @@ -1669,11 +1669,11 @@ qed -theorem great_Picard: +theorem%important great_Picard: assumes "open M" "z \ M" "a \ b" and holf: "f holomorphic_on (M - {z})" and fab: "\w. w \ M - {z} \ f w \ a \ f w \ b" obtains l where "(f \ l) (at z) \ ((inverse \ f) \ l) (at z)" -proof - +proof%unimportant - obtain r where "0 < r" and zrM: "ball z r \ M" and r: "bounded((\z. f z - a) ` (ball z r - {z})) \ bounded((inverse \ (\z. f z - a)) ` (ball z r - {z}))" @@ -1776,7 +1776,7 @@ qed -corollary great_Picard_alt: +corollary%important great_Picard_alt: assumes M: "open M" "z \ M" and holf: "f holomorphic_on (M - {z})" and non: "\l. \ (f \ l) (at z)" "\l. \ ((inverse \ f) \ l) (at z)" obtains a where "- {a} \ f ` (M - {z})" @@ -1784,11 +1784,11 @@ by%unimportant (metis great_Picard [OF M _ holf] non) -corollary great_Picard_infinite: +corollary%important great_Picard_infinite: assumes M: "open M" "z \ M" and holf: "f holomorphic_on (M - {z})" and non: "\l. \ (f \ l) (at z)" "\l. \ ((inverse \ f) \ l) (at z)" obtains a where "\w. w \ a \ infinite {x. x \ M - {z} \ f x = w}" -proof - +proof%unimportant - have False if "a \ b" and ab: "finite {x. x \ M - {z} \ f x = a}" "finite {x. x \ M - {z} \ f x = b}" for a b proof - have finab: "finite {x. x \ M - {z} \ f x \ {a,b}}" @@ -1830,11 +1830,11 @@ by meson qed -theorem Casorati_Weierstrass: +corollary%important Casorati_Weierstrass: assumes "open M" "z \ M" "f holomorphic_on (M - {z})" and "\l. \ (f \ l) (at z)" "\l. \ ((inverse \ f) \ l) (at z)" shows "closure(f ` (M - {z})) = UNIV" -proof - +proof%unimportant - obtain a where a: "- {a} \ f ` (M - {z})" using great_Picard_alt [OF assms] . have "UNIV = closure(- {a})" diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Homeomorphism.thy --- a/src/HOL/Analysis/Homeomorphism.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Homeomorphism.thy Thu Jan 17 16:22:21 2019 -0500 @@ -8,7 +8,7 @@ imports Homotopy begin -lemma homeomorphic_spheres': +lemma%unimportant homeomorphic_spheres': fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space" assumes "0 < \" and dimeq: "DIM('a) = DIM('b)" shows "(sphere a \) homeomorphic (sphere b \)" @@ -28,7 +28,7 @@ done qed -lemma homeomorphic_spheres_gen: +lemma%unimportant homeomorphic_spheres_gen: fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space" assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)" shows "(sphere a r homeomorphic sphere b s)" @@ -38,7 +38,7 @@ subsection%important \Homeomorphism of all convex compact sets with nonempty interior\ -proposition ray_to_rel_frontier: +proposition%important ray_to_rel_frontier: fixes a :: "'a::real_inner" assumes "bounded S" and a: "a \ rel_interior S" @@ -46,7 +46,7 @@ and "l \ 0" obtains d where "0 < d" "(a + d *\<^sub>R l) \ rel_frontier S" "\e. \0 \ e; e < d\ \ (a + e *\<^sub>R l) \ rel_interior S" -proof - +proof%unimportant - have aaff: "a \ affine hull S" by (meson a hull_subset rel_interior_subset rev_subsetD) let ?D = "{d. 0 < d \ a + d *\<^sub>R l \ rel_interior S}" @@ -139,14 +139,14 @@ by (rule that [OF \0 < d\ infront inint]) qed -corollary ray_to_frontier: +corollary%important ray_to_frontier: fixes a :: "'a::euclidean_space" assumes "bounded S" and a: "a \ interior S" and "l \ 0" obtains d where "0 < d" "(a + d *\<^sub>R l) \ frontier S" "\e. \0 \ e; e < d\ \ (a + e *\<^sub>R l) \ interior S" -proof - +proof%unimportant - have "interior S = rel_interior S" using a rel_interior_nonempty_interior by auto then have "a \ rel_interior S" @@ -158,7 +158,7 @@ qed -lemma segment_to_rel_frontier_aux: +lemma%unimportant segment_to_rel_frontier_aux: fixes x :: "'a::euclidean_space" assumes "convex S" "bounded S" and x: "x \ rel_interior S" and y: "y \ S" and xy: "x \ y" obtains z where "z \ rel_frontier S" "y \ closed_segment x z" @@ -198,7 +198,7 @@ qed qed -lemma segment_to_rel_frontier: +lemma%unimportant segment_to_rel_frontier: fixes x :: "'a::euclidean_space" assumes S: "convex S" "bounded S" and x: "x \ rel_interior S" and y: "y \ S" and xy: "\(x = y \ S = {x})" @@ -216,11 +216,11 @@ using segment_to_rel_frontier_aux [OF S x y] that by blast qed -proposition rel_frontier_not_sing: +proposition%important rel_frontier_not_sing: fixes a :: "'a::euclidean_space" assumes "bounded S" shows "rel_frontier S \ {a}" -proof (cases "S = {}") +proof%unimportant (cases "S = {}") case True then show ?thesis by simp next case False @@ -278,7 +278,7 @@ qed qed -proposition (*FIXME needs name *) +proposition%important fixes S :: "'a::euclidean_space set" assumes "compact S" and 0: "0 \ rel_interior S" and star: "\x. x \ S \ open_segment 0 x \ rel_interior S" @@ -288,7 +288,7 @@ and starlike_compact_projective2_0: "S homeomorphic cball 0 1 \ affine hull S" (is "S homeomorphic ?CBALL") -proof - +proof%unimportant - have starI: "(u *\<^sub>R x) \ rel_interior S" if "x \ S" "0 \ u" "u < 1" for x u proof (cases "x=0 \ u=0") case True with 0 show ?thesis by force @@ -540,7 +540,7 @@ done qed -corollary (* FIXME needs name *) +corollary%important fixes S :: "'a::euclidean_space set" assumes "compact S" and a: "a \ rel_interior S" and star: "\x. x \ S \ open_segment a x \ rel_interior S" @@ -548,7 +548,7 @@ "S - rel_interior S homeomorphic sphere a 1 \ affine hull S" and starlike_compact_projective2: "S homeomorphic cball a 1 \ affine hull S" -proof - +proof%unimportant - have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation) have 2: "0 \ rel_interior ((+) (-a) ` S)" using a rel_interior_translation [of "- a" S] by (simp cong: image_cong_simp) @@ -580,12 +580,12 @@ finally show "S homeomorphic cball a 1 \ affine hull S" . qed -corollary starlike_compact_projective_special: +corollary%important starlike_compact_projective_special: assumes "compact S" and cb01: "cball (0::'a::euclidean_space) 1 \ S" and scale: "\x u. \x \ S; 0 \ u; u < 1\ \ u *\<^sub>R x \ S - frontier S" shows "S homeomorphic (cball (0::'a::euclidean_space) 1)" -proof - +proof%unimportant - have "ball 0 1 \ interior S" using cb01 interior_cball interior_mono by blast then have 0: "0 \ rel_interior S" @@ -604,13 +604,13 @@ using starlike_compact_projective2_0 [OF \compact S\ 0 star] by simp qed -lemma homeomorphic_convex_lemma: +lemma%important homeomorphic_convex_lemma: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "convex S" "compact S" "convex T" "compact T" and affeq: "aff_dim S = aff_dim T" shows "(S - rel_interior S) homeomorphic (T - rel_interior T) \ S homeomorphic T" -proof (cases "rel_interior S = {} \ rel_interior T = {}") +proof%unimportant (cases "rel_interior S = {} \ rel_interior T = {}") case True then show ?thesis by (metis Diff_empty affeq \convex S\ \convex T\ aff_dim_empty homeomorphic_empty rel_interior_eq_empty aff_dim_empty) @@ -708,7 +708,7 @@ using 1 2 by blast qed -lemma homeomorphic_convex_compact_sets: +lemma%unimportant homeomorphic_convex_compact_sets: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "convex S" "compact S" "convex T" "compact T" and affeq: "aff_dim S = aff_dim T" @@ -716,7 +716,7 @@ using homeomorphic_convex_lemma [OF assms] assms by (auto simp: rel_frontier_def) -lemma homeomorphic_rel_frontiers_convex_bounded_sets: +lemma%unimportant homeomorphic_rel_frontiers_convex_bounded_sets: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "convex S" "bounded S" "convex T" "bounded T" and affeq: "aff_dim S = aff_dim T" @@ -729,7 +729,7 @@ text\Including the famous stereoscopic projection of the 3-D sphere to the complex plane\ text\The special case with centre 0 and radius 1\ -lemma homeomorphic_punctured_affine_sphere_affine_01: +lemma%unimportant homeomorphic_punctured_affine_sphere_affine_01: assumes "b \ sphere 0 1" "affine T" "0 \ T" "b \ T" "affine p" and affT: "aff_dim T = aff_dim p + 1" shows "(sphere 0 1 \ T) - {b} homeomorphic p" @@ -823,12 +823,12 @@ finally show ?thesis . qed -theorem homeomorphic_punctured_affine_sphere_affine: +theorem%important homeomorphic_punctured_affine_sphere_affine: fixes a :: "'a :: euclidean_space" assumes "0 < r" "b \ sphere a r" "affine T" "a \ T" "b \ T" "affine p" and aff: "aff_dim T = aff_dim p + 1" shows "(sphere a r \ T) - {b} homeomorphic p" -proof - +proof%unimportant - have "a \ b" using assms by auto then have inj: "inj (\x::'a. x /\<^sub>R norm (a - b))" by (simp add: inj_on_def) @@ -847,14 +847,14 @@ finally show ?thesis . qed -corollary homeomorphic_punctured_sphere_affine: +corollary%important homeomorphic_punctured_sphere_affine: fixes a :: "'a :: euclidean_space" assumes "0 < r" and b: "b \ sphere a r" and "affine T" and affS: "aff_dim T + 1 = DIM('a)" shows "(sphere a r - {b}) homeomorphic T" using%unimportant homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by%unimportant auto -corollary homeomorphic_punctured_sphere_hyperplane: +corollary%important homeomorphic_punctured_sphere_hyperplane: fixes a :: "'a :: euclidean_space" assumes "0 < r" and b: "b \ sphere a r" and "c \ 0" @@ -864,12 +864,12 @@ apply (auto simp: affine_hyperplane of_nat_diff) done -proposition homeomorphic_punctured_sphere_affine_gen: +proposition%important homeomorphic_punctured_sphere_affine_gen: fixes a :: "'a :: euclidean_space" assumes "convex S" "bounded S" and a: "a \ rel_frontier S" and "affine T" and affS: "aff_dim S = aff_dim T + 1" shows "rel_frontier S - {a} homeomorphic T" -proof - +proof%unimportant - obtain U :: "'a set" where "affine U" "convex U" and affdS: "aff_dim U = aff_dim S" using choose_affine_subset [OF affine_UNIV aff_dim_geq] by (meson aff_dim_affine_hull affine_affine_hull affine_imp_convex) @@ -912,13 +912,13 @@ is homeomorphic to a closed subset of a convex set, and if the set is locally compact we can take the convex set to be the universe.\ -proposition homeomorphic_closedin_convex: +proposition%important homeomorphic_closedin_convex: fixes S :: "'m::euclidean_space set" assumes "aff_dim S < DIM('n)" obtains U and T :: "'n::euclidean_space set" where "convex U" "U \ {}" "closedin (subtopology euclidean U) T" "S homeomorphic T" -proof (cases "S = {}") +proof%unimportant (cases "S = {}") case True then show ?thesis by (rule_tac U=UNIV and T="{}" in that) auto next @@ -1009,11 +1009,11 @@ text\ Locally compact sets are closed in an open set and are homeomorphic to an absolutely closed set if we have one more dimension to play with.\ -lemma locally_compact_open_Int_closure: +lemma%important locally_compact_open_Int_closure: fixes S :: "'a :: metric_space set" assumes "locally compact S" obtains T where "open T" "S = T \ closure S" -proof - +proof%unimportant - have "\x\S. \T v u. u = S \ T \ x \ u \ u \ v \ v \ S \ open T \ compact v" by (metis assms locally_compact openin_open) then obtain t v where @@ -1048,14 +1048,14 @@ qed -lemma locally_compact_closedin_open: +lemma%unimportant locally_compact_closedin_open: fixes S :: "'a :: metric_space set" assumes "locally compact S" obtains T where "open T" "closedin (subtopology euclidean T) S" by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int) -lemma locally_compact_homeomorphism_projection_closed: +lemma%unimportant locally_compact_homeomorphism_projection_closed: assumes "locally compact S" obtains T and f :: "'a \ 'a :: euclidean_space \ 'b :: euclidean_space" where "closed T" "homeomorphism S T f fst" @@ -1108,14 +1108,14 @@ done qed -lemma locally_compact_closed_Int_open: +lemma%unimportant locally_compact_closed_Int_open: fixes S :: "'a :: euclidean_space set" shows "locally compact S \ (\U u. closed U \ open u \ S = U \ u)" by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact) -lemma lowerdim_embeddings: +lemma%unimportant lowerdim_embeddings: assumes "DIM('a) < DIM('b)" obtains f :: "'a::euclidean_space*real \ 'b::euclidean_space" and g :: "'b \ 'a*real" @@ -1161,11 +1161,11 @@ qed qed -proposition locally_compact_homeomorphic_closed: +proposition%important locally_compact_homeomorphic_closed: fixes S :: "'a::euclidean_space set" assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)" obtains T :: "'b::euclidean_space set" where "closed T" "S homeomorphic T" -proof - +proof%unimportant - obtain U:: "('a*real)set" and h where "closed U" and homU: "homeomorphism S U h fst" using locally_compact_homeomorphism_projection_closed assms by metis @@ -1191,13 +1191,13 @@ qed -lemma homeomorphic_convex_compact_lemma: +lemma%important homeomorphic_convex_compact_lemma: fixes S :: "'a::euclidean_space set" assumes "convex S" and "compact S" and "cball 0 1 \ S" shows "S homeomorphic (cball (0::'a) 1)" -proof (rule starlike_compact_projective_special[OF assms(2-3)]) +proof%unimportant (rule starlike_compact_projective_special[OF assms(2-3)]) fix x u assume "x \ S" and "0 \ u" and "u < (1::real)" have "open (ball (u *\<^sub>R x) (1 - u))" @@ -1223,7 +1223,7 @@ using frontier_def and interior_subset by auto qed -proposition homeomorphic_convex_compact_cball: +proposition%important homeomorphic_convex_compact_cball: fixes e :: real and S :: "'a::euclidean_space set" assumes "convex S" @@ -1231,7 +1231,7 @@ and "interior S \ {}" and "e > 0" shows "S homeomorphic (cball (b::'a) e)" -proof - +proof%unimportant - obtain a where "a \ interior S" using assms(3) by auto then obtain d where "d > 0" and d: "cball a d \ S" @@ -1259,7 +1259,7 @@ done qed -corollary homeomorphic_convex_compact: +corollary%important homeomorphic_convex_compact: fixes S :: "'a::euclidean_space set" and T :: "'a set" assumes "convex S" "compact S" "interior S \ {}" @@ -1268,7 +1268,7 @@ using assms by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym) -subsection\Covering spaces and lifting results for them\ +subsection%important\Covering spaces and lifting results for them\ definition%important covering_space :: "'a::topological_space set \ ('a \ 'b) \ 'b::topological_space set \ bool" @@ -1281,19 +1281,19 @@ pairwise disjnt v \ (\u \ v. \q. homeomorphism u T p q)))" -lemma covering_space_imp_continuous: "covering_space c p S \ continuous_on c p" +lemma%unimportant covering_space_imp_continuous: "covering_space c p S \ continuous_on c p" by (simp add: covering_space_def) -lemma covering_space_imp_surjective: "covering_space c p S \ p ` c = S" +lemma%unimportant covering_space_imp_surjective: "covering_space c p S \ p ` c = S" by (simp add: covering_space_def) -lemma homeomorphism_imp_covering_space: "homeomorphism S T f g \ covering_space S f T" +lemma%unimportant homeomorphism_imp_covering_space: "homeomorphism S T f g \ covering_space S f T" apply (simp add: homeomorphism_def covering_space_def, clarify) apply (rule_tac x=T in exI, simp) apply (rule_tac x="{S}" in exI, auto) done -lemma covering_space_local_homeomorphism: +lemma%unimportant covering_space_local_homeomorphism: assumes "covering_space c p S" "x \ c" obtains T u q where "x \ T" "openin (subtopology euclidean c) T" "p x \ u" "openin (subtopology euclidean S) u" @@ -1304,13 +1304,13 @@ by (metis IntI UnionE vimage_eq) -lemma covering_space_local_homeomorphism_alt: +lemma%important covering_space_local_homeomorphism_alt: assumes p: "covering_space c p S" and "y \ S" obtains x T U q where "p x = y" "x \ T" "openin (subtopology euclidean c) T" "y \ U" "openin (subtopology euclidean S) U" "homeomorphism T U p q" -proof - +proof%unimportant - obtain x where "p x = y" "x \ c" using assms covering_space_imp_surjective by blast show ?thesis @@ -1318,11 +1318,11 @@ using that \p x = y\ by blast qed -proposition covering_space_open_map: +proposition%important covering_space_open_map: fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set" assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T" shows "openin (subtopology euclidean S) (p ` T)" -proof - +proof%unimportant - have pce: "p ` c = S" and covs: "\x. x \ S \ @@ -1368,7 +1368,7 @@ with openin_subopen show ?thesis by blast qed -lemma covering_space_lift_unique_gen: +lemma%important covering_space_lift_unique_gen: fixes f :: "'a::topological_space \ 'b::topological_space" fixes g1 :: "'a \ 'c::real_normed_vector" assumes cov: "covering_space c p S" @@ -1380,7 +1380,7 @@ and fg2: "\x. x \ T \ f x = p(g2 x)" and u_compt: "U \ components T" and "a \ U" "x \ U" shows "g1 x = g2 x" -proof - +proof%unimportant - have "U \ T" by (rule in_components_subset [OF u_compt]) define G12 where "G12 \ {x \ U. g1 x - g2 x = 0}" have "connected U" by (rule in_components_connected [OF u_compt]) @@ -1427,7 +1427,7 @@ using \x \ U\ by force qed -proposition covering_space_lift_unique: +proposition%important covering_space_lift_unique: fixes f :: "'a::topological_space \ 'b::topological_space" fixes g1 :: "'a \ 'c::real_normed_vector" assumes "covering_space c p S" @@ -1437,10 +1437,10 @@ "continuous_on T g2" "g2 ` T \ c" "\x. x \ T \ f x = p(g2 x)" "connected T" "a \ T" "x \ T" shows "g1 x = g2 x" - using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv - by blast + using%unimportant covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv + by%unimportant blast -lemma covering_space_locally: +lemma%unimportant covering_space_locally: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes loc: "locally \ C" and cov: "covering_space C p S" and pim: "\T. \T \ C; \ T\ \ \(p ` T)" @@ -1456,14 +1456,14 @@ qed -proposition covering_space_locally_eq: +proposition%important covering_space_locally_eq: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes cov: "covering_space C p S" and pim: "\T. \T \ C; \ T\ \ \(p ` T)" and qim: "\q U. \U \ S; continuous_on U q; \ U\ \ \(q ` U)" shows "locally \ S \ locally \ C" (is "?lhs = ?rhs") -proof +proof%unimportant assume L: ?lhs show ?rhs proof (rule locallyI) @@ -1518,7 +1518,7 @@ using cov covering_space_locally pim by blast qed -lemma covering_space_locally_compact_eq: +lemma%unimportant covering_space_locally_compact_eq: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes "covering_space C p S" shows "locally compact S \ locally compact C" @@ -1526,7 +1526,7 @@ apply (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous) using compact_continuous_image by blast -lemma covering_space_locally_connected_eq: +lemma%unimportant covering_space_locally_connected_eq: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes "covering_space C p S" shows "locally connected S \ locally connected C" @@ -1534,7 +1534,7 @@ apply (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous) using connected_continuous_image by blast -lemma covering_space_locally_path_connected_eq: +lemma%unimportant covering_space_locally_path_connected_eq: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes "covering_space C p S" shows "locally path_connected S \ locally path_connected C" @@ -1543,26 +1543,26 @@ using path_connected_continuous_image by blast -lemma covering_space_locally_compact: +lemma%unimportant covering_space_locally_compact: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes "locally compact C" "covering_space C p S" shows "locally compact S" using assms covering_space_locally_compact_eq by blast -lemma covering_space_locally_connected: +lemma%unimportant covering_space_locally_connected: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes "locally connected C" "covering_space C p S" shows "locally connected S" using assms covering_space_locally_connected_eq by blast -lemma covering_space_locally_path_connected: +lemma%unimportant covering_space_locally_path_connected: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes "locally path_connected C" "covering_space C p S" shows "locally path_connected S" using assms covering_space_locally_path_connected_eq by blast -proposition covering_space_lift_homotopy: +proposition%important covering_space_lift_homotopy: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" and h :: "real \ 'c::real_normed_vector \ 'b" assumes cov: "covering_space C p S" @@ -1574,7 +1574,7 @@ "k ` ({0..1} \ U) \ C" "\y. y \ U \ k(0, y) = f y" "\z. z \ {0..1} \ U \ h z = p(k z)" -proof - +proof%unimportant - have "\V k. openin (subtopology euclidean U) V \ y \ V \ continuous_on ({0..1} \ V) k \ k ` ({0..1} \ V) \ C \ (\z \ V. k(0, z) = f z) \ (\z \ {0..1} \ V. h z = p(k z))" @@ -1912,7 +1912,7 @@ qed (auto simp: contk) qed -corollary covering_space_lift_homotopy_alt: +corollary%important covering_space_lift_homotopy_alt: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" and h :: "'c::real_normed_vector \ real \ 'b" assumes cov: "covering_space C p S" @@ -1924,7 +1924,7 @@ "k ` (U \ {0..1}) \ C" "\y. y \ U \ k(y, 0) = f y" "\z. z \ U \ {0..1} \ h z = p(k z)" -proof - +proof%unimportant - have "continuous_on ({0..1} \ U) (h \ (\z. (snd z, fst z)))" by (intro continuous_intros continuous_on_subset [OF conth]) auto then obtain k where contk: "continuous_on ({0..1} \ U) k" @@ -1940,7 +1940,7 @@ done qed -corollary covering_space_lift_homotopic_function: +corollary%important covering_space_lift_homotopic_function: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" and g:: "'c::real_normed_vector \ 'a" assumes cov: "covering_space C p S" and contg: "continuous_on U g" @@ -1948,7 +1948,7 @@ and pgeq: "\y. y \ U \ p(g y) = f y" and hom: "homotopic_with (\x. True) U S f f'" obtains g' where "continuous_on U g'" "image g' U \ C" "\y. y \ U \ p(g' y) = f' y" -proof - +proof%unimportant - obtain h where conth: "continuous_on ({0..1::real} \ U) h" and him: "h ` ({0..1} \ U) \ S" and h0: "\x. h(0, x) = f x" @@ -1972,12 +1972,12 @@ qed qed -corollary covering_space_lift_inessential_function: +corollary%important covering_space_lift_inessential_function: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" and U :: "'c::real_normed_vector set" assumes cov: "covering_space C p S" and hom: "homotopic_with (\x. True) U S f (\x. a)" obtains g where "continuous_on U g" "g ` U \ C" "\y. y \ U \ p(g y) = f y" -proof (cases "U = {}") +proof%unimportant (cases "U = {}") case True then show ?thesis using that continuous_on_empty by blast @@ -1997,14 +1997,14 @@ subsection%important\ Lifting of general functions to covering space\ -proposition covering_space_lift_path_strong: +proposition%important covering_space_lift_path_strong: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" and f :: "'c::real_normed_vector \ 'b" assumes cov: "covering_space C p S" and "a \ C" and "path g" and pag: "path_image g \ S" and pas: "pathstart g = p a" obtains h where "path h" "path_image h \ C" "pathstart h = a" and "\t. t \ {0..1} \ p(h t) = g t" -proof - +proof%unimportant - obtain k:: "real \ 'c \ 'a" where contk: "continuous_on ({0..1} \ {undefined}) k" and kim: "k ` ({0..1} \ {undefined}) \ C" @@ -2033,11 +2033,11 @@ qed qed -corollary covering_space_lift_path: +corollary%important covering_space_lift_path: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes cov: "covering_space C p S" and "path g" and pig: "path_image g \ S" obtains h where "path h" "path_image h \ C" "\t. t \ {0..1} \ p(h t) = g t" -proof - +proof%unimportant - obtain a where "a \ C" "pathstart g = p a" by (metis pig cov covering_space_imp_surjective imageE pathstart_in_path_image subsetCE) show ?thesis @@ -2046,7 +2046,7 @@ qed -proposition covering_space_lift_homotopic_paths: +proposition%important covering_space_lift_homotopic_paths: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes cov: "covering_space C p S" and "path g1" and pig1: "path_image g1 \ S" @@ -2056,7 +2056,7 @@ and "path h2" and pih2: "path_image h2 \ C" and ph2: "\t. t \ {0..1} \ p(h2 t) = g2 t" and h1h2: "pathstart h1 = pathstart h2" shows "homotopic_paths C h1 h2" -proof - +proof%unimportant - obtain h :: "real \ real \ 'b" where conth: "continuous_on ({0..1} \ {0..1}) h" and him: "h ` ({0..1} \ {0..1}) \ S" @@ -2117,7 +2117,7 @@ qed -corollary covering_space_monodromy: +corollary%important covering_space_monodromy: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes cov: "covering_space C p S" and "path g1" and pig1: "path_image g1 \ S" @@ -2131,7 +2131,7 @@ by%unimportant blast -corollary covering_space_lift_homotopic_path: +corollary%important covering_space_lift_homotopic_path: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes cov: "covering_space C p S" and hom: "homotopic_paths S f f'" @@ -2140,7 +2140,7 @@ and pgeq: "\t. t \ {0..1} \ p(g t) = f t" obtains g' where "path g'" "path_image g' \ C" "pathstart g' = a" "pathfinish g' = b" "\t. t \ {0..1} \ p(g' t) = f' t" -proof (rule covering_space_lift_path_strong [OF cov, of a f']) +proof%unimportant (rule covering_space_lift_path_strong [OF cov, of a f']) show "a \ C" using a pig by auto show "path f'" "path_image f' \ S" @@ -2150,7 +2150,7 @@ qed (metis (mono_tags, lifting) assms cov covering_space_monodromy hom homotopic_paths_imp_path homotopic_paths_imp_subset pgeq pig) -proposition covering_space_lift_general: +proposition%important covering_space_lift_general: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" and f :: "'c::real_normed_vector \ 'b" assumes cov: "covering_space C p S" and "a \ C" "z \ U" @@ -2162,7 +2162,7 @@ pathstart q = a \ pathfinish q = a \ homotopic_paths S (f \ r) (p \ q)" obtains g where "continuous_on U g" "g ` U \ C" "g z = a" "\y. y \ U \ p(g y) = f y" -proof - +proof%unimportant - have *: "\g h. path g \ path_image g \ U \ pathstart g = z \ pathfinish g = y \ path h \ path_image h \ C \ pathstart h = a \ @@ -2405,7 +2405,7 @@ qed -corollary covering_space_lift_stronger: +corollary%important covering_space_lift_stronger: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" and f :: "'c::real_normed_vector \ 'b" assumes cov: "covering_space C p S" "a \ C" "z \ U" @@ -2415,7 +2415,7 @@ and hom: "\r. \path r; path_image r \ U; pathstart r = z; pathfinish r = z\ \ \b. homotopic_paths S (f \ r) (linepath b b)" obtains g where "continuous_on U g" "g ` U \ C" "g z = a" "\y. y \ U \ p(g y) = f y" -proof (rule covering_space_lift_general [OF cov U contf fim feq]) +proof%unimportant (rule covering_space_lift_general [OF cov U contf fim feq]) fix r assume "path r" "path_image r \ U" "pathstart r = z" "pathfinish r = z" then obtain b where b: "homotopic_paths S (f \ r) (linepath b b)" @@ -2432,7 +2432,7 @@ by (force simp: \a \ C\) qed auto -corollary covering_space_lift_strong: +corollary%important covering_space_lift_strong: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" and f :: "'c::real_normed_vector \ 'b" assumes cov: "covering_space C p S" "a \ C" "z \ U" @@ -2440,7 +2440,7 @@ and contf: "continuous_on U f" and fim: "f ` U \ S" and feq: "f z = p a" obtains g where "continuous_on U g" "g ` U \ C" "g z = a" "\y. y \ U \ p(g y) = f y" -proof (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq]) +proof%unimportant (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq]) show "path_connected U" using scU simply_connected_eq_contractible_loop_some by blast fix r @@ -2453,14 +2453,14 @@ by blast qed blast -corollary covering_space_lift: +corollary%important covering_space_lift: fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" and f :: "'c::real_normed_vector \ 'b" assumes cov: "covering_space C p S" and U: "simply_connected U" "locally path_connected U" and contf: "continuous_on U f" and fim: "f ` U \ S" obtains g where "continuous_on U g" "g ` U \ C" "\y. y \ U \ p(g y) = f y" -proof (cases "U = {}") +proof%unimportant (cases "U = {}") case True with that show ?thesis by auto next diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Improper_Integral.thy --- a/src/HOL/Analysis/Improper_Integral.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Improper_Integral.thy Thu Jan 17 16:22:21 2019 -0500 @@ -28,11 +28,11 @@ unfolding equiintegrable_on_def Ball_def by (erule conj_forward imp_forward all_forward ex_forward | blast)+ -lemma equiintegrable_on_Un: +lemma%important equiintegrable_on_Un: assumes "F equiintegrable_on I" "G equiintegrable_on I" shows "(F \ G) equiintegrable_on I" unfolding equiintegrable_on_def -proof (intro conjI impI allI) +proof%unimportant (intro conjI impI allI) show "\f\F \ G. f integrable_on I" using assms unfolding equiintegrable_on_def by blast show "\\. gauge \ \ @@ -76,12 +76,12 @@ text\ Main limit theorem for an equiintegrable sequence.\ -theorem equiintegrable_limit: +theorem%important equiintegrable_limit: fixes g :: "'a :: euclidean_space \ 'b :: banach" assumes feq: "range f equiintegrable_on cbox a b" and to_g: "\x. x \ cbox a b \ (\n. f n x) \ g x" shows "g integrable_on cbox a b \ (\n. integral (cbox a b) (f n)) \ integral (cbox a b) g" -proof - +proof%unimportant - have "Cauchy (\n. integral(cbox a b) (f n))" proof (clarsimp simp add: Cauchy_def) fix e::real @@ -151,10 +151,10 @@ qed -lemma equiintegrable_reflect: +lemma%important equiintegrable_reflect: assumes "F equiintegrable_on cbox a b" shows "(\f. f \ uminus) ` F equiintegrable_on cbox (-b) (-a)" -proof - +proof%unimportant - have "\\. gauge \ \ (\f \. f \ (\f. f \ uminus) ` F \ \ tagged_division_of cbox (- b) (- a) \ \ fine \ \ norm ((\(x,K) \ \. content K *\<^sub>R f x) - integral (cbox (- b) (- a)) f) < e)" @@ -246,13 +246,13 @@ qed -lemma content_division_lemma1: +lemma%important content_division_lemma1: assumes div: "\ division_of S" and S: "S \ cbox a b" and i: "i \ Basis" and mt: "\K. K \ \ \ content K \ 0" and disj: "(\K \ \. K \ {x. x \ i = a \ i} \ {}) \ (\K \ \. K \ {x. x \ i = b \ i} \ {})" shows "(b \ i - a \ i) * (\K\\. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ content(cbox a b)" (is "?lhs \ ?rhs") -proof - +proof%unimportant - have "finite \" using div by blast define extend where @@ -409,13 +409,13 @@ qed -proposition sum_content_area_over_thin_division: +proposition%important sum_content_area_over_thin_division: assumes div: "\ division_of S" and S: "S \ cbox a b" and i: "i \ Basis" and "a \ i \ c" "c \ b \ i" and nonmt: "\K. K \ \ \ K \ {x. x \ i = c} \ {}" shows "(b \ i - a \ i) * (\K\\. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ 2 * content(cbox a b)" -proof (cases "content(cbox a b) = 0") +proof%unimportant (cases "content(cbox a b) = 0") case True have "(\K\\. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) = 0" using S div by (force intro!: sum.neutral content_0_subset [OF True]) @@ -609,7 +609,7 @@ -proposition bounded_equiintegral_over_thin_tagged_partial_division: +proposition%important bounded_equiintegral_over_thin_tagged_partial_division: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes F: "F equiintegrable_on cbox a b" and f: "f \ F" and "0 < \" and norm_f: "\h x. \h \ F; x \ cbox a b\ \ norm(h x) \ norm(f x)" @@ -617,7 +617,7 @@ "\c i S h. \c \ cbox a b; i \ Basis; S tagged_partial_division_of cbox a b; \ fine S; h \ F; \x K. (x,K) \ S \ (K \ {x. x \ i = c \ i} \ {})\ \ (\(x,K) \ S. norm (integral K h)) < \" -proof (cases "content(cbox a b) = 0") +proof%unimportant (cases "content(cbox a b) = 0") case True show ?thesis proof @@ -813,13 +813,13 @@ -proposition equiintegrable_halfspace_restrictions_le: +proposition%important equiintegrable_halfspace_restrictions_le: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes F: "F equiintegrable_on cbox a b" and f: "f \ F" and norm_f: "\h x. \h \ F; x \ cbox a b\ \ norm(h x) \ norm(f x)" shows "(\i \ Basis. \c. \h \ F. {(\x. if x \ i \ c then h x else 0)}) equiintegrable_on cbox a b" -proof (cases "content(cbox a b) = 0") +proof%unimportant (cases "content(cbox a b) = 0") case True then show ?thesis by simp next @@ -1172,13 +1172,13 @@ -corollary equiintegrable_halfspace_restrictions_ge: +corollary%important equiintegrable_halfspace_restrictions_ge: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes F: "F equiintegrable_on cbox a b" and f: "f \ F" and norm_f: "\h x. \h \ F; x \ cbox a b\ \ norm(h x) \ norm(f x)" shows "(\i \ Basis. \c. \h \ F. {(\x. if x \ i \ c then h x else 0)}) equiintegrable_on cbox a b" -proof - +proof%unimportant - have *: "(\i\Basis. \c. \h\(\f. f \ uminus) ` F. {\x. if x \ i \ c then h x else 0}) equiintegrable_on cbox (- b) (- a)" proof (rule equiintegrable_halfspace_restrictions_le) @@ -1203,11 +1203,11 @@ qed -proposition equiintegrable_closed_interval_restrictions: +proposition%important equiintegrable_closed_interval_restrictions: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes f: "f integrable_on cbox a b" shows "(\c d. {(\x. if x \ cbox c d then f x else 0)}) equiintegrable_on cbox a b" -proof - +proof%unimportant - let ?g = "\B c d x. if \i\B. c \ i \ x \ i \ x \ i \ d \ i then f x else 0" have *: "insert f (\c d. {?g B c d}) equiintegrable_on cbox a b" if "B \ Basis" for B proof - @@ -1266,14 +1266,14 @@ subsection%important\Continuity of the indefinite integral\ -proposition indefinite_integral_continuous: +proposition%important indefinite_integral_continuous: fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space" assumes int_f: "f integrable_on cbox a b" and c: "c \ cbox a b" and d: "d \ cbox a b" "0 < \" obtains \ where "0 < \" "\c' d'. \c' \ cbox a b; d' \ cbox a b; norm(c' - c) \ \; norm(d' - d) \ \\ \ norm(integral(cbox c' d') f - integral(cbox c d) f) < \" -proof - +proof%unimportant - { assume "\c' d'. c' \ cbox a b \ d' \ cbox a b \ norm(c' - c) \ \ \ norm(d' - d) \ \ \ norm(integral(cbox c' d') f - integral(cbox c d) f) \ \" (is "\c' d'. ?\ c' d' \") if "0 < \" for \ @@ -1358,11 +1358,11 @@ by (meson not_le that) qed -corollary indefinite_integral_uniformly_continuous: +corollary%important indefinite_integral_uniformly_continuous: fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space" assumes "f integrable_on cbox a b" shows "uniformly_continuous_on (cbox (Pair a a) (Pair b b)) (\y. integral (cbox (fst y) (snd y)) f)" -proof - +proof%unimportant - show ?thesis proof (rule compact_uniformly_continuous, clarsimp simp add: continuous_on_iff) fix c d and \::real @@ -1383,11 +1383,11 @@ qed -corollary bounded_integrals_over_subintervals: +corollary%important bounded_integrals_over_subintervals: fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space" assumes "f integrable_on cbox a b" shows "bounded {integral (cbox c d) f |c d. cbox c d \ cbox a b}" -proof - +proof%unimportant - have "bounded ((\y. integral (cbox (fst y) (snd y)) f) ` cbox (a, a) (b, b))" (is "bounded ?I") by (blast intro: bounded_cbox bounded_uniformly_continuous_image indefinite_integral_uniformly_continuous [OF assms]) @@ -1414,7 +1414,7 @@ We only need to assume that the integrals are bounded, and we get absolute integrability, but we also need a (rather weak) bound assumption on the function.\ -theorem absolutely_integrable_improper: +theorem%important absolutely_integrable_improper: fixes f :: "'M::euclidean_space \ 'N::euclidean_space" assumes int_f: "\c d. cbox c d \ box a b \ f integrable_on cbox c d" and bo: "bounded {integral (cbox c d) f |c d. cbox c d \ box a b}" @@ -1422,7 +1422,7 @@ \ \g. g absolutely_integrable_on cbox a b \ ((\x \ cbox a b. f x \ i \ g x) \ (\x \ cbox a b. f x \ i \ g x))" shows "f absolutely_integrable_on cbox a b" -proof (cases "content(cbox a b) = 0") +proof%unimportant (cases "content(cbox a b) = 0") case True then show ?thesis by auto diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Interval_Integral.thy --- a/src/HOL/Analysis/Interval_Integral.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Interval_Integral.thy Thu Jan 17 16:22:21 2019 -0500 @@ -4,15 +4,15 @@ Lebesgue integral over an interval (with endpoints possibly +-\) *) -theory Interval_Integral (*FIX ME rename? Lebesgue *) +theory Interval_Integral imports Equivalence_Lebesgue_Henstock_Integration begin -lemma continuous_on_vector_derivative: +lemma%important continuous_on_vector_derivative: "(\x. x \ S \ (f has_vector_derivative f' x) (at x within S)) \ continuous_on S f" - by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous) + by%unimportant (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous) -definition "einterval a b = {x. a < ereal x \ ereal x < b}" +definition%important "einterval a b = {x. a < ereal x \ ereal x < b}" lemma einterval_eq[simp]: shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}" @@ -37,16 +37,16 @@ lemma borel_einterval[measurable]: "einterval a b \ sets borel" unfolding einterval_def by measurable -subsection%important \Approximating a (possibly infinite) interval\ +subsection\Approximating a (possibly infinite) interval\ lemma filterlim_sup1: "(LIM x F. f x :> G1) \ (LIM x F. f x :> (sup G1 G2))" unfolding filterlim_def by (auto intro: le_supI1) -lemma ereal_incseq_approx: +lemma%important ereal_incseq_approx: fixes a b :: ereal assumes "a < b" obtains X :: "nat \ real" where "incseq X" "\i. a < X i" "\i. X i < b" "X \ b" -proof (cases b) +proof%unimportant (cases b) case PInf with \a < b\ have "a = -\ \ (\r. a = ereal r)" by (cases a) auto @@ -78,12 +78,12 @@ (auto simp: real incseq_def intro!: divide_left_mono) qed (insert \a < b\, auto) -lemma ereal_decseq_approx: +lemma%important ereal_decseq_approx: fixes a b :: ereal assumes "a < b" obtains X :: "nat \ real" where "decseq X" "\i. a < X i" "\i. X i < b" "X \ a" -proof - +proof%unimportant - have "-b < -a" using \a < b\ by simp from ereal_incseq_approx[OF this] guess X . then show thesis @@ -93,14 +93,14 @@ done qed -proposition einterval_Icc_approximation: +lemma%important einterval_Icc_approximation: fixes a b :: ereal assumes "a < b" obtains u l :: "nat \ real" where "einterval a b = (\i. {l i .. u i})" "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" "l \ a" "u \ b" -proof - +proof%unimportant - from dense[OF \a < b\] obtain c where "a < c" "c < b" by safe from ereal_incseq_approx[OF \c < b\] guess u . note u = this from ereal_decseq_approx[OF \a < c\] guess l . note l = this @@ -202,17 +202,17 @@ interval_lebesgue_integrable M a b (\x. c * f x)" by (simp add: interval_lebesgue_integrable_def) -lemma interval_lebesgue_integrable_mult_left [intro, simp]: +lemma%important interval_lebesgue_integrable_mult_left [intro, simp]: fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, second_countable_topology}" shows "(c \ 0 \ interval_lebesgue_integrable M a b f) \ interval_lebesgue_integrable M a b (\x. f x * c)" - by (simp add: interval_lebesgue_integrable_def) + by%unimportant (simp add: interval_lebesgue_integrable_def) -lemma interval_lebesgue_integrable_divide [intro, simp]: +lemma%important interval_lebesgue_integrable_divide [intro, simp]: fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, field, second_countable_topology}" shows "(c \ 0 \ interval_lebesgue_integrable M a b f) \ interval_lebesgue_integrable M a b (\x. f x / c)" - by (simp add: interval_lebesgue_integrable_def) + by%unimportant (simp add: interval_lebesgue_integrable_def) lemma interval_lebesgue_integral_mult_right [simp]: fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, second_countable_topology}" @@ -220,11 +220,11 @@ c * interval_lebesgue_integral M a b f" by (simp add: interval_lebesgue_integral_def) -lemma interval_lebesgue_integral_mult_left [simp]: +lemma%important interval_lebesgue_integral_mult_left [simp]: fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, second_countable_topology}" shows "interval_lebesgue_integral M a b (\x. f x * c) = interval_lebesgue_integral M a b f * c" - by (simp add: interval_lebesgue_integral_def) + by%unimportant (simp add: interval_lebesgue_integral_def) lemma interval_lebesgue_integral_divide [simp]: fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, field, second_countable_topology}" @@ -242,11 +242,11 @@ unfolding interval_lebesgue_integral_def by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real) -lemma interval_lebesgue_integral_le_eq: +lemma%important interval_lebesgue_integral_le_eq: fixes a b f assumes "a \ b" shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)" - using assms by (auto simp: interval_lebesgue_integral_def) +using%unimportant assms by (auto simp: interval_lebesgue_integral_def) lemma interval_lebesgue_integral_gt_eq: fixes a b f @@ -271,9 +271,9 @@ interval_lebesgue_integrable lborel b a f" by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same) -lemma interval_integral_reflect: +lemma%important interval_integral_reflect: "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))" -proof (induct a b rule: linorder_wlog) +proof%unimportant (induct a b rule: linorder_wlog) case (sym a b) then show ?case by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse split: if_split_asm) @@ -299,7 +299,7 @@ lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..\ | M. f x) = (LINT x : {a<..} | M. f x)" unfolding interval_lebesgue_integral_def by auto -proposition interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \ f) = +lemma%important interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \ f) = (set_integrable M {a<..} f)" unfolding%unimportant interval_lebesgue_integrable_def by auto @@ -317,12 +317,12 @@ unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def) -lemma interval_integral_cong_AE: +lemma%important interval_integral_cong_AE: assumes [measurable]: "f \ borel_measurable borel" "g \ borel_measurable borel" assumes "AE x \ einterval (min a b) (max a b) in lborel. f x = g x" shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g" using assms -proof (induct a b rule: linorder_wlog) +proof%unimportant (induct a b rule: linorder_wlog) case (sym a b) then show ?case by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b]) next @@ -331,11 +331,11 @@ intro!: set_lebesgue_integral_cong_AE) qed -lemma interval_integral_cong: +lemma%important interval_integral_cong: assumes "\x. x \ einterval (min a b) (max a b) \ f x = g x" shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g" using assms -proof (induct a b rule: linorder_wlog) +proof%unimportant (induct a b rule: linorder_wlog) case (sym a b) then show ?case by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b]) next @@ -407,11 +407,11 @@ apply (auto simp: eq anti_eq einterval_iff split: split_indicator) done -lemma interval_integral_sum: +lemma%important interval_integral_sum: fixes a b c :: ereal assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f" shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)" -proof - +proof%unimportant - let ?I = "\a b. LBINT x=a..b. f x" { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \ b" "b \ c" then have ord: "a \ b" "b \ c" "a \ c" and f': "set_integrable lborel (einterval a c) f" @@ -446,11 +446,11 @@ (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3) qed -lemma interval_integrable_isCont: +lemma%important interval_integrable_isCont: fixes a b and f :: "real \ 'a::{banach, second_countable_topology}" shows "(\x. min a b \ x \ x \ max a b \ isCont f x) \ interval_lebesgue_integrable lborel a b f" -proof (induct a b rule: linorder_wlog) +proof%unimportant (induct a b rule: linorder_wlog) case (le a b) then show ?case unfolding interval_lebesgue_integrable_def set_integrable_def by (auto simp: interval_lebesgue_integrable_def @@ -478,7 +478,7 @@ subsection%important\General limit approximation arguments\ -proposition interval_integral_Icc_approx_nonneg: +lemma%important interval_integral_Icc_approx_nonneg: fixes a b :: ereal assumes "a < b" fixes u l :: "nat \ real" @@ -493,7 +493,7 @@ shows "set_integrable lborel (einterval a b) f" "(LBINT x=a..b. f x) = C" -proof - +proof%unimportant - have 1 [unfolded set_integrable_def]: "\i. set_integrable lborel {l i..u i} f" by (rule f_integrable) have 2: "AE x in lborel. mono (\n. indicator {l n..u n} x *\<^sub>R f x)" proof - @@ -534,7 +534,7 @@ by (rule integrable_monotone_convergence[OF 1 2 3 4 5]) qed -proposition interval_integral_Icc_approx_integrable: +lemma%important interval_integral_Icc_approx_integrable: fixes u l :: "nat \ real" and a b :: ereal fixes f :: "real \ 'a::{banach, second_countable_topology}" assumes "a < b" @@ -543,7 +543,7 @@ "l \ a" "u \ b" assumes f_integrable: "set_integrable lborel (einterval a b) f" shows "(\i. LBINT x=l i.. u i. f x) \ (LBINT x=a..b. f x)" -proof - +proof%unimportant - have "(\i. LBINT x:{l i.. u i}. f x) \ (LBINT x:einterval a b. f x)" unfolding set_lebesgue_integral_def proof (rule integral_dominated_convergence) @@ -580,13 +580,13 @@ TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.) *) -lemma interval_integral_FTC_finite: +lemma%important interval_integral_FTC_finite: fixes f F :: "real \ 'a::euclidean_space" and a b :: real assumes f: "continuous_on {min a b..max a b} f" assumes F: "\x. min a b \ x \ x \ max a b \ (F has_vector_derivative (f x)) (at x within {min a b..max a b})" shows "(LBINT x=a..b. f x) = F b - F a" -proof (cases "a \ b") +proof%unimportant (cases "a \ b") case True have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)" by (simp add: True interval_integral_Icc set_lebesgue_integral_def) @@ -617,7 +617,7 @@ qed -lemma interval_integral_FTC_nonneg: +lemma%important interval_integral_FTC_nonneg: fixes f F :: "real \ real" and a b :: ereal assumes "a < b" assumes F: "\x. a < ereal x \ ereal x < b \ DERIV F x :> f x" @@ -628,7 +628,7 @@ shows "set_integrable lborel (einterval a b) f" "(LBINT x=a..b. f x) = B - A" -proof - +proof%unimportant - obtain u l where approx: "einterval a b = (\i. {l i .. u i})" "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" @@ -669,7 +669,7 @@ by (rule interval_integral_Icc_approx_nonneg [OF \a < b\ approx 1 f_nonneg 2 3]) qed -theorem interval_integral_FTC_integrable: +lemma%important interval_integral_FTC_integrable: fixes f F :: "real \ 'a::euclidean_space" and a b :: ereal assumes "a < b" assumes F: "\x. a < ereal x \ ereal x < b \ (F has_vector_derivative f x) (at x)" @@ -678,7 +678,7 @@ assumes A: "((F \ real_of_ereal) \ A) (at_right a)" assumes B: "((F \ real_of_ereal) \ B) (at_left b)" shows "(LBINT x=a..b. f x) = B - A" -proof - +proof%unimportant - obtain u l where approx: "einterval a b = (\i. {l i .. u i})" "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" @@ -714,14 +714,14 @@ einterval. *) -theorem interval_integral_FTC2: +lemma%important interval_integral_FTC2: fixes a b c :: real and f :: "real \ 'a::euclidean_space" assumes "a \ c" "c \ b" and contf: "continuous_on {a..b} f" fixes x :: real assumes "a \ x" and "x \ b" shows "((\u. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})" -proof - +proof%unimportant - let ?F = "(\u. LBINT y=a..u. f y)" have intf: "set_integrable lborel {a..b} f" by (rule borel_integrable_atLeastAtMost', rule contf) @@ -746,11 +746,11 @@ qed (insert assms, auto) qed -proposition einterval_antiderivative: +lemma%important einterval_antiderivative: fixes a b :: ereal and f :: "real \ 'a::euclidean_space" assumes "a < b" and contf: "\x :: real. a < x \ x < b \ isCont f x" shows "\F. \x :: real. a < x \ x < b \ (F has_vector_derivative f x) (at x)" -proof - +proof%unimportant - from einterval_nonempty [OF \a < b\] obtain c :: real where [simp]: "a < c" "c < b" by (auto simp: einterval_def) let ?F = "(\u. LBINT y=c..u. f y)" @@ -786,14 +786,14 @@ text\Once again, three versions: first, for finite intervals, and then two versions for arbitrary intervals.\ -theorem interval_integral_substitution_finite: +lemma%important interval_integral_substitution_finite: fixes a b :: real and f :: "real \ 'a::euclidean_space" assumes "a \ b" and derivg: "\x. a \ x \ x \ b \ (g has_real_derivative (g' x)) (at x within {a..b})" and contf : "continuous_on (g ` {a..b}) f" and contg': "continuous_on {a..b} g'" shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y" -proof- +proof%unimportant- have v_derivg: "\x. a \ x \ x \ b \ (g has_vector_derivative (g' x)) (at x within {a..b})" using derivg unfolding has_field_derivative_iff_has_vector_derivative . then have contg [simp]: "continuous_on {a..b} g" @@ -833,7 +833,7 @@ (* TODO: is it possible to lift the assumption here that g' is nonnegative? *) -theorem interval_integral_substitution_integrable: +lemma%important interval_integral_substitution_integrable: fixes f :: "real \ 'a::euclidean_space" and a b u v :: ereal assumes "a < b" and deriv_g: "\x. a < ereal x \ ereal x < b \ DERIV g x :> g' x" @@ -845,7 +845,7 @@ and integrable: "set_integrable lborel (einterval a b) (\x. g' x *\<^sub>R f (g x))" and integrable2: "set_integrable lborel (einterval A B) (\x. f x)" shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))" -proof - +proof%unimportant - obtain u l where approx [simp]: "einterval a b = (\i. {l i .. u i})" "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" @@ -932,7 +932,7 @@ An alternative: make the second one the main one, and then have another lemma that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *) -theorem interval_integral_substitution_nonneg: +lemma%important interval_integral_substitution_nonneg: fixes f g g':: "real \ real" and a b u v :: ereal assumes "a < b" and deriv_g: "\x. a < ereal x \ ereal x < b \ DERIV g x :> g' x" @@ -946,7 +946,7 @@ shows "set_integrable lborel (einterval A B) f" "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))" -proof - +proof%unimportant - from einterval_Icc_approximation[OF \a < b\] guess u l . note approx [simp] = this note less_imp_le [simp] have aless[simp]: "\x i. l i \ x \ a < ereal x" @@ -1079,17 +1079,17 @@ translations "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\x. f)" -proposition interval_integral_norm: +lemma%important interval_integral_norm: fixes f :: "real \ 'a :: {banach, second_countable_topology}" shows "interval_lebesgue_integrable lborel a b f \ a \ b \ norm (LBINT t=a..b. f t) \ LBINT t=a..b. norm (f t)" using%unimportant integral_norm_bound[of lborel "\x. indicator (einterval a b) x *\<^sub>R f x"] by%unimportant (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def) -proposition interval_integral_norm2: +lemma%important interval_integral_norm2: "interval_lebesgue_integrable lborel a b f \ norm (LBINT t=a..b. f t) \ \LBINT t=a..b. norm (f t)\" -proof (induct a b rule: linorder_wlog) +proof%unimportant (induct a b rule: linorder_wlog) case (sym a b) then show ?case by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b]) next diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Tagged_Division.thy --- a/src/HOL/Analysis/Tagged_Division.thy Thu Jan 17 16:08:41 2019 +0000 +++ b/src/HOL/Analysis/Tagged_Division.thy Thu Jan 17 16:22:21 2019 -0500 @@ -32,7 +32,7 @@ subsection%unimportant \Sundries\ - +(*FIXME restructure this entire section consists of single lemma *) text\A transitive relation is well-founded if all initial segments are finite.\ lemma wf_finite_segments: @@ -55,7 +55,7 @@ by (simp add: field_simps) qed -subsection%important \Some useful lemmas about intervals\ +subsection%unimportant \Some useful lemmas about intervals\ lemma interior_subset_union_intervals: assumes "i = cbox a b" @@ -152,22 +152,22 @@ lemmas interval_bounds = interval_upperbound interval_lowerbound -lemma +lemma%important fixes X::"real set" shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X" and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X" - by (auto simp: interval_upperbound_def interval_lowerbound_def) + by%unimportant (auto simp: interval_upperbound_def interval_lowerbound_def) -lemma interval_bounds'[simp]: +lemma%important interval_bounds'[simp]: assumes "cbox a b \ {}" shows "interval_upperbound (cbox a b) = b" and "interval_lowerbound (cbox a b) = a" - using assms unfolding box_ne_empty by auto + using%unimportant assms unfolding box_ne_empty by auto -lemma interval_upperbound_Times: +lemma%important interval_upperbound_Times: assumes "A \ {}" and "B \ {}" shows "interval_upperbound (A \ B) = (interval_upperbound A, interval_upperbound B)" -proof- +proof%unimportant- from assms have fst_image_times': "A = fst ` (A \ B)" by simp have "(\i\Basis. (SUP x\A \ B. x \ (i, 0)) *\<^sub>R i) = (\i\Basis. (SUP x\A. x \ i) *\<^sub>R i)" by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0) @@ -178,10 +178,10 @@ by (subst sum_Basis_prod_eq) (auto simp add: sum_prod) qed -lemma interval_lowerbound_Times: +lemma%important interval_lowerbound_Times: assumes "A \ {}" and "B \ {}" shows "interval_lowerbound (A \ B) = (interval_lowerbound A, interval_lowerbound B)" -proof- +proof%unimportant- from assms have fst_image_times': "A = fst ` (A \ B)" by simp have "(\i\Basis. (INF x\A \ B. x \ (i, 0)) *\<^sub>R i) = (\i\Basis. (INF x\A. x \ i) *\<^sub>R i)" by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0) @@ -226,11 +226,11 @@ using equation_minus_iff by (auto simp: gauge_def surj_def intro!: open_surjective_linear_image linear_uminus) -lemma gauge_Inter: +lemma%important gauge_Inter: assumes "finite S" and "\u. u\S \ gauge (f u)" shows "gauge (\x. \{f u x | u. u \ S})" -proof - +proof%unimportant - have *: "\x. {f u x |u. u \ S} = (\u. f u x) ` S" by auto show ?thesis @@ -238,12 +238,12 @@ using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto qed -lemma gauge_existence_lemma: +lemma%important gauge_existence_lemma: "(\x. \d :: real. p x \ 0 < d \ q d x) \ (\x. \d>0. p x \ q d x)" - by (metis zero_less_one) + by%unimportant (metis zero_less_one) -subsection%important \Attempt a systematic general set of "offset" results for components\ -(*FIXME Restructure, the subsection consists only of 1 lemma *) +subsection%unimportant \Attempt a systematic general set of "offset" results for components\ +(*FIXME Restructure *) lemma gauge_modify: assumes "(\S. open S \ open {x. f(x) \ S})" "gauge d" shows "gauge (\x. {y. f y \ d (f x)})" @@ -605,10 +605,10 @@ qed qed -proposition partial_division_extend_interval: +proposition%important partial_division_extend_interval: assumes "p division_of (\p)" "(\p) \ cbox a b" obtains q where "p \ q" "q division_of cbox a (b::'a::euclidean_space)" -proof (cases "p = {}") +proof%unimportant (cases "p = {}") case True obtain q where "q division_of (cbox a b)" by (rule elementary_interval) @@ -687,11 +687,11 @@ "p division_of S \ \a b. S \ cbox a (b::'a::euclidean_space)" by (meson bounded_subset_cbox_symmetric elementary_bounded) -proposition division_union_intervals_exists: +lemma%important division_union_intervals_exists: fixes a b :: "'a::euclidean_space" assumes "cbox a b \ {}" obtains p where "(insert (cbox a b) p) division_of (cbox a b \ cbox c d)" -proof (cases "cbox c d = {}") +proof%unimportant (cases "cbox c d = {}") case True with assms that show ?thesis by force next @@ -739,11 +739,11 @@ shows "\f division_of \\f" using assms by (auto intro!: division_ofI) -lemma elementary_union_interval: +lemma%important elementary_union_interval: fixes a b :: "'a::euclidean_space" assumes "p division_of \p" obtains q where "q division_of (cbox a b \ \p)" -proof (cases "p = {} \ cbox a b = {}") +proof%unimportant (cases "p = {} \ cbox a b = {}") case True obtain p where "p division_of (cbox a b)" by (rule elementary_interval) @@ -855,11 +855,11 @@ using that by auto qed -lemma elementary_union: +lemma%important elementary_union: fixes S T :: "'a::euclidean_space set" assumes "ps division_of S" "pt division_of T" obtains p where "p division_of (S \ T)" -proof - +proof%unimportant - have *: "S \ T = \ps \ \pt" using assms unfolding division_of_def by auto show ?thesis @@ -868,13 +868,13 @@ by (simp add: * that) qed -lemma partial_division_extend: +lemma%important partial_division_extend: fixes T :: "'a::euclidean_space set" assumes "p division_of S" and "q division_of T" and "S \ T" obtains r where "p \ r" and "r division_of T" -proof - +proof%unimportant - note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)] obtain a b where ab: "T \ cbox a b" using elementary_subset_cbox[OF assms(2)] by auto @@ -931,7 +931,7 @@ qed -lemma division_split: +lemma%important division_split: fixes a :: "'a::euclidean_space" assumes "p division_of (cbox a b)" and k: "k\Basis" @@ -939,7 +939,7 @@ (is "?p1 division_of ?I1") and "{l \ {x. x\k \ c} | l. l \ p \ l \ {x. x\k \ c} \ {}} division_of (cbox a b \ {x. x\k \ c})" (is "?p2 division_of ?I2") -proof (rule_tac[!] division_ofI) +proof%unimportant (rule_tac[!] division_ofI) note p = division_ofD[OF assms(1)] show "finite ?p1" "finite ?p2" using p(1) by auto @@ -1020,14 +1020,14 @@ lemma tagged_division_of_finite: "s tagged_division_of i \ finite s" unfolding tagged_division_of_def tagged_partial_division_of_def by auto -lemma tagged_division_of: +lemma%important tagged_division_of: "s tagged_division_of i \ finite s \ (\x K. (x, K) \ s \ x \ K \ K \ i \ (\a b. K = cbox a b)) \ (\x1 K1 x2 K2. (x1, K1) \ s \ (x2, K2) \ s \ (x1, K1) \ (x2, K2) \ interior K1 \ interior K2 = {}) \ (\{K. \x. (x,K) \ s} = i)" - unfolding tagged_division_of_def tagged_partial_division_of_def by auto + unfolding%unimportant tagged_division_of_def tagged_partial_division_of_def by auto lemma tagged_division_ofI: assumes "finite s" @@ -1052,10 +1052,10 @@ and "(\{K. \x. (x,K) \ s} = i)" using assms unfolding tagged_division_of by blast+ -lemma division_of_tagged_division: +lemma%important division_of_tagged_division: assumes "s tagged_division_of i" shows "(snd ` s) division_of i" -proof (rule division_ofI) +proof%unimportant (rule division_ofI) note assm = tagged_division_ofD[OF assms] show "\(snd ` s) = i" "finite (snd ` s)" using assm by auto @@ -1073,10 +1073,10 @@ using assm(5) k'(2) xk by blast qed -lemma partial_division_of_tagged_division: +lemma%important partial_division_of_tagged_division: assumes "s tagged_partial_division_of i" shows "(snd ` s) division_of \(snd ` s)" -proof (rule division_ofI) +proof%unimportant (rule division_ofI) note assm = tagged_partial_division_ofD[OF assms] show "finite (snd ` s)" "\(snd ` s) = \(snd ` s)" using assm by auto @@ -1121,12 +1121,12 @@ unfolding box_real[symmetric] by (rule tagged_division_of_self) -lemma tagged_division_Un: +lemma%important tagged_division_Un: assumes "p1 tagged_division_of s1" and "p2 tagged_division_of s2" and "interior s1 \ interior s2 = {}" shows "(p1 \ p2) tagged_division_of (s1 \ s2)" -proof (rule tagged_division_ofI) +proof%unimportant (rule tagged_division_ofI) note p1 = tagged_division_ofD[OF assms(1)] note p2 = tagged_division_ofD[OF assms(2)] show "finite (p1 \ p2)" @@ -1149,12 +1149,12 @@ by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2)) qed -lemma tagged_division_Union: +lemma%important tagged_division_Union: assumes "finite I" and tag: "\i. i\I \ pfn i tagged_division_of i" and disj: "\i1 i2. \i1 \ I; i2 \ I; i1 \ i2\ \ interior(i1) \ interior(i2) = {}" shows "\(pfn ` I) tagged_division_of (\I)" -proof (rule tagged_division_ofI) +proof%unimportant (rule tagged_division_ofI) note assm = tagged_division_ofD[OF tag] show "finite (\(pfn ` I))" using assms by auto @@ -1229,13 +1229,13 @@ unfolding box_real[symmetric] by (rule tagged_division_Un_interval) -lemma tagged_division_split_left_inj: +lemma%important tagged_division_split_left_inj: assumes d: "d tagged_division_of i" and tags: "(x1, K1) \ d" "(x2, K2) \ d" and "K1 \ K2" and eq: "K1 \ {x. x \ k \ c} = K2 \ {x. x \ k \ c}" shows "interior (K1 \ {x. x\k \ c}) = {}" -proof - +proof%unimportant - have "interior (K1 \ K2) = {} \ (x2, K2) = (x1, K1)" using tags d by (metis (no_types) interior_Int tagged_division_ofD(5)) then show ?thesis @@ -1255,11 +1255,11 @@ using eq \K1 \ K2\ by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject) qed -lemma (in comm_monoid_set) over_tagged_division_lemma: +lemma%important (in comm_monoid_set) over_tagged_division_lemma: assumes "p tagged_division_of i" and "\u v. box u v = {} \ d (cbox u v) = \<^bold>1" shows "F (\(_, k). d k) p = F d (snd ` p)" -proof - +proof%unimportant - have *: "(\(_ ,k). d k) = d \ snd" by (simp add: fun_eq_iff) note assm = tagged_division_ofD[OF assms(1)] @@ -1293,7 +1293,7 @@ \<^typ>\bool\.\ paragraph%important \Using additivity of lifted function to encode definedness.\ -text \%whitespace\ +text%important \%whitespace\ definition%important lift_option :: "('a \ 'b \ 'c) \ 'a option \ 'b option \ 'c option" where "lift_option f a' b' = Option.bind a' (\a. Option.bind b' (\b. Some (f a b)))" @@ -1307,7 +1307,7 @@ lemma%important comm_monoid_lift_option: assumes "comm_monoid f z" shows "comm_monoid (lift_option f) (Some z)" -proof - +proof%unimportant - from assms interpret comm_monoid f z . show ?thesis by standard (auto simp: lift_option_def ac_simps split: bind_split) @@ -1334,16 +1334,16 @@ paragraph \Division points\ -text \%whitespace\ +text%important \%whitespace\ definition%important "division_points (k::('a::euclidean_space) set) d = {(j,x). j \ Basis \ (interval_lowerbound k)\j < x \ x < (interval_upperbound k)\j \ (\i\d. (interval_lowerbound i)\j = x \ (interval_upperbound i)\j = x)}" -lemma division_points_finite: +lemma%important division_points_finite: fixes i :: "'a::euclidean_space set" assumes "d division_of i" shows "finite (division_points i d)" -proof - +proof%unimportant - note assm = division_ofD[OF assms] let ?M = "\j. {(j,x)|x. (interval_lowerbound i)\j < x \ x < (interval_upperbound i)\j \ (\i\d. (interval_lowerbound i)\j = x \ (interval_upperbound i)\j = x)}" @@ -1353,7 +1353,7 @@ unfolding * using assm by auto qed -lemma division_points_subset: +lemma%important division_points_subset: fixes a :: "'a::euclidean_space" assumes "d division_of (cbox a b)" and "\i\Basis. a\i < b\i" "a\k < c" "c < b\k" @@ -1362,7 +1362,7 @@ division_points (cbox a b) d" (is ?t1) and "division_points (cbox a b \ {x. x\k \ c}) {l \ {x. x\k \ c} | l . l \ d \ \(l \ {x. x\k \ c} = {})} \ division_points (cbox a b) d" (is ?t2) -proof - +proof%unimportant - note assm = division_ofD[OF assms(1)] have *: "\i\Basis. a\i \ b\i" "\i\Basis. a\i \ (\i\Basis. (if i = k then min (b \ k) c else b \ i) *\<^sub>R i) \ i" @@ -1423,7 +1423,7 @@ by force qed -lemma division_points_psubset: +lemma%important division_points_psubset: fixes a :: "'a::euclidean_space" assumes d: "d division_of (cbox a b)" and altb: "\i\Basis. a\i < b\i" "a\k < c" "c < b\k" @@ -1434,7 +1434,7 @@ division_points (cbox a b) d" (is "?D1 \ ?D") and "division_points (cbox a b \ {x. x\k \ c}) {l \ {x. x\k \ c} | l. l\d \ l \ {x. x\k \ c} \ {}} \ division_points (cbox a b) d" (is "?D2 \ ?D") -proof - +proof%unimportant - have ab: "\i\Basis. a\i \ b\i" using altb by (auto intro!:less_imp_le) obtain u v where l: "l = cbox u v" @@ -1485,13 +1485,13 @@ using \K1 \ \\ \K1 \ K2\ by auto qed -lemma division_split_right_inj: +lemma%important division_split_right_inj: fixes S :: "'a::euclidean_space set" assumes div: "\ division_of S" and eq: "K1 \ {x::'a. x\k \ c} = K2 \ {x. x\k \ c}" and "K1 \ \" "K2 \ \" "K1 \ K2" shows "interior (K1 \ {x. x\k \ c}) = {}" -proof - +proof%unimportant - have "interior K2 \ interior {a. a \ k \ c} = interior K1 \ interior {a. a \ k \ c}" by (metis (no_types) eq interior_Int) moreover have "\A. interior A \ interior K2 = {} \ A = K2 \ A \ \" @@ -1515,13 +1515,13 @@ unfolding * ** interval_split[OF assms] by (rule refl) qed -lemma division_doublesplit: +lemma%important division_doublesplit: fixes a :: "'a::euclidean_space" assumes "p division_of (cbox a b)" and k: "k \ Basis" shows "(\l. l \ {x. \x\k - c\ \ e}) ` {l\p. l \ {x. \x\k - c\ \ e} \ {}} division_of (cbox a b \ {x. \x\k - c\ \ e})" -proof - +proof%unimportant - have *: "\x c. \x - c\ \ e \ x \ c - e \ x \ c + e" by auto have **: "\p q p' q'. p division_of q \ p = p' \ q = q' \ p' division_of q'" @@ -1560,9 +1560,9 @@ using box_empty_imp [of One "-One"] by simp qed -lemma division: +lemma%important division: "F g d = g (cbox a b)" if "d division_of (cbox a b)" -proof - +proof%unimportant - define C where [abs_def]: "C = card (division_points (cbox a b) d)" then show ?thesis using that proof (induction C arbitrary: a b d rule: less_induct) @@ -1747,10 +1747,10 @@ qed qed -proposition tagged_division: +lemma%important tagged_division: assumes "d tagged_division_of (cbox a b)" shows "F (\(_, l). g l) d = g (cbox a b)" -proof - +proof%unimportant - have "F (\(_, k). g k) d = F g (snd ` d)" using assms box_empty_imp by (rule over_tagged_division_lemma) then show ?thesis @@ -1830,12 +1830,12 @@ subsection%important \Special case of additivity we need for the FTC\ (*fix add explanation here *) -lemma additive_tagged_division_1: +lemma%important additive_tagged_division_1: fixes f :: "real \ 'a::real_normed_vector" assumes "a \ b" and "p tagged_division_of {a..b}" shows "sum (\(x,k). f(Sup k) - f(Inf k)) p = f b - f a" -proof - +proof%unimportant - let ?f = "(\k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))" interpret operative_real plus 0 ?f rewrites "comm_monoid_set.F (+) 0 = sum" @@ -1881,21 +1881,21 @@ lemma fine_Un: "d fine p1 \ d fine p2 \ d fine (p1 \ p2)" unfolding fine_def by blast -lemma fine_Union: "(\p. p \ ps \ d fine p) \ d fine (\ps)" +lemma%important fine_Union: "(\p. p \ ps \ d fine p) \ d fine (\ps)" unfolding fine_def by auto -lemma fine_subset: "p \ q \ d fine q \ d fine p" +lemma%unimportant fine_subset: "p \ q \ d fine q \ d fine p" unfolding fine_def by blast subsection%important \Some basic combining lemmas\ -lemma tagged_division_Union_exists: +lemma%important tagged_division_Union_exists: assumes "finite I" and "\i\I. \p. p tagged_division_of i \ d fine p" and "\i1\I. \i2\I. i1 \ i2 \ interior i1 \ interior i2 = {}" and "\I = i" obtains p where "p tagged_division_of i" and "d fine p" -proof - +proof%unimportant - obtain pfn where pfn: "\x. x \ I \ pfn x tagged_division_of x" "\x. x \ I \ d fine pfn x" @@ -1913,17 +1913,17 @@ fixes i :: "'n::euclidean_space set" shows "s division_of i \ closed i" unfolding division_of_def by fastforce -(* FIXME structure here, do not have one lemma in each subsection *) + subsection%important \General bisection principle for intervals; might be useful elsewhere\ -(* FIXME move? *) -lemma interval_bisection_step: + +lemma%important interval_bisection_step: fixes type :: "'a::euclidean_space" assumes emp: "P {}" and Un: "\S T. \P S; P T; interior(S) \ interior(T) = {}\ \ P (S \ T)" and non: "\ P (cbox a (b::'a))" obtains c d where "\ P (cbox c d)" and "\i. i \ Basis \ a\i \ c\i \ c\i \ d\i \ d\i \ b\i \ 2 * (d\i - c\i) \ b\i - a\i" -proof - +proof%unimportant - have "cbox a b \ {}" using emp non by metis then have ab: "\i. i\Basis \ a \ i \ b \ i" @@ -2029,14 +2029,14 @@ by (metis (no_types, lifting) assms(3) that) qed -lemma interval_bisection: +lemma%important interval_bisection: fixes type :: "'a::euclidean_space" assumes "P {}" and Un: "\S T. \P S; P T; interior(S) \ interior(T) = {}\ \ P (S \ T)" and "\ P (cbox a (b::'a))" obtains x where "x \ cbox a b" and "\e>0. \c d. x \ cbox c d \ cbox c d \ ball x e \ cbox c d \ cbox a b \ \ P (cbox c d)" -proof - +proof%unimportant - have "\x. \y. \ P (cbox (fst x) (snd x)) \ (\ P (cbox (fst y) (snd y)) \ (\i\Basis. fst x\i \ fst y\i \ fst y\i \ snd y\i \ snd y\i \ snd x\i \ 2 * (snd y\i - fst y\i) \ snd x\i - fst x\i))" (is "\x. ?P x") @@ -2182,11 +2182,11 @@ subsection%important \Cousin's lemma\ -lemma fine_division_exists: (*FIXME rename(?) *) +lemma%important fine_division_exists: fixes a b :: "'a::euclidean_space" assumes "gauge g" obtains p where "p tagged_division_of (cbox a b)" "g fine p" -proof (cases "\p. p tagged_division_of (cbox a b) \ g fine p") +proof%unimportant (cases "\p. p tagged_division_of (cbox a b) \ g fine p") case True then show ?thesis using that by auto @@ -2228,14 +2228,14 @@ subsection%important \A technical lemma about "refinement" of division\ -lemma tagged_division_finer: +lemma%important tagged_division_finer: fixes p :: "('a::euclidean_space \ ('a::euclidean_space set)) set" assumes ptag: "p tagged_division_of (cbox a b)" and "gauge d" obtains q where "q tagged_division_of (cbox a b)" and "d fine q" and "\(x,k) \ p. k \ d(x) \ (x,k) \ q" -proof - +proof%unimportant - have p: "finite p" "p tagged_partial_division_of (cbox a b)" using ptag unfolding tagged_division_of_def by auto have "(\q. q tagged_division_of (\{k. \x. (x,k) \ p}) \ d fine q \ (\(x,k) \ p. k \ d(x) \ (x,k) \ q))" @@ -2307,7 +2307,7 @@ lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's "Introduction to Gauge Integrals". \ -proposition covering_lemma: +proposition%important covering_lemma: assumes "S \ cbox a b" "box a b \ {}" "gauge g" obtains \ where "countable \" "\\ \ cbox a b" @@ -2316,7 +2316,7 @@ "\K. K \ \ \ \x \ S \ K. K \ g x" "\u v. cbox u v \ \ \ \n. \i \ Basis. v \ i - u \ i = (b \ i - a \ i) / 2^n" "S \ \\" -proof - +proof%unimportant - have aibi: "\i. i \ Basis \ a \ i \ b \ i" and normab: "0 < norm(b - a)" using \box a b \ {}\ box_eq_empty box_sing by fastforce+ let ?K0 = "\(n, f::'a\nat). @@ -2578,11 +2578,11 @@ definition%important division_filter :: "'a::euclidean_space set \ ('a \ 'a set) set filter" where "division_filter s = (INF g\{g. gauge g}. principal {p. p tagged_division_of s \ g fine p})" -proposition eventually_division_filter: +lemma%important eventually_division_filter: "(\\<^sub>F p in division_filter s. P p) \ (\g. gauge g \ (\p. p tagged_division_of s \ g fine p \ P p))" - unfolding division_filter_def -proof (subst eventually_INF_base; clarsimp) + unfolding%unimportant division_filter_def +proof%unimportant (subst eventually_INF_base; clarsimp) fix g1 g2 :: "'a \ 'a set" show "gauge g1 \ gauge g2 \ \x. gauge x \ {p. p tagged_division_of s \ x fine p} \ {p. p tagged_division_of s \ g1 fine p} \ {p. p tagged_division_of s \ x fine p} \ {p. p tagged_division_of s \ g2 fine p}" @@ -2593,7 +2593,7 @@ unfolding trivial_limit_def eventually_division_filter by (auto elim: fine_division_exists) -lemma eventually_division_filter_tagged_division: +lemma%important eventually_division_filter_tagged_division: "eventually (\p. p tagged_division_of s) (division_filter s)" unfolding eventually_division_filter by (intro exI[of _ "\x. ball x 1"]) auto