# HG changeset patch # User paulson # Date 1474555487 -3600 # Node ID f6ce08859d4c015a71dae3e5ba4e59f629960d27 # Parent d81fb5b46a5c01c2eb35a8524a0229f1c9c3c565 More mainly topological results diff -r d81fb5b46a5c -r f6ce08859d4c src/HOL/Analysis/Bounded_Linear_Function.thy --- a/src/HOL/Analysis/Bounded_Linear_Function.thy Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Thu Sep 22 15:44:47 2016 +0100 @@ -391,7 +391,7 @@ also have "\ = (\i\Basis. (x \ i * (f i \ b)))" using b by (simp add: setsum.delta) also have "\ = f x \ b" - by (subst linear_componentwise[symmetric]) (unfold_locales, rule) + by (metis (mono_tags, lifting) Linear_Algebra.linear_componentwise linear_axioms) finally show "(\j\Basis. \i\Basis. (x \ i * (f i \ j)) *\<^sub>R j) \ b = f x \ b" . qed diff -r d81fb5b46a5c -r f6ce08859d4c src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Sep 22 15:44:47 2016 +0100 @@ -1,7 +1,7 @@ section \Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\ theory Cartesian_Euclidean_Space -imports Finite_Cartesian_Product Derivative (* Henstock_Kurzweil_Integration *) +imports Finite_Cartesian_Product Derivative begin lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}" @@ -11,6 +11,7 @@ "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by simp +(*move up?*) lemma setsum_UNIV_sum: fixes g :: "'a::finite + 'b::finite \ _" shows "(\x\UNIV. g x) = (\x\UNIV. g (Inl x)) + (\x\UNIV. g (Inr x))" @@ -33,7 +34,6 @@ qed simp qed simp - subsection\Basic componentwise operations on vectors.\ instantiation vec :: (times, finite) times @@ -598,7 +598,7 @@ lemma basis_expansion: "setsum (\i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)" by (auto simp add: axis_def vec_eq_iff if_distrib setsum.If_cases cong del: if_weak_cong) -lemma linear_componentwise: +lemma linear_componentwise_expansion: fixes f:: "real ^'m \ real ^ _" assumes lf: "linear f" shows "(f x)$j = setsum (\i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") @@ -636,9 +636,7 @@ assumes lf: "linear f" shows "matrix f *v x = f (x::real ^ 'n)" apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute) - apply clarify - apply (rule linear_componentwise[OF lf, symmetric]) - done + by (simp add: linear_componentwise_expansion lf) lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::real ^ 'n))" by (simp add: ext matrix_works) diff -r d81fb5b46a5c -r f6ce08859d4c src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Sep 22 15:44:47 2016 +0100 @@ -2163,7 +2163,7 @@ { fix x y z n assume At: "At x y z n" then have contf': "continuous_on (convex hull {x,y,z}) f" - using contf At_def continuous_on_subset by blast + using contf At_def continuous_on_subset by metis have "\x' y' z'. At x' y' z' (Suc n) \ convex hull {x',y',z'} \ convex hull {x,y,z}" using At apply (simp add: At_def) @@ -3213,11 +3213,6 @@ using contour_integral_nearby [OF assms, where atends=False] unfolding linked_paths_def by simp_all -corollary differentiable_polynomial_function: - fixes p :: "real \ 'a::euclidean_space" - shows "polynomial_function p \ p differentiable_on s" -by (meson has_vector_derivative_polynomial_function differentiable_at_imp_differentiable_on differentiable_def has_vector_derivative_def) - lemma C1_differentiable_polynomial_function: fixes p :: "real \ 'a::euclidean_space" shows "polynomial_function p \ p C1_differentiable_on s" @@ -3255,7 +3250,7 @@ done then obtain p' where p': "polynomial_function p'" "\x. (p has_vector_derivative (p' x)) (at x)" - using has_vector_derivative_polynomial_function by force + by (blast intro: has_vector_derivative_polynomial_function that elim: ) then have "bounded(p' ` {0..1})" using continuous_on_polymonial_function by (force simp: intro!: compact_imp_bounded compact_continuous_image) diff -r d81fb5b46a5c -r f6ce08859d4c src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Sep 22 15:44:47 2016 +0100 @@ -1,5 +1,5 @@ -(* Title: HOL/Analysis/Convex_Euclidean_Space.thy - Authors: Robert Himmelmann, TU Muenchen; Bogdan Grechuk, University of Edinburgh; LCP +(* Author: L C Paulson, University of Cambridge + Authors: Robert Himmelmann, TU Muenchen; Bogdan Grechuk, University of Edinburgh *) section \Convex sets, functions and related things\ @@ -219,7 +219,7 @@ from gxy have th0: "g (x - y) = 0" by (simp add: linear_diff[OF g(1)]) have th1: "x - y \ span B" using x' y' - by (metis span_sub) + by (metis span_diff) have "x = y" using g0[OF th1 th0] by simp } then have giS: "inj_on g S" unfolding inj_on_def by blast @@ -2267,7 +2267,7 @@ apply (rule subset_le_dim) unfolding subset_eq using \a\s\ - apply (auto simp add:span_superset span_sub) + apply (auto simp add:span_superset span_diff) done also have "\ < dim s + 1" by auto also have "\ \ card (s - {a})" diff -r d81fb5b46a5c -r f6ce08859d4c src/HOL/Analysis/Derivative.thy --- a/src/HOL/Analysis/Derivative.thy Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Analysis/Derivative.thy Thu Sep 22 15:44:47 2016 +0100 @@ -9,29 +9,7 @@ imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function begin -lemma bounded_linear_component [intro]: "bounded_linear (\x::'a::euclidean_space. x \ k)" - by (rule bounded_linear_inner_left) - -lemma onorm_inner_left: - assumes "bounded_linear r" - shows "onorm (\x. r x \ f) \ onorm r * norm f" -proof (rule onorm_bound) - fix x - have "norm (r x \ f) \ norm (r x) * norm f" - by (simp add: Cauchy_Schwarz_ineq2) - also have "\ \ onorm r * norm x * norm f" - by (intro mult_right_mono onorm assms norm_ge_zero) - finally show "norm (r x \ f) \ onorm r * norm f * norm x" - by (simp add: ac_simps) -qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le assms) - -lemma onorm_inner_right: - assumes "bounded_linear r" - shows "onorm (\x. f \ r x) \ norm f * onorm r" - apply (subst inner_commute) - apply (rule onorm_inner_left[OF assms, THEN order_trans]) - apply simp - done +declare bounded_linear_inner_left [intro] declare has_derivative_bounded_linear[dest] diff -r d81fb5b46a5c -r f6ce08859d4c src/HOL/Analysis/Euclidean_Space.thy --- a/src/HOL/Analysis/Euclidean_Space.thy Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Analysis/Euclidean_Space.thy Thu Sep 22 15:44:47 2016 +0100 @@ -105,10 +105,10 @@ apply (blast intro: assms) done -lemma DIM_positive: "0 < DIM('a::euclidean_space)" +lemma DIM_positive [simp]: "0 < DIM('a::euclidean_space)" by (simp add: card_gt_0_iff) -lemma DIM_ge_Suc0 [iff]: "Suc 0 \ card Basis" +lemma DIM_ge_Suc0 [simp]: "Suc 0 \ card Basis" by (meson DIM_positive Suc_leI) diff -r d81fb5b46a5c -r f6ce08859d4c src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Sep 22 15:44:47 2016 +0100 @@ -2902,7 +2902,7 @@ fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes "f integrable_on s" shows "integral s (\x. f x \ k) = integral s f \ k" - unfolding integral_linear[OF assms(1) bounded_linear_component,unfolded o_def] .. + unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] .. lemma has_integral_setsum: assumes "finite t" @@ -3090,7 +3090,7 @@ shows "(f has_integral y) A \ (\b\Basis. ((\x. f x \ b) has_integral (y \ b)) A)" proof safe fix b :: 'b assume "(f has_integral y) A" - from has_integral_linear[OF this(1) bounded_linear_component, of b] + from has_integral_linear[OF this(1) bounded_linear_inner_left, of b] show "((\x. f x \ b) has_integral (y \ b)) A" by (simp add: o_def) next assume "(\b\Basis. ((\x. f x \ b) has_integral (y \ b)) A)" @@ -3148,7 +3148,7 @@ lemma integrable_component: "f integrable_on A \ (\x. f x \ (y :: 'b :: euclidean_space)) integrable_on A" - by (drule integrable_linear[OF _ bounded_linear_component[of y]]) (simp add: o_def) + by (drule integrable_linear[OF _ bounded_linear_inner_left[of y]]) (simp add: o_def) diff -r d81fb5b46a5c -r f6ce08859d4c src/HOL/Analysis/L2_Norm.thy --- a/src/HOL/Analysis/L2_Norm.thy Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Analysis/L2_Norm.thy Thu Sep 22 15:44:47 2016 +0100 @@ -165,12 +165,7 @@ done lemma member_le_setL2: "\finite A; i \ A\ \ f i \ setL2 f A" - apply (rule_tac s="insert i (A - {i})" and t="A" in subst) - apply fast - apply (subst setL2_insert) - apply simp - apply simp - apply simp - done + unfolding setL2_def + by (auto intro!: member_le_setsum real_le_rsqrt) end diff -r d81fb5b46a5c -r f6ce08859d4c src/HOL/Analysis/Linear_Algebra.thy --- a/src/HOL/Analysis/Linear_Algebra.thy Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Analysis/Linear_Algebra.thy Thu Sep 22 15:44:47 2016 +0100 @@ -457,7 +457,7 @@ lemma span_neg: "x \ span S \ - x \ span S" by (metis subspace_neg subspace_span) -lemma span_sub: "x \ span S \ y \ span S \ x - y \ span S" +lemma span_diff: "x \ span S \ y \ span S \ x - y \ span S" by (metis subspace_span subspace_diff) lemma (in real_vector) span_setsum: "(\x. x \ A \ f x \ span S) \ setsum f A \ span S" @@ -2615,7 +2615,7 @@ from gxy have th0: "g (x - y) = 0" by (simp add: linear_diff[OF g(1)]) have th1: "x - y \ span B" - using x' y' by (metis span_sub) + using x' y' by (metis span_diff) have "x = y" using g0[OF th1 th0] by simp } diff -r d81fb5b46a5c -r f6ce08859d4c src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Sep 21 16:59:51 2016 +0100 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Sep 22 15:44:47 2016 +0100 @@ -1,4 +1,4 @@ -(* title: HOL/Library/Topology_Euclidian_Space.thy +(* Author: L C Paulson, University of Cambridge Author: Amine Chaieb, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Brian Huffman, Portland State University @@ -4040,6 +4040,11 @@ by auto qed +corollary infinite_openin: + fixes S :: "'a :: t1_space set" + shows "\openin (subtopology euclidean U) S; x \ S; x islimpt U\ \ infinite S" + by (clarsimp simp add: openin_open islimpt_eq_acc_point inf_commute) + lemma islimpt_range_imp_convergent_subsequence: fixes l :: "'a :: {t1_space, first_countable_topology}" assumes l: "l islimpt (range f)" @@ -6906,7 +6911,7 @@ show "\e>0. \y. dist y (f x) < e \ y \ f ` A" proof (intro exI conjI) show "\ > 0" - using \e > 0\ \B > 0\ by (simp add: \_def divide_simps) (simp add: mult_less_0_iff) + using \e > 0\ \B > 0\ by (simp add: \_def divide_simps) have "y \ f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y proof - define u where "u \ y - f x" @@ -9712,6 +9717,126 @@ apply (simp add: convergent_imp_bounded) by (simp add: closed_limpt islimpt_insert sequence_unique_limpt) + +subsection\Componentwise limits and continuity\ + +text\But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\ +lemma Euclidean_dist_upper: "i \ Basis \ dist (x \ i) (y \ i) \ dist x y" + by (metis (no_types) member_le_setL2 euclidean_dist_l2 finite_Basis) + +text\But is the premise @{term \i \ Basis\} really necessary?\ +lemma open_preimage_inner: + assumes "open S" "i \ Basis" + shows "open {x. x \ i \ S}" +proof (rule openI, simp) + fix x + assume x: "x \ i \ S" + with assms obtain e where "0 < e" and e: "ball (x \ i) e \ S" + by (auto simp: open_contains_ball_eq) + have "\e>0. ball (y \ i) e \ S" if dxy: "dist x y < e / 2" for y + proof (intro exI conjI) + have "dist (x \ i) (y \ i) < e / 2" + by (meson \i \ Basis\ dual_order.trans Euclidean_dist_upper not_le that) + then have "dist (x \ i) z < e" if "dist (y \ i) z < e / 2" for z + by (metis dist_commute dist_triangle_half_l that) + then have "ball (y \ i) (e / 2) \ ball (x \ i) e" + using mem_ball by blast + with e show "ball (y \ i) (e / 2) \ S" + by (metis order_trans) + qed (simp add: \0 < e\) + then show "\e>0. ball x e \ {s. s \ i \ S}" + by (metis (no_types, lifting) \0 < e\ \open S\ half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI) +qed + +proposition tendsto_componentwise_iff: + fixes f :: "_ \ 'b::euclidean_space" + shows "(f \ l) F \ (\i \ Basis. ((\x. (f x \ i)) \ (l \ i)) F)" + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + unfolding tendsto_def + apply clarify + apply (drule_tac x="{s. s \ i \ S}" in spec) + apply (auto simp: open_preimage_inner) + done +next + assume R: ?rhs + then have "\e. e > 0 \ \i\Basis. \\<^sub>F x in F. dist (f x \ i) (l \ i) < e" + unfolding tendsto_iff by blast + then have R': "\e. e > 0 \ \\<^sub>F x in F. \i\Basis. dist (f x \ i) (l \ i) < e" + by (simp add: eventually_ball_finite_distrib [symmetric]) + show ?lhs + unfolding tendsto_iff + proof clarify + fix e::real + assume "0 < e" + have *: "setL2 (\i. dist (f x \ i) (l \ i)) Basis < e" + if "\i\Basis. dist (f x \ i) (l \ i) < e / real DIM('b)" for x + proof - + have "setL2 (\i. dist (f x \ i) (l \ i)) Basis \ setsum (\i. dist (f x \ i) (l \ i)) Basis" + by (simp add: setL2_le_setsum) + also have "... < DIM('b) * (e / real DIM('b))" + apply (rule setsum_bounded_above_strict) + using that by auto + also have "... = e" + by (simp add: field_simps) + finally show "setL2 (\i. dist (f x \ i) (l \ i)) Basis < e" . + qed + have "\\<^sub>F x in F. \i\Basis. dist (f x \ i) (l \ i) < e / DIM('b)" + apply (rule R') + using \0 < e\ by simp + then show "\\<^sub>F x in F. dist (f x) l < e" + apply (rule eventually_mono) + apply (subst euclidean_dist_l2) + using * by blast + qed +qed + + +corollary continuous_componentwise: + "continuous F f \ (\i \ Basis. continuous F (\x. (f x \ i)))" +by (simp add: continuous_def tendsto_componentwise_iff [symmetric]) + +corollary continuous_on_componentwise: + fixes S :: "'a :: t2_space set" + shows "continuous_on S f \ (\i \ Basis. continuous_on S (\x. (f x \ i)))" + apply (simp add: continuous_on_eq_continuous_within) + using continuous_componentwise by blast + +lemma linear_componentwise_iff: + "(linear f') \ (\i\Basis. linear (\x. f' x \ i))" + apply (auto simp: linear_iff inner_left_distrib) + apply (metis inner_left_distrib euclidean_eq_iff) + by (metis euclidean_eqI inner_scaleR_left) + +lemma bounded_linear_componentwise_iff: + "(bounded_linear f') \ (\i\Basis. bounded_linear (\x. f' x \ i))" + (is "?lhs = ?rhs") +proof + assume ?lhs then show ?rhs + by (simp add: bounded_linear_inner_left_comp) +next + assume ?rhs + then have "(\i\Basis. \K. \x. \f' x \ i\ \ norm x * K)" "linear f'" + by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_componentwise_iff [symmetric] ball_conj_distrib) + then obtain F where F: "\i x. i \ Basis \ \f' x \ i\ \ norm x * F i" + by metis + have "norm (f' x) \ norm x * setsum F Basis" for x + proof - + have "norm (f' x) \ (\i\Basis. \f' x \ i\)" + by (rule norm_le_l1) + also have "... \ (\i\Basis. norm x * F i)" + by (metis F setsum_mono) + also have "... = norm x * setsum F Basis" + by (simp add: setsum_distrib_left) + finally show ?thesis . + qed + then show ?lhs + by (force simp: bounded_linear_def bounded_linear_axioms_def \linear f'\) +qed + + no_notation eucl_less (infix "By L C Paulson (2015)\ theory Weierstrass_Theorems -imports Uniform_Limit Path_Connected +imports Uniform_Limit Path_Connected Derivative begin subsection \Bernstein polynomials\ @@ -171,13 +171,13 @@ DOI: 10.2307/2043993 http://www.jstor.org/stable/2043993\ locale function_ring_on = - fixes R :: "('a::t2_space \ real) set" and s :: "'a set" - assumes compact: "compact s" - assumes continuous: "f \ R \ continuous_on s f" + fixes R :: "('a::t2_space \ real) set" and S :: "'a set" + assumes compact: "compact S" + assumes continuous: "f \ R \ continuous_on S f" assumes add: "f \ R \ g \ R \ (\x. f x + g x) \ R" assumes mult: "f \ R \ g \ R \ (\x. f x * g x) \ R" assumes const: "(\_. c) \ R" - assumes separable: "x \ s \ y \ s \ x \ y \ \f\R. f x \ f y" + assumes separable: "x \ S \ y \ S \ x \ y \ \f\R. f x \ f y" begin lemma minus: "f \ R \ (\x. - f x) \ R" @@ -196,24 +196,24 @@ by (induct I rule: finite_induct; simp add: const mult) definition normf :: "('a::t2_space \ real) \ real" - where "normf f \ SUP x:s. \f x\" + where "normf f \ SUP x:S. \f x\" - lemma normf_upper: "\continuous_on s f; x \ s\ \ \f x\ \ normf f" + lemma normf_upper: "\continuous_on S f; x \ S\ \ \f x\ \ normf f" apply (simp add: normf_def) apply (rule cSUP_upper, assumption) by (simp add: bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs) - lemma normf_least: "s \ {} \ (\x. x \ s \ \f x\ \ M) \ normf f \ M" + lemma normf_least: "S \ {} \ (\x. x \ S \ \f x\ \ M) \ normf f \ M" by (simp add: normf_def cSUP_least) end lemma (in function_ring_on) one: - assumes U: "open U" and t0: "t0 \ s" "t0 \ U" and t1: "t1 \ s-U" - shows "\V. open V \ t0 \ V \ s \ V \ U \ - (\e>0. \f \ R. f ` s \ {0..1} \ (\t \ s \ V. f t < e) \ (\t \ s - U. f t > 1 - e))" + assumes U: "open U" and t0: "t0 \ S" "t0 \ U" and t1: "t1 \ S-U" + shows "\V. open V \ t0 \ V \ S \ V \ U \ + (\e>0. \f \ R. f ` S \ {0..1} \ (\t \