# HG changeset patch # User huffman # Date 1244589198 25200 # Node ID e7a282113145921fcc1e94bb3d4f26180ff87807 # Parent 16068eb224c0b0ebb8ed77be9e52d4071b4b419f remove uses of vec1 in continuity lemmas diff -r 16068eb224c0 -r e7a282113145 src/HOL/Library/Convex_Euclidean_Space.thy --- a/src/HOL/Library/Convex_Euclidean_Space.thy Tue Jun 09 11:12:08 2009 -0700 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy Tue Jun 09 16:13:18 2009 -0700 @@ -1213,9 +1213,22 @@ qed qed +lemma open_dest_vec1_vimage: "open S \ open (dest_vec1 -` S)" +unfolding open_vector_def all_1 +by (auto simp add: dest_vec1_def) + +lemma tendsto_dest_vec1: "(f ---> l) net \ ((\x. dest_vec1 (f x)) ---> dest_vec1 l) net" + unfolding tendsto_def + apply clarify + apply (drule_tac x="dest_vec1 -` S" in spec) + apply (simp add: open_dest_vec1_vimage) + done + +lemma continuous_dest_vec1: "continuous net f \ continuous net (\x. dest_vec1 (f x))" + unfolding continuous_def by (rule tendsto_dest_vec1) lemma compact_convex_combinations: - fixes s t :: "(real ^ _) set" + fixes s t :: "(real ^ 'n::finite) set" assumes "compact s" "compact t" shows "compact { (1 - u) *s x + u *s y | x y u. 0 \ u \ u \ 1 \ x \ s \ y \ t}" proof- @@ -1229,9 +1242,10 @@ hence "continuous (at (pastecart u (pastecart x y))) (\z. fstcart (sndcart z) - dest_vec1 (fstcart z) *s fstcart (sndcart z) + dest_vec1 (fstcart z) *s sndcart (sndcart z))" - apply (auto intro!: continuous_add continuous_sub continuous_mul simp add: o_def vec1_dest_vec1) + apply (auto intro!: continuous_add continuous_sub continuous_mul continuous_dest_vec1 + simp add: o_def vec1_dest_vec1) using linear_continuous_at linear_fstcart linear_sndcart linear_sndcart - using linear_compose[unfolded o_def] by auto } + using linear_compose[unfolded o_def] by auto } hence "continuous_on {pastecart u w |u w. u \ {vec1 0..vec1 1} \ w \ {pastecart x y |x y. x \ s \ y \ t}} (\z. (1 - dest_vec1 (fstcart z)) *s fstcart (sndcart z) + dest_vec1 (fstcart z) *s sndcart (sndcart z))" apply(rule_tac continuous_at_imp_continuous_on) unfolding mem_Collect_eq @@ -1888,7 +1902,9 @@ unfolding image_image[of "\u. u *s x" "\x. dest_vec1 x", THEN sym] unfolding dest_vec1_inverval vec1_dest_vec1 by auto have "compact ?A" unfolding A apply(rule compact_continuous_image, rule continuous_at_imp_continuous_on) - apply(rule, rule continuous_vmul) unfolding o_def vec1_dest_vec1 apply(rule continuous_at_id) by(rule compact_interval) + apply(rule, rule continuous_vmul) + apply (rule continuous_dest_vec1) + apply(rule continuous_at_id) by(rule compact_interval) moreover have "{y. \u\0. u \ b / norm x \ y = u *s x} \ s \ {}" apply(rule not_disjointI[OF _ assms(2)]) unfolding mem_Collect_eq using `b>0` assms(3) by(auto intro!: divide_nonneg_pos) ultimately obtain u y where obt: "u\0" "u \ b / norm x" "y = u *s x" @@ -1925,12 +1941,13 @@ have injpi:"\x y. pi x = pi y \ norm x = norm y \ x = y" unfolding pi_def by auto have contpi:"continuous_on (UNIV - {0}) pi" apply(rule continuous_at_imp_continuous_on) - apply rule unfolding pi_def apply(rule continuous_mul) unfolding o_def - apply(rule continuous_at_inv[unfolded o_def]) unfolding continuous_at_vec1_range[unfolded o_def] - apply(rule,rule) apply(rule_tac x=e in exI) apply(rule,assumption,rule,rule) - proof- fix e x y assume "0 < e" "norm (y - x::real^'n) < e" - thus "\norm y - norm x\ < e" using norm_triangle_ineq3[of y x] by auto - qed(auto intro!:continuous_at_id) + apply rule unfolding pi_def + apply (rule continuous_mul) + apply (rule continuous_at_inv[unfolded o_def]) + apply (rule continuous_at_norm) + apply simp + apply (rule continuous_at_id) + done def sphere \ "{x::real^'n. norm x = 1}" have pi:"\x. x \ 0 \ pi x \ sphere" "\x u. u>0 \ pi (u *s x) = pi x" unfolding pi_def sphere_def by auto @@ -2015,7 +2032,7 @@ prefer 4 apply(rule continuous_at_imp_continuous_on, rule) apply(rule_tac [3] hom2) proof- fix x::"real^'n" assume as:"x \ cball 0 1" thus "continuous (at x) (\x. norm x *s surf (pi x))" proof(cases "x=0") - case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_vec1_norm) + case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_norm) using cont_surfpi unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def by auto next guess a using UNIV_witness[where 'a = 'n] .. obtain B where B:"\x\s. norm x \ B" using compact_imp_bounded[OF assms(1)] unfolding bounded_iff by auto @@ -2332,8 +2349,8 @@ lemma convex_on_bounded_continuous: assumes "open s" "convex_on s f" "\x\s. abs(f x) \ b" - shows "continuous_on s (vec1 o f)" - apply(rule continuous_at_imp_continuous_on) unfolding continuous_at_vec1_range proof(rule,rule,rule) + shows "continuous_on s f" + apply(rule continuous_at_imp_continuous_on) unfolding continuous_at_real_range proof(rule,rule,rule) fix x e assume "x\s" "(0::real) < e" def B \ "abs b + 1" have B:"0 < B" "\x. x\s \ abs (f x) \ B" @@ -2398,7 +2415,7 @@ lemma convex_on_continuous: assumes "open (s::(real^'n::finite) set)" "convex_on s f" - shows "continuous_on s (vec1 \ f)" + shows "continuous_on s f" unfolding continuous_on_eq_continuous_at[OF assms(1)] proof note dimge1 = dimindex_ge_1[where 'a='n] fix x assume "x\s" @@ -2428,9 +2445,9 @@ using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by(auto simp add: vector_component) } thus "f y \ k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm by(auto simp add: vector_component_simps) qed - hence "continuous_on (ball x d) (vec1 \ f)" apply(rule_tac convex_on_bounded_continuous) + hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous) apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) by auto - thus "continuous (at x) (vec1 \ f)" unfolding continuous_on_eq_continuous_at[OF open_ball] using `d>0` by auto qed + thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball] using `d>0` by auto qed subsection {* Line segments, starlike sets etc. *) (* Use the same overloading tricks as for intervals, so that *) @@ -2975,7 +2992,8 @@ unfolding pathfinish_def linepath_def by auto lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)" - unfolding linepath_def by(auto simp add: vec1_dest_vec1 o_def intro!: continuous_intros) + unfolding linepath_def + by (intro continuous_intros continuous_dest_vec1) lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)" using continuous_linepath_at by(auto intro!: continuous_at_imp_continuous_on) @@ -3202,9 +3220,9 @@ have ***:"\xa. (if xa = 0 then 0 else 1) \ 1 \ xa = 0" apply(rule ccontr) by auto have **:"{x::real^'n. norm x = 1} = (\x. (1/norm x) *s x) ` (UNIV - {0})" apply(rule set_ext,rule) unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq norm_mul by(auto intro!: ***) - have "continuous_on (UNIV - {0}) (vec1 \ (\x::real^'n. 1 / norm x))" unfolding o_def continuous_on_eq_continuous_within + have "continuous_on (UNIV - {0}) (\x::real^'n. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within) - apply(rule continuous_at_vec1_norm[unfolded o_def]) by auto + apply(rule continuous_at_norm[unfolded o_def]) by auto thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms] by(auto intro!: path_connected_continuous_image continuous_on_intros continuous_on_mul) qed diff -r 16068eb224c0 -r e7a282113145 src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Tue Jun 09 11:12:08 2009 -0700 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Tue Jun 09 16:13:18 2009 -0700 @@ -1245,6 +1245,9 @@ unfolding linear_conv_bounded_linear by (rule bounded_linear.tendsto) +lemma Lim_ident_at: "((\x. x) ---> a) (at a)" + unfolding tendsto_def Limits.eventually_at_topological by fast + lemma Lim_const: "((\x. a) ---> a) net" by (rule tendsto_const) @@ -1271,44 +1274,73 @@ shows "(f ---> l) net \ (g ---> m) net \ ((\x. f(x) - g(x)) ---> l - m) net" by (rule tendsto_diff) +lemma dist_triangle3: (* TODO: move *) + fixes x y :: "'a::metric_space" + shows "dist x y \ dist a x + dist a y" +using dist_triangle2 [of x y a] +by (simp add: dist_commute) + +lemma tendsto_dist: (* TODO: move *) + assumes f: "(f ---> l) net" and g: "(g ---> m) net" + shows "((\x. dist (f x) (g x)) ---> dist l m) net" +proof (rule tendstoI) + fix e :: real assume "0 < e" + hence e2: "0 < e/2" by simp + from tendstoD [OF f e2] tendstoD [OF g e2] + show "eventually (\x. dist (dist (f x) (g x)) (dist l m) < e) net" + proof (rule eventually_elim2) + fix x assume x: "dist (f x) l < e/2" "dist (g x) m < e/2" + have "dist (f x) (g x) - dist l m \ dist (f x) l + dist (g x) m" + using dist_triangle2 [of "f x" "g x" "l"] + using dist_triangle2 [of "g x" "l" "m"] + by arith + moreover + have "dist l m - dist (f x) (g x) \ dist (f x) l + dist (g x) m" + using dist_triangle3 [of "l" "m" "f x"] + using dist_triangle [of "f x" "m" "g x"] + by arith + ultimately + have "dist (dist (f x) (g x)) (dist l m) \ dist (f x) l + dist (g x) m" + unfolding dist_norm real_norm_def by arith + with x show "dist (dist (f x) (g x)) (dist l m) < e" + by arith + qed +qed + lemma Lim_null: fixes f :: "'a \ 'b::real_normed_vector" shows "(f ---> l) net \ ((\x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm) lemma Lim_null_norm: fixes f :: "'a \ 'b::real_normed_vector" - shows "(f ---> 0) net \ ((\x. vec1(norm(f x))) ---> 0) net" - by (simp add: Lim dist_norm norm_vec1) + shows "(f ---> 0) net \ ((\x. norm(f x)) ---> 0) net" + by (simp add: Lim dist_norm) lemma Lim_null_comparison: fixes f :: "'a \ 'b::real_normed_vector" - assumes "eventually (\x. norm(f x) <= g x) net" "((\x. vec1(g x)) ---> 0) net" + assumes "eventually (\x. norm (f x) \ g x) net" "(g ---> 0) net" shows "(f ---> 0) net" proof(simp add: tendsto_iff, rule+) fix e::real assume "0 g x" "dist (vec1 (g x)) 0 < e" - hence "dist (f x) 0 < e" unfolding vec_def using dist_vec1[of "g x" "0"] - by (vector dist_norm norm_vec1 real_vector_norm_def dot_def vec1_def) + assume "norm (f x) \ g x" "dist (g x) 0 < e" + hence "dist (f x) 0 < e" by (simp add: dist_norm) } thus "eventually (\x. dist (f x) 0 < e) net" - using eventually_and[of "\x. norm(f x) <= g x" "\x. dist (vec1 (g x)) 0 < e" net] - using eventually_mono[of "(\x. norm (f x) \ g x \ dist (vec1 (g x)) 0 < e)" "(\x. dist (f x) 0 < e)" net] + using eventually_and[of "\x. norm(f x) <= g x" "\x. dist (g x) 0 < e" net] + using eventually_mono[of "(\x. norm (f x) \ g x \ dist (g x) 0 < e)" "(\x. dist (f x) 0 < e)" net] using assms `e>0` unfolding tendsto_iff by auto qed -lemma Lim_component: "(f ---> l) net - ==> ((\a. vec1((f a :: real ^'n::finite)$i)) ---> vec1(l$i)) net" +lemma Lim_component: + fixes f :: "'a \ 'b::metric_space ^ 'n::finite" + shows "(f ---> l) net \ ((\a. f a $i) ---> l$i) net" unfolding tendsto_iff - apply (simp add: dist_norm vec1_sub[symmetric] norm_vec1 vector_minus_component[symmetric] del: vector_minus_component) - apply (auto simp del: vector_minus_component) - apply (erule_tac x=e in allE) - apply clarify - apply (erule eventually_rev_mono) - apply (auto simp del: vector_minus_component) - apply (rule order_le_less_trans) - apply (rule component_le_norm) - by auto + apply (clarify) + apply (drule spec, drule (1) mp) + apply (erule eventually_elim1) + apply (erule le_less_trans [OF dist_nth_le]) + done lemma Lim_transform_bound: fixes f :: "'a \ 'b::real_normed_vector" @@ -1504,12 +1536,6 @@ netlimit :: "'a::metric_space net \ 'a" where "netlimit net = (SOME a. \r>0. eventually (\x. dist x a < r) net)" -lemma dist_triangle3: - fixes x y :: "'a::metric_space" - shows "dist x y \ dist a x + dist a y" -using dist_triangle2 [of x y a] -by (simp add: dist_commute) - lemma netlimit_within: assumes "\ trivial_limit (at a within S)" shows "netlimit (at a within S) = a" @@ -1694,14 +1720,14 @@ apply (subgoal_tac "\N k (n::nat). N + k <= n ==> N <= n - k \ (n - k) + k = n") by metis arith -lemma seq_harmonic: "((\n. vec1(inverse (real n))) ---> 0) sequentially" +lemma seq_harmonic: "((\n. inverse (real n)) ---> 0) sequentially" proof- { fix e::real assume "e>0" hence "\N::nat. \n::nat\N. inverse (real n) < e" using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI) - by (metis dlo_simps(4) le_imp_inverse_le linorder_not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7)) + by (metis not_le le_imp_inverse_le not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7)) } - thus ?thesis unfolding Lim_sequentially dist_norm apply simp unfolding norm_vec1 by auto + thus ?thesis unfolding Lim_sequentially dist_norm by simp qed text{* More properties of closed balls. *} @@ -2123,26 +2149,26 @@ text{* Some theorems on sups and infs using the notion "bounded". *} -lemma bounded_vec1: +lemma bounded_real: fixes S :: "real set" - shows "bounded(vec1 ` S) \ (\a. \x\S. abs x <= a)" - by (simp add: bounded_iff forall_vec1 norm_vec1 vec1_in_image_vec1) - -lemma bounded_has_rsup: assumes "bounded(vec1 ` S)" "S \ {}" + shows "bounded S \ (\a. \x\S. abs x <= a)" + by (simp add: bounded_iff) + +lemma bounded_has_rsup: assumes "bounded S" "S \ {}" shows "\x\S. x <= rsup S" and "\b. (\x\S. x <= b) \ rsup S <= b" proof fix x assume "x\S" - from assms(1) obtain a where a:"\x\S. \x\ \ a" unfolding bounded_vec1 by auto + from assms(1) obtain a where a:"\x\S. \x\ \ a" unfolding bounded_real by auto hence *:"S *<= a" using setleI[of S a] by (metis abs_le_interval_iff mem_def) - thus "x \ rsup S" using rsup[OF `S\{}`] using assms(1)[unfolded bounded_vec1] using isLubD2[of UNIV S "rsup S" x] using `x\S` by auto + thus "x \ rsup S" using rsup[OF `S\{}`] using assms(1)[unfolded bounded_real] using isLubD2[of UNIV S "rsup S" x] using `x\S` by auto next show "\b. (\x\S. x \ b) \ rsup S \ b" using assms using rsup[of S, unfolded isLub_def isUb_def leastP_def setle_def setge_def] - apply (auto simp add: bounded_vec1) + apply (auto simp add: bounded_real) by (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def) qed -lemma rsup_insert: assumes "bounded (vec1 ` S)" +lemma rsup_insert: assumes "bounded S" shows "rsup(insert x S) = (if S = {} then x else max x (rsup S))" proof(cases "S={}") case True thus ?thesis using rsup_finite_in[of "{x}"] by auto @@ -2168,17 +2194,17 @@ by simp lemma bounded_has_rinf: - assumes "bounded(vec1 ` S)" "S \ {}" + assumes "bounded S" "S \ {}" shows "\x\S. x >= rinf S" and "\b. (\x\S. x >= b) \ rinf S >= b" proof fix x assume "x\S" - from assms(1) obtain a where a:"\x\S. \x\ \ a" unfolding bounded_vec1 by auto + from assms(1) obtain a where a:"\x\S. \x\ \ a" unfolding bounded_real by auto hence *:"- a <=* S" using setgeI[of S "-a"] unfolding abs_le_interval_iff by auto thus "x \ rinf S" using rinf[OF `S\{}`] using isGlbD2[of UNIV S "rinf S" x] using `x\S` by auto next show "\b. (\x\S. x >= b) \ rinf S \ b" using assms using rinf[of S, unfolded isGlb_def isLb_def greatestP_def setle_def setge_def] - apply (auto simp add: bounded_vec1) + apply (auto simp add: bounded_real) by (auto simp add: isGlb_def isLb_def greatestP_def setle_def setge_def) qed @@ -2189,7 +2215,7 @@ apply (blast intro!: order_antisym dest!: isGlb_le_isLb) done -lemma rinf_insert: assumes "bounded (vec1 ` S)" +lemma rinf_insert: assumes "bounded S" shows "rinf(insert x S) = (if S = {} then x else min x (rinf S))" (is "?lhs = ?rhs") proof(cases "S={}") case True thus ?thesis using rinf_finite_in[of "{x}"] by auto @@ -4050,68 +4076,52 @@ subsection{* Topological stuff lifted from and dropped to R *} -lemma open_vec1: - fixes s :: "real set" shows - "open(vec1 ` s) \ - (\x \ s. \e>0. \x'. abs(x' - x) < e --> x' \ s)" (is "?lhs = ?rhs") - unfolding open_dist apply simp unfolding forall_vec1 dist_vec1 vec1_in_image_vec1 by simp - -lemma islimpt_approachable_vec1: +lemma open_real: fixes s :: "real set" shows - "(vec1 x) islimpt (vec1 ` s) \ - (\e>0. \x'\ s. x' \ x \ abs(x' - x) < e)" - by (auto simp add: islimpt_approachable dist_vec1 vec1_eq) - -lemma closed_vec1: - fixes s :: "real set" shows - "closed (vec1 ` s) \ + "open s \ + (\x \ s. \e>0. \x'. abs(x' - x) < e --> x' \ s)" (is "?lhs = ?rhs") + unfolding open_dist dist_norm by simp + +lemma islimpt_approachable_real: + fixes s :: "real set" + shows "x islimpt s \ (\e>0. \x'\ s. x' \ x \ abs(x' - x) < e)" + unfolding islimpt_approachable dist_norm by simp + +lemma closed_real: + fixes s :: "real set" + shows "closed s \ (\x. (\e>0. \x' \ s. x' \ x \ abs(x' - x) < e) --> x \ s)" - unfolding closed_limpt islimpt_approachable forall_vec1 apply simp - unfolding dist_vec1 vec1_in_image_vec1 abs_minus_commute by auto - -lemma continuous_at_vec1_range: - fixes f :: "real ^ _ \ real" - shows "continuous (at x) (vec1 o f) \ (\e>0. \d>0. + unfolding closed_limpt islimpt_approachable dist_norm by simp + +lemma continuous_at_real_range: + fixes f :: "'a::real_normed_vector \ real" + shows "continuous (at x) f \ (\e>0. \d>0. \x'. norm(x' - x) < d --> abs(f x' - f x) < e)" - unfolding continuous_at unfolding Lim_at apply simp unfolding dist_vec1 unfolding dist_nz[THEN sym] unfolding dist_norm apply auto + unfolding continuous_at unfolding Lim_at + unfolding dist_nz[THEN sym] unfolding dist_norm apply auto apply(erule_tac x=e in allE) apply auto apply (rule_tac x=d in exI) apply auto apply (erule_tac x=x' in allE) apply auto apply(erule_tac x=e in allE) by auto -lemma continuous_on_vec1_range: +lemma continuous_on_real_range: fixes f :: "'a::real_normed_vector \ real" - shows "continuous_on s (vec1 o f) \ (\x \ s. \e>0. \d>0. (\x' \ s. norm(x' - x) < d --> abs(f x' - f x) < e))" - unfolding continuous_on_def apply (simp del: dist_commute) unfolding dist_vec1 unfolding dist_norm .. - -lemma continuous_at_vec1_norm: - fixes x :: "real ^ _" - shows "continuous (at x) (vec1 o norm)" - unfolding continuous_at_vec1_range using real_abs_sub_norm order_le_less_trans by blast - -lemma continuous_on_vec1_norm: - fixes s :: "(real ^ _) set" - shows "continuous_on s (vec1 o norm)" -unfolding continuous_on_vec1_range norm_vec1[THEN sym] by (metis norm_vec1 order_le_less_trans real_abs_sub_norm) - -lemma continuous_at_vec1_component: - shows "continuous (at (a::real^'a::finite)) (\ x. vec1(x$i))" -proof- - { fix e::real and x assume "0 < dist x a" "dist x a < e" "e>0" - hence "\x $ i - a $ i\ < e" using component_le_norm[of "x - a" i] unfolding dist_norm by auto } - thus ?thesis unfolding continuous_at tendsto_iff eventually_at dist_vec1 by auto -qed - -lemma continuous_on_vec1_component: - shows "continuous_on s (\ x::real^'a::finite. vec1(x$i))" -proof- - { fix e::real and x xa assume "x\s" "e>0" "xa\s" "0 < norm (xa - x) \ norm (xa - x) < e" - hence "\xa $ i - x $ i\ < e" using component_le_norm[of "xa - x" i] by auto } - thus ?thesis unfolding continuous_on Lim_within dist_vec1 unfolding dist_norm by auto -qed - -lemma continuous_at_vec1_infnorm: - "continuous (at x) (vec1 o infnorm)" - unfolding continuous_at Lim_at o_def unfolding dist_vec1 unfolding dist_norm + shows "continuous_on s f \ (\x \ s. \e>0. \d>0. (\x' \ s. norm(x' - x) < d --> abs(f x' - f x) < e))" + unfolding continuous_on_def dist_norm by simp + +lemma continuous_at_norm: "continuous (at x) norm" + unfolding continuous_at by (intro tendsto_norm Lim_ident_at) + +lemma continuous_on_norm: "continuous_on s norm" +unfolding continuous_on by (intro ballI tendsto_norm Lim_at_within Lim_ident_at) + +lemma continuous_at_component: "continuous (at a) (\x. x $ i)" +unfolding continuous_at by (intro Lim_component Lim_ident_at) + +lemma continuous_on_component: "continuous_on s (\x. x $ i)" +unfolding continuous_on by (intro ballI Lim_component Lim_at_within Lim_ident_at) + +lemma continuous_at_infnorm: "continuous (at x) infnorm" + unfolding continuous_at Lim_at o_def unfolding dist_norm apply auto apply (rule_tac x=e in exI) apply auto using order_trans[OF real_abs_sub_infnorm infnorm_le_norm, of _ x] by (metis xt1(7)) @@ -4119,23 +4129,23 @@ lemma compact_attains_sup: fixes s :: "real set" - assumes "compact (vec1 ` s)" "s \ {}" + assumes "compact s" "s \ {}" shows "\x \ s. \y \ s. y \ x" proof- - from assms(1) have a:"bounded (vec1 ` s)" "closed (vec1 ` s)" unfolding compact_eq_bounded_closed by auto + from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto { fix e::real assume as: "\x\s. x \ rsup s" "rsup s \ s" "0 < e" "\x'\s. x' = rsup s \ \ rsup s - x' < e" have "isLub UNIV s (rsup s)" using rsup[OF assms(2)] unfolding setle_def using as(1) by auto moreover have "isUb UNIV s (rsup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto ultimately have False using isLub_le_isUb[of UNIV s "rsup s" "rsup s - e"] using `e>0` by auto } - thus ?thesis using bounded_has_rsup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_vec1, THEN spec[where x="rsup s"]] + thus ?thesis using bounded_has_rsup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rsup s"]] apply(rule_tac x="rsup s" in bexI) by auto qed lemma compact_attains_inf: fixes s :: "real set" - assumes "compact (vec1 ` s)" "s \ {}" shows "\x \ s. \y \ s. x \ y" + assumes "compact s" "s \ {}" shows "\x \ s. \y \ s. x \ y" proof- - from assms(1) have a:"bounded (vec1 ` s)" "closed (vec1 ` s)" unfolding compact_eq_bounded_closed by auto + from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto { fix e::real assume as: "\x\s. x \ rinf s" "rinf s \ s" "0 < e" "\x'\s. x' = rinf s \ \ abs (x' - rinf s) < e" have "isGlb UNIV s (rinf s)" using rinf[OF assms(2)] unfolding setge_def using as(1) by auto @@ -4145,43 +4155,40 @@ have "rinf s + e \ x" using as(4)[THEN bspec[where x=x]] using as(2) `x\s` unfolding * by auto } hence "isLb UNIV s (rinf s + e)" unfolding isLb_def and setge_def by auto ultimately have False using isGlb_le_isLb[of UNIV s "rinf s" "rinf s + e"] using `e>0` by auto } - thus ?thesis using bounded_has_rinf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_vec1, THEN spec[where x="rinf s"]] + thus ?thesis using bounded_has_rinf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rinf s"]] apply(rule_tac x="rinf s" in bexI) by auto qed lemma continuous_attains_sup: fixes f :: "'a::metric_space \ real" - shows "compact s \ s \ {} \ continuous_on s (vec1 o f) + shows "compact s \ s \ {} \ continuous_on s f ==> (\x \ s. \y \ s. f y \ f x)" using compact_attains_sup[of "f ` s"] - using compact_continuous_image[of s "vec1 \ f"] unfolding image_compose by auto + using compact_continuous_image[of s f] by auto lemma continuous_attains_inf: fixes f :: "'a::metric_space \ real" - shows "compact s \ s \ {} \ continuous_on s (vec1 o f) + shows "compact s \ s \ {} \ continuous_on s f \ (\x \ s. \y \ s. f x \ f y)" using compact_attains_inf[of "f ` s"] - using compact_continuous_image[of s "vec1 \ f"] unfolding image_compose by auto + using compact_continuous_image[of s f] by auto lemma distance_attains_sup: - fixes s :: "(real ^ _) set" assumes "compact s" "s \ {}" shows "\x \ s. \y \ s. dist a y \ dist a x" -proof- - { fix x assume "x\s" fix e::real assume "e>0" - { fix x' assume "x'\s" and as:"norm (x' - x) < e" - hence "\norm (x' - a) - norm (x - a)\ < e" - using real_abs_sub_norm[of "x' - a" "x - a"] by auto } - hence "\d>0. \x'\s. norm (x' - x) < d \ \dist x' a - dist x a\ < e" using `e>0` unfolding dist_norm by auto } - thus ?thesis using assms - using continuous_attains_sup[of s "\x. dist a x"] - unfolding continuous_on_vec1_range by (auto simp add: dist_commute) +proof (rule continuous_attains_sup [OF assms]) + { fix x assume "x\s" + have "(dist a ---> dist a x) (at x within s)" + by (intro tendsto_dist tendsto_const Lim_at_within Lim_ident_at) + } + thus "continuous_on s (dist a)" + unfolding continuous_on .. qed text{* For *minimal* distance, we only need closure, not compactness. *} lemma distance_attains_inf: - fixes a :: "real ^ _" (* FIXME: generalize *) + fixes a :: "'a::heine_borel" assumes "closed s" "s \ {}" shows "\x \ s. \y \ s. dist a x \ dist a y" proof- @@ -4192,14 +4199,25 @@ moreover { fix x assume "x\?B" fix e::real assume "e>0" - { fix x' assume "x'\?B" and as:"norm (x' - x) < e" - hence "\norm (x' - a) - norm (x - a)\ < e" - using real_abs_sub_norm[of "x' - a" "x - a"] by auto } - hence "\d>0. \x'\?B. norm (x' - x) < d \ \dist x' a - dist x a\ < e" using `e>0` unfolding dist_norm by auto } - hence "continuous_on (cball a (dist b a) \ s) (vec1 \ dist a)" unfolding continuous_on_vec1_range - by (auto simp add: dist_commute) - moreover have "compact ?B" using compact_cball[of a "dist b a"] unfolding compact_eq_bounded_closed using bounded_Int and closed_Int and assms(1) by auto - ultimately obtain x where "x\cball a (dist b a) \ s" "\y\cball a (dist b a) \ s. dist a x \ dist a y" using continuous_attains_inf[of ?B "dist a"] by fastsimp + { fix x' assume "x'\?B" and as:"dist x' x < e" + from as have "\dist a x' - dist a x\ < e" + unfolding abs_less_iff minus_diff_eq + using dist_triangle2 [of a x' x] + using dist_triangle [of a x x'] + by arith + } + hence "\d>0. \x'\?B. dist x' x < d \ \dist a x' - dist a x\ < e" + using `e>0` by auto + } + hence "continuous_on (cball a (dist b a) \ s) (dist a)" + unfolding continuous_on Lim_within dist_norm real_norm_def + by fast + moreover have "compact ?B" + using compact_cball[of a "dist b a"] + unfolding compact_eq_bounded_closed + using bounded_Int and closed_Int and assms(1) by auto + ultimately obtain x where "x\cball a (dist b a) \ s" "\y\cball a (dist b a) \ s. dist a x \ dist a y" + using continuous_attains_inf[of ?B "dist a"] by fastsimp thus ?thesis by fastsimp qed @@ -4207,39 +4225,34 @@ lemma Lim_mul: fixes f :: "'a \ real ^ _" - assumes "((vec1 o c) ---> vec1 d) net" "(f ---> l) net" + assumes "(c ---> d) net" "(f ---> l) net" shows "((\x. c(x) *s f x) ---> (d *s l)) net" -proof- - have "bilinear (\x. op *s (dest_vec1 (x::real^1)))" unfolding bilinear_def linear_def - unfolding dest_vec1_add dest_vec1_cmul - apply vector apply auto unfolding semiring_class.right_distrib semiring_class.left_distrib by auto - thus ?thesis using Lim_bilinear[OF assms, of "\x y. (dest_vec1 x) *s y"] by auto -qed + unfolding smult_conv_scaleR using assms by (rule scaleR.tendsto) lemma Lim_vmul: fixes c :: "'a \ real" - shows "((vec1 o c) ---> vec1 d) net ==> ((\x. c(x) *s v) ---> d *s v) net" + shows "(c ---> d) net ==> ((\x. c(x) *s v) ---> d *s v) net" using Lim_mul[of c d net "\x. v" v] using Lim_const[of v] by auto lemma continuous_vmul: fixes c :: "'a::metric_space \ real" - shows "continuous net (vec1 o c) ==> continuous net (\x. c(x) *s v)" + shows "continuous net c ==> continuous net (\x. c(x) *s v)" unfolding continuous_def using Lim_vmul[of c] by auto lemma continuous_mul: fixes c :: "'a::metric_space \ real" - shows "continuous net (vec1 o c) \ continuous net f + shows "continuous net c \ continuous net f ==> continuous net (\x. c(x) *s f x) " unfolding continuous_def using Lim_mul[of c] by auto lemma continuous_on_vmul: fixes c :: "'a::metric_space \ real" - shows "continuous_on s (vec1 o c) ==> continuous_on s (\x. c(x) *s v)" + shows "continuous_on s c ==> continuous_on s (\x. c(x) *s v)" unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto lemma continuous_on_mul: fixes c :: "'a::metric_space \ real" - shows "continuous_on s (vec1 o c) \ continuous_on s f + shows "continuous_on s c \