SSL Elementary_Normed_Spaces.thy Sprache: Isabelle

(*  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 \<open>Elementary Normed Vector Spaces\<close>

theory Elementary_Normed_Spaces
  imports
  "HOL-Library.FuncSet"
  Elementary_Metric_Spaces Cartesian_Space
  Connected
begin
subsection \<open>Orthogonal Transformation of Balls\<close>

subsection\<^marker>\<open>tag unimportant\<close> \<open>Various Lemmas Combining Imports\<close>

lemma open_sums:
  fixes T :: "('b::real_normed_vector) set"
  assumes "open S \ open T"
  shows "open (\x\ S. \y \ T. {x + y})"
  using assms
proof
  assume S: "open S"
  show ?thesis
  proof (clarsimp simp: open_dist)
    fix x y
    assume "x \ S" "y \ T"
    with S obtain e where "e > 0" and e: "\x'. dist x' x < e \ x' \ S"
      by (auto simp: open_dist)
    then have "\z. dist z (x + y) < e \ \x\S. \y\T. z = x + y"
      by (metis \<open>y \<in> T\<close> diff_add_cancel dist_add_cancel2)
    then show "\e>0. \z. dist z (x + y) < e \ (\x\S. \y\T. z = x + y)"
      using \<open>0 < e\<close> \<open>x \<in> S\<close> by blast
  qed
next
  assume T: "open T"
  show ?thesis
  proof (clarsimp simp: open_dist)
    fix x y
    assume "x \ S" "y \ T"
    with T obtain e where "e > 0" and e: "\x'. dist x' y < e \ x' \ T"
      by (auto simp: open_dist)
    then have "\z. dist z (x + y) < e \ \x\S. \y\T. z = x + y"
      by (metis \<open>x \<in> S\<close> add_diff_cancel_left' add_diff_eq diff_diff_add dist_norm)
    then show "\e>0. \z. dist z (x + y) < e \ (\x\S. \y\T. z = x + y)"
      using \<open>0 < e\<close> \<open>y \<in> T\<close> 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 \<open>Support\<close>

definition (in monoid_add) support_on :: "'b set \ ('b \ 'a) \ 'b set"
  where "support_on S f = {x\S. f x \ 0}"

lemma in_support_on: "x \ support_on S f \ x \ S \ f x \ 0"
  by (simp add: support_on_def)

lemma support_on_simps[simp]:
  "support_on {} f = {}"
  "support_on (insert x S) f =
    (if f x = 0 then support_on S f else insert x (support_on S f))"
  "support_on (S \ T) f = support_on S f \ support_on T f"
  "support_on (S \ T) f = support_on S f \ support_on T f"
  "support_on (S - T) f = support_on S f - support_on T f"
  "support_on (f ` S) g = f ` (support_on S (g \ f))"
  unfolding support_on_def by auto

lemma support_on_cong:
  "(\x. x \ S \ f x = 0 \ g x = 0) \ support_on S f = support_on S g"
  by (auto simp: support_on_def)

lemma support_on_if: "a \ 0 \ support_on A (\x. if P x then a else 0) = {x\A. P x}"
  by (auto simp: support_on_def)

lemma support_on_if_subset: "support_on A (\x. if P x then a else 0) \ {x \ A. P x}"
  by (auto simp: support_on_def)

lemma finite_support[intro]: "finite S \ finite (support_on S f)"
  unfolding support_on_def by auto

(* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *)
definition (in comm_monoid_add) supp_sum :: "('b \ 'a) \ 'b set \ 'a"
  where "supp_sum f S = (\x\support_on S f. f x)"

lemma supp_sum_empty[simp]: "supp_sum f {} = 0"
  unfolding supp_sum_def by auto

lemma supp_sum_insert[simp]:
  "finite (support_on S f) \
    supp_sum f (insert x S) = (if x \<in> 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 \<open>Intervals\<close>

lemma image_affinity_interval:
  fixes c :: "'a::ordered_real_vector"
  shows "((\x. m *\<^sub>R x + c) ` {a..b}) =
           (if {a..b}={} then {}
            else if 0 \<le> m then {m *\<^sub>R a + c .. m  *\<^sub>R b + c}
            else {m *\<^sub>R b + c .. m *\<^sub>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 *\<^sub>R a + c..m *\<^sub>R b + c}\
            \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x
        using False
        by (rule_tac x="inverse m *\<^sub>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 *\<^sub>R b + c..m *\<^sub>R a + c}\
            \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x
        by (rule_tac x="inverse m *\<^sub>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 \<open>Limit Points\<close>

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 \<open>?lhs\<close>
        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] \<open>?lhs\<close>
      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 \<open>d \<le> dist x y\<close> \<open>d>0\<close> by auto
          then show ?thesis
            by auto
        next
          case False
          have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) =
            norm (x - y + (d / (2 * norm (y - x))) *\<^sub>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 \<open>x\<noteq>y\<close>  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)) *\<^sub>R (y - x) \ ball x e" using \d>0\
            by auto
          moreover
          have "(d / (2*dist y x)) *\<^sub>R (y - x) \ 0"
            using \<open>x\<noteq>y\<close>[unfolded dist_nz] \<open>d>0\<close> unfolding scaleR_eq_0_iff
            by (auto simp: dist_commute)
          moreover
          have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d"
            using \<open>0 < d\<close> by (fastforce simp: dist_norm)
          ultimately show ?thesis
            by (rule_tac x = "y - (d / (2*dist y x)) *\<^sub>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 \<open>d > 0\<close> \<open>e>0\<close> by auto
          show ?thesis
            by (metis True z dist_commute mem_ball min_less_iff_conj)
        next
          case False
          then show ?thesis
            using \<open>d>0\<close> \<open>d > dist x y\<close> \<open>?rhs\<close> 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
  \<comment>\<open>choose point between @{term x} and @{term y}, within distance @{term r} of @{term y}.\<close>
  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 \<open>0 < r\<close>
    by (simp add: dist_norm min_def)
  then have "z \ T"
    using \<open>\<forall>z. dist z y < r \<longrightarrow> z \<in> T\<close> by simp
  have "dist x z < dist x y"
    using \<open>0 < r\<close> 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 \<open>x \<noteq> y\<close> \<open>0 < r\<close>
    by (simp add: min_def)
  show "\z\ball x (dist x y). z \ T \ z \ y"
    using \<open>z \<in> ball x (dist x y)\<close> \<open>z \<in> T\<close> \<open>z \<noteq> y\<close>
    by fast
qed

subsection \<open>Balls and Spheres in Normed Spaces\<close>

lemma mem_ball_0 [simp]: "x \ ball 0 e \ norm x < e"
  for x :: "'a::real_normed_vector"
  by simp

lemma mem_cball_0 [simp]: "x \ cball 0 e \ norm x \ e"
  for x :: "'a::real_normed_vector"
  by simp

lemma closure_ball [simp]:
  fixes x :: "'a::real_normed_vector"
  assumes "0 < e"
  shows "closure (ball x e) = cball x e"
proof
  show "closure (ball x e) \ cball x e"
    using closed_cball closure_minimal by blast
  have "\y. dist x y < e \ dist x y = e \ y \ closure (ball x e)"
    by (metis Un_iff assms closure_ball_lemma closure_def dist_eq_0_iff mem_Collect_eq mem_ball)
  then show "cball x e \ closure (ball x e)"
    by force
qed

lemma mem_sphere_0 [simp]: "x \ sphere 0 e \ norm x = e"
  for x :: "'a::real_normed_vector"
  by simp

(* In a trivial vector space, this fails for e = 0. *)
lemma interior_cball [simp]:
  fixes x :: "'a::{real_normed_vector, perfect_space}"
  shows "interior (cball x e) = ball x e"
proof (cases "e \ 0")
  case False note cs = this
  from cs have null: "ball x e = {}"
    using ball_empty[of e x] by auto
  moreover
  have "cball x e = {}"
  proof (rule equals0I)
    fix y
    assume "y \ cball x e"
    then show False
      by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball
          subset_antisym subset_ball)
  qed
  then have "interior (cball x e) = {}"
    using interior_empty by auto
  ultimately show ?thesis by blast
next
  case True note cs = this
  have "ball x e \ cball x e"
    using ball_subset_cball by auto
  moreover
  {
    fix S y
    assume as: "S \ cball x e" "open S" "y\S"
    then obtain d where "d>0" and d: "\x'. dist x' y < d \ x' \ S"
      unfolding open_dist by blast
    then obtain xa where xa_y: "xa \ y" and xa: "dist xa y < d"
      using perfect_choose_dist [of d] by auto
    have "xa \ S"
      using d[THEN spec[where x = xa]]
      using xa by (auto simp: dist_commute)
    then have xa_cball: "xa \ cball x e"
      using as(1) by auto
    then have "y \ ball x e"
    proof (cases "x = y")
      case True
      then have "e > 0" using cs order.order_iff_strict xa_cball xa_y by fastforce
      then show "y \ ball x e"
        using \<open>x = y \<close> by simp
    next
      case False
      have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) y < d"
        unfolding dist_norm
        using \<open>d>0\<close> norm_ge_zero[of "y - x"] \<open>x \<noteq> y\<close> by auto
      then have *: "y + (d / 2 / dist y x) *\<^sub>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 \<open>d>0\<close> by auto
      have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x =
        norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)"
        by (auto simp: dist_norm algebra_simps)
      also have "\ = norm ((1 + d / (2 * norm (y - x))) *\<^sub>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 \<open>d>0\<close> by auto
    qed
  }
  then have "\S \ cball x e. open S \ S \ ball x e"
    by auto
  ultimately show ?thesis
    using interior_unique[of "ball x e" "cball x e"]
    using open_ball[of x e]
    by auto
qed

lemma frontier_ball [simp]:
  fixes a :: "'a::real_normed_vector"
  shows "0 < e \ frontier (ball a e) = sphere a e"
  by (force simp: frontier_def)

lemma frontier_cball [simp]:
  fixes a :: "'a::{real_normed_vector, perfect_space}"
  shows "frontier (cball a e) = sphere a e"
  by (force simp: frontier_def)

corollary compact_sphere [simp]:
  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
  shows "compact (sphere a r)"
using compact_frontier [of "cball a r"] by simp

corollary bounded_sphere [simp]:
  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
  shows "bounded (sphere a r)"
by (simp add: compact_imp_bounded)

corollary closed_sphere  [simp]:
  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
  shows "closed (sphere a r)"
by (simp add: compact_imp_closed)

lemma image_add_ball [simp]:
  fixes a :: "'a::real_normed_vector"
  shows "(+) b ` ball a r = ball (a+b) r"
proof -
  { fix x :: 'a
    assume "dist (a + b) x < r"
    moreover
    have "b + (x - b) = x"
      by simp
    ultimately have "x \ (+) b ` ball a r"
      by (metis add.commute dist_add_cancel image_eqI mem_ball) }
  then show ?thesis
    by (auto simp: add.commute)
qed

lemma image_add_cball [simp]:
  fixes a :: "'a::real_normed_vector"
  shows "(+) b ` cball a r = cball (a+b) r"
proof -
  have "\x. dist (a + b) x \ r \ \y\cball a r. x = b + y"
    by (metis (no_types) add.commute diff_add_cancel dist_add_cancel2 mem_cball)
  then show ?thesis
    by (force simp: add.commute)
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Various Lemmas on Normed Algebras\<close>

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 \<open>dist y x < 1\<close> show "y = x"
    by (auto elim!: Ints_cases simp: dist_of_int)
qed

subsection \<open>Filters\<close>

definition indirection :: "'a::real_normed_vector \ 'a \ 'a filter" (infixr \indirection\ 70)
  where "a indirection v = at a within {b. \c\0. b - a = scaleR c v}"

subsection \<open>Trivial Limits\<close>

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) *\<^sub>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 \<open>Limits\<close>

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)
         \<Longrightarrow> ((f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f \<longlongrightarrow> 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 "\\<^sub>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 "\\<^sub>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 *\<^sub>R g n) \ 0) net"
proof
  fix \<epsilon>::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 "\\<^sub>F x in net. dist (f x *\<^sub>R g x) 0 < \"
    using \<open>0 < \<epsilon>\<close> 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\<open>Limit under bilinear function\<close>

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 \<open>bounded_bilinear h\<close> \<open>(f \<longlongrightarrow> l) net\<close> \<open>(g \<longlongrightarrow> m) net\<close>
  by (rule bounded_bilinear.tendsto)

lemma Lim_at_zero:
  fixes a :: "'a::real_normed_vector"
    and l :: "'b::topological_space"
  shows "(f \ l) (at a) \ ((\x. f(a + x)) \ l) (at 0)"
  using LIM_offset_zero LIM_offset_zero_cancel ..

subsection\<^marker>\<open>tag unimportant\<close> \<open>Limit Point of Filter\<close>

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 \<open>Boundedness\<close>

lemma continuous_on_closure_norm_le:
  fixes f :: "'a::metric_space \ 'b::real_normed_vector"
  assumes "continuous_on (closure s) f"
    and "\y \ s. norm(f y) \ b"
    and "x \ (closure s)"
  shows "norm (f x) \ b"
proof -
  have *: "f ` s \ cball 0 b"
    using assms(2)[unfolded mem_cball_0[symmetric]] by auto
  show ?thesis
    by (meson "*" assms(1) assms(3) closed_cball image_closure_subset image_subset_iff mem_cball_0)
qed

lemma bounded_pos: "bounded S \ (\b>0. \x\ S. norm x \ b)"
  unfolding bounded_iff
  by (meson less_imp_le not_le order_trans zero_less_one)

lemma bounded_pos_less: "bounded S \ (\b>0. \x\ S. norm x < b)"
  by (metis bounded_pos le_less_trans less_imp_le linordered_field_no_ub)

lemma bounded_normE:
  assumes "bounded A"
  obtains B where "B > 0" "\z. z \ A \ norm z \ B"
  by (meson assms bounded_pos)

lemma bounded_normE_less:
  assumes "bounded A"
  obtains B where "B > 0" "\z. z \ A \ norm z < B"
  by (meson assms bounded_pos_less)

lemma Bseq_eq_bounded:
  fixes f :: "nat \ 'a::real_normed_vector"
  shows "Bseq f \ bounded (range f)"
  unfolding Bseq_def bounded_pos by auto

lemma bounded_linear_image:
  assumes "bounded S"
    and "bounded_linear f"
  shows "bounded (f ` S)"
proof -
  from assms(1) obtain b where "b > 0" and b: "\x\S. norm x \ b"
    unfolding bounded_pos by auto
  from assms(2) obtain B where B: "B > 0" "\x. norm (f x) \ B * norm x"
    using bounded_linear.pos_bounded by (auto simp: ac_simps)
  show ?thesis
    unfolding bounded_pos
  proof (intro exI, safe)
    show "norm (f x) \ B * b" if "x \ S" for x
      by (meson B b less_imp_le mult_left_mono order_trans that)
  qed (use \<open>b > 0\<close> \<open>B > 0\<close> in auto)
qed

lemma bounded_scaling:
  fixes S :: "'a::real_normed_vector set"
  shows "bounded S \ bounded ((\x. c *\<^sub>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 *\<^sub>R f x) ` S)"
  using bounded_scaling[of "f ` S" r] assms
  by (auto simp: image_image)

lemma bounded_translation:
  fixes S :: "'a::real_normed_vector set"
  assumes "bounded S"
  shows "bounded ((\x. a + x) ` S)"
proof -
  from assms obtain b where b: "b > 0" "\x\S. norm x \ b"
    unfolding bounded_pos by auto
  {
    fix x
    assume "x \ S"
    then have "norm (a + x) \ b + norm a"
      using norm_triangle_ineq[of a x] b by auto
  }
  then show ?thesis
    unfolding bounded_pos
    using norm_ge_zero[of a] b(1) and add_strict_increasing[of b 0 "norm a"]
    by (auto intro!: exI[of _ "b + norm a"])
qed

lemma bounded_translation_minus:
  fixes S :: "'a::real_normed_vector set"
  shows "bounded S \ bounded ((\x. x - a) ` S)"
using bounded_translation [of S "-a"] by simp

lemma bounded_uminus [simp]:
  fixes X :: "'a::real_normed_vector set"
  shows "bounded (uminus ` X) \ bounded X"
by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp: add.commute norm_minus_commute)

lemma uminus_bounded_comp [simp]:
  fixes f :: "'a \ 'b::real_normed_vector"
  shows "bounded ((\x. - f x) ` S) \ bounded (f ` S)"
  using bounded_uminus[of "f ` S"]
  by (auto simp: image_image)

lemma bounded_plus_comp:
  fixes f g::"'a \ 'b::real_normed_vector"
  assumes "bounded (f ` S)"
  assumes "bounded (g ` S)"
  shows "bounded ((\x. f x + g x) ` S)"
proof -
  {
    fix B C
    assume "\x. x\S \ norm (f x) \ B" "\x. x\S \ norm (g x) \ C"
    then have "\x. x \ S \ norm (f x + g x) \ B + C"
      by (auto intro!: norm_triangle_le add_mono)
  } then show ?thesis
    using assms by (fastforce simp: bounded_iff)
qed

lemma bounded_plus:
  fixes S ::"'a::real_normed_vector set"
  assumes "bounded S" "bounded T"
  shows "bounded ((\(x,y). x + y) ` (S \ T))"
  using bounded_plus_comp [of fst "S \ T" snd] assms
  by (auto simp: split_def split: if_split_asm)

lemma bounded_minus_comp:
  "bounded (f ` S) \ bounded (g ` S) \ bounded ((\x. f x - g x) ` S)"
  for f g::"'a \ 'b::real_normed_vector"
  using bounded_plus_comp[of "f" S "\x. - g x"]
  by auto

lemma bounded_minus:
  fixes S ::"'a::real_normed_vector set"
  assumes "bounded S" "bounded T"
  shows "bounded ((\(x,y). x - y) ` (S \ T))"
  using bounded_minus_comp [of fst "S \ T" snd] assms
  by (auto simp: split_def split: if_split_asm)

lemma bounded_sums:
  fixes S :: "'a::real_normed_vector set"
  assumes "bounded S" and "bounded T"
  shows "bounded (\x\ S. \y \ T. {x + y})"
  using assms by (simp add: bounded_iff) (meson norm_triangle_mono)

lemma bounded_differences:
  fixes S :: "'a::real_normed_vector set"
  assumes "bounded S" and "bounded T"
  shows "bounded (\x\ S. \y \ T. {x - y})"
  using assms by (simp add: bounded_iff) (meson add_mono norm_triangle_le_diff)

lemma not_bounded_UNIV[simp]:
  "\ bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)"
proof (auto simp: bounded_pos not_le)
  obtain x :: 'a where "x \ 0"
    using perfect_choose_dist [OF zero_less_one] by fast
  fix b :: real
  assume b: "b >0"
  have b1: "b +1 \ 0"
    using b by simp
  with \<open>x \<noteq> 0\<close> have "b < norm (scaleR (b + 1) (sgn x))"
    by (simp add: norm_sgn)
  then show "\x::'a. b < norm x" ..
qed

corollary cobounded_imp_unbounded:
    fixes S :: "'a::{real_normed_vector, perfect_space} set"
    shows "bounded (- S) \ \ bounded S"
  using bounded_Un [of S "-S"]  by (simp)

subsection\<^marker>\<open>tag unimportant\<close>\<open>Relations among convergence and absolute convergence for power series\<close>

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 {..
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 \<open>Normed spaces with the Heine-Borel property\<close>

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\<open>Representing sets as the union of a chain of compact sets.\<close>
lemma closed_Union_compact_subsets:
  fixes S :: "'a::{heine_borel,real_normed_vector} set"
  assumes "closed S"
  obtains F where "\n. compact(F n)" "\n. F n \ S" "\n. F n \ F(Suc n)"
                  "(\n. F n) = S" "\K. \compact K; K \ S\ \ \N. \n \ N. K \ F n"
proof
  show "compact (S \ cball 0 (of_nat n))" for n
    using assms compact_eq_bounded_closed by auto
next
  show "(\n. S \ cball 0 (real n)) = S"
    by (auto simp: real_arch_simple)
next
  fix K :: "'a set"
  assume "compact K" "K \ S"
  then obtain N where "K \ cball 0 N"
    by (meson bounded_pos mem_cball_0 compact_imp_bounded subsetI)
  then show "\N. \n\N. K \ S \ cball 0 (real n)"
    by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans)
qed auto

subsection \<open>Intersecting chains of compact sets and the Baire property\<close>

proposition bounded_closed_chain:
  fixes \<F> :: "'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 \<G> rule: finite_induct)
      case empty
      with assms show ?case by force
    next
      case (insert U \<G>)
      then have "U \ \" and ne: "B \ \\ \ {}" by auto
      then consider "B \ U" | "U \ B"
          using \<open>B \<in> \<F>\<close> 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 \<open>U \<in> \<F>\<close> \<open>{} \<notin> \<F>\<close> 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 \<open>U \<noteq> {}\<close>)
            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 \<F> :: "'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\<open>The Baire property of dense sets\<close>
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 \<inter> closure Y \<subseteq> ?g n \<and> closure Y \<subseteq> ball x e) \<and> Y \<subseteq> 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 \<open>openin (top_of_set S) U\<close> by (auto simp: openin_subtopology)
        with \<open>U \<noteq> {}\<close> have "T \<inter> closure (?g n) \<noteq> {}"
          using gin ope by fastforce
        then have "T \ ?g n \ {}"
          using \<open>open T\<close> 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 \<open>0 < d\<close> \<open>y \<in> U\<close> 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 \<open>d > 0\<close> 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 \<open>d > 0\<close> 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: \<open>closed S\<close> 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 ?\<Phi> = "\<lambda>n X. openin (top_of_set S) X \<and> X \<noteq> {} \<and>
                      S \<inter> closure X \<subseteq> ?g n \<and> closure X \<subseteq> 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 \<open>e > 0\<close> 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 \<open>0 < e\<close> \<open>x \<in> S\<close> 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 \<open>closed S\<close>])
      show "\n. S \ closure (TF n) \ {}"
        by (metis Int_absorb1 opeF \<open>closed S\<close> 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 \<open>countable \<G>\<close>] 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 \<open>Continuity\<close>

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Structural rules for uniform continuity\<close>

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 *\<^sub>R f(x))"
  using bounded_linear_scaleR_right assms
  by (rule bounded_linear.uniformly_continuous_on)

lemma dist_minus:
  fixes x y :: "'a::real_normed_vector"
  shows "dist (- x) (- y) = dist x y"
  unfolding dist_norm minus_diff_minus norm_minus_cancel ..

lemma uniformly_continuous_on_minus[continuous_intros]:
  fixes f :: "'a::metric_space \ 'b::real_normed_vector"
  shows "uniformly_continuous_on s f \ uniformly_continuous_on s (\x. - f x)"
  unfolding uniformly_continuous_on_def dist_minus .

lemma uniformly_continuous_on_add[continuous_intros]:
  fixes f g :: "'a::metric_space \ 'b::real_normed_vector"
  assumes "uniformly_continuous_on s f"
    and "uniformly_continuous_on s g"
  shows "uniformly_continuous_on s (\x. f x + g x)"
  using assms
  unfolding uniformly_continuous_on_sequentially
  unfolding dist_norm tendsto_norm_zero_iff add_diff_add
  by (auto intro: tendsto_add_zero)

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

lemma uniformly_continuous_on_sum [continuous_intros]:
  fixes f :: "'a \ 'b::metric_space \ 'c::real_normed_vector"
  shows "(\i. i \ I \ uniformly_continuous_on S (f i)) \ uniformly_continuous_on S (\x. \i\I. f i x)"
  by (induction I rule: infinite_finite_induct)
     (auto simp: uniformly_continuous_on_add uniformly_continuous_on_const)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic Preserves Topological Properties\<close>

lemma open_scaling[intro]:
  fixes S :: "'a::real_normed_vector set"
  assumes "c \ 0"
    and "open S"
  shows "open((\x. c *\<^sub>R x) ` S)"
proof -
  {
    fix x
    assume "x \ S"
    then obtain \<epsilon> where "\<epsilon>>0"
      and \<epsilon>: "\<forall>x'. dist x' x < \<epsilon> \<longrightarrow> x' \<in> S" using assms(2)[unfolded open_dist, THEN bspec[where x=x]]
      by auto
    have "\ * \c\ > 0"
      using assms(1)[unfolded zero_less_abs_iff[symmetric]] \<open>\<epsilon>>0\<close> by auto
    moreover
    {
      fix y
      assume "dist y (c *\<^sub>R x) < \ * \c\"
      then have "norm (c *\<^sub>R ((1 / c) *\<^sub>R y - x)) < \ * norm c"
        by (simp add: \<open>c \<noteq> 0\<close> dist_norm scale_right_diff_distrib)
      then have "norm ((1 / c) *\<^sub>R y - x) < \"
        by (simp add: \<open>c \<noteq> 0\<close>)
      then have "y \ (*\<^sub>R) c ` S"
        using rev_image_eqI[of "(1 / c) *\<^sub>R y" S y "(*\<^sub>R) c"]
        by (simp add: \<open>c \<noteq> 0\<close> dist_norm \<epsilon>)
    }
    ultimately have "\e>0. \x'. dist x' (c *\<^sub>R x) < e \ x' \ (*\<^sub>R) c ` S"
      by (rule_tac x="\ * \c\" in exI, auto)
  }
  then show ?thesis unfolding open_dist by auto
qed

lemma open_times_image:
  fixes S::"'a::real_normed_field set"
  assumes "c\0" "open S"
  shows "open (((*) c) ` S)"
proof -
  let ?f = "\x. x/c" and ?g="((*) c)"
  have "continuous_on UNIV ?f" using \<open>c\<noteq>0\<close> by (auto intro:continuous_intros)
  then have "open (?f -` S)" using \<open>open S\<close> by (auto elim:open_vimage)
  moreover have "?g ` S = ?f -` S" using \<open>c\<noteq>0\<close>
    using image_iff by fastforce
  ultimately show ?thesis 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 *\<^sub>R x) ` S)"
proof -
  have *: "(\x. a + c *\<^sub>R x) = (\x. a + x) \ (\x. c *\<^sub>R x)"
    unfolding o_def ..
  have "(+) a ` (*\<^sub>R) c ` S = ((+) a \ (*\<^sub>R) c) ` S"
    by auto
  then show ?thesis
    using assms open_translation[of "(*\<^sub>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 \<open>0 < e\<close> 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 \<open>e > 0\<close> 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 *\<^sub>R x) ` s)"
proof -
  let ?f = "\x. scaleR c x"
  have *: "bounded_linear ?f" by (rule bounded_linear_scaleR_right)
  show ?thesis
    using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
    using linear_continuous_at[OF *] assms
    by auto
qed

lemma compact_negations:
  fixes s :: "'a::real_normed_vector set"
  assumes "compact s"
  shows "compact ((\x. - x) ` s)"
  using compact_scaling [OF assms, of "- 1"] by auto

lemma compact_sums:
  fixes s t :: "'a::real_normed_vector set"
  assumes "compact s"
    and "compact t"
  shows "compact {x + y | x y. x \ s \ y \ t}"
proof -
  have *: "{x + y | x y. x \ s \ y \ t} = (\z. fst z + snd z) ` (s \ t)"
    by (fastforce simp: image_iff)
  have "continuous_on (s \ t) (\z. fst z + snd z)"
    unfolding continuous_on by (rule ballI) (intro tendsto_intros)
  then show ?thesis
    unfolding * using compact_continuous_image compact_Times [OF assms] by auto
qed

lemma compact_differences:
  fixes s t :: "'a::real_normed_vector set"
  assumes "compact s"
    and "compact t"
  shows "compact {x - y | x y. x \ s \ y \ t}"
proof-
  have "{x - y | x y. x\s \ y \ t} = {x + y | x y. x \ s \ y \ (uminus ` t)}"
    using diff_conv_add_uminus by force
  then show ?thesis
    using compact_sums[OF assms(1) compact_negations[OF assms(2)]] by auto
qed

lemma compact_sums':
  fixes S :: "'a::real_normed_vector set"
  assumes "compact S" and "compact T"
  shows "compact (\x\ S. \y \ T. {x + y})"
proof -
  have "(\x\S. \y\T. {x + y}) = {x + y |x y. x \ S \ y \ T}"
    by blast
  then show ?thesis
    using compact_sums [OF assms] by simp
qed

lemma compact_differences':
  fixes S :: "'a::real_normed_vector set"
  assumes "compact S" and "compact T"
  shows "compact (\x\ S. \y \ T. {x - y})"
proof -
  have "(\x\S. \y\T. {x - y}) = {x - y |x y. x \ S \ y \ T}"
    by blast
  then show ?thesis
    using compact_differences [OF assms] by simp
qed

lemma compact_translation:
  "compact ((+) a ` s)" if "compact s" for s :: "'a::real_normed_vector set"
proof -
  have "{x + y |x y. x \ s \ y \ {a}} = (\x. a + x) ` s"
    by auto
  then show ?thesis
    using compact_sums [OF that compact_sing [of a]] by auto
qed

lemma compact_translation_subtract:
  "compact ((\x. x - a) ` s)" if "compact s" for s :: "'a::real_normed_vector set"
  using that compact_translation [of s "- a"] by (simp cong: image_cong_simp)

lemma compact_affinity:
  fixes s :: "'a::real_normed_vector set"
  assumes "compact s"
  shows "compact ((\x. a + c *\<^sub>R x) ` s)"
proof -
  have "(+) a ` (*\<^sub>R) c ` s = (\x. a + c *\<^sub>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 *\<^sub>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 *\<^sub>R x) -` S)"
    by (simp add: continuous_closed_vimage)
  also have "(\x. inverse c *\<^sub>R x) -` S = (\x. c *\<^sub>R x) ` S"
    using \<open>c \<noteq> 0\<close> 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'\<in>S" and r: "strict_mono r" and lr: "(((\<lambda>n. fst (f n)) \<circ> r) \<longlongrightarrow> 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 \<open>l' \<in> S\<close> 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)

subsection\<^marker>\<open>tag unimportant\<close>\<open>Homeomorphisms\<close>

lemma homeomorphic_scaling:
  fixes S :: "'a::real_normed_vector set"
  assumes "c \ 0"
  shows "S homeomorphic ((\x. c *\<^sub>R x) ` S)"
  unfolding homeomorphic_minimal
  apply (rule_tac x="\x. c *\<^sub>R x" in exI)
  apply (rule_tac x="\x. (1 / c) *\<^sub>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 *\<^sub>R x) ` S)"
proof -
  have *: "(+) a ` (*\<^sub>R) c ` S = (\x. a + c *\<^sub>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) *\<^sub>R (x - a)" in exI)
    apply(rule_tac x="\x. a + (d/e) *\<^sub>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) *\<^sub>R (x - a)" in exI)
    apply(rule_tac x="\x. a + (d/e) *\<^sub>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) *\<^sub>R (x - a)" in exI)
    apply(rule_tac x="\x. a + (d/e) *\<^sub>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 /\<^sub>R (1 - norm z)) ` ball 0 1" for x::'a
    apply (rule_tac x="x /\<^sub>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 /\<^sub>R (1 - norm z)) ` ?B = ?U"
    by blast
  have "x \ range (\z. (1 / (1 + norm z)) *\<^sub>R z)" if "norm x < 1" for x::'a
    using that
--> --------------------

--> maximum size reached

--> --------------------

quality91%

¤ Dauer der Verarbeitung: 0.68 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.