# HG changeset patch # User Angeliki KoutsoukouArgyraki # Date 1547740228 0 # Node ID 0f4d4a13dc16459e71a81d1465e328db9b6754fb # Parent a06b204527e689e10ba41cc9f31a1a94ce79329e# Parent cc47e7e06f383419ec8fcc465b8ea4cfe5247bc8 more tagging diff -r a06b204527e6 -r 0f4d4a13dc16 src/HOL/Analysis/Cartesian_Euclidean_Space.thy diff -r a06b204527e6 -r 0f4d4a13dc16 src/HOL/Analysis/Cartesian_Space.thy diff -r a06b204527e6 -r 0f4d4a13dc16 src/HOL/Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Jan 16 21:27:33 2019 +0000 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Jan 17 15:50:28 2019 +0000 @@ -13,7 +13,7 @@ "HOL-Library.FuncSet" begin -subsection%important \Finite Cartesian products, with indexing and lambdas\ +subsection%unimportant \Finite Cartesian products, with indexing and lambdas\ typedef ('a, 'b) vec = "UNIV :: ('b::finite \ 'a) set" morphisms vec_nth vec_lambda .. @@ -104,10 +104,10 @@ by (auto elim!: countableE) qed -lemma infinite_UNIV_vec: +lemma%important infinite_UNIV_vec: assumes "infinite (UNIV :: 'a set)" shows "infinite (UNIV :: ('a^'b) set)" -proof (subst bij_betw_finite) +proof%unimportant (subst bij_betw_finite) show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\_. UNIV :: 'a set))" by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff) have "infinite (PiE (UNIV :: 'b set) (\_. UNIV :: 'a set))" (is "infinite ?A") @@ -125,9 +125,9 @@ finally show "infinite (Pi (UNIV :: 'b set) (\_. UNIV :: 'a set))" . qed -lemma CARD_vec [simp]: +lemma%important CARD_vec [simp]: "CARD('a^'b) = CARD('a) ^ CARD('b)" -proof (cases "finite (UNIV :: 'a set)") +proof%unimportant (cases "finite (UNIV :: 'a set)") case True show ?thesis proof (subst bij_betw_same_card) @@ -143,7 +143,7 @@ qed qed (simp_all add: infinite_UNIV_vec) -lemma countable_vector: +lemma%unimportant countable_vector: fixes B:: "'n::finite \ 'a set" assumes "\i. countable (B i)" shows "countable {V. \i::'n::finite. V $ i \ B i}" @@ -165,7 +165,7 @@ by (simp add: image_comp o_def vec_nth_inverse) qed -subsection%important \Group operations and class instances\ +subsection%unimportant \Group operations and class instances\ instantiation vec :: (zero, finite) zero begin @@ -230,7 +230,7 @@ by standard (simp_all add: vec_eq_iff) -subsection%important\Basic componentwise operations on vectors\ +subsection%unimportant\Basic componentwise operations on vectors\ instantiation vec :: (times, finite) times begin @@ -295,12 +295,12 @@ text\Also the scalar-vector multiplication.\ -definition%important vector_scalar_mult:: "'a::times \ 'a ^ 'n \ 'a ^ 'n" (infixl "*s" 70) +definition vector_scalar_mult:: "'a::times \ 'a ^ 'n \ 'a ^ 'n" (infixl "*s" 70) where "c *s x = (\ i. c * (x$i))" text \scalar product\ -definition%important scalar_product :: "'a :: semiring_1 ^ 'n \ 'a ^ 'n \ 'a" where +definition scalar_product :: "'a :: semiring_1 ^ 'n \ 'a ^ 'n \ 'a" where "scalar_product v w = (\ i \ UNIV. v $ i * w $ i)" @@ -311,7 +311,7 @@ definition%important "scaleR \ (\ r x. (\ i. scaleR r (x$i)))" -lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)" +lemma%important vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)" unfolding scaleR_vec_def by simp instance%unimportant @@ -330,7 +330,7 @@ (\x\S. \A. (\i. open (A i) \ x$i \ A i) \ (\y. (\i. y$i \ A i) \ y \ S))" -instance proof +instance proof%unimportant show "open (UNIV :: ('a ^ 'b) set)" unfolding open_vec_def by auto next @@ -358,30 +358,30 @@ end -lemma open_vector_box: "\i. open (S i) \ open {x. \i. x $ i \ S i}" +lemma%unimportant open_vector_box: "\i. open (S i) \ open {x. \i. x $ i \ S i}" unfolding open_vec_def by auto -lemma open_vimage_vec_nth: "open S \ open ((\x. x $ i) -` S)" +lemma%unimportant open_vimage_vec_nth: "open S \ open ((\x. x $ i) -` S)" unfolding open_vec_def apply clarify apply (rule_tac x="\k. if k = i then S else UNIV" in exI, simp) done -lemma closed_vimage_vec_nth: "closed S \ closed ((\x. x $ i) -` S)" +lemma%unimportant closed_vimage_vec_nth: "closed S \ closed ((\x. x $ i) -` S)" unfolding closed_open vimage_Compl [symmetric] by (rule open_vimage_vec_nth) -lemma closed_vector_box: "\i. closed (S i) \ closed {x. \i. x $ i \ S i}" +lemma%unimportant closed_vector_box: "\i. closed (S i) \ closed {x. \i. x $ i \ S i}" proof - have "{x. \i. x $ i \ S i} = (\i. (\x. x $ i) -` S i)" by auto thus "\i. closed (S i) \ closed {x. \i. x $ i \ S i}" by (simp add: closed_INT closed_vimage_vec_nth) qed -lemma tendsto_vec_nth [tendsto_intros]: +lemma%important tendsto_vec_nth [tendsto_intros]: assumes "((\x. f x) \ a) net" shows "((\x. f x $ i) \ a $ i) net" -proof (rule topological_tendstoI) +proof%unimportant (rule topological_tendstoI) fix S assume "open S" "a $ i \ S" then have "open ((\y. y $ i) -` S)" "a \ ((\y. y $ i) -` S)" by (simp_all add: open_vimage_vec_nth) @@ -391,13 +391,13 @@ by simp qed -lemma isCont_vec_nth [simp]: "isCont f a \ isCont (\x. f x $ i) a" +lemma%unimportant isCont_vec_nth [simp]: "isCont f a \ isCont (\x. f x $ i) a" unfolding isCont_def by (rule tendsto_vec_nth) -lemma vec_tendstoI: +lemma%important vec_tendstoI: assumes "\i. ((\x. f x $ i) \ a $ i) net" shows "((\x. f x) \ a) net" -proof (rule topological_tendstoI) +proof%unimportant (rule topological_tendstoI) fix S assume "open S" and "a \ S" then obtain A where A: "\i. open (A i)" "\i. a $ i \ A i" and S: "\y. \i. y $ i \ A i \ y \ S" @@ -410,13 +410,13 @@ by (rule eventually_mono, simp add: S) qed -lemma tendsto_vec_lambda [tendsto_intros]: +lemma%unimportant tendsto_vec_lambda [tendsto_intros]: assumes "\i. ((\x. f x i) \ a i) net" shows "((\x. \ i. f x i) \ (\ i. a i)) net" using assms by (simp add: vec_tendstoI) -lemma open_image_vec_nth: assumes "open S" shows "open ((\x. x $ i) ` S)" -proof (rule openI) +lemma%important open_image_vec_nth: assumes "open S" shows "open ((\x. x $ i) ` S)" +proof%unimportant (rule openI) fix a assume "a \ (\x. x $ i) ` S" then obtain z where "a = z $ i" and "z \ S" .. then obtain A where A: "\i. open (A i) \ z $ i \ A i" @@ -470,10 +470,10 @@ instantiation%unimportant vec :: (metric_space, finite) metric_space begin -lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \ dist x y" +lemma%important dist_vec_nth_le: "dist (x $ i) (y $ i) \ dist x y" unfolding dist_vec_def by (rule member_le_L2_set) simp_all -instance proof +instance proof%unimportant fix x y :: "'a ^ 'b" show "dist x y = 0 \ x = y" unfolding dist_vec_def @@ -532,15 +532,15 @@ end -lemma Cauchy_vec_nth: +lemma%important Cauchy_vec_nth: "Cauchy (\n. X n) \ Cauchy (\n. X n $ i)" unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_vec_nth_le]) -lemma vec_CauchyI: +lemma%important vec_CauchyI: fixes X :: "nat \ 'a::metric_space ^ 'n" assumes X: "\i. Cauchy (\n. X n $ i)" shows "Cauchy (\n. X n)" -proof (rule metric_CauchyI) +proof%unimportant (rule metric_CauchyI) fix r :: real assume "0 < r" hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp define N where "N i = (LEAST N. \m\N. \n\N. dist (X m $ i) (X n $ i) < ?s)" for i @@ -591,7 +591,7 @@ definition%important "sgn (x::'a^'b) = scaleR (inverse (norm x)) x" -instance proof +instance proof%unimportant fix a :: real and x y :: "'a ^ 'b" show "norm x = 0 \ x = 0" unfolding norm_vec_def @@ -613,32 +613,32 @@ end -lemma norm_nth_le: "norm (x $ i) \ norm x" +lemma%unimportant norm_nth_le: "norm (x $ i) \ norm x" unfolding norm_vec_def by (rule member_le_L2_set) simp_all -lemma norm_le_componentwise_cart: +lemma%important norm_le_componentwise_cart: fixes x :: "'a::real_normed_vector^'n" assumes "\i. norm(x$i) \ norm(y$i)" shows "norm x \ norm y" - unfolding norm_vec_def - by (rule L2_set_mono) (auto simp: assms) + unfolding%unimportant norm_vec_def + by%unimportant (rule L2_set_mono) (auto simp: assms) -lemma component_le_norm_cart: "\x$i\ \ norm x" +lemma%unimportant component_le_norm_cart: "\x$i\ \ norm x" apply (simp add: norm_vec_def) apply (rule member_le_L2_set, simp_all) done -lemma norm_bound_component_le_cart: "norm x \ e ==> \x$i\ \ e" +lemma%unimportant norm_bound_component_le_cart: "norm x \ e ==> \x$i\ \ e" by (metis component_le_norm_cart order_trans) -lemma norm_bound_component_lt_cart: "norm x < e ==> \x$i\ < e" +lemma%unimportant norm_bound_component_lt_cart: "norm x < e ==> \x$i\ < e" by (metis component_le_norm_cart le_less_trans) -lemma norm_le_l1_cart: "norm x \ sum(\i. \x$i\) UNIV" +lemma%unimportant norm_le_l1_cart: "norm x \ sum(\i. \x$i\) UNIV" by (simp add: norm_vec_def L2_set_le_sum) -lemma bounded_linear_vec_nth: "bounded_linear (\x. x $ i)" +lemma%unimportant bounded_linear_vec_nth: "bounded_linear (\x. x $ i)" apply standard apply (rule vector_add_component) apply (rule vector_scaleR_component) @@ -655,7 +655,7 @@ definition%important "inner x y = sum (\i. inner (x$i) (y$i)) UNIV" -instance proof +instance proof%unimportant fix r :: real and x y z :: "'a ^ 'b" show "inner x y = inner y x" unfolding inner_vec_def @@ -686,13 +686,13 @@ definition%important "axis k x = (\ i. if i = k then x else 0)" -lemma axis_nth [simp]: "axis i x $ i = x" +lemma%unimportant axis_nth [simp]: "axis i x $ i = x" unfolding axis_def by simp -lemma axis_eq_axis: "axis i x = axis j y \ x = y \ i = j \ x = 0 \ y = 0" +lemma%unimportant axis_eq_axis: "axis i x = axis j y \ x = y \ i = j \ x = 0 \ y = 0" unfolding axis_def vec_eq_iff by auto -lemma inner_axis_axis: +lemma%unimportant inner_axis_axis: "inner (axis i x) (axis j y) = (if i = j then inner x y else 0)" unfolding inner_vec_def apply (cases "i = j") @@ -702,10 +702,10 @@ apply (rule sum.neutral, simp add: axis_def) done -lemma inner_axis: "inner x (axis i y) = inner (x $ i) y" +lemma%unimportant inner_axis: "inner x (axis i y) = inner (x $ i) y" by (simp add: inner_vec_def axis_def sum.remove [where x=i]) -lemma inner_axis': "inner(axis i y) x = inner y (x $ i)" +lemma%unimportant inner_axis': "inner(axis i y) x = inner y (x $ i)" by (simp add: inner_axis inner_commute) instantiation%unimportant vec :: (euclidean_space, finite) euclidean_space @@ -713,7 +713,7 @@ definition%important "Basis = (\i. \u\Basis. {axis i u})" -instance proof +instance proof%unimportant show "(Basis :: ('a ^ 'b) set) \ {}" unfolding Basis_vec_def by simp next @@ -732,8 +732,8 @@ by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff) qed -proposition DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)" -proof - +lemma%important DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)" +proof%unimportant - have "card (\i::'b. \u::'a\Basis. {axis i u}) = (\i::'b\UNIV. card (\u::'a\Basis. {axis i u}))" by (rule card_UN_disjoint) (auto simp: axis_eq_axis) also have "... = CARD('b) * DIM('a)" @@ -744,30 +744,30 @@ end -lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1" +lemma%unimportant norm_axis_1 [simp]: "norm (axis m (1::real)) = 1" by (simp add: inner_axis' norm_eq_1) -lemma sum_norm_allsubsets_bound_cart: +lemma%important sum_norm_allsubsets_bound_cart: fixes f:: "'a \ real ^'n" assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (sum f Q) \ e" shows "sum (\x. norm (f x)) P \ 2 * real CARD('n) * e" - using sum_norm_allsubsets_bound[OF assms] - by simp + using%unimportant sum_norm_allsubsets_bound[OF assms] + by%unimportant simp -lemma cart_eq_inner_axis: "a $ i = inner a (axis i 1)" +lemma%unimportant cart_eq_inner_axis: "a $ i = inner a (axis i 1)" by (simp add: inner_axis) -lemma axis_eq_0_iff [simp]: +lemma%unimportant axis_eq_0_iff [simp]: shows "axis m x = 0 \ x = 0" by (simp add: axis_def vec_eq_iff) -lemma axis_in_Basis_iff [simp]: "axis i a \ Basis \ a \ Basis" +lemma%unimportant axis_in_Basis_iff [simp]: "axis i a \ Basis \ a \ Basis" by (auto simp: Basis_vec_def axis_eq_axis) text\Mapping each basis element to the corresponding finite index\ definition axis_index :: "('a::comm_ring_1)^'n \ 'n" where "axis_index v \ SOME i. v = axis i 1" -lemma axis_inverse: +lemma%unimportant axis_inverse: fixes v :: "real^'n" assumes "v \ Basis" shows "\i. v = axis i 1" @@ -778,20 +778,20 @@ by (force simp add: vec_eq_iff) qed -lemma axis_index: +lemma%unimportant axis_index: fixes v :: "real^'n" assumes "v \ Basis" shows "v = axis (axis_index v) 1" by (metis (mono_tags) assms axis_inverse axis_index_def someI_ex) -lemma axis_index_axis [simp]: +lemma%unimportant axis_index_axis [simp]: fixes UU :: "real^'n" shows "(axis_index (axis u 1 :: real^'n)) = (u::'n)" by (simp add: axis_eq_axis axis_index_def) subsection%unimportant \A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\ -lemma sum_cong_aux: +lemma%unimportant sum_cong_aux: "(\x. x \ A \ f x = g x) \ sum f A = sum g A" by (auto intro: sum.cong) @@ -823,22 +823,22 @@ end \ "lift trivial vector statements to real arith statements" -lemma vec_0[simp]: "vec 0 = 0" by vector -lemma vec_1[simp]: "vec 1 = 1" by vector +lemma%unimportant vec_0[simp]: "vec 0 = 0" by vector +lemma%unimportant vec_1[simp]: "vec 1 = 1" by vector -lemma vec_inj[simp]: "vec x = vec y \ x = y" by vector +lemma%unimportant vec_inj[simp]: "vec x = vec y \ x = y" by vector -lemma vec_in_image_vec: "vec x \ (vec ` S) \ x \ S" by auto +lemma%unimportant vec_in_image_vec: "vec x \ (vec ` S) \ x \ S" by auto -lemma vec_add: "vec(x + y) = vec x + vec y" by vector -lemma vec_sub: "vec(x - y) = vec x - vec y" by vector -lemma vec_cmul: "vec(c * x) = c *s vec x " by vector -lemma vec_neg: "vec(- x) = - vec x " by vector +lemma%unimportant vec_add: "vec(x + y) = vec x + vec y" by vector +lemma%unimportant vec_sub: "vec(x - y) = vec x - vec y" by vector +lemma%unimportant vec_cmul: "vec(c * x) = c *s vec x " by vector +lemma%unimportant vec_neg: "vec(- x) = - vec x " by vector -lemma vec_scaleR: "vec(c * x) = c *\<^sub>R vec x" +lemma%unimportant vec_scaleR: "vec(c * x) = c *\<^sub>R vec x" by vector -lemma vec_sum: +lemma%unimportant vec_sum: assumes "finite S" shows "vec(sum f S) = sum (vec \ f) S" using assms @@ -852,24 +852,24 @@ text\Obvious "component-pushing".\ -lemma vec_component [simp]: "vec x $ i = x" +lemma%unimportant vec_component [simp]: "vec x $ i = x" by vector -lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i" +lemma%unimportant vector_mult_component [simp]: "(x * y)$i = x$i * y$i" by vector -lemma vector_smult_component [simp]: "(c *s y)$i = c * (y$i)" +lemma%unimportant vector_smult_component [simp]: "(c *s y)$i = c * (y$i)" by vector -lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector +lemma%unimportant cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector -lemmas vector_component = +lemmas%unimportant vector_component = vec_component vector_add_component vector_mult_component vector_smult_component vector_minus_component vector_uminus_component vector_scaleR_component cond_component -subsection%important \Some frequently useful arithmetic lemmas over vectors\ +subsection%unimportant \Some frequently useful arithmetic lemmas over vectors\ instance vec :: (semigroup_mult, finite) semigroup_mult by standard (vector mult.assoc) @@ -1011,7 +1011,7 @@ definition%important map_matrix::"('a \ 'b) \ (('a, 'i::finite)vec, 'j::finite) vec \ (('b, 'i)vec, 'j) vec" where "map_matrix f x = (\ i j. f (x $ i $ j))" -lemma nth_map_matrix[simp]: "map_matrix f x $ i $ j = f (x $ i $ j)" +lemma%unimportant nth_map_matrix[simp]: "map_matrix f x $ i $ j = f (x $ i $ j)" by (simp add: map_matrix_def) definition%important matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \ 'a ^'p^'n \ 'a ^ 'p ^'m" @@ -1034,17 +1034,17 @@ definition%unimportant "rows(A::'a^'n^'m) = { row i A | i. i \ (UNIV :: 'm set)}" definition%unimportant "columns(A::'a^'n^'m) = { column i A | i. i \ (UNIV :: 'n set)}" -lemma times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0" +lemma%unimportant times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0" by (simp add: matrix_matrix_mult_def zero_vec_def) -lemma times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0" +lemma%unimportant times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0" by (simp add: matrix_matrix_mult_def zero_vec_def) -lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def) -lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)" +lemma%unimportant mat_0[simp]: "mat 0 = 0" by (vector mat_def) +lemma%unimportant matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)" by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps) -lemma matrix_mul_lid [simp]: +lemma%unimportant matrix_mul_lid [simp]: fixes A :: "'a::semiring_1 ^ 'm ^ 'n" shows "mat 1 ** A = A" apply (simp add: matrix_matrix_mult_def mat_def) @@ -1053,7 +1053,7 @@ mult_1_left mult_zero_left if_True UNIV_I) done -lemma matrix_mul_rid [simp]: +lemma%unimportant matrix_mul_rid [simp]: fixes A :: "'a::semiring_1 ^ 'm ^ 'n" shows "A ** mat 1 = A" apply (simp add: matrix_matrix_mult_def mat_def) @@ -1062,39 +1062,47 @@ mult_1_right mult_zero_right if_True UNIV_I cong: if_cong) done -proposition matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C" +lemma%unimportant matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C" apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc) apply (subst sum.swap) apply simp done -proposition matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x" +lemma%unimportant matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x" apply (vector matrix_matrix_mult_def matrix_vector_mult_def sum_distrib_left sum_distrib_right mult.assoc) apply (subst sum.swap) apply simp done -lemma scalar_matrix_assoc: +lemma%unimportant scalar_matrix_assoc: fixes A :: "('a::real_algebra_1)^'m^'n" shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B" by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff scaleR_sum_right) -lemma matrix_scalar_ac: +lemma%unimportant matrix_scalar_ac: fixes A :: "('a::real_algebra_1)^'m^'n" shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B" by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff) -lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)" +lemma%unimportant matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)" apply (vector matrix_vector_mult_def mat_def) apply (simp add: if_distrib if_distribR sum.delta' cong del: if_weak_cong) done -lemma matrix_transpose_mul: +lemma%unimportant matrix_transpose_mul: "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)" by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult.commute) -lemma matrix_eq: +lemma%unimportant matrix_mult_transpose_dot_column: + shows "transpose A ** A = (\ i j. inner (column i A) (column j A))" + by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def) + +lemma%unimportant matrix_mult_transpose_dot_row: + shows "A ** transpose A = (\ i j. inner (row i A) (row j A))" + by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def) + +lemma%unimportant matrix_eq: fixes A B :: "'a::semiring_1 ^ 'n ^ 'm" shows "A = B \ (\x. A *v x = B *v x)" (is "?lhs \ ?rhs") apply auto @@ -1107,49 +1115,49 @@ sum.delta[OF finite] cong del: if_weak_cong) done -lemma matrix_vector_mul_component: "(A *v x)$k = inner (A$k) x" +lemma%unimportant matrix_vector_mul_component: "(A *v x)$k = inner (A$k) x" by (simp add: matrix_vector_mult_def inner_vec_def) -lemma dot_lmul_matrix: "inner ((x::real ^_) v* A) y = inner x (A *v y)" +lemma%unimportant dot_lmul_matrix: "inner ((x::real ^_) v* A) y = inner x (A *v y)" apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps) apply (subst sum.swap) apply simp done -lemma transpose_mat [simp]: "transpose (mat n) = mat n" +lemma%unimportant transpose_mat [simp]: "transpose (mat n) = mat n" by (vector transpose_def mat_def) -lemma transpose_transpose [simp]: "transpose(transpose A) = A" +lemma%unimportant transpose_transpose [simp]: "transpose(transpose A) = A" by (vector transpose_def) -lemma row_transpose [simp]: "row i (transpose A) = column i A" +lemma%unimportant row_transpose [simp]: "row i (transpose A) = column i A" by (simp add: row_def column_def transpose_def vec_eq_iff) -lemma column_transpose [simp]: "column i (transpose A) = row i A" +lemma%unimportant column_transpose [simp]: "column i (transpose A) = row i A" by (simp add: row_def column_def transpose_def vec_eq_iff) -lemma rows_transpose [simp]: "rows(transpose A) = columns A" +lemma%unimportant rows_transpose [simp]: "rows(transpose A) = columns A" by (auto simp add: rows_def columns_def intro: set_eqI) -lemma columns_transpose [simp]: "columns(transpose A) = rows A" +lemma%unimportant columns_transpose [simp]: "columns(transpose A) = rows A" by (metis transpose_transpose rows_transpose) -lemma transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A" +lemma%unimportant transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A" unfolding transpose_def by (simp add: vec_eq_iff) -lemma transpose_iff [iff]: "transpose A = transpose B \ A = B" +lemma%unimportant transpose_iff [iff]: "transpose A = transpose B \ A = B" by (metis transpose_transpose) -lemma matrix_mult_sum: +lemma%unimportant matrix_mult_sum: "(A::'a::comm_semiring_1^'n^'m) *v x = sum (\i. (x$i) *s column i A) (UNIV:: 'n set)" by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult.commute) -lemma vector_componentwise: +lemma%unimportant vector_componentwise: "(x::'a::ring_1^'n) = (\ j. \i\UNIV. (x$i) * (axis i 1 :: 'a^'n) $ j)" by (simp add: axis_def if_distrib sum.If_cases vec_eq_iff) -lemma basis_expansion: "sum (\i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)" +lemma%unimportant basis_expansion: "sum (\i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)" by (auto simp add: axis_def vec_eq_iff if_distrib sum.If_cases cong del: if_weak_cong) @@ -1158,51 +1166,51 @@ definition%important matrix :: "('a::{plus,times, one, zero}^'m \ 'a ^ 'n) \ 'a^'m^'n" where "matrix f = (\ i j. (f(axis j 1))$i)" -lemma matrix_id_mat_1: "matrix id = mat 1" +lemma%unimportant matrix_id_mat_1: "matrix id = mat 1" by (simp add: mat_def matrix_def axis_def) -lemma matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r" +lemma%unimportant matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r" by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong) -lemma matrix_vector_mul_linear[intro, simp]: "linear (\x. A *v (x::'a::real_algebra_1 ^ _))" +lemma%unimportant matrix_vector_mul_linear[intro, simp]: "linear (\x. A *v (x::'a::real_algebra_1 ^ _))" by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum_distrib_left sum.distrib scaleR_right.sum) -lemma vector_matrix_left_distrib [algebra_simps]: +lemma%unimportant vector_matrix_left_distrib [algebra_simps]: shows "(x + y) v* A = x v* A + y v* A" unfolding vector_matrix_mult_def by (simp add: algebra_simps sum.distrib vec_eq_iff) -lemma matrix_vector_right_distrib [algebra_simps]: +lemma%unimportant matrix_vector_right_distrib [algebra_simps]: "A *v (x + y) = A *v x + A *v y" by (vector matrix_vector_mult_def sum.distrib distrib_left) -lemma matrix_vector_mult_diff_distrib [algebra_simps]: +lemma%unimportant matrix_vector_mult_diff_distrib [algebra_simps]: fixes A :: "'a::ring_1^'n^'m" shows "A *v (x - y) = A *v x - A *v y" by (vector matrix_vector_mult_def sum_subtractf right_diff_distrib) -lemma matrix_vector_mult_scaleR[algebra_simps]: +lemma%unimportant matrix_vector_mult_scaleR[algebra_simps]: fixes A :: "real^'n^'m" shows "A *v (c *\<^sub>R x) = c *\<^sub>R (A *v x)" using linear_iff matrix_vector_mul_linear by blast -lemma matrix_vector_mult_0_right [simp]: "A *v 0 = 0" +lemma%unimportant matrix_vector_mult_0_right [simp]: "A *v 0 = 0" by (simp add: matrix_vector_mult_def vec_eq_iff) -lemma matrix_vector_mult_0 [simp]: "0 *v w = 0" +lemma%unimportant matrix_vector_mult_0 [simp]: "0 *v w = 0" by (simp add: matrix_vector_mult_def vec_eq_iff) -lemma matrix_vector_mult_add_rdistrib [algebra_simps]: +lemma%unimportant matrix_vector_mult_add_rdistrib [algebra_simps]: "(A + B) *v x = (A *v x) + (B *v x)" by (vector matrix_vector_mult_def sum.distrib distrib_right) -lemma matrix_vector_mult_diff_rdistrib [algebra_simps]: +lemma%unimportant matrix_vector_mult_diff_rdistrib [algebra_simps]: fixes A :: "'a :: ring_1^'n^'m" shows "(A - B) *v x = (A *v x) - (B *v x)" by (vector matrix_vector_mult_def sum_subtractf left_diff_distrib) -lemma matrix_vector_column: +lemma%unimportant matrix_vector_column: "(A::'a::comm_semiring_1^'n^_) *v x = sum (\i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)" by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult.commute) @@ -1215,17 +1223,17 @@ "matrix_inv(A:: 'a::semiring_1^'n^'m) = (SOME A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" -lemma inj_matrix_vector_mult: +lemma%unimportant inj_matrix_vector_mult: fixes A::"'a::field^'n^'m" assumes "invertible A" shows "inj ((*v) A)" by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid) -lemma scalar_invertible: +lemma%important scalar_invertible: fixes A :: "('a::real_algebra_1)^'m^'n" assumes "k \ 0" and "invertible A" shows "invertible (k *\<^sub>R A)" -proof - +proof%unimportant - obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1" using assms unfolding invertible_def by auto with \k \ 0\ @@ -1235,50 +1243,50 @@ unfolding invertible_def by auto qed -lemma scalar_invertible_iff: +lemma%unimportant scalar_invertible_iff: fixes A :: "('a::real_algebra_1)^'m^'n" assumes "k \ 0" and "invertible A" shows "invertible (k *\<^sub>R A) \ k \ 0 \ invertible A" by (simp add: assms scalar_invertible) -lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v x" +lemma%unimportant vector_transpose_matrix [simp]: "x v* transpose A = A *v x" unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def by simp -lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* A" +lemma%unimportant transpose_matrix_vector [simp]: "transpose A *v x = x v* A" unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def by simp -lemma vector_scalar_commute: +lemma%unimportant vector_scalar_commute: fixes A :: "'a::{field}^'m^'n" shows "A *v (c *s x) = c *s (A *v x)" by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left) -lemma scalar_vector_matrix_assoc: +lemma%unimportant scalar_vector_matrix_assoc: fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n" shows "(k *s x) v* A = k *s (x v* A)" by (metis transpose_matrix_vector vector_scalar_commute) -lemma vector_matrix_mult_0 [simp]: "0 v* A = 0" +lemma%unimportant vector_matrix_mult_0 [simp]: "0 v* A = 0" unfolding vector_matrix_mult_def by (simp add: zero_vec_def) -lemma vector_matrix_mult_0_right [simp]: "x v* 0 = 0" +lemma%unimportant vector_matrix_mult_0_right [simp]: "x v* 0 = 0" unfolding vector_matrix_mult_def by (simp add: zero_vec_def) -lemma vector_matrix_mul_rid [simp]: +lemma%unimportant vector_matrix_mul_rid [simp]: fixes v :: "('a::semiring_1)^'n" shows "v v* mat 1 = v" by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix) -lemma scaleR_vector_matrix_assoc: +lemma%unimportant scaleR_vector_matrix_assoc: fixes k :: real and x :: "real^'n" and A :: "real^'m^'n" shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)" by (metis matrix_vector_mult_scaleR transpose_matrix_vector) -lemma vector_scaleR_matrix_ac: +lemma%important vector_scaleR_matrix_ac: fixes k :: real and x :: "real^'n" and A :: "real^'m^'n" shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)" -proof - +proof%unimportant - have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A" unfolding vector_matrix_mult_def by (simp add: algebra_simps) diff -r a06b204527e6 -r 0f4d4a13dc16 src/HOL/Analysis/Further_Topology.thy --- a/src/HOL/Analysis/Further_Topology.thy Wed Jan 16 21:27:33 2019 +0000 +++ b/src/HOL/Analysis/Further_Topology.thy Thu Jan 17 15:50:28 2019 +0000 @@ -1,4 +1,4 @@ -section%important \Extending Continous Maps, Invariance of Domain, etc\ +section%important \Extending Continous Maps, Invariance of Domain, etc\ (*FIX rename? *) 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%important spheremap_lemma1: +lemma 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%unimportant +proof 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%important spheremap_lemma2: +lemma 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%unimportant - +proof - 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%important spheremap_lemma3: +lemma 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%unimportant (cases "S = {}") +proof (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%important inessential_spheremap_lowdim_gen: +proposition 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%unimportant (cases "S = {}") +proof (cases "S = {}") case True then show ?thesis by (simp add: that) @@ -350,7 +350,7 @@ qed qed -lemma%unimportant inessential_spheremap_lowdim: +lemma 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%unimportant extending_maps_Union_aux: +lemma 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%unimportant extending_maps_Union: +lemma 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%important extend_map_lemma: +lemma 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%unimportant (cases "\ - \ = {}") +proof (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%unimportant extend_map_lemma_cofinite0: +lemma 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%unimportant extend_map_lemma_cofinite1: +lemma 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%important extend_map_lemma_cofinite: +lemma 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%unimportant - +proof - 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%important extend_map_cell_complex_to_sphere: +theorem 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%unimportant - +proof - 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%important extend_map_cell_complex_to_sphere_cofinite: +theorem 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%unimportant - +proof - 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%unimportant disjnt_Diff1: "X \ Y' \ disjnt (X - Y) (X' - Y')" +lemma disjnt_Diff1: "X \ Y' \ disjnt (X - Y) (X' - Y')" by (auto simp: disjnt_def) -proposition%important extend_map_affine_to_sphere_cofinite_simple: +proposition 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%unimportant - +proof - 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%important extend_map_affine_to_sphere1: +lemma 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%unimportant (cases "K = {}") +proof (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%important extend_map_affine_to_sphere2: +lemma 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%unimportant - +proof - 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%important extend_map_affine_to_sphere_cofinite_gen: +proposition 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%unimportant (cases "S = {}") +proof (cases "S = {}") case True show ?thesis proof (cases "rel_frontier U = {}") @@ -1645,7 +1645,7 @@ qed -corollary%important extend_map_affine_to_sphere_cofinite: +corollary 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%unimportant (cases "r = 0") +proof (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%important extend_map_UNIV_to_sphere_cofinite: +corollary 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%important extend_map_UNIV_to_sphere_no_bounded_component: +corollary 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%important Borsuk_separation_theorem_gen: +theorem 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%unimportant +proof assume L [rule_format]: ?lhs show ?rhs proof clarify @@ -1734,14 +1734,14 @@ qed -corollary%important Borsuk_separation_theorem: +corollary 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%unimportant +proof assume L: ?lhs show ?rhs proof (cases "S = {}") @@ -1764,7 +1764,7 @@ qed -lemma%unimportant homotopy_eqv_separation: +lemma 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 -lemma%important Jordan_Brouwer_separation: +proposition 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%unimportant - +proof - have "- sphere a r \ ball a r \ {}" using \0 < r\ by (simp add: Int_absorb1 subset_eq) moreover @@ -1817,11 +1817,11 @@ qed -lemma%important Jordan_Brouwer_frontier: +proposition 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%unimportant (cases r rule: linorder_cases) +proof (cases r rule: linorder_cases) assume "r < 0" with S T show ?thesis by auto next @@ -1866,11 +1866,11 @@ qed (rule T) qed -lemma%important Jordan_Brouwer_nonseparation: +proposition 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%unimportant - +proof - 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%unimportant invariance_of_domain_ball: +lemma 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%important invariance_of_domain: +theorem 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%unimportant clarify +proof clarify fix a assume "a \ S" obtain \ where "\ > 0" and \: "cball a \ \ S" @@ -2004,7 +2004,7 @@ qed qed -lemma%unimportant inv_of_domain_ss0: +lemma 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%unimportant inv_of_domain_ss1: +lemma 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%important invariance_of_domain_subspaces: +corollary 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%unimportant - +proof - 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%important invariance_of_dimension_subspaces: +corollary 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%unimportant - +proof - 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%important invariance_of_domain_affine_sets: +corollary 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%unimportant (cases "S = {}") +proof (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%important invariance_of_dimension_affine_sets: +corollary 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%unimportant - +proof - 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%important invariance_of_dimension: +corollary 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%important continuous_injective_image_subspace_dim_le: +corollary 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%unimportant invariance_of_dimension_convex_domain: +lemma 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%unimportant homeomorphic_convex_sets_le: +lemma 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%unimportant homeomorphic_convex_sets: +lemma 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%unimportant homeomorphic_convex_compact_sets_eq: +lemma 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%unimportant invariance_of_domain_gen: +lemma 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%unimportant injective_into_1d_imp_open_map_UNIV: +lemma 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%unimportant continuous_on_inverse_open: +lemma 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%unimportant invariance_of_domain_homeomorphism: +lemma 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%important invariance_of_domain_homeomorphic: +corollary 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%unimportant continuous_image_subset_interior: +lemma 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%important homeomorphic_interiors_same_dimension: +lemma 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%unimportant (clarify elim!: ex_forward) +proof (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%unimportant homeomorphic_open_imp_same_dimension: +lemma 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 -lemma%unimportant homeomorphic_interiors: +proposition 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%unimportant homeomorphic_frontiers_same_dimension: +lemma 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%unimportant homeomorphic_frontiers: +lemma 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%unimportant continuous_image_subset_rel_interior: +lemma 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%unimportant homeomorphic_rel_interiors_same_dimension: +lemma 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%important homeomorphic_rel_interiors: +lemma 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%unimportant (cases "rel_interior T = {}") +proof (cases "rel_interior T = {}") case True with assms show ?thesis by auto next @@ -2630,7 +2630,7 @@ qed -lemma%unimportant homeomorphic_rel_boundaries_same_dimension: +lemma 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%unimportant homeomorphic_rel_boundaries: +lemma 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%important uniformly_continuous_homeomorphism_UNIV_trivial: +proposition 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%unimportant (cases "S = {}") +proof (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%unimportant homeomorphic_subspaces_eq: +lemma 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%unimportant homeomorphic_affine_sets_eq: +lemma 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%unimportant homeomorphic_hyperplanes_eq: +lemma 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%unimportant homeomorphic_UNIV_UNIV: +lemma 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%unimportant simply_connected_sphere_gen: +lemma 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\ - -proposition%important invariance_of_domain_sphere_affine_set_gen: +subsection%important\more invariance of domain\(*FIX ME title? *) + +proposition 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%unimportant (cases "rel_frontier U = {}") +proof (cases "rel_frontier U = {}") case True then show ?thesis using ope openin_subset by force @@ -2927,7 +2927,7 @@ qed -lemma%unimportant invariance_of_domain_sphere_affine_set: +lemma 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%unimportant no_embedding_sphere_lowdim: +lemma 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%unimportant simply_connected_sphere: +lemma 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%unimportant simply_connected_sphere_eq: +lemma 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%unimportant simply_connected_punctured_universe_eq: +lemma 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%unimportant not_simply_connected_circle: +lemma not_simply_connected_circle: fixes a :: complex shows "0 < r \ \ simply_connected(sphere a r)" by (simp add: simply_connected_sphere_eq) -proposition%important simply_connected_punctured_convex: +proposition simply_connected_punctured_convex: fixes a :: "'a::euclidean_space" assumes "convex S" and 3: "3 \ aff_dim S" shows "simply_connected(S - {a})" -proof%unimportant (cases "a \ rel_interior S") +proof (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%important simply_connected_punctured_universe: +corollary simply_connected_punctured_universe: fixes a :: "'a::euclidean_space" assumes "3 \ DIM('a)" shows "simply_connected(- {a})" -proof%unimportant - +proof - 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%important covering_space_power_punctured_plane: +proposition covering_space_power_punctured_plane: assumes "0 < n" shows "covering_space (- {0}) (\z::complex. z^n) (- {0})" -proof%unimportant - +proof - 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%important covering_space_square_punctured_plane: +corollary covering_space_square_punctured_plane: "covering_space (- {0}) (\z::complex. z^2) (- {0})" by%unimportant (simp add: covering_space_power_punctured_plane) -proposition%important covering_space_exp_punctured_plane: +proposition covering_space_exp_punctured_plane: "covering_space UNIV (\z::complex. exp z) (- {0})" -proof%unimportant (simp add: covering_space_def, intro conjI ballI) +proof (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\ - -lemma%unimportant inessential_eq_continuous_logarithm: +subsection%important\Hence the Borsukian results about mappings into circles\(*FIX ME title *) + +lemma 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%important inessential_imp_continuous_logarithm_circle: +corollary 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%unimportant inessential_eq_continuous_logarithm_circle: +lemma 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 -lemma%important homotopic_with_sphere_times: +proposition 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%unimportant - +proof - 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,14 +3585,13 @@ done qed - -lemma%important homotopic_circlemaps_divide: +proposition 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%unimportant - +proof - 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 - @@ -3646,7 +3645,7 @@ text\Many similar proofs below.\ -lemma%unimportant upper_hemicontinuous: +lemma 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}) \ @@ -3677,7 +3676,7 @@ by (simp add: openin_closedin_eq) qed -lemma%unimportant lower_hemicontinuous: +lemma 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}) \ @@ -3708,7 +3707,7 @@ by (simp add: openin_closedin_eq) qed -lemma%unimportant open_map_iff_lower_hemicontinuous_preimage: +lemma open_map_iff_lower_hemicontinuous_preimage: assumes "f ` S \ T" shows "((\U. openin (subtopology euclidean S) U \ openin (subtopology euclidean T) (f ` U)) \ @@ -3739,7 +3738,7 @@ using assms openin_imp_subset [OF opeSU] by (force simp: openin_closedin_eq) qed -lemma%unimportant closed_map_iff_upper_hemicontinuous_preimage: +lemma closed_map_iff_upper_hemicontinuous_preimage: assumes "f ` S \ T" shows "((\U. closedin (subtopology euclidean S) U \ closedin (subtopology euclidean T) (f ` U)) \ @@ -3770,7 +3769,7 @@ by (simp add: openin_closedin_eq) qed -proposition%important upper_lower_hemicontinuous_explicit: +proposition 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 @@ -3782,7 +3781,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%unimportant - +proof - 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) @@ -3843,11 +3842,11 @@ subsection%important\Complex logs exist on various "well-behaved" sets\ -lemma%important continuous_logarithm_on_contractible: +lemma 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%unimportant - +proof - obtain c where hom: "homotopic_with (\h. True) S (-{0}) f (\x. c)" using nullhomotopic_from_contractible assms by (metis imageE subset_Compl_singleton) @@ -3855,27 +3854,27 @@ by (metis inessential_eq_continuous_logarithm that) qed -lemma%important continuous_logarithm_on_simply_connected: +lemma 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%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: + 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: 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%unimportant continuous_logarithm_on_ball: +lemma 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%unimportant continuous_sqrt_on_contractible: +lemma 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" @@ -3892,7 +3891,7 @@ qed qed -lemma%unimportant continuous_sqrt_on_simply_connected: +lemma 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" @@ -3912,12 +3911,12 @@ subsection%important\Another simple case where sphere maps are nullhomotopic\ -lemma%important inessential_spheremap_2_aux: +lemma 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%unimportant - +proof - 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]) @@ -3939,12 +3938,12 @@ by metis qed -lemma%important inessential_spheremap_2: +lemma 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%unimportant (cases "s \ 0") +proof (cases "s \ 0") case True then show ?thesis using contf contractible_sphere fim nullhomotopic_into_contractible that by blast @@ -3978,12 +3977,12 @@ subsection%important\Holomorphic logarithms and square roots\ -lemma%important contractible_imp_holomorphic_log: +lemma 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%unimportant - +proof - 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)" @@ -4026,12 +4025,12 @@ qed (*Identical proofs*) -lemma%important simply_connected_imp_holomorphic_log: +lemma 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%unimportant - +proof - 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)" @@ -4074,7 +4073,7 @@ qed -lemma%unimportant contractible_imp_holomorphic_sqrt: +lemma contractible_imp_holomorphic_sqrt: assumes holf: "f holomorphic_on S" and S: "contractible S" and fnz: "\z. z \ S \ f z \ 0" @@ -4092,7 +4091,7 @@ qed qed -lemma%unimportant simply_connected_imp_holomorphic_sqrt: +lemma 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" @@ -4112,11 +4111,11 @@ text\ Related theorems about holomorphic inverse cosines.\ -lemma%important contractible_imp_holomorphic_arccos: +lemma 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%unimportant - +proof - 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" @@ -4150,11 +4149,11 @@ qed -lemma%important contractible_imp_holomorphic_arccos_bounded: +lemma 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%unimportant - +proof - 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)" @@ -4200,11 +4199,11 @@ \f. continuous_on S f \ f ` S \ (- {0::complex}) \ (\a. homotopic_with (\h. True) S (- {0}) f (\x. a))" -lemma%important Borsukian_retraction_gen: +lemma 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%unimportant - +proof - interpret R: Retracts S h T k using assms by (simp add: Retracts.intro) show ?thesis @@ -4214,42 +4213,42 @@ done qed -lemma%unimportant retract_of_Borsukian: "\Borsukian T; S retract_of T\ \ Borsukian S" +lemma 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%unimportant homeomorphic_Borsukian: "\Borsukian S; S homeomorphic T\ \ Borsukian T" +lemma homeomorphic_Borsukian: "\Borsukian S; S homeomorphic T\ \ Borsukian T" using Borsukian_retraction_gen order_refl by (fastforce simp add: homeomorphism_def homeomorphic_def) -lemma%unimportant homeomorphic_Borsukian_eq: +lemma homeomorphic_Borsukian_eq: "S homeomorphic T \ Borsukian S \ Borsukian T" by (meson homeomorphic_Borsukian homeomorphic_sym) -lemma%unimportant Borsukian_translation: +lemma 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%unimportant Borsukian_injective_linear_image: +lemma 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%unimportant homotopy_eqv_Borsukianness: +lemma 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%unimportant Borsukian_alt: +lemma Borsukian_alt: fixes S :: "'a::real_normed_vector set" shows "Borsukian S \ @@ -4259,20 +4258,20 @@ unfolding Borsukian_def homotopic_triviality by (simp add: path_connected_punctured_universe) -lemma%unimportant Borsukian_continuous_logarithm: +lemma 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%important Borsukian_continuous_logarithm_circle: +lemma 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%unimportant +proof assume ?lhs then show ?rhs by (force simp: Borsukian_continuous_logarithm) next @@ -4302,13 +4301,13 @@ qed -lemma%important Borsukian_continuous_logarithm_circle_real: +lemma 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%unimportant +proof assume LHS: ?lhs show ?rhs proof (clarify) @@ -4335,52 +4334,52 @@ qed qed -lemma%unimportant Borsukian_circle: +lemma 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%unimportant contractible_imp_Borsukian: "contractible S \ Borsukian S" +lemma contractible_imp_Borsukian: "contractible S \ Borsukian S" by (meson Borsukian_def nullhomotopic_from_contractible) -lemma%unimportant simply_connected_imp_Borsukian: +lemma 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%unimportant starlike_imp_Borsukian: +lemma 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%unimportant Borsukian_empty: "Borsukian {}" +lemma Borsukian_empty: "Borsukian {}" by (auto simp: contractible_imp_Borsukian) -lemma%unimportant Borsukian_UNIV: "Borsukian (UNIV :: 'a::real_normed_vector set)" +lemma Borsukian_UNIV: "Borsukian (UNIV :: 'a::real_normed_vector set)" by (auto simp: contractible_imp_Borsukian) -lemma%unimportant convex_imp_Borsukian: +lemma 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) -lemma%unimportant Borsukian_sphere: +proposition 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 -lemma%important Borsukian_open_Un: +proposition 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%unimportant (clarsimp simp add: Borsukian_continuous_logarithm) +proof (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" @@ -4444,13 +4443,13 @@ qed text\The proof is a duplicate of that of \Borsukian_open_Un\.\ -lemma%important Borsukian_closed_Un: +lemma 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%unimportant (clarsimp simp add: Borsukian_continuous_logarithm) +proof (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" @@ -4513,18 +4512,18 @@ qed qed -lemma%unimportant Borsukian_separation_compact: +lemma 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%important Borsukian_monotone_image_compact: +lemma 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%unimportant (clarsimp simp add: Borsukian_continuous_logarithm) +proof (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)" @@ -4584,13 +4583,13 @@ qed -lemma%important Borsukian_open_map_image_compact: +lemma 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%unimportant (clarsimp simp add: Borsukian_continuous_logarithm_circle_real) +proof (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)" @@ -4671,12 +4670,12 @@ text\If two points are separated by a closed set, there's a minimal one.\ -proposition%important closed_irreducible_separator: +proposition 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%unimportant (cases "a \ S \ b \ S") +proof (cases "a \ S \ b \ S") case True then show ?thesis proof @@ -4779,7 +4778,7 @@ qed qed -lemma%unimportant frontier_minimal_separating_closed_pointwise: +lemma 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" @@ -4816,21 +4815,21 @@ closedin (subtopology euclidean U) S \ closedin (subtopology euclidean U) T \ connected (S \ T)" -lemma%unimportant unicoherentI [intro?]: +lemma 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%unimportant unicoherentD: +lemma 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 -lemma%important homeomorphic_unicoherent: +proposition homeomorphic_unicoherent: assumes ST: "S homeomorphic T" and S: "unicoherent S" shows "unicoherent T" -proof%unimportant - +proof - 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) @@ -4871,24 +4870,24 @@ qed -lemma%unimportant homeomorphic_unicoherent_eq: +lemma homeomorphic_unicoherent_eq: "S homeomorphic T \ (unicoherent S \ unicoherent T)" by (meson homeomorphic_sym homeomorphic_unicoherent) -lemma%unimportant unicoherent_translation: +lemma 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%unimportant unicoherent_injective_linear_image: +lemma 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%unimportant Borsukian_imp_unicoherent: +lemma Borsukian_imp_unicoherent: fixes U :: "'a::euclidean_space set" assumes "Borsukian U" shows "unicoherent U" unfolding unicoherent_def @@ -4998,27 +4997,27 @@ qed -corollary%important contractible_imp_unicoherent: +corollary 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%important convex_imp_unicoherent: +corollary 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%important unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)" +corollary unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)" by%unimportant (simp add: convex_imp_unicoherent) -lemma%important unicoherent_monotone_image_compact: +lemma 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%unimportant +proof fix U V assume UV: "connected U" "connected V" "T = U \ V" and cloU: "closedin (subtopology euclidean T) U" @@ -5054,7 +5053,7 @@ subsection%important\Several common variants of unicoherence\ -lemma%unimportant connected_frontier_simple: +lemma connected_frontier_simple: fixes S :: "'a :: euclidean_space set" assumes "connected S" "connected(- S)" shows "connected(frontier S)" unfolding frontier_closures @@ -5062,18 +5061,18 @@ apply (simp_all add: assms connected_imp_connected_closure) by (simp add: closure_def) -lemma%unimportant connected_frontier_component_complement: +lemma 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%important connected_frontier_disjoint: +lemma 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%unimportant (cases "S = UNIV") +proof (cases "S = UNIV") case True then show ?thesis by simp next @@ -5107,11 +5106,11 @@ subsection%important\Some separation results\ -lemma%important separation_by_component_closed_pointwise: +lemma 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%unimportant (cases "a \ S \ b \ S") +proof (cases "a \ S \ b \ S") case True then show ?thesis using connected_component_in componentsI that by fastforce @@ -5144,11 +5143,11 @@ qed -lemma%important separation_by_component_closed: +lemma separation_by_component_closed: fixes S :: "'a :: euclidean_space set" assumes "closed S" "\ connected(- S)" obtains C where "C \ components S" "\ connected(- C)" -proof%unimportant - +proof - 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" @@ -5158,12 +5157,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%important separation_by_Un_closed_pointwise: +lemma 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%unimportant (rule ccontr) +proof (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" @@ -5182,14 +5181,14 @@ by (meson Compl_anti_mono C conS conT connected_component_of_subset) qed -lemma%unimportant separation_by_Un_closed: +lemma 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%unimportant open_unicoherent_UNIV: +lemma 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)" @@ -5200,7 +5199,7 @@ by simp qed -lemma%unimportant separation_by_component_open_aux: +lemma separation_by_component_open_aux: fixes S :: "'a :: euclidean_space set" assumes ST: "closed S" "closed T" "S \ T = {}" and "S \ {}" "T \ {}" @@ -5280,11 +5279,11 @@ qed -lemma%important separation_by_component_open: +proposition 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%unimportant - +proof - 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) @@ -5307,18 +5306,18 @@ qed qed -lemma%unimportant separation_by_Un_open: +lemma 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%important nonseparation_by_component_eq: +lemma 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%unimportant +proof assume ?lhs with assms show ?rhs by (meson separation_by_component_closed separation_by_component_open) next @@ -5328,13 +5327,13 @@ text\Another interesting equivalent of an inessential mapping into C-{0}\ -proposition%important inessential_eq_extensible: +proposition 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%unimportant +proof assume ?lhs then obtain a where a: "homotopic_with (\h. True) S (-{0}) f (\t. a)" .. show ?rhs @@ -5394,14 +5393,14 @@ by (simp add: inessential_eq_continuous_logarithm) qed -lemma%important inessential_on_clopen_Union: +lemma 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%unimportant (cases "\\ = {}") +proof (cases "\\ = {}") case True with that show ?thesis by force @@ -5442,12 +5441,12 @@ then show ?thesis .. qed -lemma%important Janiszewski_dual: +proposition Janiszewski_dual: fixes S :: "complex set" assumes "compact S" "compact T" "connected S" "connected T" "connected(- (S \ T))" shows "connected(S \ T)" -proof%unimportant - +proof - have ST: "compact (S \ T)" by (simp add: assms compact_Un) with Borsukian_imp_unicoherent [of "S \ T"] ST assms diff -r a06b204527e6 -r 0f4d4a13dc16 src/HOL/Analysis/Great_Picard.thy --- a/src/HOL/Analysis/Great_Picard.thy Wed Jan 16 21:27:33 2019 +0000 +++ b/src/HOL/Analysis/Great_Picard.thy Thu Jan 17 15:50:28 2019 +0000 @@ -9,13 +9,13 @@ subsection\Schottky's theorem\ -lemma%important Schottky_lemma0: +lemma 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%unimportant - +proof - 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%unimportant Schottky_lemma1: +lemma Schottky_lemma1: fixes n::nat assumes "0 < n" shows "0 < n + sqrt(real n ^ 2 - 1)" @@ -54,7 +54,7 @@ qed -lemma%unimportant Schottky_lemma2: +lemma 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%important Schottky_lemma3: +lemma 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%unimportant - +proof - 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%important Schottky: +theorem 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%unimportant - +proof - 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\ -lemma%important Landau_Picard: +proposition 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%unimportant - +proof - 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%important little_Picard_01: +lemma 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%unimportant - +proof - 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%important little_Picard: +theorem little_Picard: assumes holf: "f holomorphic_on UNIV" and "a \ b" "range f \ {a,b} = {}" obtains c where "f = (\x. c)" -proof%unimportant - +proof - 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%unimportant holomorphic_periodic_fixpoint: +lemma 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%unimportant holomorphic_involution_point: +lemma 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%unimportant subsequence_diagonalization_lemma: +lemma 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%unimportant function_convergent_subsequence: +lemma 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%important Arzela_Ascoli: +theorem 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%unimportant - +proof - 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%important Montel: +theorem 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%unimportant - +proof - 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%important Hurwitz_no_zeros: +proposition 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%unimportant +proof 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%important Hurwitz_injective: +corollary 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%unimportant - +proof - 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%important GPicard1: +lemma 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%unimportant - +proof - 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%important GPicard2: +lemma GPicard2: assumes "S \ T" "connected T" "S \ {}" "open S" "\x. \x islimpt S; x \ T\ \ x \ S" shows "S = T" - by%unimportant (metis assms open_subset connected_clopen closedin_limpt) + by (metis assms open_subset connected_clopen closedin_limpt) -lemma%important GPicard3: +lemma 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%unimportant - +proof - 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%important GPicard4: +lemma 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%unimportant - +proof - 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%important GPicard5: +lemma 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%unimportant - +proof - 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%important GPicard6: +lemma 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%unimportant - +proof - 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%important great_Picard: +theorem 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%unimportant - +proof - 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%important great_Picard_alt: +corollary 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%important great_Picard_infinite: +corollary 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%unimportant - +proof - 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 -corollary%important Casorati_Weierstrass: +theorem 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%unimportant - +proof - obtain a where a: "- {a} \ f ` (M - {z})" using great_Picard_alt [OF assms] . have "UNIV = closure(- {a})" diff -r a06b204527e6 -r 0f4d4a13dc16 src/HOL/Analysis/Homeomorphism.thy --- a/src/HOL/Analysis/Homeomorphism.thy Wed Jan 16 21:27:33 2019 +0000 +++ b/src/HOL/Analysis/Homeomorphism.thy Thu Jan 17 15:50:28 2019 +0000 @@ -8,7 +8,7 @@ imports Homotopy begin -lemma%unimportant homeomorphic_spheres': +lemma 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%unimportant homeomorphic_spheres_gen: +lemma 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%important ray_to_rel_frontier: +proposition 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%unimportant - +proof - 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%important ray_to_frontier: +corollary 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%unimportant - +proof - 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%unimportant segment_to_rel_frontier_aux: +lemma 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%unimportant segment_to_rel_frontier: +lemma 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%important rel_frontier_not_sing: +proposition rel_frontier_not_sing: fixes a :: "'a::euclidean_space" assumes "bounded S" shows "rel_frontier S \ {a}" -proof%unimportant (cases "S = {}") +proof (cases "S = {}") case True then show ?thesis by simp next case False @@ -278,7 +278,7 @@ qed qed -proposition%important +proposition (*FIXME needs name *) 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%unimportant - +proof - 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%important +corollary (* FIXME needs name *) 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%unimportant - +proof - 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%important starlike_compact_projective_special: +corollary 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%unimportant - +proof - 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%important homeomorphic_convex_lemma: +lemma 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%unimportant (cases "rel_interior S = {} \ rel_interior T = {}") +proof (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%unimportant homeomorphic_convex_compact_sets: +lemma 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%unimportant homeomorphic_rel_frontiers_convex_bounded_sets: +lemma 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%unimportant homeomorphic_punctured_affine_sphere_affine_01: +lemma 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%important homeomorphic_punctured_affine_sphere_affine: +theorem 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%unimportant - +proof - 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%important homeomorphic_punctured_sphere_affine: +corollary 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%important homeomorphic_punctured_sphere_hyperplane: +corollary 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%important homeomorphic_punctured_sphere_affine_gen: +proposition 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%unimportant - +proof - 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%important homeomorphic_closedin_convex: +proposition 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%unimportant (cases "S = {}") +proof (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%important locally_compact_open_Int_closure: +lemma 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%unimportant - +proof - 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%unimportant locally_compact_closedin_open: +lemma 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%unimportant locally_compact_homeomorphism_projection_closed: +lemma 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%unimportant locally_compact_closed_Int_open: +lemma 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%unimportant lowerdim_embeddings: +lemma 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%important locally_compact_homeomorphic_closed: +proposition 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%unimportant - +proof - 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%important homeomorphic_convex_compact_lemma: +lemma 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%unimportant (rule starlike_compact_projective_special[OF assms(2-3)]) +proof (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%important homeomorphic_convex_compact_cball: +proposition 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%unimportant - +proof - 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%important homeomorphic_convex_compact: +corollary 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%important\Covering spaces and lifting results for them\ +subsection\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%unimportant covering_space_imp_continuous: "covering_space c p S \ continuous_on c p" +lemma covering_space_imp_continuous: "covering_space c p S \ continuous_on c p" by (simp add: covering_space_def) -lemma%unimportant covering_space_imp_surjective: "covering_space c p S \ p ` c = S" +lemma covering_space_imp_surjective: "covering_space c p S \ p ` c = S" by (simp add: covering_space_def) -lemma%unimportant homeomorphism_imp_covering_space: "homeomorphism S T f g \ covering_space S f T" +lemma 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%unimportant covering_space_local_homeomorphism: +lemma 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%important covering_space_local_homeomorphism_alt: +lemma 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%unimportant - +proof - 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%important covering_space_open_map: +proposition 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%unimportant - +proof - have pce: "p ` c = S" and covs: "\x. x \ S \ @@ -1368,7 +1368,7 @@ with openin_subopen show ?thesis by blast qed -lemma%important covering_space_lift_unique_gen: +lemma 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%unimportant - +proof - 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%important covering_space_lift_unique: +proposition 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%unimportant covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv - by%unimportant blast + using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv + by blast -lemma%unimportant covering_space_locally: +lemma 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%important covering_space_locally_eq: +proposition 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%unimportant +proof assume L: ?lhs show ?rhs proof (rule locallyI) @@ -1518,7 +1518,7 @@ using cov covering_space_locally pim by blast qed -lemma%unimportant covering_space_locally_compact_eq: +lemma 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%unimportant covering_space_locally_connected_eq: +lemma 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%unimportant covering_space_locally_path_connected_eq: +lemma 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%unimportant covering_space_locally_compact: +lemma 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%unimportant covering_space_locally_connected: +lemma 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%unimportant covering_space_locally_path_connected: +lemma 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%important covering_space_lift_homotopy: +proposition 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%unimportant - +proof - 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%important covering_space_lift_homotopy_alt: +corollary 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%unimportant - +proof - 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%important covering_space_lift_homotopic_function: +corollary 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%unimportant - +proof - 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%important covering_space_lift_inessential_function: +corollary 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%unimportant (cases "U = {}") +proof (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%important covering_space_lift_path_strong: +proposition 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%unimportant - +proof - 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%important covering_space_lift_path: +corollary 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%unimportant - +proof - 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%important covering_space_lift_homotopic_paths: +proposition 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%unimportant - +proof - 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%important covering_space_monodromy: +corollary 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%important covering_space_lift_homotopic_path: +corollary 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%unimportant (rule covering_space_lift_path_strong [OF cov, of a f']) +proof (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%important covering_space_lift_general: +proposition 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%unimportant - +proof - 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%important covering_space_lift_stronger: +corollary 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%unimportant (rule covering_space_lift_general [OF cov U contf fim feq]) +proof (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%important covering_space_lift_strong: +corollary 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%unimportant (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq]) +proof (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%important covering_space_lift: +corollary 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%unimportant (cases "U = {}") +proof (cases "U = {}") case True with that show ?thesis by auto next diff -r a06b204527e6 -r 0f4d4a13dc16 src/HOL/Analysis/Improper_Integral.thy --- a/src/HOL/Analysis/Improper_Integral.thy Wed Jan 16 21:27:33 2019 +0000 +++ b/src/HOL/Analysis/Improper_Integral.thy Thu Jan 17 15:50:28 2019 +0000 @@ -28,11 +28,11 @@ unfolding equiintegrable_on_def Ball_def by (erule conj_forward imp_forward all_forward ex_forward | blast)+ -lemma%important equiintegrable_on_Un: +lemma equiintegrable_on_Un: assumes "F equiintegrable_on I" "G equiintegrable_on I" shows "(F \ G) equiintegrable_on I" unfolding equiintegrable_on_def -proof%unimportant (intro conjI impI allI) +proof (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%important equiintegrable_limit: +theorem 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%unimportant - +proof - have "Cauchy (\n. integral(cbox a b) (f n))" proof (clarsimp simp add: Cauchy_def) fix e::real @@ -151,10 +151,10 @@ qed -lemma%important equiintegrable_reflect: +lemma equiintegrable_reflect: assumes "F equiintegrable_on cbox a b" shows "(\f. f \ uminus) ` F equiintegrable_on cbox (-b) (-a)" -proof%unimportant - +proof - 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%important content_division_lemma1: +lemma 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%unimportant - +proof - have "finite \" using div by blast define extend where @@ -409,13 +409,13 @@ qed -proposition%important sum_content_area_over_thin_division: +proposition 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%unimportant (cases "content(cbox a b) = 0") +proof (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%important bounded_equiintegral_over_thin_tagged_partial_division: +proposition 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%unimportant (cases "content(cbox a b) = 0") +proof (cases "content(cbox a b) = 0") case True show ?thesis proof @@ -813,13 +813,13 @@ -proposition%important equiintegrable_halfspace_restrictions_le: +proposition 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%unimportant (cases "content(cbox a b) = 0") +proof (cases "content(cbox a b) = 0") case True then show ?thesis by simp next @@ -1172,13 +1172,13 @@ -corollary%important equiintegrable_halfspace_restrictions_ge: +corollary 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%unimportant - +proof - 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%important equiintegrable_closed_interval_restrictions: +proposition 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%unimportant - +proof - 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%important indefinite_integral_continuous: +proposition 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%unimportant - +proof - { 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%important indefinite_integral_uniformly_continuous: +corollary 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%unimportant - +proof - show ?thesis proof (rule compact_uniformly_continuous, clarsimp simp add: continuous_on_iff) fix c d and \::real @@ -1383,11 +1383,11 @@ qed -corollary%important bounded_integrals_over_subintervals: +corollary 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%unimportant - +proof - 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%important absolutely_integrable_improper: +theorem 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%unimportant (cases "content(cbox a b) = 0") +proof (cases "content(cbox a b) = 0") case True then show ?thesis by auto diff -r a06b204527e6 -r 0f4d4a13dc16 src/HOL/Analysis/Interval_Integral.thy --- a/src/HOL/Analysis/Interval_Integral.thy Wed Jan 16 21:27:33 2019 +0000 +++ b/src/HOL/Analysis/Interval_Integral.thy Thu Jan 17 15:50:28 2019 +0000 @@ -4,15 +4,15 @@ Lebesgue integral over an interval (with endpoints possibly +-\) *) -theory Interval_Integral +theory Interval_Integral (*FIX ME rename? Lebesgue *) imports Equivalence_Lebesgue_Henstock_Integration begin -lemma%important continuous_on_vector_derivative: +lemma continuous_on_vector_derivative: "(\x. x \ S \ (f has_vector_derivative f' x) (at x within S)) \ continuous_on S f" - by%unimportant (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous) + by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous) -definition%important "einterval a b = {x. a < ereal x \ ereal x < b}" +definition "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\Approximating a (possibly infinite) interval\ +subsection%important \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%important ereal_incseq_approx: +lemma 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%unimportant (cases b) +proof (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%important ereal_decseq_approx: +lemma 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%unimportant - +proof - 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 -lemma%important einterval_Icc_approximation: +proposition 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%unimportant - +proof - 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%important interval_lebesgue_integrable_mult_left [intro, simp]: +lemma 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%unimportant (simp add: interval_lebesgue_integrable_def) + by (simp add: interval_lebesgue_integrable_def) -lemma%important interval_lebesgue_integrable_divide [intro, simp]: +lemma 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%unimportant (simp add: interval_lebesgue_integrable_def) + by (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%important interval_lebesgue_integral_mult_left [simp]: +lemma 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%unimportant (simp add: interval_lebesgue_integral_def) + by (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%important interval_lebesgue_integral_le_eq: +lemma 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%unimportant assms by (auto simp: interval_lebesgue_integral_def) + using 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%important interval_integral_reflect: +lemma interval_integral_reflect: "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))" -proof%unimportant (induct a b rule: linorder_wlog) +proof (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 -lemma%important interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \ f) = +proposition 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%important interval_integral_cong_AE: +lemma 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%unimportant (induct a b rule: linorder_wlog) +proof (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%important interval_integral_cong: +lemma 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%unimportant (induct a b rule: linorder_wlog) +proof (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%important interval_integral_sum: +lemma 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%unimportant - +proof - 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%important interval_integrable_isCont: +lemma 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%unimportant (induct a b rule: linorder_wlog) +proof (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\ -lemma%important interval_integral_Icc_approx_nonneg: +proposition 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%unimportant - +proof - 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 -lemma%important interval_integral_Icc_approx_integrable: +proposition 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%unimportant - +proof - 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%important interval_integral_FTC_finite: +lemma 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%unimportant (cases "a \ b") +proof (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%important interval_integral_FTC_nonneg: +lemma 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%unimportant - +proof - 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 -lemma%important interval_integral_FTC_integrable: +theorem 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%unimportant - +proof - 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. *) -lemma%important interval_integral_FTC2: +theorem 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%unimportant - +proof - 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 -lemma%important einterval_antiderivative: +proposition 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%unimportant - +proof - 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.\ -lemma%important interval_integral_substitution_finite: +theorem 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%unimportant- +proof- 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? *) -lemma%important interval_integral_substitution_integrable: +theorem 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%unimportant - +proof - 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. *) -lemma%important interval_integral_substitution_nonneg: +theorem 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%unimportant - +proof - 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)" -lemma%important interval_integral_norm: +proposition 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) -lemma%important interval_integral_norm2: +proposition 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%unimportant (induct a b rule: linorder_wlog) +proof (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 a06b204527e6 -r 0f4d4a13dc16 src/HOL/Library/Numeral_Type.thy