(* 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 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 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)
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 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]] \<open>e>0\<close> by auto
moreover
{
fix y
assume "dist y (c *\<^sub>R x) < e * \c\"
then have "norm (c *\<^sub>R ((1 / c) *\<^sub>R y - x)) < e * 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) < e"
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 e)
}
ultimately have "\e>0. \x'. dist x' (c *\<^sub>R x) < e \ x' \ (*\<^sub>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 *\<^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_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
by (rule_tac x="x /\<^sub>R (1 - norm x)" in image_eqI) (auto simp: field_split_simps)
then show "(\z::'a. z /\<^sub>R (1 + norm z)) ` ?U = ?B"
by (force simp: field_split_simps dest: add_less_zeroD)
show "continuous_on (ball 0 1) (\z. z /\<^sub>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 /\<^sub>R (1 + norm z))"
by (auto intro!: continuous_intros)
show "\x. x \ ball 0 1 \
x /\<^sub>R (1 - norm x) /\<^sub>R (1 + norm (x /\<^sub>R (1 - norm x))) = x"
by (auto simp: field_split_simps)
show "\y. y /\<^sub>R (1 + norm y) /\<^sub>R (1 - norm (y /\<^sub>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
subsection\<^marker>\<open>tag unimportant\<close> \<open>Discrete\<close>
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
subsection\<^marker>\<open>tag unimportant\<close> \<open>Completeness of "Isometry" (up to constant bounds)\<close>
lemma cauchy_isometric:\<comment> \<open>TODO: rename lemma to \<open>Cauchy_isometric\<close>\<close>
assumes e: "e > 0"
and s: "subspace s"
and f: "bounded_linear f"
and normf: "\x\s. norm (f x) \ e * norm x"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.84 Sekunden
(vorverarbeitet)
¤
|
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.
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
