(* Author: L C Paulson, University of Cambridge Author: Amine Chaieb, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Brian Huffman, Portland State University *) section ‹Elementary Normed Vector Spaces› theory Elementary_Normed_Spaces imports "HOL-Library.FuncSet" Elementary_Metric_Spaces Cartesian_Space Connected begin subsection ‹Orthogonal Transformation of Balls› subsection✐‹tag unimportant› ‹Various Lemmas Combining Imports› lemma open_sums: fixes T :: "('b::real_normed_vector) set" assumes "open S ∨ open T" shows "open (⋃x∈ S. ⋃y ∈ T. {x + y})" using assms proof assume S: "open S" show ?thesis proof (clarsimp simp: open_dist) fix x y assume "x ∈ S" "y ∈ T" with S obtain e where "e > 0" and e: "⋀x'. dist x' x < e ⟹ x' ∈ S" by (auto simp: open_dist) then have "⋀z. dist z (x + y) < e ⟹ ∃x∈S. ∃y∈T. z = x + y" by (metis ‹y ∈ T› diff_add_cancel dist_add_cancel2) then show "∃e>0. ∀z. dist z (x + y) < e ⟶ (∃x∈S. ∃y∈T. z = x + y)" using ‹0 < e› ‹x ∈ S› by blast qed next assume T: "open T" show ?thesis proof (clarsimp simp: open_dist) fix x y assume "x ∈ S" "y ∈ T" with T obtain e where "e > 0" and e: "⋀x'. dist x' y < e ⟹ x' ∈ T" by (auto simp: open_dist) then have "⋀z. dist z (x + y) < e ⟹ ∃x∈S. ∃y∈T. z = x + y" by (metis ‹x ∈ S› add_diff_cancel_left' add_diff_eq diff_diff_add dist_norm) then show "∃e>0. ∀z. dist z (x + y) < e ⟶ (∃x∈S. ∃y∈T. z = x + y)" using ‹0 < e› ‹y ∈ T› by blast qed qed lemma image_orthogonal_transformation_ball: fixes f :: "'a::euclidean_space ⇒ 'a" assumes "orthogonal_transformation f" shows "f ` ball x r = ball (f x) r" proof (intro equalityI subsetI) fix y assume "y ∈ f ` ball x r" with assms show "y ∈ ball (f x) r" by (auto simp: orthogonal_transformation_isometry) next fix y assume y: "y ∈ ball (f x) r" then obtain z where z: "y = f z" using assms orthogonal_transformation_surj by blast with y assms show "y ∈ f ` ball x r" by (auto simp: orthogonal_transformation_isometry) qed lemma image_orthogonal_transformation_cball: fixes f :: "'a::euclidean_space ⇒ 'a" assumes "orthogonal_transformation f" shows "f ` cball x r = cball (f x) r" proof (intro equalityI subsetI) fix y assume "y ∈ f ` cball x r" with assms show "y ∈ cball (f x) r" by (auto simp: orthogonal_transformation_isometry) next fix y assume y: "y ∈ cball (f x) r" then obtain z where z: "y = f z" using assms orthogonal_transformation_surj by blast with y assms show "y ∈ f ` cball x r" by (auto simp: orthogonal_transformation_isometry) qed subsection ‹Support› definition (in monoid_add) support_on :: "'b set ⇒ ('b ⇒ 'a) ⇒ 'b set" where "support_on S f = {x∈S. f x ≠ 0}" lemma in_support_on: "x ∈ support_on S f ⟷ x ∈ S ∧ f x ≠ 0" by (simp add: support_on_def) lemma support_on_simps[simp]: "support_on {} f = {}" "support_on (insert x S) f = (if f x = 0 then support_on S f else insert x (support_on S f))" "support_on (S ∪ T) f = support_on S f ∪ support_on T f" "support_on (S ∩ T) f = support_on S f ∩ support_on T f" "support_on (S - T) f = support_on S f - support_on T f" "support_on (f ` S) g = f ` (support_on S (g ∘ f))" unfolding support_on_def by auto lemma support_on_cong: "(⋀x. x ∈ S ⟹ f x = 0 ⟷ g x = 0) ⟹ support_on S f = support_on S g" by (auto simp: support_on_def) lemma support_on_if: "a ≠ 0 ⟹ support_on A (λx. if P x then a else 0) = {x∈A. P x}" by (auto simp: support_on_def) lemma support_on_if_subset: "support_on A (λx. if P x then a else 0) ⊆ {x ∈ A. P x}" by (auto simp: support_on_def) lemma finite_support[intro]: "finite S ⟹ finite (support_on S f)" unfolding support_on_def by auto (* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *) definition (in comm_monoid_add) supp_sum :: "('b ⇒ 'a) ⇒ 'b set ⇒ 'a" where "supp_sum f S = (∑x∈support_on S f. f x)" lemma supp_sum_empty[simp]: "supp_sum f {} = 0" unfolding supp_sum_def by auto lemma supp_sum_insert[simp]: "finite (support_on S f) ⟹ supp_sum f (insert x S) = (if x ∈ S then supp_sum f S else f x + supp_sum f S)" by (simp add: supp_sum_def in_support_on insert_absorb) lemma supp_sum_divide_distrib: "supp_sum f A / (r::'a::field) = supp_sum (λn. f n / r) A" by (cases "r = 0") (auto simp: supp_sum_def sum_divide_distrib intro!: sum.cong support_on_cong) subsection ‹Intervals› lemma image_affinity_interval: fixes c :: "'a::ordered_real_vector" shows "((λx. m *⇩_{R}x + c) ` {a..b}) = (if {a..b}={} then {} else if 0 ≤ m then {m *⇩_{R}a + c .. m *⇩_{R}b + c} else {m *⇩_{R}b + c .. m *⇩_{R}a + c})" (is "?lhs = ?rhs") proof (cases "m=0") case True then show ?thesis by force next case False show ?thesis proof show "?lhs ⊆ ?rhs" by (auto simp: scaleR_left_mono scaleR_left_mono_neg) show "?rhs ⊆ ?lhs" proof (clarsimp, intro conjI impI subsetI) show "⟦0 ≤ m; a ≤ b; x ∈ {m *⇩_{R}a + c..m *⇩_{R}b + c}⟧ ⟹ x ∈ (λx. m *⇩_{R}x + c) ` {a..b}" for x using False by (rule_tac x="inverse m *⇩_{R}(x-c)" in image_eqI) (auto simp: pos_le_divideR_eq pos_divideR_le_eq le_diff_eq diff_le_eq) show "⟦¬ 0 ≤ m; a ≤ b; x ∈ {m *⇩_{R}b + c..m *⇩_{R}a + c}⟧ ⟹ x ∈ (λx. m *⇩_{R}x + c) ` {a..b}" for x by (rule_tac x="inverse m *⇩_{R}(x-c)" in image_eqI) (auto simp add: neg_le_divideR_eq neg_divideR_le_eq le_diff_eq diff_le_eq) qed qed qed subsection ‹Limit Points› lemma islimpt_ball: fixes x y :: "'a::{real_normed_vector,perfect_space}" shows "y islimpt ball x e ⟷ 0 < e ∧ y ∈ cball x e" (is "?lhs ⟷ ?rhs") proof show ?rhs if ?lhs proof { assume "e ≤ 0" then have *: "ball x e = {}" using ball_eq_empty[of x e] by auto have False using ‹?lhs› unfolding * using islimpt_EMPTY[of y] by auto } then show "e > 0" by (metis not_less) show "y ∈ cball x e" using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"] ball_subset_cball[of x e] ‹?lhs› unfolding closed_limpt by auto qed show ?lhs if ?rhs proof - from that have "e > 0" by auto { fix d :: real assume "d > 0" have "∃x'∈ball x e. x' ≠ y ∧ dist x' y < d" proof (cases "d ≤ dist x y") case True then show ?thesis proof (cases "x = y") case True then have False using ‹d ≤ dist x y› ‹d>0› by auto then show ?thesis by auto next case False have "dist x (y - (d / (2 * dist y x)) *⇩_{R}(y - x)) = norm (x - y + (d / (2 * norm (y - x))) *⇩_{R}(y - x))" unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[symmetric] by auto also have "… = ¦- 1 + d / (2 * norm (x - y))¦ * norm (x - y)" using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"] unfolding scaleR_minus_left scaleR_one by (auto simp: norm_minus_commute) also have "… = ¦- norm (x - y) + d / 2¦" unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]] unfolding distrib_right using ‹x≠y› by auto also have "… ≤ e - d/2" using ‹d ≤ dist x y› and ‹d>0› and ‹?rhs› by (auto simp: dist_norm) finally have "y - (d / (2 * dist y x)) *⇩_{R}(y - x) ∈ ball x e" using ‹d>0› by auto moreover have "(d / (2*dist y x)) *⇩_{R}(y - x) ≠ 0" using ‹x≠y›[unfolded dist_nz] ‹d>0› unfolding scaleR_eq_0_iff by (auto simp: dist_commute) moreover have "dist (y - (d / (2 * dist y x)) *⇩_{R}(y - x)) y < d" using ‹0 < d› by (fastforce simp: dist_norm) ultimately show ?thesis by (rule_tac x = "y - (d / (2*dist y x)) *⇩_{R}(y - x)" in bexI) auto qed next case False then have "d > dist x y" by auto show "∃x' ∈ ball x e. x' ≠ y ∧ dist x' y < d" proof (cases "x = y") case True obtain z where z: "z ≠ y" "dist z y < min e d" using perfect_choose_dist[of "min e d" y] using ‹d > 0› ‹e>0› by auto show ?thesis by (metis True z dist_commute mem_ball min_less_iff_conj) next case False then show ?thesis using ‹d>0› ‹d > dist x y› ‹?rhs› by force qed qed } then show ?thesis unfolding mem_cball islimpt_approachable mem_ball by auto qed qed lemma closure_ball_lemma: fixes x y :: "'a::real_normed_vector" assumes "x ≠ y" shows "y islimpt ball x (dist x y)" proof (rule islimptI) fix T assume "y ∈ T" "open T" then obtain r where "0 < r" "∀z. dist z y < r ⟶ z ∈ T" unfolding open_dist by fast ―‹choose point between @{term x} and @{term y}, within distance @{term r} of @{term y}.› define k where "k = min 1 (r / (2 * dist x y))" define z where "z = y + scaleR k (x - y)" have z_def2: "z = x + scaleR (1 - k) (y - x)" unfolding z_def by (simp add: algebra_simps) have "dist z y < r" unfolding z_def k_def using ‹0 < r› by (simp add: dist_norm min_def) then have "z ∈ T" using ‹∀z. dist z y < r ⟶ z ∈ T› by simp have "dist x z < dist x y" using ‹0 < r› assms by (simp add: z_def2 k_def dist_norm norm_minus_commute) then have "z ∈ ball x (dist x y)" by simp have "z ≠ y" unfolding z_def k_def using ‹x ≠ y› ‹0 < r› by (simp add: min_def) show "∃z∈ball x (dist x y). z ∈ T ∧ z ≠ y" using ‹z ∈ ball x (dist x y)› ‹z ∈ T› ‹z ≠ y› by fast qed subsection ‹Balls and Spheres in Normed Spaces› lemma mem_ball_0 [simp]: "x ∈ ball 0 e ⟷ norm x < e" for x :: "'a::real_normed_vector" by simp lemma mem_cball_0 [simp]: "x ∈ cball 0 e ⟷ norm x ≤ e" for x :: "'a::real_normed_vector" by simp lemma closure_ball [simp]: fixes x :: "'a::real_normed_vector" assumes "0 < e" shows "closure (ball x e) = cball x e" proof show "closure (ball x e) ⊆ cball x e" using closed_cball closure_minimal by blast have "⋀y. dist x y < e ∨ dist x y = e ⟹ y ∈ closure (ball x e)" by (metis Un_iff assms closure_ball_lemma closure_def dist_eq_0_iff mem_Collect_eq mem_ball) then show "cball x e ⊆ closure (ball x e)" by force qed lemma mem_sphere_0 [simp]: "x ∈ sphere 0 e ⟷ norm x = e" for x :: "'a::real_normed_vector" by simp (* In a trivial vector space, this fails for e = 0. *) lemma interior_cball [simp]: fixes x :: "'a::{real_normed_vector, perfect_space}" shows "interior (cball x e) = ball x e" proof (cases "e ≥ 0") case False note cs = this from cs have null: "ball x e = {}" using ball_empty[of e x] by auto moreover have "cball x e = {}" proof (rule equals0I) fix y assume "y ∈ cball x e" then show False by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball subset_antisym subset_ball) qed then have "interior (cball x e) = {}" using interior_empty by auto ultimately show ?thesis by blast next case True note cs = this have "ball x e ⊆ cball x e" using ball_subset_cball by auto moreover { fix S y assume as: "S ⊆ cball x e" "open S" "y∈S" then obtain d where "d>0" and d: "∀x'. dist x' y < d ⟶ x' ∈ S" unfolding open_dist by blast then obtain xa where xa_y: "xa ≠ y" and xa: "dist xa y < d" using perfect_choose_dist [of d] by auto have "xa ∈ S" using d[THEN spec[where x = xa]] using xa by (auto simp: dist_commute) then have xa_cball: "xa ∈ cball x e" using as(1) by auto then have "y ∈ ball x e" proof (cases "x = y") case True then have "e > 0" using cs order.order_iff_strict xa_cball xa_y by fastforce then show "y ∈ ball x e" using ‹x = y › by simp next case False have "dist (y + (d / 2 / dist y x) *⇩_{R}(y - x)) y < d" unfolding dist_norm using ‹d>0› norm_ge_zero[of "y - x"] ‹x ≠ y› by auto then have *: "y + (d / 2 / dist y x) *⇩_{R}(y - x) ∈ cball x e" using d as(1)[unfolded subset_eq] by blast have "y - x ≠ 0" using ‹x ≠ y› by auto hence **:"d / (2 * norm (y - x)) > 0" unfolding zero_less_norm_iff[symmetric] using ‹d>0› by auto have "dist (y + (d / 2 / dist y x) *⇩_{R}(y - x)) x = norm (y + (d / (2 * norm (y - x))) *⇩_{R}y - (d / (2 * norm (y - x))) *⇩_{R}x - x)" by (auto simp: dist_norm algebra_simps) also have "… = norm ((1 + d / (2 * norm (y - x))) *⇩_{R}(y - x))" by (auto simp: algebra_simps) also have "… = ¦1 + d / (2 * norm (y - x))¦ * norm (y - x)" using ** by auto also have "… = (dist y x) + d/2" using ** by (auto simp: distrib_right dist_norm) finally have "e ≥ dist x y +d/2" using *[unfolded mem_cball] by (auto simp: dist_commute) then show "y ∈ ball x e" unfolding mem_ball using ‹d>0› by auto qed } then have "∀S ⊆ cball x e. open S ⟶ S ⊆ ball x e" by auto ultimately show ?thesis using interior_unique[of "ball x e" "cball x e"] using open_ball[of x e] by auto qed lemma frontier_ball [simp]: fixes a :: "'a::real_normed_vector" shows "0 < e ⟹ frontier (ball a e) = sphere a e" by (force simp: frontier_def) lemma frontier_cball [simp]: fixes a :: "'a::{real_normed_vector, perfect_space}" shows "frontier (cball a e) = sphere a e" by (force simp: frontier_def) corollary compact_sphere [simp]: fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}" shows "compact (sphere a r)" using compact_frontier [of "cball a r"] by simp corollary bounded_sphere [simp]: fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}" shows "bounded (sphere a r)" by (simp add: compact_imp_bounded) corollary closed_sphere [simp]: fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}" shows "closed (sphere a r)" by (simp add: compact_imp_closed) lemma image_add_ball [simp]: fixes a :: "'a::real_normed_vector" shows "(+) b ` ball a r = ball (a+b) r" proof - { fix x :: 'a assume "dist (a + b) x < r" moreover have "b + (x - b) = x" by simp ultimately have "x ∈ (+) b ` ball a r" by (metis add.commute dist_add_cancel image_eqI mem_ball) } then show ?thesis by (auto simp: add.commute) qed lemma image_add_cball [simp]: fixes a :: "'a::real_normed_vector" shows "(+) b ` cball a r = cball (a+b) r" proof - have "⋀x. dist (a + b) x ≤ r ⟹ ∃y∈cball a r. x = b + y" by (metis (no_types) add.commute diff_add_cancel dist_add_cancel2 mem_cball) then show ?thesis by (force simp: add.commute) qed subsection✐‹tag unimportant› ‹Various Lemmas on Normed Algebras› lemma closed_of_nat_image: "closed (of_nat ` A :: 'a::real_normed_algebra_1 set)" by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_nat) lemma closed_of_int_image: "closed (of_int ` A :: 'a::real_normed_algebra_1 set)" by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_int) lemma closed_Nats [simp]: "closed (ℕ :: 'a :: real_normed_algebra_1 set)" unfolding Nats_def by (rule closed_of_nat_image) lemma closed_Ints [simp]: "closed (ℤ :: 'a :: real_normed_algebra_1 set)" unfolding Ints_def by (rule closed_of_int_image) lemma closed_subset_Ints: fixes A :: "'a :: real_normed_algebra_1 set" assumes "A ⊆ ℤ" shows "closed A" proof (intro discrete_imp_closed[OF zero_less_one] ballI impI, goal_cases) case (1 x y) with assms have "x ∈ ℤ" and "y ∈ ℤ" by auto with ‹dist y x < 1› show "y = x" by (auto elim!: Ints_cases simp: dist_of_int) qed subsection ‹Filters› definition indirection :: "'a::real_normed_vector ⇒ 'a ⇒ 'a filter" (infixr "indirection" 70) where "a indirection v = at a within {b. ∃c≥0. b - a = scaleR c v}" subsection ‹Trivial Limits› lemma trivial_limit_at_infinity: "¬ trivial_limit (at_infinity :: ('a::{real_normed_vector,perfect_space}) filter)" proof - obtain x::'a where "x ≠ 0" by (meson perfect_choose_dist zero_less_one) then have "b ≤ norm ((b / norm x) *⇩_{R}x)" for b by simp then show ?thesis unfolding trivial_limit_def eventually_at_infinity by blast qed lemma at_within_ball_bot_iff: fixes x y :: "'a::{real_normed_vector,perfect_space}" shows "at x within ball y r = bot ⟷ (r=0 ∨ x ∉ cball y r)" unfolding trivial_limit_within by (metis (no_types) cball_empty equals0D islimpt_ball less_linear) subsection ‹Limits› proposition Lim_at_infinity: "(f ⤏ l) at_infinity ⟷ (∀e>0. ∃b. ∀x. norm x ≥ b ⟶ dist (f x) l < e)" by (auto simp: tendsto_iff eventually_at_infinity) corollary Lim_at_infinityI [intro?]: assumes "⋀e. e > 0 ⟹ ∃B. ∀x. norm x ≥ B ⟶ dist (f x) l ≤ e" shows "(f ⤏ l) at_infinity" proof - have "⋀e. e > 0 ⟹ ∃B. ∀x. norm x ≥ B ⟶ dist (f x) l < e" by (meson assms dense le_less_trans) then show ?thesis using Lim_at_infinity by blast qed lemma Lim_transform_within_set_eq: fixes a :: "'a::metric_space" and l :: "'b::metric_space" shows "eventually (λx. x ∈ S ⟷ x ∈ T) (at a) ⟹ ((f ⤏ l) (at a within S) ⟷ (f ⤏ l) (at a within T))" by (force intro: Lim_transform_within_set elim: eventually_mono) 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_comparison: fixes f :: "'a ⇒ 'b::real_normed_vector" assumes "eventually (λx. norm (f x) ≤ g x) net" "(g ⤏ 0) net" shows "(f ⤏ 0) net" using assms(2) proof (rule metric_tendsto_imp_tendsto) show "eventually (λx. dist (f x) 0 ≤ dist (g x) 0) net" using assms(1) by (rule eventually_mono) (simp add: dist_norm) qed lemma Lim_transform_bound: fixes f :: "'a ⇒ 'b::real_normed_vector" and g :: "'a ⇒ 'c::real_normed_vector" assumes "eventually (λn. norm (f n) ≤ norm (g n)) net" and "(g ⤏ 0) net" shows "(f ⤏ 0) net" using assms(1) tendsto_norm_zero [OF assms(2)] by (rule Lim_null_comparison) lemma lim_null_mult_right_bounded: fixes f :: "'a ⇒ 'b::real_normed_div_algebra" assumes f: "(f ⤏ 0) F" and g: "eventually (λx. norm(g x) ≤ B) F" shows "((λz. f z * g z) ⤏ 0) F" proof - have "((λx. norm (f x) * norm (g x)) ⤏ 0) F" proof (rule Lim_null_comparison) show "∀⇩_{F}x in F. norm (norm (f x) * norm (g x)) ≤ norm (f x) * B" by (simp add: eventually_mono [OF g] mult_left_mono) show "((λx. norm (f x) * B) ⤏ 0) F" by (simp add: f tendsto_mult_left_zero tendsto_norm_zero) qed then show ?thesis by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult) qed lemma lim_null_mult_left_bounded: fixes f :: "'a ⇒ 'b::real_normed_div_algebra" assumes g: "eventually (λx. norm(g x) ≤ B) F" and f: "(f ⤏ 0) F" shows "((λz. g z * f z) ⤏ 0) F" proof - have "((λx. norm (g x) * norm (f x)) ⤏ 0) F" proof (rule Lim_null_comparison) show "∀⇩_{F}x in F. norm (norm (g x) * norm (f x)) ≤ B * norm (f x)" by (simp add: eventually_mono [OF g] mult_right_mono) show "((λx. B * norm (f x)) ⤏ 0) F" by (simp add: f tendsto_mult_right_zero tendsto_norm_zero) qed then show ?thesis by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult) qed lemma lim_null_scaleR_bounded: assumes f: "(f ⤏ 0) net" and gB: "eventually (λa. f a = 0 ∨ norm(g a) ≤ B) net" shows "((λn. f n *⇩_{R}g n) ⤏ 0) net" proof fix ε::real assume "0 < ε" then have B: "0 < ε / (abs B + 1)" by simp have *: "¦f x¦ * norm (g x) < ε" if f: "¦f x¦ * (¦B¦ + 1) < ε" and g: "norm (g x) ≤ B" for x proof - have "¦f x¦ * norm (g x) ≤ ¦f x¦ * B" by (simp add: mult_left_mono g) also have "… ≤ ¦f x¦ * (¦B¦ + 1)" by (simp add: mult_left_mono) also have "… < ε" by (rule f) finally show ?thesis . qed have "⋀x. ⟦¦f x¦ < ε / (¦B¦ + 1); norm (g x) ≤ B⟧ ⟹ ¦f x¦ * norm (g x) < ε" by (simp add: "*" pos_less_divide_eq) then show "∀⇩_{F}x in net. dist (f x *⇩_{R}g x) 0 < ε" using ‹0 < ε› by (auto intro: eventually_mono [OF eventually_conj [OF tendstoD [OF f B] gB]]) qed lemma Lim_norm_ubound: fixes f :: "'a ⇒ 'b::real_normed_vector" assumes "¬(trivial_limit net)" "(f ⤏ l) net" "eventually (λx. norm(f x) ≤ e) net" shows "norm(l) ≤ e" using assms by (fast intro: tendsto_le tendsto_intros) lemma Lim_norm_lbound: fixes f :: "'a ⇒ 'b::real_normed_vector" assumes "¬ trivial_limit net" and "(f ⤏ l) net" and "eventually (λx. e ≤ norm (f x)) net" shows "e ≤ norm l" using assms by (fast intro: tendsto_le tendsto_intros) text‹Limit under bilinear function› lemma Lim_bilinear: assumes "(f ⤏ l) net" and "(g ⤏ m) net" and "bounded_bilinear h" shows "((λx. h (f x) (g x)) ⤏ (h l m)) net" using ‹bounded_bilinear h› ‹(f ⤏ l) net› ‹(g ⤏ m) net› by (rule bounded_bilinear.tendsto) lemma Lim_at_zero: fixes a :: "'a::real_normed_vector" and l :: "'b::topological_space" shows "(f ⤏ l) (at a) ⟷ ((λx. f(a + x)) ⤏ l) (at 0)" using LIM_offset_zero LIM_offset_zero_cancel .. subsection✐‹tag unimportant› ‹Limit Point of Filter› lemma netlimit_at_vector: fixes a :: "'a::real_normed_vector" shows "netlimit (at a) = a" proof (cases "∃x. x ≠ a") case True then obtain x where x: "x ≠ a" .. have "⋀d. 0 < d ⟹ ∃x. x ≠ a ∧ norm (x - a) < d" by (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI) (simp add: norm_sgn sgn_zero_iff x) then have "¬ trivial_limit (at a)" by (auto simp: trivial_limit_def eventually_at dist_norm) then show ?thesis by (rule Lim_ident_at [of a UNIV]) qed simp subsection ‹Boundedness› lemma continuous_on_closure_norm_le: fixes f :: "'a::metric_space ⇒ 'b::real_normed_vector" assumes "continuous_on (closure s) f" and "∀y ∈ s. norm(f y) ≤ b" and "x ∈ (closure s)" shows "norm (f x) ≤ b" proof - have *: "f ` s ⊆ cball 0 b" using assms(2)[unfolded mem_cball_0[symmetric]] by auto show ?thesis by (meson "*" assms(1) assms(3) closed_cball image_closure_subset image_subset_iff mem_cball_0) qed lemma bounded_pos: "bounded S ⟷ (∃b>0. ∀x∈ S. norm x ≤ b)" unfolding bounded_iff by (meson less_imp_le not_le order_trans zero_less_one) lemma bounded_pos_less: "bounded S ⟷ (∃b>0. ∀x∈ S. norm x < b)" by (metis bounded_pos le_less_trans less_imp_le linordered_field_no_ub) lemma bounded_normE: assumes "bounded A" obtains B where "B > 0" "⋀z. z ∈ A ⟹ norm z ≤ B" by (meson assms bounded_pos) lemma bounded_normE_less: assumes "bounded A" obtains B where "B > 0" "⋀z. z ∈ A ⟹ norm z < B" by (meson assms bounded_pos_less) lemma Bseq_eq_bounded: fixes f :: "nat ⇒ 'a::real_normed_vector" shows "Bseq f ⟷ bounded (range f)" unfolding Bseq_def bounded_pos by auto lemma bounded_linear_image: assumes "bounded S" and "bounded_linear f" shows "bounded (f ` S)" proof - from assms(1) obtain b where "b > 0" and b: "∀x∈S. norm x ≤ b" unfolding bounded_pos by auto from assms(2) obtain B where B: "B > 0" "∀x. norm (f x) ≤ B * norm x" using bounded_linear.pos_bounded by (auto simp: ac_simps) show ?thesis unfolding bounded_pos proof (intro exI, safe) show "norm (f x) ≤ B * b" if "x ∈ S" for x by (meson B b less_imp_le mult_left_mono order_trans that) qed (use ‹b > 0› ‹B > 0› in auto) qed lemma bounded_scaling: fixes S :: "'a::real_normed_vector set" shows "bounded S ⟹ bounded ((λx. c *⇩_{R}x) ` S)" by (simp add: bounded_linear_image bounded_linear_scaleR_right) lemma bounded_scaleR_comp: fixes f :: "'a ⇒ 'b::real_normed_vector" assumes "bounded (f ` S)" shows "bounded ((λx. r *⇩_{R}f x) ` S)" using bounded_scaling[of "f ` S" r] assms by (auto simp: image_image) lemma bounded_translation: fixes S :: "'a::real_normed_vector set" assumes "bounded S" shows "bounded ((λx. a + x) ` S)" proof - from assms obtain b where b: "b > 0" "∀x∈S. norm x ≤ b" unfolding bounded_pos by auto { fix x assume "x ∈ S" then have "norm (a + x) ≤ b + norm a" using norm_triangle_ineq[of a x] b by auto } then show ?thesis unfolding bounded_pos using norm_ge_zero[of a] b(1) and add_strict_increasing[of b 0 "norm a"] by (auto intro!: exI[of _ "b + norm a"]) qed lemma bounded_translation_minus: fixes S :: "'a::real_normed_vector set" shows "bounded S ⟹ bounded ((λx. x - a) ` S)" using bounded_translation [of S "-a"] by simp lemma bounded_uminus [simp]: fixes X :: "'a::real_normed_vector set" shows "bounded (uminus ` X) ⟷ bounded X" by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp: add.commute norm_minus_commute) lemma uminus_bounded_comp [simp]: fixes f :: "'a ⇒ 'b::real_normed_vector" shows "bounded ((λx. - f x) ` S) ⟷ bounded (f ` S)" using bounded_uminus[of "f ` S"] by (auto simp: image_image) lemma bounded_plus_comp: fixes f g::"'a ⇒ 'b::real_normed_vector" assumes "bounded (f ` S)" assumes "bounded (g ` S)" shows "bounded ((λx. f x + g x) ` S)" proof - { fix B C assume "⋀x. x∈S ⟹ norm (f x) ≤ B" "⋀x. x∈S ⟹ norm (g x) ≤ C" then have "⋀x. x ∈ S ⟹ norm (f x + g x) ≤ B + C" by (auto intro!: norm_triangle_le add_mono) } then show ?thesis using assms by (fastforce simp: bounded_iff) qed lemma bounded_plus: fixes S ::"'a::real_normed_vector set" assumes "bounded S" "bounded T" shows "bounded ((λ(x,y). x + y) ` (S × T))" using bounded_plus_comp [of fst "S × T" snd] assms by (auto simp: split_def split: if_split_asm) lemma bounded_minus_comp: "bounded (f ` S) ⟹ bounded (g ` S) ⟹ bounded ((λx. f x - g x) ` S)" for f g::"'a ⇒ 'b::real_normed_vector" using bounded_plus_comp[of "f" S "λx. - g x"] by auto lemma bounded_minus: fixes S ::"'a::real_normed_vector set" assumes "bounded S" "bounded T" shows "bounded ((λ(x,y). x - y) ` (S × T))" using bounded_minus_comp [of fst "S × T" snd] assms by (auto simp: split_def split: if_split_asm) lemma bounded_sums: fixes S :: "'a::real_normed_vector set" assumes "bounded S" and "bounded T" shows "bounded (⋃x∈ S. ⋃y ∈ T. {x + y})" using assms by (simp add: bounded_iff) (meson norm_triangle_mono) lemma bounded_differences: fixes S :: "'a::real_normed_vector set" assumes "bounded S" and "bounded T" shows "bounded (⋃x∈ S. ⋃y ∈ T. {x - y})" using assms by (simp add: bounded_iff) (meson add_mono norm_triangle_le_diff) lemma not_bounded_UNIV[simp]: "¬ bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)" proof (auto simp: bounded_pos not_le) obtain x :: 'a where "x ≠ 0" using perfect_choose_dist [OF zero_less_one] by fast fix b :: real assume b: "b >0" have b1: "b +1 ≥ 0" using b by simp with ‹x ≠ 0› have "b < norm (scaleR (b + 1) (sgn x))" by (simp add: norm_sgn) then show "∃x::'a. b < norm x" .. qed corollary cobounded_imp_unbounded: fixes S :: "'a::{real_normed_vector, perfect_space} set" shows "bounded (- S) ⟹ ¬ bounded S" using bounded_Un [of S "-S"] by (simp) subsection✐‹tag unimportant›‹Relations among convergence and absolute convergence for power series› lemma summable_imp_bounded: fixes f :: "nat ⇒ 'a::real_normed_vector" shows "summable f ⟹ bounded (range f)" by (frule summable_LIMSEQ_zero) (simp add: convergent_imp_bounded) lemma summable_imp_sums_bounded: "summable f ⟹ bounded (range (λn. sum f {..<n}))" by (auto simp: summable_def sums_def dest: convergent_imp_bounded) lemma power_series_conv_imp_absconv_weak: fixes a:: "nat ⇒ 'a::{real_normed_div_algebra,banach}" and w :: 'a assumes sum: "summable (λn. a n * z ^ n)" and no: "norm w < norm z" shows "summable (λn. of_real(norm(a n)) * w ^ n)" proof - obtain M where M: "⋀x. norm (a x * z ^ x) ≤ M" using summable_imp_bounded [OF sum] by (force simp: bounded_iff) show ?thesis proof (rule series_comparison_complex) have "⋀n. norm (a n) * norm z ^ n ≤ M" by (metis (no_types) M norm_mult norm_power) then show "summable (λn. complex_of_real (norm (a n) * norm w ^ n))" using Abel_lemma no norm_ge_zero summable_of_real by blast qed (auto simp: norm_mult norm_power) qed subsection ‹Normed spaces with the Heine-Borel property› lemma not_compact_UNIV[simp]: fixes s :: "'a::{real_normed_vector,perfect_space,heine_borel} set" shows "¬ compact (UNIV::'a set)" by (simp add: compact_eq_bounded_closed) lemma not_compact_space_euclideanreal [simp]: "¬ compact_space euclideanreal" by (simp add: compact_space_def) text‹Representing sets as the union of a chain of compact sets.› lemma closed_Union_compact_subsets: fixes S :: "'a::{heine_borel,real_normed_vector} set" assumes "closed S" obtains F where "⋀n. compact(F n)" "⋀n. F n ⊆ S" "⋀n. F n ⊆ F(Suc n)" "(⋃n. F n) = S" "⋀K. ⟦compact K; K ⊆ S⟧ ⟹ ∃N. ∀n ≥ N. K ⊆ F n" proof show "compact (S ∩ cball 0 (of_nat n))" for n using assms compact_eq_bounded_closed by auto next show "(⋃n. S ∩ cball 0 (real n)) = S" by (auto simp: real_arch_simple) next fix K :: "'a set" assume "compact K" "K ⊆ S" then obtain N where "K ⊆ cball 0 N" by (meson bounded_pos mem_cball_0 compact_imp_bounded subsetI) then show "∃N. ∀n≥N. K ⊆ S ∩ cball 0 (real n)" by (metis of_nat_le_iff Int_subset_iff ‹K ⊆ S› real_arch_simple subset_cball subset_trans) qed auto subsection ‹Intersecting chains of compact sets and the Baire property› proposition bounded_closed_chain: fixes ℱ :: "'a::heine_borel set set" assumes "B ∈ ℱ" "bounded B" and ℱ: "⋀S. S ∈ ℱ ⟹ closed S" and "{} ∉ ℱ" and chain: "⋀S T. S ∈ ℱ ∧ T ∈ ℱ ⟹ S ⊆ T ∨ T ⊆ S" shows "⋂ℱ ≠ {}" proof - have "B ∩ ⋂ℱ ≠ {}" proof (rule compact_imp_fip) show "compact B" "⋀T. T ∈ ℱ ⟹ closed T" by (simp_all add: assms compact_eq_bounded_closed) show "⟦finite 𝒢; 𝒢 ⊆ ℱ⟧ ⟹ B ∩ ⋂𝒢 ≠ {}" for 𝒢 proof (induction 𝒢 rule: finite_induct) case empty with assms show ?case by force next case (insert U 𝒢) then have "U ∈ ℱ" and ne: "B ∩ ⋂𝒢 ≠ {}" by auto then consider "B ⊆ U" | "U ⊆ B" using ‹B ∈ ℱ› chain by blast then show ?case proof cases case 1 then show ?thesis using Int_left_commute ne by auto next case 2 have "U ≠ {}" using ‹U ∈ ℱ› ‹{} ∉ ℱ› by blast moreover have False if "⋀x. x ∈ U ⟹ ∃Y∈𝒢. x ∉ Y" proof - have "⋀x. x ∈ U ⟹ ∃Y∈𝒢. Y ⊆ U" by (metis chain contra_subsetD insert.prems insert_subset that) then obtain Y where "Y ∈ 𝒢" "Y ⊆ U" by (metis all_not_in_conv ‹U ≠ {}›) moreover obtain x where "x ∈ ⋂𝒢" by (metis Int_emptyI ne) ultimately show ?thesis by (metis Inf_lower subset_eq that) qed with 2 show ?thesis by blast qed qed qed then show ?thesis by blast qed corollary compact_chain: fixes ℱ :: "'a::heine_borel set set" assumes "⋀S. S ∈ ℱ ⟹ compact S" "{} ∉ ℱ" "⋀S T. S ∈ ℱ ∧ T ∈ ℱ ⟹ S ⊆ T ∨ T ⊆ S" shows "⋂ ℱ ≠ {}" proof (cases "ℱ = {}") case True then show ?thesis by auto next case False show ?thesis by (metis False all_not_in_conv assms compact_imp_bounded compact_imp_closed bounded_closed_chain) qed lemma compact_nest: fixes F :: "'a::linorder ⇒ 'b::heine_borel set" assumes F: "⋀n. compact(F n)" "⋀n. F n ≠ {}" and mono: "⋀m n. m ≤ n ⟹ F n ⊆ F m" shows "⋂(range F) ≠ {}" proof - have *: "⋀S T. S ∈ range F ∧ T ∈ range F ⟹ S ⊆ T ∨ T ⊆ S" by (metis mono image_iff le_cases) show ?thesis using F by (intro compact_chain [OF _ _ *]; blast dest: *) qed text‹The Baire property of dense sets› theorem Baire: fixes S::"'a::{real_normed_vector,heine_borel} set" assumes "closed S" "countable 𝒢" and ope: "⋀T. T ∈ 𝒢 ⟹ openin (top_of_set S) T ∧ S ⊆ closure T" shows "S ⊆ closure(⋂𝒢)" proof (cases "𝒢 = {}") case True then show ?thesis using closure_subset by auto next let ?g = "from_nat_into 𝒢" case False then have gin: "?g n ∈ 𝒢" for n by (simp add: from_nat_into) show ?thesis proof (clarsimp simp: closure_approachable) fix x and e::real assume "x ∈ S" "0 < e" obtain TF where opeF: "⋀n. openin (top_of_set S) (TF n)" and ne: "⋀n. TF n ≠ {}" and subg: "⋀n. S ∩ closure(TF n) ⊆ ?g n" and subball: "⋀n. closure(TF n) ⊆ ball x e" and decr: "⋀n. TF(Suc n) ⊆ TF n" proof - have *: "∃Y. (openin (top_of_set S) Y ∧ Y ≠ {} ∧ S ∩ closure Y ⊆ ?g n ∧ closure Y ⊆ ball x e) ∧ Y ⊆ U" if opeU: "openin (top_of_set S) U" and "U ≠ {}" and cloU: "closure U ⊆ ball x e" for U n proof - obtain T where T: "open T" "U = T ∩ S" using ‹openin (top_of_set S) U› by (auto simp: openin_subtopology) with ‹U ≠ {}› have "T ∩ closure (?g n) ≠ {}" using gin ope by fastforce then have "T ∩ ?g n ≠ {}" using ‹open T› open_Int_closure_eq_empty by blast then obtain y where "y ∈ U" "y ∈ ?g n" using T ope [of "?g n", OF gin] by (blast dest: openin_imp_subset) moreover have "openin (top_of_set S) (U ∩ ?g n)" using gin ope opeU by blast ultimately obtain d where U: "U ∩ ?g n ⊆ S" and "d > 0" and d: "ball y d ∩ S ⊆ U ∩ ?g n" by (force simp: openin_contains_ball) show ?thesis proof (intro exI conjI) show "openin (top_of_set S) (S ∩ ball y (d/2))" by (simp add: openin_open_Int) show "S ∩ ball y (d/2) ≠ {}" using ‹0 < d› ‹y ∈ U› opeU openin_imp_subset by fastforce have "S ∩ closure (S ∩ ball y (d/2)) ⊆ S ∩ closure (ball y (d/2))" using closure_mono by blast also have "... ⊆ ?g n" using ‹d > 0› d by force finally show "S ∩ closure (S ∩ ball y (d/2)) ⊆ ?g n" . have "closure (S ∩ ball y (d/2)) ⊆ S ∩ ball y d" proof - have "closure (ball y (d/2)) ⊆ ball y d" using ‹d > 0› by auto then have "closure (S ∩ ball y (d/2)) ⊆ ball y d" by (meson closure_mono inf.cobounded2 subset_trans) then show ?thesis by (simp add: ‹closed S› closure_minimal) qed also have "... ⊆ ball x e" using cloU closure_subset d by blast finally show "closure (S ∩ ball y (d/2)) ⊆ ball x e" . show "S ∩ ball y (d/2) ⊆ U" using ball_divide_subset_numeral d by blast qed qed let ?Φ = "λn X. openin (top_of_set S) X ∧ X ≠ {} ∧ S ∩ closure X ⊆ ?g n ∧ closure X ⊆ ball x e" have "closure (S ∩ ball x (e/2)) ⊆ closure(ball x (e/2))" by (simp add: closure_mono) also have "... ⊆ ball x e" using ‹e > 0› by auto finally have "closure (S ∩ ball x (e/2)) ⊆ ball x e" . moreover have"openin (top_of_set S) (S ∩ ball x (e/2))" "S ∩ ball x (e/2) ≠ {}" using ‹0 < e› ‹x ∈ S› by auto ultimately obtain Y where Y: "?Φ 0 Y ∧ Y ⊆ S ∩ ball x (e/2)" using * [of "S ∩ ball x (e/2)" 0] by metis show thesis proof (rule exE [OF dependent_nat_choice]) show "∃x. ?Φ 0 x" using Y by auto show "∃Y. ?Φ (Suc n) Y ∧ Y ⊆ X" if "?Φ n X" for X n using that by (blast intro: *) qed (use that in metis) qed have "(⋂n. S ∩ closure (TF n)) ≠ {}" proof (rule compact_nest) show "⋀n. compact (S ∩ closure (TF n))" by (metis closed_closure subball bounded_subset_ballI compact_eq_bounded_closed closed_Int_compact [OF ‹closed S›]) show "⋀n. S ∩ closure (TF n) ≠ {}" by (metis Int_absorb1 opeF ‹closed S› closure_eq_empty closure_minimal ne openin_imp_subset) show "⋀m n. m ≤ n ⟹ S ∩ closure (TF n) ⊆ S ∩ closure (TF m)" by (meson closure_mono decr dual_order.refl inf_mono lift_Suc_antimono_le) qed moreover have "(⋂n. S ∩ closure (TF n)) ⊆ {y ∈ ⋂𝒢. dist y x < e}" proof (clarsimp, intro conjI) fix y assume "y ∈ S" and y: "∀n. y ∈ closure (TF n)" then show "∀T∈𝒢. y ∈ T" by (metis Int_iff from_nat_into_surj [OF ‹countable 𝒢›] subsetD subg) show "dist y x < e" by (metis y dist_commute mem_ball subball subsetCE) qed ultimately show "∃y ∈ ⋂𝒢. dist y x < e" by auto qed qed subsection ‹Continuity› subsubsection✐‹tag unimportant› ‹Structural rules for uniform continuity› lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]: fixes g :: "_::metric_space ⇒ _" assumes "uniformly_continuous_on s g" shows "uniformly_continuous_on s (λx. f (g x))" using assms unfolding uniformly_continuous_on_sequentially unfolding dist_norm tendsto_norm_zero_iff diff[symmetric] by (auto intro: tendsto_zero) lemma uniformly_continuous_on_dist[continuous_intros]: fixes f g :: "'a::metric_space ⇒ 'b::metric_space" assumes "uniformly_continuous_on s f" and "uniformly_continuous_on s g" shows "uniformly_continuous_on s (λx. dist (f x) (g x))" proof - { fix a b c d :: 'b have "¦dist a b - dist c d¦ ≤ dist a c + dist b d" using dist_triangle2 [of a b c] dist_triangle2 [of b c d] using dist_triangle3 [of c d a] dist_triangle [of a d b] by arith } note le = this { fix x y assume f: "(λn. dist (f (x n)) (f (y n))) ⇢ 0" assume g: "(λn. dist (g (x n)) (g (y n))) ⇢ 0" have "(λn. ¦dist (f (x n)) (g (x n)) - dist (f (y n)) (g (y n))¦) ⇢ 0" by (rule Lim_transform_bound [OF _ tendsto_add_zero [OF f g]], simp add: le) } then show ?thesis using assms unfolding uniformly_continuous_on_sequentially unfolding dist_real_def by simp qed lemma uniformly_continuous_on_cmul_right [continuous_intros]: fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_algebra" shows "uniformly_continuous_on s f ⟹ uniformly_continuous_on s (λx. f x * c)" using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] . lemma uniformly_continuous_on_cmul_left[continuous_intros]: fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_algebra" assumes "uniformly_continuous_on s f" shows "uniformly_continuous_on s (λx. c * f x)" by (metis assms bounded_linear.uniformly_continuous_on bounded_linear_mult_right) lemma uniformly_continuous_on_norm[continuous_intros]: fixes f :: "'a :: metric_space ⇒ 'b :: real_normed_vector" assumes "uniformly_continuous_on s f" shows "uniformly_continuous_on s (λx. norm (f x))" unfolding norm_conv_dist using assms by (intro uniformly_continuous_on_dist uniformly_continuous_on_const) lemma uniformly_continuous_on_cmul[continuous_intros]: fixes f :: "'a::metric_space ⇒ 'b::real_normed_vector" assumes "uniformly_continuous_on s f" shows "uniformly_continuous_on s (λx. c *⇩_{R}f(x))" using bounded_linear_scaleR_right assms by (rule bounded_linear.uniformly_continuous_on) lemma dist_minus: fixes x y :: "'a::real_normed_vector" shows "dist (- x) (- y) = dist x y" unfolding dist_norm minus_diff_minus norm_minus_cancel .. lemma uniformly_continuous_on_minus[continuous_intros]: fixes f :: "'a::metric_space ⇒ 'b::real_normed_vector" shows "uniformly_continuous_on s f ⟹ uniformly_continuous_on s (λx. - f x)" unfolding uniformly_continuous_on_def dist_minus . lemma uniformly_continuous_on_add[continuous_intros]: fixes f g :: "'a::metric_space ⇒ 'b::real_normed_vector" assumes "uniformly_continuous_on s f" and "uniformly_continuous_on s g" shows "uniformly_continuous_on s (λx. f x + g x)" using assms unfolding uniformly_continuous_on_sequentially unfolding dist_norm tendsto_norm_zero_iff add_diff_add by (auto intro: tendsto_add_zero) lemma uniformly_continuous_on_diff[continuous_intros]: fixes f :: "'a::metric_space ⇒ 'b::real_normed_vector" assumes "uniformly_continuous_on s f" and "uniformly_continuous_on s g" shows "uniformly_continuous_on s (λx. f x - g x)" using assms uniformly_continuous_on_add [of s f "- g"] by (simp add: fun_Compl_def uniformly_continuous_on_minus) lemma uniformly_continuous_on_sum [continuous_intros]: fixes f :: "'a ⇒ 'b::metric_space ⇒ 'c::real_normed_vector" shows "(⋀i. i ∈ I ⟹ uniformly_continuous_on S (f i)) ⟹ uniformly_continuous_on S (λx. ∑i∈I. f i x)" by (induction I rule: infinite_finite_induct) (auto simp: uniformly_continuous_on_add uniformly_continuous_on_const) subsection✐‹tag unimportant› ‹Arithmetic Preserves Topological Properties› lemma open_scaling[intro]: fixes s :: "'a::real_normed_vector set" assumes "c ≠ 0" and "open s" shows "open((λx. c *⇩_{R}x) ` s)" proof - { fix x assume "x ∈ s" then obtain e where "e>0" and e:"∀x'. dist x' x < e ⟶ x' ∈ s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]] by auto have "e * ¦c¦ > 0" using assms(1)[unfolded zero_less_abs_iff[symmetric]] ‹e>0› by auto moreover { fix y assume "dist y (c *⇩_{R}x) < e * ¦c¦" then have "norm (c *⇩_{R}((1 / c) *⇩_{R}y - x)) < e * norm c" by (simp add: ‹c ≠ 0› dist_norm scale_right_diff_distrib) then have "norm ((1 / c) *⇩_{R}y - x) < e" by (simp add: ‹c ≠ 0›) then have "y ∈ (*⇩_{R}) c ` s" using rev_image_eqI[of "(1 / c) *⇩_{R}y" s y "(*⇩_{R}) c"] by (simp add: ‹c ≠ 0› dist_norm e) } ultimately have "∃e>0. ∀x'. dist x' (c *⇩_{R}x) < e ⟶ x' ∈ (*⇩_{R}) c ` s" by (rule_tac x="e * ¦c¦" in exI, auto) } then show ?thesis unfolding open_dist by auto qed lemma minus_image_eq_vimage: fixes A :: "'a::ab_group_add set" shows "(λx. - x) ` A = (λx. - x) -` A" by (auto intro!: image_eqI [where f="λx. - x"]) lemma open_negations: fixes S :: "'a::real_normed_vector set" shows "open S ⟹ open ((λx. - x) ` S)" using open_scaling [of "- 1" S] by simp lemma open_translation: fixes S :: "'a::real_normed_vector set" assumes "open S" shows "open((λx. a + x) ` S)" proof - { fix x have "continuous (at x) (λx. x - a)" by (intro continuous_diff continuous_ident continuous_const) } moreover have "{x. x - a ∈ S} = (+) a ` S" by force ultimately show ?thesis by (metis assms continuous_open_vimage vimage_def) qed lemma open_translation_subtract: fixes S :: "'a::real_normed_vector set" assumes "open S" shows "open ((λx. x - a) ` S)" using assms open_translation [of S "- a"] by (simp cong: image_cong_simp) lemma open_neg_translation: fixes S :: "'a::real_normed_vector set" assumes "open S" shows "open((λx. a - x) ` S)" using open_translation[OF open_negations[OF assms], of a] by (auto simp: image_image) lemma open_affinity: fixes S :: "'a::real_normed_vector set" assumes "open S" "c ≠ 0" shows "open ((λx. a + c *⇩_{R}x) ` S)" proof - have *: "(λx. a + c *⇩_{R}x) = (λx. a + x) ∘ (λx. c *⇩_{R}x)" unfolding o_def .. have "(+) a ` (*⇩_{R}) c ` S = ((+) a ∘ (*⇩_{R}) c) ` S" by auto then show ?thesis using assms open_translation[of "(*⇩_{R}) c ` S" a] unfolding * by auto qed lemma interior_translation: "interior ((+) a ` S) = (+) a ` (interior S)" for S :: "'a::real_normed_vector set" proof (rule set_eqI, rule) fix x assume "x ∈ interior ((+) a ` S)" then obtain e where "e > 0" and e: "ball x e ⊆ (+) a ` S" unfolding mem_interior by auto then have "ball (x - a) e ⊆ S" unfolding subset_eq Ball_def mem_ball dist_norm by (auto simp: diff_diff_eq) then show "x ∈ (+) a ` interior S" unfolding image_iff by (metis ‹0 < e› add.commute diff_add_cancel mem_interior) next fix x assume "x ∈ (+) a ` interior S" then obtain y e where "e > 0" and e: "ball y e ⊆ S" and y: "x = a + y" unfolding image_iff Bex_def mem_interior by auto { fix z have *: "a + y - z = y + a - z" by auto assume "z ∈ ball x e" then have "z - a ∈ S" using e[unfolded subset_eq, THEN bspec[where x="z - a"]] unfolding mem_ball dist_norm y group_add_class.diff_diff_eq2 * by auto then have "z ∈ (+) a ` S" unfolding image_iff by (auto intro!: bexI[where x="z - a"]) } then have "ball x e ⊆ (+) a ` S" unfolding subset_eq by auto then show "x ∈ interior ((+) a ` S)" unfolding mem_interior using ‹e > 0› by auto qed lemma interior_translation_subtract: "interior ((λx. x - a) ` S) = (λx. x - a) ` interior S" for S :: "'a::real_normed_vector set" using interior_translation [of "- a"] by (simp cong: image_cong_simp) lemma compact_scaling: fixes s :: "'a::real_normed_vector set" assumes "compact s" shows "compact ((λx. c *⇩_{R}x) ` s)" proof - let ?f = "λx. scaleR c x" have *: "bounded_linear ?f" by (rule bounded_linear_scaleR_right) show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f] using linear_continuous_at[OF *] assms by auto qed lemma compact_negations: fixes s :: "'a::real_normed_vector set" assumes "compact s" shows "compact ((λx. - x) ` s)" using compact_scaling [OF assms, of "- 1"] by auto lemma compact_sums: fixes s t :: "'a::real_normed_vector set" assumes "compact s" and "compact t" shows "compact {x + y | x y. x ∈ s ∧ y ∈ t}" proof - have *: "{x + y | x y. x ∈ s ∧ y ∈ t} = (λz. fst z + snd z) ` (s × t)" by (fastforce simp: image_iff) have "continuous_on (s × t) (λz. fst z + snd z)" unfolding continuous_on by (rule ballI) (intro tendsto_intros) then show ?thesis unfolding * using compact_continuous_image compact_Times [OF assms] by auto qed lemma compact_differences: fixes s t :: "'a::real_normed_vector set" assumes "compact s" and "compact t" shows "compact {x - y | x y. x ∈ s ∧ y ∈ t}" proof- have "{x - y | x y. x∈s ∧ y ∈ t} = {x + y | x y. x ∈ s ∧ y ∈ (uminus ` t)}" using diff_conv_add_uminus by force then show ?thesis using compact_sums[OF assms(1) compact_negations[OF assms(2)]] by auto qed lemma compact_sums': fixes S :: "'a::real_normed_vector set" assumes "compact S" and "compact T" shows "compact (⋃x∈ S. ⋃y ∈ T. {x + y})" proof - have "(⋃x∈S. ⋃y∈T. {x + y}) = {x + y |x y. x ∈ S ∧ y ∈ T}" by blast then show ?thesis using compact_sums [OF assms] by simp qed lemma compact_differences': fixes S :: "'a::real_normed_vector set" assumes "compact S" and "compact T" shows "compact (⋃x∈ S. ⋃y ∈ T. {x - y})" proof - have "(⋃x∈S. ⋃y∈T. {x - y}) = {x - y |x y. x ∈ S ∧ y ∈ T}" by blast then show ?thesis using compact_differences [OF assms] by simp qed lemma compact_translation: "compact ((+) a ` s)" if "compact s" for s :: "'a::real_normed_vector set" proof - have "{x + y |x y. x ∈ s ∧ y ∈ {a}} = (λx. a + x) ` s" by auto then show ?thesis using compact_sums [OF that compact_sing [of a]] by auto qed lemma compact_translation_subtract: "compact ((λx. x - a) ` s)" if "compact s" for s :: "'a::real_normed_vector set" using that compact_translation [of s "- a"] by (simp cong: image_cong_simp) lemma compact_affinity: fixes s :: "'a::real_normed_vector set" assumes "compact s" shows "compact ((λx. a + c *⇩_{R}x) ` s)" proof - have "(+) a ` (*⇩_{R}) c ` s = (λx. a + c *⇩_{R}x) ` s" by auto then show ?thesis using compact_translation[OF compact_scaling[OF assms], of a c] by auto qed lemma closed_scaling: fixes S :: "'a::real_normed_vector set" assumes "closed S" shows "closed ((λx. c *⇩_{R}x) ` S)" proof (cases "c = 0") case True then show ?thesis by (auto simp: image_constant_conv) next case False from assms have "closed ((λx. inverse c *⇩_{R}x) -` S)" by (simp add: continuous_closed_vimage) also have "(λx. inverse c *⇩_{R}x) -` S = (λx. c *⇩_{R}x) ` S" using ‹c ≠ 0› by (auto elim: image_eqI [rotated]) finally show ?thesis . qed lemma closed_negations: fixes S :: "'a::real_normed_vector set" assumes "closed S" shows "closed ((λx. -x) ` S)" using closed_scaling[OF assms, of "- 1"] by simp lemma compact_closed_sums: fixes S :: "'a::real_normed_vector set" assumes "compact S" and "closed T" shows "closed (⋃x∈ S. ⋃y ∈ T. {x + y})" proof - let ?S = "{x + y |x y. x ∈ S ∧ y ∈ T}" { fix x l assume as: "∀n. x n ∈ ?S" "(x ⤏ l) sequentially" from as(1) obtain f where f: "∀n. x n = fst (f n) + snd (f n)" "∀n. fst (f n) ∈ S" "∀n. snd (f n) ∈ T" using choice[of "λn y. x n = (fst y) + (snd y) ∧ fst y ∈ S ∧ snd y ∈ T"] by auto obtain l' r where "l'∈S" and r: "strict_mono r" and lr: "(((λn. fst (f n)) ∘ r) ⤏ l') sequentially" using assms(1)[unfolded compact_def, THEN spec[where x="λ n. fst (f n)"]] using f(2) by auto have "((λn. snd (f (r n))) ⤏ l - l') sequentially" using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1) unfolding o_def by auto then have "l - l' ∈ T" using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="λ n. snd (f (r n))"], THEN spec[where x="l - l'"]] using f(3) by auto then have "l ∈ ?S" using ‹l' ∈ S› by force } moreover have "?S = (⋃x∈ S. ⋃y ∈ T. {x + y})" by force ultimately show ?thesis unfolding closed_sequential_limits by (metis (no_types, lifting)) qed lemma closed_compact_sums: fixes S T :: "'a::real_normed_vector set" assumes "closed S" "compact T" shows "closed (⋃x∈ S. ⋃y ∈ T. {x + y})" proof - have "(⋃x∈ T. ⋃y ∈ S. {x + y}) = (⋃x∈ S. ⋃y ∈ T. {x + y})" by auto then show ?thesis using compact_closed_sums[OF assms(2,1)] by simp qed lemma compact_closed_differences: fixes S T :: "'a::real_normed_vector set" assumes "compact S" "closed T" shows "closed (⋃x∈ S. ⋃y ∈ T. {x - y})" proof - have "(⋃x∈ S. ⋃y ∈ uminus ` T. {x + y}) = (⋃x∈ S. ⋃y ∈ T. {x - y})" by force then show ?thesis by (metis assms closed_negations compact_closed_sums) qed lemma closed_compact_differences: fixes S T :: "'a::real_normed_vector set" assumes "closed S" "compact T" shows "closed (⋃x∈ S. ⋃y ∈ T. {x - y})" proof - have "(⋃x∈ S. ⋃y ∈ uminus ` T. {x + y}) = {x - y |x y. x ∈ S ∧ y ∈ T}" by auto then show ?thesis using closed_compact_sums[OF assms(1) compact_negations[OF assms(2)]] by simp qed lemma closed_translation: "closed ((+) a ` S)" if "closed S" for a :: "'a::real_normed_vector" proof - have "(⋃x∈ {a}. ⋃y ∈ S. {x + y}) = ((+) a ` S)" by auto then show ?thesis using compact_closed_sums [OF compact_sing [of a] that] by auto qed lemma closed_translation_subtract: "closed ((λx. x - a) ` S)" if "closed S" for a :: "'a::real_normed_vector" using that closed_translation [of S "- a"] by (simp cong: image_cong_simp) lemma closure_translation: "closure ((+) a ` s) = (+) a ` closure s" for a :: "'a::real_normed_vector" proof - have *: "(+) a ` (- s) = - (+) a ` s" by (auto intro!: image_eqI [where x = "x - a" for x]) show ?thesis using interior_translation [of a "- s", symmetric] by (simp add: closure_interior translation_Compl *) qed lemma closure_translation_subtract: "closure ((λx. x - a) ` s) = (λx. x - a) ` closure s" for a :: "'a::real_normed_vector" using closure_translation [of "- a" s] by (simp cong: image_cong_simp) lemma frontier_translation: "frontier ((+) a ` s) = (+) a ` frontier s" for a :: "'a::real_normed_vector" by (auto simp add: frontier_def translation_diff interior_translation closure_translation) lemma frontier_translation_subtract: "frontier ((+) a ` s) = (+) a ` frontier s" for a :: "'a::real_normed_vector" by (auto simp add: frontier_def translation_diff interior_translation closure_translation) lemma sphere_translation: "sphere (a + c) r = (+) a ` sphere c r" for a :: "'n::real_normed_vector" by (auto simp: dist_norm algebra_simps intro!: image_eqI [where x