Theory HOL-Analysis.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
  "HOL-Library.FuncSet"
  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"
      by (metis y  T diff_add_cancel dist_add_cancel2)
    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"
      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  (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 "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 = {xS. 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) = {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
    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 "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 :: "'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  ycball 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


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 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. c0. 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 ..


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

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 :: "'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. 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"
      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›

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


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"
        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. xs  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 "(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)"
    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 = "x - a" for x])

lemma sphere_translation_subtract:
  "sphere (c - a) r = (λx. x - a) ` sphere c r" for a :: "'n::real_normed_vector"
  using sphere_translation [of "- a" c] by (simp cong: image_cong_simp)

lemma cball_translation:
  "cball (a + c) r = (+) a ` cball c r" for a :: "'n::real_normed_vector"
  by (auto simp: dist_norm algebra_simps intro!: image_eqI [where x = "x - a" for x])

lemma cball_translation_subtract:
  "cball (c - a) r = (λx. x - a) ` cball c r" for a :: "'n::real_normed_vector"
  using cball_translation [of "- a" c] by (simp cong: image_cong_simp)

lemma ball_translation:
  "ball (a + c) r = (+) a ` ball c r" for a :: "'n::real_normed_vector"
  by (auto simp: dist_norm algebra_simps intro!: image_eqI [where x = "x - a" for x])

lemma ball_translation_subtract:
  "ball (c - a) r = (λx. x - a) ` ball c r" for a :: "'n::real_normed_vector"
  using ball_translation [of "- a" c] by (simp cong: image_cong_simp)


subsectiontag unimportant›‹Homeomorphisms›

lemma homeomorphic_scaling:
  fixes S :: "'a::real_normed_vector set"
  assumes "c  0"
  shows "S homeomorphic ((λx. c *R x) ` S)"
  unfolding homeomorphic_minimal
  apply (rule_tac x="λx. c *R x" in exI)
  apply (rule_tac x="λx. (1 / c) *R x" in exI)
  using assms by (auto simp: continuous_intros)

lemma homeomorphic_translation:
  fixes S :: "'a::real_normed_vector set"
  shows "S homeomorphic ((λx. a + x) ` S)"
  unfolding homeomorphic_minimal
  apply (rule_tac x="λx. a + x" in exI)
  apply (rule_tac x="λx. -a + x" in exI)
  by (auto simp: continuous_intros)

lemma homeomorphic_affinity:
  fixes S :: "'a::real_normed_vector set"
  assumes "c  0"
  shows "S homeomorphic ((λx. a + c *R x) ` S)"
proof -
  have *: "(+) a ` (*R) c ` S = (λx. a + c *R x) ` S" by auto
  show ?thesis
    by (metis "*" assms homeomorphic_scaling homeomorphic_trans homeomorphic_translation)
qed

lemma homeomorphic_balls:
  fixes a b ::"'a::real_normed_vector"
  assumes "0 < d"  "0 < e"
  shows "(ball a d) homeomorphic  (ball b e)" (is ?th)
    and "(cball a d) homeomorphic (cball b e)" (is ?cth)
proof -
  show ?th unfolding homeomorphic_minimal
    apply(rule_tac x="λx. b + (e/d) *R (x - a)" in exI)
    apply(rule_tac x="λx. a + (d/e) *R (x - b)" in exI)
    using assms
    by (auto intro!: continuous_intros simp: dist_commute dist_norm pos_divide_less_eq)
  show ?cth unfolding homeomorphic_minimal
    apply(rule_tac x="λx. b + (e/d) *R (x - a)" in exI)
    apply(rule_tac x="λx. a + (d/e) *R (x - b)" in exI)
    using assms
    by (auto intro!: continuous_intros simp: dist_commute dist_norm pos_divide_le_eq)
qed

lemma homeomorphic_spheres:
  fixes a b ::"'a::real_normed_vector"
  assumes "0 < d"  "0 < e"
  shows "(sphere a d) homeomorphic (sphere b e)"
unfolding homeomorphic_minimal
    apply(rule_tac x="λx. b + (e/d) *R (x - a)" in exI)
    apply(rule_tac x="λx. a + (d/e) *R (x - b)" in exI)
    using assms
    by (auto intro!: continuous_intros simp: dist_commute dist_norm pos_divide_less_eq)

lemma homeomorphic_ball01_UNIV:
  "ball (0::'a::real_normed_vector) 1 homeomorphic (UNIV:: 'a set)"
  (is "?B homeomorphic ?U")
proof
  have "x  (λz. z /R (1 - norm z)) ` ball 0 1" for x::'a
    apply (rule_tac x="x /R (1 + norm x)" in image_eqI)
     apply (auto simp: field_split_simps)
    using norm_ge_zero [of x] apply linarith+
    done
  then show "(λz::'a. z /R (1 - norm z)) ` ?B = ?U"
    by blast
  have "x  range (λz. (1 / (1 + norm z)) *R z)" if "norm x < 1" for x::'a
    using that
    by (rule_tac x="x /R (1 - norm x)" in image_eqI) (auto simp: field_split_simps)
  then show "(λz::'a. z /R (1 + norm z)) ` ?U = ?B"
    by (force simp: field_split_simps dest: add_less_zeroD)
  show "continuous_on (ball 0 1) (λz. z /R (1 - norm z))"
    by (rule continuous_intros | force)+
  have 0: "z. 1 + norm z  0"
    by (metis (no_types) le_add_same_cancel1 norm_ge_zero not_one_le_zero)
  then show "continuous_on UNIV (λz. z /R (1 + norm z))"
    by (auto intro!: continuous_intros)
  show "x. x  ball 0 1 
         x /R (1 - norm x) /R (1 + norm (x /R (1 - norm x))) = x"
    by (auto simp: field_split_simps)
  show "y. y /R (1 + norm y) /R (1 - norm (y /R (1 + norm y))) = y"
    using 0 by (auto simp: field_split_simps)
qed

proposition homeomorphic_ball_UNIV:
  fixes a ::"'a::real_normed_vector"
  assumes "0 < r" shows "ball a r homeomorphic (UNIV:: 'a set)"
  using assms homeomorphic_ball01_UNIV homeomorphic_balls(1) homeomorphic_trans zero_less_one by blast


subsectiontag unimportant› ‹Discrete›

lemma finite_implies_discrete:
  fixes S :: "'a::topological_space set"
  assumes "finite (f ` S)"
  shows "(x  S. e>0. y. y  S  f y  f x  e  norm (f y - f x))"
proof -
  have "e>0. y. y  S  f y  f x  e  norm (f y - f x)" if "x  S" for x
  proof (cases "f ` S - {f x} = {}")
    case True
    with zero_less_numeral show ?thesis
      by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
  next
    case False
    then obtain z where "z  S" "f z  f x"
      by blast
    moreover have finn: "finite {norm (z - f x) |z. z  f ` S - {f x}}"
      using assms by simp
    ultimately have *: "0 < Inf{norm(z - f x) | z. z  f ` S - {f x}}"
      by (force intro: finite_imp_less_Inf)
    show ?thesis
      by (force intro!: * cInf_le_finite [OF finn])
  qed
  with assms show ?thesis
    by blast
qed


subsectiontag unimportant› ‹Completeness of "Isometry" (up to constant bounds)›

lemma cauchy_isometric:― ‹TODO: rename lemma to Cauchy_isometric›
  assumes e: "e > 0"
    and s: "subspace s"
    and f: "bounded_linear f"
    and normf: "xs. norm (f x)  e * norm x"
    and xs: "n. x n  s"
    and cf: "Cauchy (f  x)"
  shows "Cauchy x"
proof -
  interpret f: bounded_linear f by fact
  have "N. nN. norm (x n - x N) < d" if "d > 0" for d :: real
  proof -
    from that obtain N where N: "nN. norm (f (x n) - f (x N)) < e * d"
      using cf[unfolded Cauchy_def o_def dist_norm, THEN spec[where x="e*d"]] e
      by auto
    have "norm (x n - x N) < d" if "n  N" for n
    proof -
      have "e * norm (x n - x N)  norm (f (x n - x N))"
        using subspace_diff[OF s, of "x n" "x N"]
        using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
        using normf[THEN bspec[where x="x n - x N"]]
        by auto
      also have "norm (f (x n - x N)) < e * d"
        using N  n N unfolding f.diff[symmetric] by auto
      finally show ?thesis
        using e>0 by simp
    qed
    then show ?thesis by auto
  qed
  then show ?thesis
    by (simp add: Cauchy_altdef2 dist_norm)
qed

lemma complete_isometric_image:
  assumes "0 < e"
    and s: "subspace s"
    and f: "bounded_linear f"
    and normf: "xs. norm(f x)  e * norm(x)"
    and cs: "complete s"
  shows "complete (f ` s)"
proof -
  have "lf ` s. (g  l) sequentially"
    if as:"n::nat. g n  f ` s" and cfg:"Cauchy g" for g
  proof -
    from that obtain x where "n. x n  s  g n = f (x n)"
      using choice[of "λ n xa. xa  s  g n = f xa"] by auto
    then have x: "n. x n  s" "n. g n = f (x n)" by auto
    then have "f  x = g" by (simp add: fun_eq_iff)
    then obtain l where "ls" and l:"(x  l) sequentially"
      using cs[unfolded complete_def, THEN spec[where x=x]]
      using cauchy_isometric[OF 0 < e s f normf] and cfg and x(1)
      by auto
    then show ?thesis
      using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l]
      by (auto simp: f  x = g)
  qed
  then show ?thesis
    unfolding complete_def by auto
qed

subsection ‹Connected Normed Spaces›

lemma compact_components:
  fixes s :: "'a::heine_borel set"
  shows "compact s; c  components s  compact c"
by (meson bounded_subset closed_components in_components_subset compact_eq_bounded_closed)

lemma discrete_subset_disconnected:
  fixes S :: "'a::topological_space set"
  fixes t :: "'b::real_normed_vector set"
  assumes conf: "continuous_on S f"
      and no: "x. x  S  e>0. y. y  S  f y  f x  e  norm (f y - f x)"
   shows "f ` S  {y. connected_component_set (f ` S) y = {y}}"
proof -
  { fix x assume x: "x  S"
    then obtain e where "e>0" and ele: "y. y  S; f y  f x  e  norm (f y - f x)"
      using conf no [OF x] by auto
    then have e2: "0  e/2"
      by simp
    define F where "F  connected_component_set (f ` S) (f x)"
    have False if "y  S" and ccs: "f y  F" and not: "f y  f x" for y 
    proof -
      define C where "C  cball (f x) (e/2)"
      define D where "D  - ball (f x) e"
      have disj: "C  D = {}"
        unfolding C_def D_def using 0 < e by fastforce
      moreover have FCD: "F  C  D"
      proof -
        have "t  C  t  D" if "t  F" for t
        proof -
          obtain y where "y  S" "t = f y"
            using F_def t  F connected_component_in by blast
          then show ?thesis
            by (metis C_def ComplI D_def centre_in_cball dist_norm e2 ele mem_ball norm_minus_commute not_le)
        qed
        then show ?thesis
          by auto
      qed
      ultimately have "C  F = {}  D  F = {}"
        using connected_closed [of "F"] e>0 not
        unfolding C_def D_def
        by (metis Elementary_Metric_Spaces.open_ball F_def closed_cball connected_connected_component inf_bot_left open_closed)
      moreover have "C  F  {}"
        unfolding disjoint_iff
        by (metis FCD ComplD image_eqI mem_Collect_eq subsetD x  D_def F_def Un_iff 0 < e centre_in_ball connected_component_refl_eq)
      moreover have "D  F  {}"
        unfolding disjoint_iff
        by (metis ComplI D_def ccs dist_norm ele mem_ball norm_minus_commute not not_le that(1))
      ultimately show ?thesis by metis
    qed
    moreover have "connected_component_set (f ` S) (f x)  f ` S"
      by (auto simp: connected_component_in)
    ultimately have "connected_component_set (f ` S) (f x) = {f x}"
      by (auto simp: x F_def)
  }
  with assms show ?thesis
    by blast
qed

lemma continuous_disconnected_range_constant_eq:
      "(connected S 
           (f::'a::topological_space  'b::real_normed_algebra_1.
            t. continuous_on S f  f ` S  t  (y  t. connected_component_set t y = {y})
             f constant_on S))" (is ?thesis1)
  and continuous_discrete_range_constant_eq:
      "(connected S 
         (f::'a::topological_space  'b::real_normed_algebra_1.
          continuous_on S f 
          (x  S. e. 0 < e  (y. y  S  (f y  f x)  e  norm(f y - f x)))
           f constant_on S))" (is ?thesis2)
  and continuous_finite_range_constant_eq:
      "(connected S 
         (f::'a::topological_space  'b::real_normed_algebra_1.
          continuous_on S f  finite (f ` S)
           f constant_on S))" (is ?thesis3)
proof -
  have *: "s t u v. s  t; t  u; u  v; v  s
     (s  t)  (s  u)  (s  v)"
    by blast
  have "?thesis1  ?thesis2  ?thesis3"
    apply (rule *)
    using continuous_disconnected_range_constant
    apply (metis image_subset_iff_funcset)
    apply (smt (verit, best) discrete_subset_disconnected mem_Collect_eq subsetD subsetI)
    apply (blast dest: finite_implies_discrete)
    apply (blast intro!: finite_range_constant_imp_connected)
    done
  then show ?thesis1 ?thesis2 ?thesis3
    by blast+
qed

lemma continuous_discrete_range_constant:
  fixes f :: "'a::topological_space  'b::real_normed_algebra_1"
  assumes S: "connected S"
      and "continuous_on S f"
      and "x. x  S  e>0. y. y  S  f y  f x  e  norm (f y - f x)"
    shows "f constant_on S"
  using continuous_discrete_range_constant_eq [THEN iffD1, OF S] assms by blast

lemma continuous_finite_range_constant:
  fixes f :: "'a::topological_space  'b::real_normed_algebra_1"
  assumes "connected S"
      and "continuous_on S f"
      and "finite (f ` S)"
    shows "f constant_on S"
  using assms continuous_finite_range_constant_eq  by blast

end