# Theory Elementary_Normed_Spaces

(*  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

Elementary_Metric_Spaces Cartesian_Space
Connected
begin
subsection ‹Orthogonal Transformation of Balls›

subsectiontag 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  xS. yT. z = x + y"
then show "e>0. z. dist z (x + y) < e  (xS. yT. 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  xS. yT. z = x + y"
then show "e>0. z. dist z (x + y) < e  (xS. yT. z = x + y)"
using 0 < e y  T by blast
qed
qed

lemma image_orthogonal_transformation_ball:
fixes f :: "'a::euclidean_space  'a"
assumes
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
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 = {xS. f x  0}"

lemma in_support_on: "x  support_on S f  x  S  f x  0"

lemma support_on_simps[simp]:

"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) = {xA. 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 = (xsupport_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 xy  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 xy[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
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
show "zball 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" "yS"
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 ::
shows "compact (sphere a r)"
using compact_frontier [of "cball a r"] by simp

corollary bounded_sphere [simp]:
fixes a ::
shows "bounded (sphere a r)"

corollary closed_sphere  [simp]:
fixes a ::
shows "closed (sphere a r)"

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"
then show ?thesis
qed

fixes a :: "'a::real_normed_vector"
shows "(+) b ` cball a r = cball (a+b) r"
proof -
have "x. dist (a + b) x  r  ycball a r. x = b + y"
then show ?thesis
qed

subsectiontag 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 ]) (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 ]) (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. c0. b - a = scaleR c v}"

subsection ‹Trivial Limits›

lemma trivial_limit_at_infinity:

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"

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"
also have "  ¦f x¦ * (¦B¦ + 1)"
also have " < ε"
by (rule f)
finally show ?thesis .
qed
have "x. ¦f x¦ < ε / (¦B¦ + 1); norm (g x)  B  ¦f x¦ * norm (g x) < ε"
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
shows "((λx. h (f x) (g x))  (h l m)) net"
using  (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 ..

subsectiontag 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 ])
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
shows "bounded (f ` S)"
proof -
from assms(1) obtain b where "b > 0" and b: "xS. 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)"

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" "xS. 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. xS  norm (f x)  B" "x. xS  norm (g x)  C"
then have "x. x  S  norm (f x + g x)  B + C"
} 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})"

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))"
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)

subsectiontag 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 ::
shows "¬ compact (UNIV::'a set)"

lemma not_compact_space_euclideanreal [simp]:

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. nN. 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"
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 =
case False
then have gin: "?g n  𝒢" for n
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))"
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))"
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›

subsubsectiontag unimportant› ‹Structural rules for uniform continuity›

lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]:
fixes g :: "_::metric_space  _"
assumes
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
and
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]],
}
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
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
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
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 .

fixes f g :: "'a::metric_space  'b::real_normed_vector"
assumes
and
shows "uniformly_continuous_on s (λx. f x + g x)"
using assms
unfolding uniformly_continuous_on_sequentially

lemma uniformly_continuous_on_diff[continuous_intros]:
fixes f :: "'a::metric_space  'b::real_normed_vector"
assumes
and
shows "uniformly_continuous_on s (λx. f x - g x)"
using assms uniformly_continuous_on_add [of s f "- g"]

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. iI. f i x)"
by (induction I rule: infinite_finite_induct)

subsectiontag 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"
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:
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
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. xs  y  t} = {x + y | x y. x  s  y  (uminus ` t)}"
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 "(xS. yT. {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 "(xS. yT. {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)"
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