# HG changeset patch # User nipkow # Date 1546019599 -3600 # Node ID bf88364c9e9462e49594d9ca9adea31699c688ae # Parent dc20f278e8f36d6f2fd8b2019fd86818f2518968 tuned headers etc, added bib-file diff -r dc20f278e8f3 -r bf88364c9e94 src/HOL/Analysis/Connected.thy --- a/src/HOL/Analysis/Connected.thy Fri Dec 28 10:29:59 2018 +0100 +++ b/src/HOL/Analysis/Connected.thy Fri Dec 28 18:53:19 2018 +0100 @@ -3519,7 +3519,7 @@ lemma homeomorphism_sym: "homeomorphism S t f g = homeomorphism t S g f" by (force simp: homeomorphism_def) -definition homeomorphic :: "'a::topological_space set \ 'b::topological_space set \ bool" +definition%important homeomorphic :: "'a::topological_space set \ 'b::topological_space set \ bool" (infixr "homeomorphic" 60) where "s homeomorphic t \ (\f g. homeomorphism s t f g)" diff -r dc20f278e8f3 -r bf88364c9e94 src/HOL/Analysis/Continuous_Extension.thy --- a/src/HOL/Analysis/Continuous_Extension.thy Fri Dec 28 10:29:59 2018 +0100 +++ b/src/HOL/Analysis/Continuous_Extension.thy Fri Dec 28 18:53:19 2018 +0100 @@ -297,10 +297,9 @@ using assms by (auto intro: Urysohn_local [of UNIV S T a b]) -subsection\The Dugundji Extension Theorem and Tietze Variants\ +subsection\Dugundji's Extension Theorem and Tietze Variants\ -text%important\J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367. -https://projecteuclid.org/euclid.pjm/1103052106\ +text \See \cite{dugundji}.\ theorem Dugundji: fixes f :: "'a::euclidean_space \ 'b::real_inner" @@ -488,7 +487,7 @@ using assms by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f]) -corollary Tietze_closed_interval: +corollary%unimportant Tietze_closed_interval: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "continuous_on S f" and "closedin (subtopology euclidean U) S" @@ -499,7 +498,7 @@ apply (rule Dugundji [of "cbox a b" U S f]) using assms by auto -corollary Tietze_closed_interval_1: +corollary%unimportant Tietze_closed_interval_1: fixes f :: "'a::euclidean_space \ real" assumes "continuous_on S f" and "closedin (subtopology euclidean U) S" @@ -510,7 +509,7 @@ apply (rule Dugundji [of "cbox a b" U S f]) using assms by (auto simp: image_subset_iff) -corollary Tietze_open_interval: +corollary%unimportant Tietze_open_interval: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "continuous_on S f" and "closedin (subtopology euclidean U) S" @@ -521,7 +520,7 @@ apply (rule Dugundji [of "box a b" U S f]) using assms by auto -corollary Tietze_open_interval_1: +corollary%unimportant Tietze_open_interval_1: fixes f :: "'a::euclidean_space \ real" assumes "continuous_on S f" and "closedin (subtopology euclidean U) S" @@ -532,7 +531,7 @@ apply (rule Dugundji [of "box a b" U S f]) using assms by (auto simp: image_subset_iff) -corollary Tietze_unbounded: +corollary%unimportant Tietze_unbounded: fixes f :: "'a::euclidean_space \ 'b::real_inner" assumes "continuous_on S f" and "closedin (subtopology euclidean U) S" diff -r dc20f278e8f3 -r bf88364c9e94 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Dec 28 10:29:59 2018 +0100 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Dec 28 18:53:19 2018 +0100 @@ -6,7 +6,7 @@ Author: Johannes Hoelzl, TU Muenchen *) -section \Convex sets, functions and related things\ +section \Convex Sets and Functions\ theory Convex_Euclidean_Space imports diff -r dc20f278e8f3 -r bf88364c9e94 src/HOL/Analysis/Operator_Norm.thy --- a/src/HOL/Analysis/Operator_Norm.thy Fri Dec 28 10:29:59 2018 +0100 +++ b/src/HOL/Analysis/Operator_Norm.thy Fri Dec 28 18:53:19 2018 +0100 @@ -3,7 +3,7 @@ Author: Brian Huffman *) -section%important \Operator Norm\ +section \Operator Norm\ theory Operator_Norm imports Complex_Main @@ -11,14 +11,15 @@ text \This formulation yields zero if \'a\ is the trivial vector space.\ -definition%important onorm :: "('a::real_normed_vector \ 'b::real_normed_vector) \ real" - where "onorm f = (SUP x. norm (f x) / norm x)" +definition%important +onorm :: "('a::real_normed_vector \ 'b::real_normed_vector) \ real" where +"onorm f = (SUP x. norm (f x) / norm x)" -lemma%important onorm_bound: +proposition onorm_bound: assumes "0 \ b" and "\x. norm (f x) \ b * norm x" shows "onorm f \ b" unfolding onorm_def -proof%unimportant (rule cSUP_least) +proof (rule cSUP_least) fix x show "norm (f x) / norm x \ b" using assms by (cases "x = 0") (simp_all add: pos_divide_le_eq) @@ -26,11 +27,11 @@ text \In non-trivial vector spaces, the first assumption is redundant.\ -lemma%important onorm_le: +lemma onorm_le: fixes f :: "'a::{real_normed_vector, perfect_space} \ 'b::real_normed_vector" assumes "\x. norm (f x) \ b * norm x" shows "onorm f \ b" -proof%unimportant (rule onorm_bound [OF _ assms]) +proof (rule onorm_bound [OF _ assms]) have "{0::'a} \ UNIV" by (metis not_open_singleton open_UNIV) then obtain a :: 'a where "a \ 0" by fast have "0 \ b * norm a" @@ -39,10 +40,10 @@ by (simp add: zero_le_mult_iff) qed -lemma%important le_onorm: +lemma le_onorm: assumes "bounded_linear f" shows "norm (f x) / norm x \ onorm f" -proof%unimportant - +proof - interpret f: bounded_linear f by fact obtain b where "0 \ b" and "\x. norm (f x) \ norm x * b" using f.nonneg_bounded by auto @@ -55,10 +56,10 @@ unfolding onorm_def by (rule cSUP_upper) qed -lemma%important onorm: +lemma onorm: assumes "bounded_linear f" shows "norm (f x) \ onorm f * norm x" -proof%unimportant - +proof - interpret f: bounded_linear f by fact show ?thesis proof (cases) @@ -73,12 +74,12 @@ qed qed -lemma%unimportant onorm_pos_le: +lemma onorm_pos_le: assumes f: "bounded_linear f" shows "0 \ onorm f" using le_onorm [OF f, where x=0] by simp -lemma%unimportant onorm_zero: "onorm (\x. 0) = 0" +lemma onorm_zero: "onorm (\x. 0) = 0" proof (rule order_antisym) show "onorm (\x. 0) \ 0" by (simp add: onorm_bound) @@ -86,20 +87,20 @@ using bounded_linear_zero by (rule onorm_pos_le) qed -lemma%unimportant onorm_eq_0: +lemma onorm_eq_0: assumes f: "bounded_linear f" shows "onorm f = 0 \ (\x. f x = 0)" using onorm [OF f] by (auto simp: fun_eq_iff [symmetric] onorm_zero) -lemma%unimportant onorm_pos_lt: +lemma onorm_pos_lt: assumes f: "bounded_linear f" shows "0 < onorm f \ \ (\x. f x = 0)" by (simp add: less_le onorm_pos_le [OF f] onorm_eq_0 [OF f]) -lemma%unimportant onorm_id_le: "onorm (\x. x) \ 1" +lemma onorm_id_le: "onorm (\x. x) \ 1" by (rule onorm_bound) simp_all -lemma%unimportant onorm_id: "onorm (\x. x::'a::{real_normed_vector, perfect_space}) = 1" +lemma onorm_id: "onorm (\x. x::'a::{real_normed_vector, perfect_space}) = 1" proof (rule antisym[OF onorm_id_le]) have "{0::'a} \ UNIV" by (metis not_open_singleton open_UNIV) then obtain x :: 'a where "x \ 0" by fast @@ -110,11 +111,11 @@ finally show "1 \ onorm (\x::'a. x)" . qed -lemma%important onorm_compose: +lemma onorm_compose: assumes f: "bounded_linear f" assumes g: "bounded_linear g" shows "onorm (f \ g) \ onorm f * onorm g" -proof%unimportant (rule onorm_bound) +proof (rule onorm_bound) show "0 \ onorm f * onorm g" by (intro mult_nonneg_nonneg onorm_pos_le f g) next @@ -127,7 +128,7 @@ by (simp add: mult.assoc) qed -lemma%unimportant onorm_scaleR_lemma: +lemma onorm_scaleR_lemma: assumes f: "bounded_linear f" shows "onorm (\x. r *\<^sub>R f x) \ \r\ * onorm f" proof (rule onorm_bound) @@ -141,10 +142,10 @@ by (simp only: norm_scaleR mult.assoc) qed -lemma%important onorm_scaleR: +lemma onorm_scaleR: assumes f: "bounded_linear f" shows "onorm (\x. r *\<^sub>R f x) = \r\ * onorm f" -proof%unimportant (cases "r = 0") +proof (cases "r = 0") assume "r \ 0" show ?thesis proof (rule order_antisym) @@ -160,7 +161,7 @@ qed qed (simp add: onorm_zero) -lemma%unimportant onorm_scaleR_left_lemma: +lemma onorm_scaleR_left_lemma: assumes r: "bounded_linear r" shows "onorm (\x. r x *\<^sub>R f) \ onorm r * norm f" proof (rule onorm_bound) @@ -173,10 +174,10 @@ by (simp add: ac_simps) qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le r) -lemma%important onorm_scaleR_left: +lemma onorm_scaleR_left: assumes f: "bounded_linear r" shows "onorm (\x. r x *\<^sub>R f) = onorm r * norm f" -proof%unimportant (cases "f = 0") +proof (cases "f = 0") assume "f \ 0" show ?thesis proof (rule order_antisym) @@ -200,15 +201,15 @@ qed qed (simp add: onorm_zero) -lemma%unimportant onorm_neg: +lemma onorm_neg: shows "onorm (\x. - f x) = onorm f" unfolding onorm_def by simp -lemma%important onorm_triangle: +lemma onorm_triangle: assumes f: "bounded_linear f" assumes g: "bounded_linear g" shows "onorm (\x. f x + g x) \ onorm f + onorm g" -proof%unimportant (rule onorm_bound) +proof (rule onorm_bound) show "0 \ onorm f + onorm g" by (intro add_nonneg_nonneg onorm_pos_le f g) next @@ -221,26 +222,26 @@ by (simp only: distrib_right) qed -lemma%important onorm_triangle_le: +lemma onorm_triangle_le: assumes "bounded_linear f" assumes "bounded_linear g" assumes "onorm f + onorm g \ e" shows "onorm (\x. f x + g x) \ e" - using%unimportant assms by%unimportant (rule onorm_triangle [THEN order_trans]) + using assms by (rule onorm_triangle [THEN order_trans]) -lemma%unimportant onorm_triangle_lt: +lemma onorm_triangle_lt: assumes "bounded_linear f" assumes "bounded_linear g" assumes "onorm f + onorm g < e" shows "onorm (\x. f x + g x) < e" using assms by (rule onorm_triangle [THEN order_le_less_trans]) -lemma%important onorm_sum: +lemma onorm_sum: assumes "finite S" assumes "\s. s \ S \ bounded_linear (f s)" shows "onorm (\x. sum (\s. f s x) S) \ sum (\s. onorm (f s)) S" - using%unimportant assms - by%unimportant (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum) + using assms + by (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum) lemmas onorm_sum_le = onorm_sum[THEN order_trans] diff -r dc20f278e8f3 -r bf88364c9e94 src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Fri Dec 28 10:29:59 2018 +0100 +++ b/src/HOL/Analysis/Path_Connected.thy Fri Dec 28 18:53:19 2018 +0100 @@ -2,7 +2,7 @@ Authors: LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light *) -section \Continuous Paths and Path-Connected Sets\ +section \Continuous Paths\ theory Path_Connected imports Continuous_Extension Continuum_Not_Denumerable @@ -759,7 +759,7 @@ by (simp add: path_image_join sup_commute) -section\Choosing a subpath of an existing path\ +subsection\Subpath\ definition%important subpath :: "real \ real \ (real \ 'a) \ real \ 'a::real_normed_vector" where "subpath a b g \ \x. g((b - a) * x + a)" @@ -1421,16 +1421,17 @@ by (rule_tac x="e/2" in exI) auto qed - -section \Path component\ - -text \(by Tom Hales)\ +section "Path-Connectedness" (* TODO: separate theory? *) + +subsection \Path component\ + +text \Original formalization by Tom Hales\ definition%important "path_component s x y \ (\g. path g \ path_image g \ s \ pathstart g = x \ pathfinish g = y)" abbreviation%important - "path_component_set s x \ Collect (path_component s x)" + "path_component_set s x \ Collect (path_component s x)" lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def @@ -3386,10 +3387,8 @@ qed -section\ Homotopy of maps p,q : X=>Y with property P of all intermediate maps\ - -text%important\ We often just want to require that it fixes some subset, but to take in - the case of a loop homotopy, it's convenient to have a general property P.\ +section \Homotopy of Maps\ (* TODO separate theory? *) + definition%important homotopic_with :: "[('a::topological_space \ 'b::topological_space) \ bool, 'a set, 'b set, 'a \ 'b, 'a \ 'b] \ bool" @@ -3403,7 +3402,11 @@ (\t \ {0..1}. P(\x. h(t, x))))" -text\ We often want to just localize the ending function equality or whatever.\ +text\$p, q$ are functions $X \to Y$, and the property $P$ restricts all intermediate maps. +We often just want to require that $P$ fixes some subset, but to include the case of a loop homotopy, +it is convenient to have a general property $P$.\ + +text \We often want to just localize the ending function equality or whatever.\ proposition homotopic_with: fixes X :: "'a::topological_space set" and Y :: "'b::topological_space set" assumes "\h k. (\x. x \ X \ h x = k x) \ (P h \ P k)" @@ -7463,7 +7466,7 @@ -subsection\Self-homeomorphisms shuffling points about\ +subsection%unimportant \Self-homeomorphisms shuffling points about\ subsubsection%unimportant\The theorem \homeomorphism_moving_points_exists\\ @@ -7595,7 +7598,7 @@ done qed -corollary homeomorphism_moving_point_2: +corollary%unimportant homeomorphism_moving_point_2: fixes a :: "'a::euclidean_space" assumes "affine T" "a \ T" and u: "u \ ball a r \ T" and v: "v \ ball a r \ T" obtains f g where "homeomorphism (cball a r \ T) (cball a r \ T) f g" @@ -7623,7 +7626,7 @@ qed -corollary homeomorphism_moving_point_3: +corollary%unimportant homeomorphism_moving_point_3: fixes a :: "'a::euclidean_space" assumes "affine T" "a \ T" and ST: "ball a r \ T \ S" "S \ T" and u: "u \ ball a r \ T" and v: "v \ ball a r \ T" @@ -7701,7 +7704,7 @@ qed -proposition homeomorphism_moving_point: +proposition%unimportant homeomorphism_moving_point: fixes a :: "'a::euclidean_space" assumes ope: "openin (subtopology euclidean (affine hull S)) S" and "S \ T" @@ -7857,7 +7860,7 @@ qed qed -proposition homeomorphism_moving_points_exists: +proposition%unimportant homeomorphism_moving_points_exists: fixes S :: "'a::euclidean_space set" assumes 2: "2 \ DIM('a)" "open S" "connected S" "S \ T" "finite K" and KS: "\i. i \ K \ x i \ S \ y i \ S" @@ -8123,7 +8126,7 @@ qed qed -proposition homeomorphism_grouping_points_exists: +proposition%unimportant homeomorphism_grouping_points_exists: fixes S :: "'a::euclidean_space set" assumes "open U" "open S" "connected S" "U \ {}" "finite K" "K \ S" "U \ S" "S \ T" obtains f g where "homeomorphism T T f g" "{x. (\ (f x = x \ g x = x))} \ S" @@ -8202,7 +8205,7 @@ qed -proposition homeomorphism_grouping_points_exists_gen: +proposition%unimportant homeomorphism_grouping_points_exists_gen: fixes S :: "'a::euclidean_space set" assumes opeU: "openin (subtopology euclidean S) U" and opeS: "openin (subtopology euclidean (affine hull S)) S" diff -r dc20f278e8f3 -r bf88364c9e94 src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Fri Dec 28 10:29:59 2018 +0100 +++ b/src/HOL/Analysis/Starlike.thy Fri Dec 28 18:53:19 2018 +0100 @@ -6,10 +6,10 @@ Author: Johannes Hoelzl, TU Muenchen *) -section \Line segments, Starlike Sets, etc\ +section \Line Segments\ theory Starlike - imports Convex_Euclidean_Space +imports Convex_Euclidean_Space begin subsection \Midpoint\ diff -r dc20f278e8f3 -r bf88364c9e94 src/HOL/Analysis/document/root.tex --- a/src/HOL/Analysis/document/root.tex Fri Dec 28 10:29:59 2018 +0100 +++ b/src/HOL/Analysis/document/root.tex Fri Dec 28 18:53:19 2018 +0100 @@ -31,4 +31,9 @@ \parindent 0pt\parskip 0.5ex \input{session} +\pagestyle{headings} +\bibliographystyle{abbrv} +\bibliography{root} +\nocite{dummy} + \end{document} diff -r dc20f278e8f3 -r bf88364c9e94 src/HOL/ROOT --- a/src/HOL/ROOT Fri Dec 28 10:29:59 2018 +0100 +++ b/src/HOL/ROOT Fri Dec 28 18:53:19 2018 +0100 @@ -69,6 +69,7 @@ Analysis document_files "root.tex" + "root.bib" session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" + theories