Theory HOL-Analysis.Topology_Euclidean_Space
chapter ‹Vector Analysis›
theory Topology_Euclidean_Space
imports
Elementary_Normed_Spaces
Linear_Algebra
Norm_Arith
begin
section ‹Elementary Topology in Euclidean Space›
lemma euclidean_dist_l2:
fixes x y :: "'a :: euclidean_space"
shows "dist x y = L2_set (λi. dist (x ∙ i) (y ∙ i)) Basis"
unfolding dist_norm norm_eq_sqrt_inner L2_set_def
by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
lemma norm_nth_le: "norm (x ∙ i) ≤ norm x" if "i ∈ Basis"
proof -
have "(x ∙ i)⇧2 = (∑i∈{i}. (x ∙ i)⇧2)"
by simp
also have "… ≤ (∑i∈Basis. (x ∙ i)⇧2)"
by (intro sum_mono2) (auto simp: that)
finally show ?thesis
unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def
by (auto intro!: real_le_rsqrt)
qed
subsection ‹Continuity of the representation WRT an orthogonal basis›
lemma orthogonal_Basis: "pairwise orthogonal Basis"
by (simp add: inner_not_same_Basis orthogonal_def pairwise_def)
lemma representation_bound:
fixes B :: "'N::real_inner set"
assumes "finite B" "independent B" "b ∈ B" and orth: "pairwise orthogonal B"
obtains m where "m > 0" "⋀x. x ∈ span B ⟹ ¦representation B x b¦ ≤ m * norm x"
proof
fix x
assume x: "x ∈ span B"
have "b ≠ 0"
using ‹independent B› ‹b ∈ B› dependent_zero by blast
have [simp]: "b ∙ b' = (if b' = b then (norm b)⇧2 else 0)"
if "b ∈ B" "b' ∈ B" for b b'
using orth by (simp add: orthogonal_def pairwise_def norm_eq_sqrt_inner that)
have "norm x = norm (∑b∈B. representation B x b *⇩R b)"
using real_vector.sum_representation_eq [OF ‹independent B› x ‹finite B› order_refl]
by simp
also have "… = sqrt ((∑b∈B. representation B x b *⇩R b) ∙ (∑b∈B. representation B x b *⇩R b))"
by (simp add: norm_eq_sqrt_inner)
also have "… = sqrt (∑b∈B. (representation B x b *⇩R b) ∙ (representation B x b *⇩R b))"
using ‹finite B›
by (simp add: inner_sum_left inner_sum_right if_distrib [of "λx. _ * x"] cong: if_cong sum.cong_simp)
also have "… = sqrt (∑b∈B. (norm (representation B x b *⇩R b))⇧2)"
by (simp add: mult.commute mult.left_commute power2_eq_square)
also have "… = sqrt (∑b∈B. (representation B x b)⇧2 * (norm b)⇧2)"
by (simp add: norm_mult power_mult_distrib)
finally have "norm x = sqrt (∑b∈B. (representation B x b)⇧2 * (norm b)⇧2)" .
moreover
have "sqrt ((representation B x b)⇧2 * (norm b)⇧2) ≤ sqrt (∑b∈B. (representation B x b)⇧2 * (norm b)⇧2)"
using ‹b ∈ B› ‹finite B› by (auto intro: member_le_sum)
then have "¦representation B x b¦ ≤ (1 / norm b) * sqrt (∑b∈B. (representation B x b)⇧2 * (norm b)⇧2)"
using ‹b ≠ 0› by (simp add: field_split_simps real_sqrt_mult del: real_sqrt_le_iff)
ultimately show "¦representation B x b¦ ≤ (1 / norm b) * norm x"
by simp
next
show "0 < 1 / norm b"
using ‹independent B› ‹b ∈ B› dependent_zero by auto
qed
lemma continuous_on_representation:
fixes B :: "'N::euclidean_space set"
assumes "finite B" "independent B" "b ∈ B" "pairwise orthogonal B"
shows "continuous_on (span B) (λx. representation B x b)"
proof
show "∃d>0. ∀x'∈span B. dist x' x < d ⟶ dist (representation B x' b) (representation B x b) ≤ e"
if "e > 0" "x ∈ span B" for x e
proof -
obtain m where "m > 0" and m: "⋀x. x ∈ span B ⟹ ¦representation B x b¦ ≤ m * norm x"
using assms representation_bound by blast
show ?thesis
unfolding dist_norm
proof (intro exI conjI ballI impI)
show "e/m > 0"
by (simp add: ‹e > 0› ‹m > 0›)
show "norm (representation B x' b - representation B x b) ≤ e"
if x': "x' ∈ span B" and less: "norm (x'-x) < e/m" for x'
proof -
have "¦representation B (x'-x) b¦ ≤ m * norm (x'-x)"
using m [of "x'-x"] ‹x ∈ span B› span_diff x' by blast
also have "… < e"
by (metis ‹m > 0› less mult.commute pos_less_divide_eq)
finally have "¦representation B (x'-x) b¦ ≤ e" by simp
then show ?thesis
by (simp add: ‹x ∈ span B› ‹independent B› representation_diff x')
qed
qed
qed
qed
subsection‹Balls in Euclidean Space›
lemma cball_subset_cball_iff:
fixes a :: "'a :: euclidean_space"
shows "cball a r ⊆ cball a' r' ⟷ dist a a' + r ≤ r' ∨ r < 0"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
then show ?rhs
proof (cases "r < 0")
case True
then show ?rhs by simp
next
case False
then have [simp]: "r ≥ 0" by simp
have "norm (a - a') + r ≤ r'"
proof (cases "a = a'")
case True
then show ?thesis
using subsetD [where c = "a + r *⇩R (SOME i. i ∈ Basis)", OF ‹?lhs›] subsetD [where c = a, OF ‹?lhs›]
by (force simp: SOME_Basis dist_norm)
next
case False
have "norm (a' - (a + (r / norm (a - a')) *⇩R (a - a'))) = norm ((-1 - (r / norm (a - a'))) *⇩R (a - a'))"
by (simp add: algebra_simps)
also from ‹a ≠ a'› have "... = ¦- norm (a - a') - r¦"
by (simp add: divide_simps)
finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *⇩R (a - a'))) = ¦norm (a - a') + r¦"
by linarith
from ‹a ≠ a'› show ?thesis
using subsetD [where c = "a' + (1 + r / norm(a - a')) *⇩R (a - a')", OF ‹?lhs›]
by (simp add: dist_norm scaleR_add_left)
qed
then show ?rhs
by (simp add: dist_norm)
qed
qed metric
lemma cball_subset_ball_iff: "cball a r ⊆ ball a' r' ⟷ dist a a' + r < r' ∨ r < 0"
(is "?lhs ⟷ ?rhs")
for a :: "'a::euclidean_space"
proof
assume ?lhs
then show ?rhs
proof (cases "r < 0")
case True then
show ?rhs by simp
next
case False
then have [simp]: "r ≥ 0" by simp
have "norm (a - a') + r < r'"
proof (cases "a = a'")
case True
then show ?thesis
using subsetD [where c = "a + r *⇩R (SOME i. i ∈ Basis)", OF ‹?lhs›] subsetD [where c = a, OF ‹?lhs›]
by (force simp: SOME_Basis dist_norm)
next
case False
have False if "norm (a - a') + r ≥ r'"
proof -
from that have "¦r' - norm (a - a')¦ ≤ r"
by (smt (verit, best) ‹0 ≤ r› ‹?lhs› ball_subset_cball cball_subset_cball_iff dist_norm order_trans)
then show ?thesis
using subsetD [where c = "a + (r' / norm(a - a') - 1) *⇩R (a - a')", OF ‹?lhs›] ‹a ≠ a'›
apply (simp add: dist_norm)
apply (simp add: scaleR_left_diff_distrib)
apply (simp add: field_simps)
done
qed
then show ?thesis by force
qed
then show ?rhs by (simp add: dist_norm)
qed
next
assume ?rhs
then show ?lhs
by metric
qed
lemma ball_subset_cball_iff: "ball a r ⊆ cball a' r' ⟷ dist a a' + r ≤ r' ∨ r ≤ 0"
(is "?lhs = ?rhs")
for a :: "'a::euclidean_space"
proof (cases "r ≤ 0")
case True
then show ?thesis
by metric
next
case False
show ?thesis
proof
assume ?lhs
then have "(cball a r ⊆ cball a' r')"
by (metis False closed_cball closure_ball closure_closed closure_mono not_less)
with False show ?rhs
by (fastforce iff: cball_subset_cball_iff)
next
assume ?rhs
with False show ?lhs
by metric
qed
qed
lemma ball_subset_ball_iff:
fixes a :: "'a :: euclidean_space"
shows "ball a r ⊆ ball a' r' ⟷ dist a a' + r ≤ r' ∨ r ≤ 0"
(is "?lhs = ?rhs")
proof (cases "r ≤ 0")
case True then show ?thesis
by metric
next
case False show ?thesis
proof
assume ?lhs
then have "0 < r'"
using False by metric
then have "cball a r ⊆ cball a' r'"
by (metis False ‹?lhs› closure_ball closure_mono not_less)
then show ?rhs
using False cball_subset_cball_iff by fastforce
qed metric
qed
lemma ball_eq_ball_iff:
fixes x :: "'a :: euclidean_space"
shows "ball x d = ball y e ⟷ d ≤ 0 ∧ e ≤ 0 ∨ x=y ∧ d=e"
by (smt (verit, del_insts) ball_empty ball_subset_cball_iff dist_norm norm_pths(2))
lemma cball_eq_cball_iff:
fixes x :: "'a :: euclidean_space"
shows "cball x d = cball y e ⟷ d < 0 ∧ e < 0 ∨ x=y ∧ d=e"
by (smt (verit, ccfv_SIG) cball_empty cball_subset_cball_iff dist_norm norm_pths(2) zero_le_dist)
lemma ball_eq_cball_iff:
fixes x :: "'a :: euclidean_space"
shows "ball x d = cball y e ⟷ d ≤ 0 ∧ e < 0" (is "?lhs = ?rhs")
by (smt (verit) ball_eq_empty ball_subset_cball_iff cball_eq_empty cball_subset_ball_iff order.refl)
lemma cball_eq_ball_iff:
fixes x :: "'a :: euclidean_space"
shows "cball x d = ball y e ⟷ d < 0 ∧ e ≤ 0"
using ball_eq_cball_iff by blast
lemma finite_ball_avoid:
fixes S :: "'a :: euclidean_space set"
assumes "open S" "finite X" "p ∈ S"
shows "∃e>0. ∀w∈ball p e. w∈S ∧ (w≠p ⟶ w∉X)"
proof -
obtain e1 where "0 < e1" and e1_b:"ball p e1 ⊆ S"
using open_contains_ball_eq[OF ‹open S›] assms by auto
obtain e2 where "0 < e2" and "∀x∈X. x ≠ p ⟶ e2 ≤ dist p x"
using finite_set_avoid[OF ‹finite X›,of p] by auto
hence "∀w∈ball p (min e1 e2). w∈S ∧ (w≠p ⟶ w∉X)" using e1_b by auto
thus "∃e>0. ∀w∈ball p e. w ∈ S ∧ (w ≠ p ⟶ w ∉ X)"
using ‹e2>0› ‹e1>0› by (rule_tac x="min e1 e2" in exI) auto
qed
lemma finite_cball_avoid:
fixes S :: "'a :: euclidean_space set"
assumes "open S" "finite X" "p ∈ S"
shows "∃e>0. ∀w∈cball p e. w∈S ∧ (w≠p ⟶ w∉X)"
proof -
obtain e1 where "e1>0" and e1: "∀w∈ball p e1. w∈S ∧ (w≠p ⟶ w∉X)"
using finite_ball_avoid[OF assms] by auto
define e2 where "e2 ≡ e1/2"
have "e2>0" and "e2 < e1" unfolding e2_def using ‹e1>0› by auto
then have "cball p e2 ⊆ ball p e1" by (subst cball_subset_ball_iff,auto)
then show "∃e>0. ∀w∈cball p e. w ∈ S ∧ (w ≠ p ⟶ w ∉ X)" using ‹e2>0› e1 by auto
qed
lemma dim_cball:
assumes "e > 0"
shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)"
proof -
{
fix x :: "'n::euclidean_space"
define y where "y = (e / norm x) *⇩R x"
then have "y ∈ cball 0 e"
using assms by auto
moreover have *: "x = (norm x / e) *⇩R y"
using y_def assms by simp
moreover from * have "x = (norm x/e) *⇩R y"
by auto
ultimately have "x ∈ span (cball 0 e)"
using span_scale[of y "cball 0 e" "norm x/e"]
span_superset[of "cball 0 e"]
by (simp add: span_base)
}
then have "span (cball 0 e) = (UNIV :: 'n::euclidean_space set)"
by auto
then show ?thesis
using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto)
qed
subsection ‹Boxes›
abbreviation One :: "'a::euclidean_space" where
"One ≡ ∑Basis"
lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False
proof -
have "dependent (Basis :: 'a set)"
apply (simp add: dependent_finite)
apply (rule_tac x="λi. 1" in exI)
using SOME_Basis apply (auto simp: assms)
done
with independent_Basis show False by force
qed
corollary One_neq_0[iff]: "One ≠ 0"
by (metis One_non_0)
corollary Zero_neq_One[iff]: "0 ≠ One"
by (metis One_non_0)
definition (in euclidean_space) eucl_less (infix "<e" 50) where
"eucl_less a b ⟷ (∀i∈Basis. a ∙ i < b ∙ i)"
definition box_eucl_less: "box a b = {x. a <e x ∧ x <e b}"
definition "cbox a b = {x. ∀i∈Basis. a ∙ i ≤ x ∙ i ∧ x ∙ i ≤ b ∙ i}"
lemma box_def: "box a b = {x. ∀i∈Basis. a ∙ i < x ∙ i ∧ x ∙ i < b ∙ i}"
and in_box_eucl_less: "x ∈ box a b ⟷ a <e x ∧ x <e b"
and mem_box: "x ∈ box a b ⟷ (∀i∈Basis. a ∙ i < x ∙ i ∧ x ∙ i < b ∙ i)"
"x ∈ cbox a b ⟷ (∀i∈Basis. a ∙ i ≤ x ∙ i ∧ x ∙ i ≤ b ∙ i)"
by (auto simp: box_eucl_less eucl_less_def cbox_def)
lemma cbox_Pair_eq: "cbox (a, c) (b, d) = cbox a b × cbox c d"
by (force simp: cbox_def Basis_prod_def)
lemma cbox_Pair_iff [iff]: "(x, y) ∈ cbox (a, c) (b, d) ⟷ x ∈ cbox a b ∧ y ∈ cbox c d"
by (force simp: cbox_Pair_eq)
lemma cbox_Complex_eq: "cbox (Complex a c) (Complex b d) = (λ(x,y). Complex x y) ` (cbox a b × cbox c d)"
by (force simp: cbox_def Basis_complex_def)
lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} ⟷ cbox a b = {} ∨ cbox c d = {}"
by (force simp: cbox_Pair_eq)
lemma swap_cbox_Pair [simp]: "prod.swap ` cbox (c, a) (d, b) = cbox (a,c) (b,d)"
by auto
lemma mem_box_real[simp]:
"(x::real) ∈ box a b ⟷ a < x ∧ x < b"
"(x::real) ∈ cbox a b ⟷ a ≤ x ∧ x ≤ b"
by (auto simp: mem_box)
lemma box_real[simp]:
fixes a b:: real
shows "box a b = {a <..< b}" "cbox a b = {a .. b}"
by auto
lemma box_Int_box:
fixes a :: "'a::euclidean_space"
shows "box a b ∩ box c d =
box (∑i∈Basis. max (a∙i) (c∙i) *⇩R i) (∑i∈Basis. min (b∙i) (d∙i) *⇩R i)"
unfolding set_eq_iff and Int_iff and mem_box by auto
lemma rational_boxes:
fixes x :: "'a::euclidean_space"
assumes "e > 0"
shows "∃a b. (∀i∈Basis. a ∙ i ∈ ℚ ∧ b ∙ i ∈ ℚ) ∧ x ∈ box a b ∧ box a b ⊆ ball x e"
proof -
define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
then have e: "e' > 0"
using assms by (auto)
have "∃y. y ∈ ℚ ∧ y < x ∙ i ∧ x ∙ i - y < e'" for i
using Rats_dense_in_real[of "x ∙ i - e'" "x ∙ i"] e by force
then obtain a where
a: "⋀u. a u ∈ ℚ ∧ a u < x ∙ u ∧ x ∙ u - a u < e'" by metis
have "∃y. y ∈ ℚ ∧ x ∙ i < y ∧ y - x ∙ i < e'" for i
using Rats_dense_in_real[of "x ∙ i" "x ∙ i + e'"] e by force
then obtain b where
b: "⋀u. b u ∈ ℚ ∧ x ∙ u < b u ∧ b u - x ∙ u < e'" by metis
let ?a = "∑i∈Basis. a i *⇩R i" and ?b = "∑i∈Basis. b i *⇩R i"
show ?thesis
proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
fix y :: 'a
assume *: "y ∈ box ?a ?b"
have "dist x y = sqrt (∑i∈Basis. (dist (x ∙ i) (y ∙ i))⇧2)"
unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
also have "… < sqrt (∑(i::'a)∈Basis. e^2 / real (DIM('a)))"
proof (rule real_sqrt_less_mono, rule sum_strict_mono)
fix i :: "'a"
assume i: "i ∈ Basis"
have "a i < y∙i ∧ y∙i < b i"
using * i by (auto simp: box_def)
moreover have "a i < x∙i" "x∙i - a i < e'" "x∙i < b i" "b i - x∙i < e'"
using a b by auto
ultimately have "¦x∙i - y∙i¦ < 2 * e'"
by auto
then have "dist (x ∙ i) (y ∙ i) < e/sqrt (real (DIM('a)))"
unfolding e'_def by (auto simp: dist_real_def)
then have "(dist (x ∙ i) (y ∙ i))⇧2 < (e/sqrt (real (DIM('a))))⇧2"
by (rule power_strict_mono) auto
then show "(dist (x ∙ i) (y ∙ i))⇧2 < e⇧2 / real DIM('a)"
by (simp add: power_divide)
qed auto
also have "… = e"
using ‹0 < e› by simp
finally show "y ∈ ball x e"
by (auto simp: ball_def)
qed (use a b in ‹auto simp: box_def›)
qed
lemma open_UNION_box:
fixes M :: "'a::euclidean_space set"
assumes "open M"
defines "a' ≡ λf :: 'a ⇒ real × real. (∑(i::'a)∈Basis. fst (f i) *⇩R i)"
defines "b' ≡ λf :: 'a ⇒ real × real. (∑(i::'a)∈Basis. snd (f i) *⇩R i)"
defines "I ≡ {f∈Basis →⇩E ℚ × ℚ. box (a' f) (b' f) ⊆ M}"
shows "M = (⋃f∈I. box (a' f) (b' f))"
proof -
have "x ∈ (⋃f∈I. box (a' f) (b' f))" if "x ∈ M" for x
proof -
obtain e where e: "e > 0" "ball x e ⊆ M"
using openE[OF ‹open M› ‹x ∈ M›] by auto
moreover obtain a b where ab:
"x ∈ box a b"
"∀i ∈ Basis. a ∙ i ∈ ℚ"
"∀i∈Basis. b ∙ i ∈ ℚ"
"box a b ⊆ ball x e"
using rational_boxes[OF e(1)] by metis
ultimately show ?thesis
by (intro UN_I[of "λi∈Basis. (a ∙ i, b ∙ i)"])
(auto simp: euclidean_representation I_def a'_def b'_def)
qed
then show ?thesis by (auto simp: I_def)
qed
corollary open_countable_Union_open_box:
fixes S :: "'a :: euclidean_space set"
assumes "open S"
obtains 𝒟 where "countable 𝒟" "𝒟 ⊆ Pow S" "⋀X. X ∈ 𝒟 ⟹ ∃a b. X = box a b" "⋃𝒟 = S"
proof -
let ?a = "λf. (∑(i::'a)∈Basis. fst (f i) *⇩R i)"
let ?b = "λf. (∑(i::'a)∈Basis. snd (f i) *⇩R i)"
let ?I = "{f∈Basis →⇩E ℚ × ℚ. box (?a f) (?b f) ⊆ S}"
let ?𝒟 = "(λf. box (?a f) (?b f)) ` ?I"
show ?thesis
proof
have "countable ?I"
by (simp add: countable_PiE countable_rat)
then show "countable ?𝒟"
by blast
show "⋃?𝒟 = S"
using open_UNION_box [OF assms] by metis
qed auto
qed
lemma rational_cboxes:
fixes x :: "'a::euclidean_space"
assumes "e > 0"
shows "∃a b. (∀i∈Basis. a ∙ i ∈ ℚ ∧ b ∙ i ∈ ℚ) ∧ x ∈ cbox a b ∧ cbox a b ⊆ ball x e"
proof -
define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
then have e: "e' > 0"
using assms by auto
have "∃y. y ∈ ℚ ∧ y < x ∙ i ∧ x ∙ i - y < e'" for i
using Rats_dense_in_real[of "x ∙ i - e'" "x ∙ i"] e by force
then obtain a where
a: "∀u. a u ∈ ℚ ∧ a u < x ∙ u ∧ x ∙ u - a u < e'" by metis
have "∃y. y ∈ ℚ ∧ x ∙ i < y ∧ y - x ∙ i < e'" for i
using Rats_dense_in_real[of "x ∙ i" "x ∙ i + e'"] e by force
then obtain b where
b: "∀u. b u ∈ ℚ ∧ x ∙ u < b u ∧ b u - x ∙ u < e'" by metis
let ?a = "∑i∈Basis. a i *⇩R i" and ?b = "∑i∈Basis. b i *⇩R i"
show ?thesis
proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
fix y :: 'a
assume *: "y ∈ cbox ?a ?b"
have "dist x y = sqrt (∑i∈Basis. (dist (x ∙ i) (y ∙ i))⇧2)"
unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
also have "… < sqrt (∑(i::'a)∈Basis. e^2 / real (DIM('a)))"
proof (rule real_sqrt_less_mono, rule sum_strict_mono)
fix i :: "'a"
assume i: "i ∈ Basis"
have "a i ≤ y∙i ∧ y∙i ≤ b i"
using * i by (auto simp: cbox_def)
moreover have "a i < x∙i" "x∙i - a i < e'" "x∙i < b i" "b i - x∙i < e'"
using a b by auto
ultimately have "¦x∙i - y∙i¦ < 2 * e'"
by auto
then have "dist (x ∙ i) (y ∙ i) < e/sqrt (real (DIM('a)))"
unfolding e'_def by (auto simp: dist_real_def)
then have "(dist (x ∙ i) (y ∙ i))⇧2 < (e/sqrt (real (DIM('a))))⇧2"
by (rule power_strict_mono) auto
then show "(dist (x ∙ i) (y ∙ i))⇧2 < e⇧2 / real DIM('a)"
by (simp add: power_divide)
qed auto
also have "… = e"
using ‹0 < e› by simp
finally show "y ∈ ball x e"
by (auto simp: ball_def)
next
show "x ∈ cbox (∑i∈Basis. a i *⇩R i) (∑i∈Basis. b i *⇩R i)"
using a b less_imp_le by (auto simp: cbox_def)
qed (use a b cbox_def in auto)
qed
lemma open_UNION_cbox:
fixes M :: "'a::euclidean_space set"
assumes "open M"
defines "a' ≡ λf. (∑(i::'a)∈Basis. fst (f i) *⇩R i)"
defines "b' ≡ λf. (∑(i::'a)∈Basis. snd (f i) *⇩R i)"
defines "I ≡ {f∈Basis →⇩E ℚ × ℚ. cbox (a' f) (b' f) ⊆ M}"
shows "M = (⋃f∈I. cbox (a' f) (b' f))"
proof -
have "x ∈ (⋃f∈I. cbox (a' f) (b' f))" if "x ∈ M" for x
proof -
obtain e where e: "e > 0" "ball x e ⊆ M"
using openE[OF ‹open M› ‹x ∈ M›] by auto
moreover obtain a b where ab: "x ∈ cbox a b" "∀i ∈ Basis. a ∙ i ∈ ℚ"
"∀i ∈ Basis. b ∙ i ∈ ℚ" "cbox a b ⊆ ball x e"
using rational_cboxes[OF e(1)] by metis
ultimately show ?thesis
by (intro UN_I[of "λi∈Basis. (a ∙ i, b ∙ i)"])
(auto simp: euclidean_representation I_def a'_def b'_def)
qed
then show ?thesis by (auto simp: I_def)
qed
corollary open_countable_Union_open_cbox:
fixes S :: "'a :: euclidean_space set"
assumes "open S"
obtains 𝒟 where "countable 𝒟" "𝒟 ⊆ Pow S" "⋀X. X ∈ 𝒟 ⟹ ∃a b. X = cbox a b" "⋃𝒟 = S"
proof -
let ?a = "λf. (∑(i::'a)∈Basis. fst (f i) *⇩R i)"
let ?b = "λf. (∑(i::'a)∈Basis. snd (f i) *⇩R i)"
let ?I = "{f∈Basis →⇩E ℚ × ℚ. cbox (?a f) (?b f) ⊆ S}"
let ?𝒟 = "(λf. cbox (?a f) (?b f)) ` ?I"
show ?thesis
proof
have "countable ?I"
by (simp add: countable_PiE countable_rat)
then show "countable ?𝒟"
by blast
show "⋃?𝒟 = S"
using open_UNION_cbox [OF assms] by metis
qed auto
qed
lemma box_eq_empty:
fixes a :: "'a::euclidean_space"
shows "(box a b = {} ⟷ (∃i∈Basis. b∙i ≤ a∙i))" (is ?th1)
and "(cbox a b = {} ⟷ (∃i∈Basis. b∙i < a∙i))" (is ?th2)
proof -
have False if "i ∈ Basis" and "b∙i ≤ a∙i" and "x ∈ box a b" for i x
by (smt (verit, ccfv_SIG) mem_box(1) that)
moreover
{ assume as: "∀i∈Basis. ¬ (b∙i ≤ a∙i)"
let ?x = "(1/2) *⇩R (a + b)"
{ fix i :: 'a
assume i: "i ∈ Basis"
have "a∙i < b∙i"
using as i by fastforce
then have "a∙i < ((1/2) *⇩R (a+b)) ∙ i" "((1/2) *⇩R (a+b)) ∙ i < b∙i"
by (auto simp: inner_add_left)
}
then have "box a b ≠ {}"
by (metis (no_types, opaque_lifting) emptyE mem_box(1))
}
ultimately show ?th1 by blast
have False if "i∈Basis" and "b∙i < a∙i" and "x ∈ cbox a b" for i x
using mem_box(2) that by force
moreover
have "cbox a b ≠ {}" if "∀i∈Basis. ¬ (b∙i < a∙i)"
by (metis emptyE linorder_linear mem_box(2) order.strict_iff_not that)
ultimately show ?th2 by blast
qed
lemma box_ne_empty:
fixes a :: "'a::euclidean_space"
shows "cbox a b ≠ {} ⟷ (∀i∈Basis. a∙i ≤ b∙i)"
and "box a b ≠ {} ⟷ (∀i∈Basis. a∙i < b∙i)"
unfolding box_eq_empty[of a b] by fastforce+
lemma
fixes a :: "'a::euclidean_space"
shows cbox_idem [simp]: "cbox a a = {a}"
and box_idem [simp]: "box a a = {}"
unfolding set_eq_iff mem_box eq_iff [symmetric] using euclidean_eq_iff by fastforce+
lemma subset_box_imp:
fixes a :: "'a::euclidean_space"
shows "(∀i∈Basis. a∙i ≤ c∙i ∧ d∙i ≤ b∙i) ⟹ cbox c d ⊆ cbox a b"
and "(∀i∈Basis. a∙i < c∙i ∧ d∙i < b∙i) ⟹ cbox c d ⊆ box a b"
and "(∀i∈Basis. a∙i ≤ c∙i ∧ d∙i ≤ b∙i) ⟹ box c d ⊆ cbox a b"
and "(∀i∈Basis. a∙i ≤ c∙i ∧ d∙i ≤ b∙i) ⟹ box c d ⊆ box a b"
unfolding subset_eq[unfolded Ball_def] unfolding mem_box
by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
lemma box_subset_cbox:
fixes a :: "'a::euclidean_space"
shows "box a b ⊆ cbox a b"
unfolding subset_eq [unfolded Ball_def] mem_box
by (fast intro: less_imp_le)
lemma subset_box:
fixes a :: "'a::euclidean_space"
shows "cbox c d ⊆ cbox a b ⟷ (∀i∈Basis. c∙i ≤ d∙i) ⟶ (∀i∈Basis. a∙i ≤ c∙i ∧ d∙i ≤ b∙i)" (is ?th1)
and "cbox c d ⊆ box a b ⟷ (∀i∈Basis. c∙i ≤ d∙i) ⟶ (∀i∈Basis. a∙i < c∙i ∧ d∙i < b∙i)" (is ?th2)
and "box c d ⊆ cbox a b ⟷ (∀i∈Basis. c∙i < d∙i) ⟶ (∀i∈Basis. a∙i ≤ c∙i ∧ d∙i ≤ b∙i)" (is ?th3)
and "box c d ⊆ box a b ⟷ (∀i∈Basis. c∙i < d∙i) ⟶ (∀i∈Basis. a∙i ≤ c∙i ∧ d∙i ≤ b∙i)" (is ?th4)
proof -
let ?lesscd = "∀i∈Basis. c∙i < d∙i"
let ?lerhs = "∀i∈Basis. a∙i ≤ c∙i ∧ d∙i ≤ b∙i"
show ?th1 ?th2
by (fastforce simp: mem_box)+
have acdb: "a∙i ≤ c∙i ∧ d∙i ≤ b∙i"
if i: "i ∈ Basis" and box: "box c d ⊆ cbox a b" and cd: "⋀i. i ∈ Basis ⟹ c∙i < d∙i" for i
proof -
have "box c d ≠ {}"
using that
unfolding box_eq_empty by force
{ let ?x = "(∑j∈Basis. (if j=i then ((min (a∙j) (d∙j))+c∙j)/2 else (c∙j+d∙j)/2) *⇩R j)::'a"
assume *: "a∙i > c∙i"
then have "c ∙ j < ?x ∙ j ∧ ?x ∙ j < d ∙ j" if "j ∈ Basis" for j
using cd that by (fastforce simp add: i *)
then have "?x ∈ box c d"
unfolding mem_box by auto
moreover have "?x ∉ cbox a b"
using i cd * by (force simp: mem_box)
ultimately have False using box by auto
}
then have "a∙i ≤ c∙i" by force
moreover
{ let ?x = "(∑j∈Basis. (if j=i then ((max (b∙j) (c∙j))+d∙j)/2 else (c∙j+d∙j)/2) *⇩R j)::'a"
assume *: "b∙i < d∙i"
then have "d ∙ j > ?x ∙ j ∧ ?x ∙ j > c ∙ j" if "j ∈ Basis" for j
using cd that by (fastforce simp add: i *)
then have "?x ∈ box c d"
unfolding mem_box by auto
moreover have "?x ∉ cbox a b"
using i cd * by (force simp: mem_box)
ultimately have False using box by auto
}
then have "b∙i ≥ d∙i" by (rule ccontr) auto
ultimately show ?thesis by auto
qed
show ?th3
using acdb by (fastforce simp add: mem_box)
have acdb': "a∙i ≤ c∙i ∧ d∙i ≤ b∙i"
if "i ∈ Basis" "box c d ⊆ box a b" "⋀i. i ∈ Basis ⟹ c∙i < d∙i" for i
using box_subset_cbox[of a b] that acdb by auto
show ?th4
using acdb' by (fastforce simp add: mem_box)
qed
lemma eq_cbox: "cbox a b = cbox c d ⟷ cbox a b = {} ∧ cbox c d = {} ∨ a = c ∧ b = d"
(is "?lhs = ?rhs")
proof
assume ?lhs
then have "cbox a b ⊆ cbox c d" "cbox c d ⊆ cbox a b"
by auto
then show ?rhs
by (force simp: subset_box box_eq_empty intro: antisym euclidean_eqI)
qed auto
lemma eq_cbox_box [simp]: "cbox a b = box c d ⟷ cbox a b = {} ∧ box c d = {}"
(is "?lhs ⟷ ?rhs")
proof
assume L: ?lhs
then have "cbox a b ⊆ box c d" "box c d ⊆ cbox a b"
by auto
with L subset_box show ?rhs
by (smt (verit) SOME_Basis box_ne_empty(1))
qed force
lemma eq_box_cbox [simp]: "box a b = cbox c d ⟷ box a b = {} ∧ cbox c d = {}"
by (metis eq_cbox_box)
lemma eq_box: "box a b = box c d ⟷ box a b = {} ∧ box c d = {} ∨ a = c ∧ b = d"
(is "?lhs ⟷ ?rhs")
proof
assume L: ?lhs
then have "box a b ⊆ box c d" "box c d ⊆ box a b"
by auto
then show ?rhs
unfolding subset_box by (smt (verit) box_ne_empty(2) euclidean_eq_iff)+
qed force
lemma subset_box_complex:
"cbox a b ⊆ cbox c d ⟷
(Re a ≤ Re b ∧ Im a ≤ Im b) ⟶ Re a ≥ Re c ∧ Im a ≥ Im c ∧ Re b ≤ Re d ∧ Im b ≤ Im d"
"cbox a b ⊆ box c d ⟷
(Re a ≤ Re b ∧ Im a ≤ Im b) ⟶ Re a > Re c ∧ Im a > Im c ∧ Re b < Re d ∧ Im b < Im d"
"box a b ⊆ cbox c d ⟷
(Re a < Re b ∧ Im a < Im b) ⟶ Re a ≥ Re c ∧ Im a ≥ Im c ∧ Re b ≤ Re d ∧ Im b ≤ Im d"
"box a b ⊆ box c d ⟷
(Re a < Re b ∧ Im a < Im b) ⟶ Re a ≥ Re c ∧ Im a ≥ Im c ∧ Re b ≤ Re d ∧ Im b ≤ Im d"
by (subst subset_box; force simp: Basis_complex_def)+
lemma in_cbox_complex_iff:
"x ∈ cbox a b ⟷ Re x ∈ {Re a..Re b} ∧ Im x ∈ {Im a..Im b}"
by (cases x; cases a; cases b) (auto simp: cbox_Complex_eq)
lemma cbox_complex_of_real: "cbox (complex_of_real x) (complex_of_real y) = complex_of_real ` {x..y}"
proof -
have "(x ≤ Re z ∧ Re z ≤ y ∧ Im z = 0) = (z ∈ complex_of_real ` {x..y})" for z
by (cases z) (simp add: complex_eq_cancel_iff2 image_iff)
then show ?thesis
by (auto simp: in_cbox_complex_iff)
qed
lemma box_Complex_eq:
"box (Complex a c) (Complex b d) = (λ(x,y). Complex x y) ` (box a b × box c d)"
by (auto simp: box_def Basis_complex_def image_iff complex_eq_iff)
lemma in_box_complex_iff:
"x ∈ box a b ⟷ Re x ∈ {Re a<..<Re b} ∧ Im x ∈ {Im a<..<Im b}"
by (cases x; cases a; cases b) (auto simp: box_Complex_eq)
lemma box_complex_of_real [simp]: "box (complex_of_real x) (complex_of_real y) = {}"
by (auto simp: in_box_complex_iff)
lemma Int_interval:
fixes a :: "'a::euclidean_space"
shows "cbox a b ∩ cbox c d =
cbox (∑i∈Basis. max (a∙i) (c∙i) *⇩R i) (∑i∈Basis. min (b∙i) (d∙i) *⇩R i)"
unfolding set_eq_iff and Int_iff and mem_box
by auto
lemma disjoint_interval:
fixes a::"'a::euclidean_space"
shows "cbox a b ∩ cbox c d = {} ⟷ (∃i∈Basis. (b∙i < a∙i ∨ d∙i < c∙i ∨ b∙i < c∙i ∨ d∙i < a∙i))" (is ?th1)
and "cbox a b ∩ box c d = {} ⟷ (∃i∈Basis. (b∙i < a∙i ∨ d∙i ≤ c∙i ∨ b∙i ≤ c∙i ∨ d∙i ≤ a∙i))" (is ?th2)
and "box a b ∩ cbox c d = {} ⟷ (∃i∈Basis. (b∙i ≤ a∙i ∨ d∙i < c∙i ∨ b∙i ≤ c∙i ∨ d∙i ≤ a∙i))" (is ?th3)
and "box a b ∩ box c d = {} ⟷ (∃i∈Basis. (b∙i ≤ a∙i ∨ d∙i ≤ c∙i ∨ b∙i ≤ c∙i ∨ d∙i ≤ a∙i))" (is ?th4)
proof -
let ?z = "(∑i∈Basis. (((max (a∙i) (c∙i)) + (min (b∙i) (d∙i))) / 2) *⇩R i)::'a"
have **: "⋀P Q. (⋀i :: 'a. i ∈ Basis ⟹ Q ?z i ⟹ P i) ⟹
(⋀i x :: 'a. i ∈ Basis ⟹ P i ⟹ Q x i) ⟹ (∀x. ∃i∈Basis. Q x i) ⟷ (∃i∈Basis. P i)"
by blast
note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10)
show ?th1 unfolding * by (intro **) auto
show ?th2 unfolding * by (intro **) auto
show ?th3 unfolding * by (intro **) auto
show ?th4 unfolding * by (intro **) auto
qed
lemma UN_box_eq_UNIV: "(⋃i::nat. box (- (real i *⇩R One)) (real i *⇩R One)) = UNIV"
proof -
have "¦x ∙ b¦ < real_of_int (⌈Max ((λb. ¦x ∙ b¦)`Basis)⌉ + 1)"
if [simp]: "b ∈ Basis" for x b :: 'a
proof -
have "¦x ∙ b¦ ≤ real_of_int ⌈¦x ∙ b¦⌉"
by (rule le_of_int_ceiling)
also have "… ≤ real_of_int ⌈Max ((λb. ¦x ∙ b¦)`Basis)⌉"
by (auto intro!: ceiling_mono)
also have "… < real_of_int (⌈Max ((λb. ¦x ∙ b¦)`Basis)⌉ + 1)"
by simp
finally show ?thesis .
qed
then have "∃n::nat. ∀b∈Basis. ¦x ∙ b¦ < real n" for x :: 'a
by (metis order.strict_trans reals_Archimedean2)
moreover have "⋀x b::'a. ⋀n::nat. ¦x ∙ b¦ < real n ⟷ - real n < x ∙ b ∧ x ∙ b < real n"
by auto
ultimately show ?thesis
by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
qed
lemma image_affinity_cbox: fixes m::real
fixes a b c :: "'a::euclidean_space"
shows "(λx. m *⇩R x + c) ` cbox a b =
(if cbox a b = {} then {}
else (if 0 ≤ m then cbox (m *⇩R a + c) (m *⇩R b + c)
else cbox (m *⇩R b + c) (m *⇩R a + c)))"
proof (cases "m = 0")
case True
{
fix x
assume "∀i∈Basis. x ∙ i ≤ c ∙ i" "∀i∈Basis. c ∙ i ≤ x ∙ i"
then have "x = c"
by (simp add: dual_order.antisym euclidean_eqI)
}
moreover have "c ∈ cbox (m *⇩R a + c) (m *⇩R b + c)"
unfolding True by auto
ultimately show ?thesis using True by (auto simp: cbox_def)
next
case False
{
fix y
assume "∀i∈Basis. a ∙ i ≤ y ∙ i" "∀i∈Basis. y ∙ i ≤ b ∙ i" "m > 0"
then have "∀i∈Basis. (m *⇩R a + c) ∙ i ≤ (m *⇩R y + c) ∙ i"
and "∀i∈Basis. (m *⇩R y + c) ∙ i ≤ (m *⇩R b + c) ∙ i"
by (auto simp: inner_distrib)
}
moreover
{
fix y
assume "∀i∈Basis. a ∙ i ≤ y ∙ i" "∀i∈Basis. y ∙ i ≤ b ∙ i" "m < 0"
then have "∀i∈Basis. (m *⇩R b + c) ∙ i ≤ (m *⇩R y + c) ∙ i"
and "∀i∈Basis. (m *⇩R y + c) ∙ i ≤ (m *⇩R a + c) ∙ i"
by (auto simp: mult_left_mono_neg inner_distrib)
}
moreover
{
fix y
assume "m > 0" and "∀i∈Basis. (m *⇩R a + c) ∙ i ≤ y ∙ i"
and "∀i∈Basis. y ∙ i ≤ (m *⇩R b + c) ∙ i"
then have "y ∈ (λx. m *⇩R x + c) ` cbox a b"
unfolding image_iff Bex_def mem_box
apply (intro exI[where x="(1 / m) *⇩R (y - c)"])
apply (auto simp: pos_le_divide_eq pos_divide_le_eq mult.commute inner_distrib inner_diff_left)
done
}
moreover
{
fix y
assume "∀i∈Basis. (m *⇩R b + c) ∙ i ≤ y ∙ i" "∀i∈Basis. y ∙ i ≤ (m *⇩R a + c) ∙ i" "m < 0"
then have "y ∈ (λx. m *⇩R x + c) ` cbox a b"
unfolding image_iff Bex_def mem_box
apply (intro exI[where x="(1 / m) *⇩R (y - c)"])
apply (auto simp: neg_le_divide_eq neg_divide_le_eq mult.commute inner_distrib inner_diff_left)
done
}
ultimately show ?thesis using False by (auto simp: cbox_def)
qed
lemma image_smult_cbox:"(λx. m *⇩R (x::_::euclidean_space)) ` cbox a b =
(if cbox a b = {} then {} else if 0 ≤ m then cbox (m *⇩R a) (m *⇩R b) else cbox (m *⇩R b) (m *⇩R a))"
using image_affinity_cbox[of m 0 a b] by auto
lemma swap_continuous:
assumes "continuous_on (cbox (a,c) (b,d)) (λ(x,y). f x y)"
shows "continuous_on (cbox (c,a) (d,b)) (λ(x, y). f y x)"
proof -
have "(λ(x, y). f y x) = (λ(x, y). f x y) ∘ prod.swap"
by auto
then show ?thesis
by (metis assms continuous_on_compose continuous_on_swap swap_cbox_Pair)
qed
lemma open_contains_cbox:
fixes x :: "'a :: euclidean_space"
assumes "open A" "x ∈ A"
obtains a b where "cbox a b ⊆ A" "x ∈ box a b" "∀i∈Basis. a ∙ i < b ∙ i"
proof -
from assms obtain R where R: "R > 0" "ball x R ⊆ A"
by (auto simp: open_contains_ball)
define r :: real where "r = R / (2 * sqrt DIM('a))"
from ‹R > 0› have [simp]: "r > 0" by (auto simp: r_def)
define d :: 'a where "d = r *⇩R Topology_Euclidean_Space.One"
have "cbox (x - d) (x + d) ⊆ A"
proof safe
fix y assume y: "y ∈ cbox (x - d) (x + d)"
have "dist x y = sqrt (∑i∈Basis. (dist (x ∙ i) (y ∙ i))⇧2)"
by (subst euclidean_dist_l2) (auto simp: L2_set_def)
also from y have "sqrt (∑i∈Basis. (dist (x ∙ i) (y ∙ i))⇧2) ≤ sqrt (∑i∈(Basis::'a set). r⇧2)"
by (intro real_sqrt_le_mono sum_mono power_mono)
(auto simp: dist_norm d_def cbox_def algebra_simps)
also have "… = sqrt (DIM('a) * r⇧2)" by simp
also have "DIM('a) * r⇧2 = (R / 2) ^ 2"
by (simp add: r_def power_divide)
also have "sqrt … = R / 2"
using ‹R > 0› by simp
also from ‹R > 0› have "… < R" by simp
finally have "y ∈ ball x R" by simp
with R show "y ∈ A" by blast
qed
thus ?thesis
using that[of "x - d" "x + d"] by (auto simp: algebra_simps d_def box_def)
qed
lemma open_contains_box:
fixes x :: "'a :: euclidean_space"
assumes "open A" "x ∈ A"
obtains a b where "box a b ⊆ A" "x ∈ box a b" "∀i∈Basis. a ∙ i < b ∙ i"
by (meson assms box_subset_cbox dual_order.trans open_contains_cbox)
lemma inner_image_box:
assumes "(i :: 'a :: euclidean_space) ∈ Basis"
assumes "∀i∈Basis. a ∙ i < b ∙ i"
shows "(λx. x ∙ i) ` box a b = {a ∙ i<..<b ∙ i}"
proof safe
fix x assume x: "x ∈ {a ∙ i<..<b ∙ i}"
let ?y = "(∑j∈Basis. (if i = j then x else (a + b) ∙ j / 2) *⇩R j)"
from x assms have "?y ∙ i ∈ (λx. x ∙ i) ` box a b"
by (intro imageI) (auto simp: box_def algebra_simps)
also have "?y ∙ i = (∑j∈Basis. (if i = j then x else (a + b) ∙ j / 2) * (j ∙ i))"
by (simp add: inner_sum_left)
also have "… = (∑j∈Basis. if i = j then x else 0)"
by (intro sum.cong) (auto simp: inner_not_same_Basis assms)
also have "… = x" using assms by simp
finally show "x ∈ (λx. x ∙ i) ` box a b" .
qed (insert assms, auto simp: box_def)
lemma inner_image_cbox:
assumes "(i :: 'a :: euclidean_space) ∈ Basis"
assumes "∀i∈Basis. a ∙ i ≤ b ∙ i"
shows "(λx. x ∙ i) ` cbox a b = {a ∙ i..b ∙ i}"
proof safe
fix x assume x: "x ∈ {a ∙ i..b ∙ i}"
let ?y = "(∑j∈Basis. (if i = j then x else a ∙ j) *⇩R j)"
from x assms have "?y ∙ i ∈ (λx. x ∙ i) ` cbox a b"
by (intro imageI) (auto simp: cbox_def)
also have "?y ∙ i = (∑j∈Basis. (if i = j then x else a ∙ j) * (j ∙ i))"
by (simp add: inner_sum_left)
also have "… = (∑j∈Basis. if i = j then x else 0)"
by (intro sum.cong) (auto simp: inner_not_same_Basis assms)
also have "… = x" using assms by simp
finally show "x ∈ (λx. x ∙ i) ` cbox a b" .
qed (insert assms, auto simp: cbox_def)
subsection ‹General Intervals›
definition "is_interval (s::('a::euclidean_space) set) ⟷
(∀a∈s. ∀b∈s. ∀x. (∀i∈Basis. ((a∙i ≤ x∙i ∧ x∙i ≤ b∙i) ∨ (b∙i ≤ x∙i ∧ x∙i ≤ a∙i))) ⟶ x ∈ s)"
lemma is_interval_1:
"is_interval (s::real set) ⟷ (∀a∈s. ∀b∈s. ∀ x. a ≤ x ∧ x ≤ b ⟶ x ∈ s)"
unfolding is_interval_def by auto
lemma is_interval_Int: "is_interval X ⟹ is_interval Y ⟹ is_interval (X ∩ Y)"
unfolding is_interval_def
by blast
lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
by (meson order_trans le_less_trans less_le_trans less_trans)+
lemma is_interval_empty [iff]: "is_interval {}"
unfolding is_interval_def by simp
lemma is_interval_univ [iff]: "is_interval UNIV"
unfolding is_interval_def by simp
lemma mem_is_intervalI:
assumes "is_interval S"
and "a ∈ S" "b ∈ S"
and "⋀i. i ∈ Basis ⟹ a ∙ i ≤ x ∙ i ∧ x ∙ i ≤ b ∙ i ∨ b ∙ i ≤ x ∙ i ∧ x ∙ i ≤ a ∙ i"
shows "x ∈ S"
using assms is_interval_def by force
lemma interval_subst:
fixes S::"'a::euclidean_space set"
assumes "is_interval S"
and "x ∈ S" "y j ∈ S"
and "j ∈ Basis"
shows "(∑i∈Basis. (if i = j then y i ∙ i else x ∙ i) *⇩R i) ∈ S"
by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms)
lemma mem_box_componentwiseI:
fixes S::"'a::euclidean_space set"
assumes "is_interval S"
assumes "⋀i. i ∈ Basis ⟹ x ∙ i ∈ ((λx. x ∙ i) ` S)"
shows "x ∈ S"
proof -
from assms have "∀i ∈ Basis. ∃s ∈ S. x ∙ i = s ∙ i"
by auto
with finite_Basis obtain s and bs::"'a list"
where s: "⋀i. i ∈ Basis ⟹ x ∙ i = s i ∙ i" "⋀i. i ∈ Basis ⟹ s i ∈ S"
and bs: "set bs = Basis" "distinct bs"
by (metis finite_distinct_list)
from nonempty_Basis s obtain j where j: "j ∈ Basis" "s j ∈ S"
by blast
define y where
"y = rec_list (s j) (λj _ Y. (∑i∈Basis. (if i = j then s i ∙ i else Y ∙ i) *⇩R i))"
have "x = (∑i∈Basis. (if i ∈ set bs then s i ∙ i else s j ∙ i) *⇩R i)"
using bs by (auto simp: s(1)[symmetric] euclidean_representation)
also have [symmetric]: "y bs = …"
using bs(2) bs(1)[THEN equalityD1]
by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
also have "y bs ∈ S"
using bs(1)[THEN equalityD1]
proof (induction bs)
case Nil
then show ?case
by (simp add: j y_def)
next
case (Cons a bs)
then show ?case
using interval_subst[OF assms(1)] s by (simp add: y_def)
qed
finally show ?thesis .
qed
lemma cbox01_nonempty [simp]: "cbox 0 One ≠ {}"
by (simp add: box_ne_empty inner_Basis inner_sum_left sum_nonneg)
lemma box01_nonempty [simp]: "box 0 One ≠ {}"
by (simp add: box_ne_empty inner_Basis inner_sum_left)
lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast
lemma interval_subset_is_interval:
assumes "is_interval S"
shows "cbox a b ⊆ S ⟷ cbox a b = {} ∨ a ∈ S ∧ b ∈ S" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs using box_ne_empty(1) mem_box(2) by fastforce
next
assume ?rhs
have "cbox a b ⊆ S" if "a ∈ S" "b ∈ S"
using assms that
by (force simp: mem_box intro: mem_is_intervalI)
with ‹?rhs› show ?lhs
by blast
qed
lemma is_real_interval_union:
"is_interval (X ∪ Y)"
if X: "is_interval X" and Y: "is_interval Y" and I: "(X ≠ {} ⟹ Y ≠ {} ⟹ X ∩ Y ≠ {})"
for X Y::"real set"
proof -
consider "X ≠ {}" "Y ≠ {}" | "X = {}" | "Y = {}" by blast
then show ?thesis
proof cases
case 1
then obtain r where "r ∈ X ∨ X ∩ Y = {}" "r ∈ Y ∨ X ∩ Y = {}"
by blast
then show ?thesis
using I 1 X Y unfolding is_interval_1
by (metis (full_types) Un_iff le_cases)
qed (use that in auto)
qed
lemma is_interval_translationI:
assumes "is_interval X"
shows "is_interval ((+) x ` X)"
unfolding is_interval_def
proof safe
fix b d e
assume "b ∈ X" "d ∈ X"
"∀i∈Basis. (x + b) ∙ i ≤ e ∙ i ∧ e ∙ i ≤ (x + d) ∙ i ∨
(x + d) ∙ i ≤ e ∙ i ∧ e ∙ i ≤ (x + b) ∙ i"
hence "e - x ∈ X"
by (intro mem_is_intervalI[OF assms ‹b ∈ X› ‹d ∈ X›, of "e - x"])
(auto simp: algebra_simps)
thus "e ∈ (+) x ` X" by force
qed
lemma is_interval_uminusI:
assumes "is_interval X"
shows "is_interval (uminus ` X)"
unfolding is_interval_def
proof safe
fix b d e
assume "b ∈ X" "d ∈ X"
"∀i∈Basis. (- b) ∙ i ≤ e ∙ i ∧ e ∙ i ≤ (- d) ∙ i ∨
(- d) ∙ i ≤ e ∙ i ∧ e ∙ i ≤ (- b) ∙ i"
hence "- e ∈ X"
by (smt (verit, ccfv_threshold) assms inner_minus_left mem_is_intervalI)
thus "e ∈ uminus ` X" by force
qed
lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"]
by (auto simp: image_image)
lemma is_interval_neg_translationI:
assumes "is_interval X"
shows "is_interval ((-) x ` X)"
proof -
have "(-) x ` X = (+) x ` uminus ` X"
by (force simp: algebra_simps)
also have "is_interval …"
by (metis is_interval_uminusI is_interval_translationI assms)
finally show ?thesis .
qed
lemma is_interval_translation[simp]:
"is_interval ((+) x ` X) = is_interval X"
using is_interval_neg_translationI[of "(+) x ` X" x]
by (auto intro!: is_interval_translationI simp: image_image)
lemma is_interval_minus_translation[simp]:
shows "is_interval ((-) x ` X) = is_interval X"
proof -
have "(-) x ` X = (+) x ` uminus ` X"
by (force simp: algebra_simps)
also have "is_interval … = is_interval X"
by simp
finally show ?thesis .
qed
lemma is_interval_minus_translation'[simp]:
shows "is_interval ((λx. x - c) ` X) = is_interval X"
using is_interval_translation[of "-c" X]
by (metis image_cong uminus_add_conv_diff)
lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
by (simp add: cball_eq_atLeastAtMost is_interval_def)
lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real
by (simp add: ball_eq_greaterThanLessThan is_interval_def)
subsection ‹Bounded Projections›
lemma bounded_inner_imp_bdd_above:
assumes "bounded s"
shows "bdd_above ((λx. x ∙ a) ` s)"
by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)
lemma bounded_inner_imp_bdd_below:
assumes "bounded s"
shows "bdd_below ((λx. x ∙ a) ` s)"
by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)
subsection ‹Structural rules for pointwise continuity›
lemma continuous_infnorm[continuous_intros]:
"continuous F f ⟹ continuous F (λx. infnorm (f x))"
unfolding continuous_def by (rule tendsto_infnorm)
lemma continuous_inner[continuous_intros]:
assumes "continuous F f"
and "continuous F g"
shows "continuous F (λx. inner (f x) (g x))"
using assms unfolding continuous_def by (rule tendsto_inner)
subsection ‹Structural rules for setwise continuity›
lemma continuous_on_infnorm[continuous_intros]:
"continuous_on s f ⟹ continuous_on s (λx. infnorm (f x))"
unfolding continuous_on by (fast intro: tendsto_infnorm)
lemma continuous_on_inner[continuous_intros]:
fixes g :: "'a::topological_space ⇒ 'b::real_inner"
assumes "continuous_on s f"
and "continuous_on s g"
shows "continuous_on s (λx. inner (f x) (g x))"
using bounded_bilinear_inner assms
by (rule bounded_bilinear.continuous_on)
subsection ‹Openness of halfspaces.›
lemma open_halfspace_lt: "open {x. inner a x < b}"
by (simp add: open_Collect_less continuous_on_inner)
lemma open_halfspace_gt: "open {x. inner a x > b}"
by (simp add: open_Collect_less continuous_on_inner)
lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. x∙i < a}"
by (simp add: open_Collect_less continuous_on_inner)
lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x∙i > a}"
by (simp add: open_Collect_less continuous_on_inner)
lemma eucl_less_eq_halfspaces:
fixes a :: "'a::euclidean_space"
shows "{x. x <e a} = (⋂i∈Basis. {x. x ∙ i < a ∙ i})"
"{x. a <e x} = (⋂i∈Basis. {x. a ∙ i < x ∙ i})"
by (auto simp: eucl_less_def)
lemma open_Collect_eucl_less[simp, intro]:
fixes a :: "'a::euclidean_space"
shows "open {x. x <e a}" "open {x. a <e x}"
by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
subsection ‹Closure and Interior of halfspaces and hyperplanes›
lemma continuous_at_inner: "continuous (at x) (inner a)"
unfolding continuous_at by (intro tendsto_intros)
lemma closed_halfspace_le: "closed {x. inner a x ≤ b}"
by (simp add: closed_Collect_le continuous_on_inner)
lemma closed_halfspace_ge: "closed {x. inner a x ≥ b}"
by (simp add: closed_Collect_le continuous_on_inner)
lemma closed_hyperplane: "closed {x. inner a x = b}"
by (simp add: closed_Collect_eq continuous_on_inner)
lemma closed_halfspace_component_le: "closed {x::'a::euclidean_space. x∙i ≤ a}"
by (simp add: closed_Collect_le continuous_on_inner)
lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. x∙i ≥ a}"
by (simp add: closed_Collect_le continuous_on_inner)
lemma closed_interval_left:
fixes b :: "'a::euclidean_space"
shows "closed {x::'a. ∀i∈Basis. x∙i ≤ b∙i}"
by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner)
lemma closed_interval_right:
fixes a :: "'a::euclidean_space"
shows "closed {x::'a. ∀i∈Basis. a∙i ≤ x∙i}"
by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner)
lemma interior_halfspace_le [simp]:
assumes "a ≠ 0"
shows "interior {x. a ∙ x ≤ b} = {x. a ∙ x < b}"
proof -
have *: "a ∙ x < b" if x: "x ∈ S" and S: "S ⊆ {x. a ∙ x ≤ b}" and "open S" for S x
proof -
obtain e where "e>0" and e: "cball x e ⊆ S"
using ‹open S› open_contains_cball x by blast
then have "x + (e / norm a) *⇩R a ∈ cball x e"
by (simp add: dist_norm)
then have "x + (e / norm a) *⇩R a ∈ S"
using e by blast
then have "x + (e / norm a) *⇩R a ∈ {x. a ∙ x ≤ b}"
using S by blast
moreover have "e * (a ∙ a) / norm a > 0"
by (simp add: ‹0 < e› assms)
ultimately show ?thesis
by (simp add: algebra_simps)
qed
show ?thesis
by (rule interior_unique) (auto simp: open_halfspace_lt *)
qed
lemma interior_halfspace_ge [simp]:
"a ≠ 0 ⟹ interior {x. a ∙ x ≥ b} = {x. a ∙ x > b}"
using interior_halfspace_le [of "-a" "-b"] by simp
lemma closure_halfspace_lt [simp]:
assumes "a ≠ 0"
shows "closure {x. a ∙ x < b} = {x. a ∙ x ≤ b}"
proof -
have [simp]: "-{x. a ∙ x < b} = {x. a ∙ x ≥ b}"
by force
then show ?thesis
using interior_halfspace_ge [of a b] assms
by (force simp: closure_interior)
qed
lemma closure_halfspace_gt [simp]:
"a ≠ 0 ⟹ closure {x. a ∙ x > b} = {x. a ∙ x ≥ b}"
using closure_halfspace_lt [of "-a" "-b"] by simp
lemma interior_hyperplane [simp]:
assumes "a ≠ 0"
shows "interior {x. a ∙ x = b} = {}"
proof -
have [simp]: "{x. a ∙ x = b} = {x. a ∙ x ≤ b} ∩ {x. a ∙ x ≥ b}"
by force
then show ?thesis
by (auto simp: assms)
qed
lemma frontier_halfspace_le:
assumes "a ≠ 0 ∨ b ≠ 0"
shows "frontier {x. a ∙ x ≤ b} = {x. a ∙ x = b}"
proof (cases "a = 0")
case True with assms show ?thesis by simp
next
case False then show ?thesis
by (force simp: frontier_def closed_halfspace_le)
qed
lemma frontier_halfspace_ge:
assumes "a ≠ 0 ∨ b ≠ 0"
shows "frontier {x. a ∙ x ≥ b} = {x. a ∙ x = b}"
proof (cases "a = 0")
case True with assms show ?thesis by simp
next
case False then show ?thesis
by (force simp: frontier_def closed_halfspace_ge)
qed
lemma frontier_halfspace_lt:
assumes "a ≠ 0 ∨ b ≠ 0"
shows "frontier {x. a ∙ x < b} = {x. a ∙ x = b}"
proof (cases "a = 0")
case True with assms show ?thesis by simp
next
case False then show ?thesis
by (force simp: frontier_def interior_open open_halfspace_lt)
qed
lemma frontier_halfspace_gt:
assumes "a ≠ 0 ∨ b ≠ 0"
shows "frontier {x. a ∙ x > b} = {x. a ∙ x = b}"
proof (cases "a = 0")
case True with assms show ?thesis by simp
next
case False then show ?thesis
by (force simp: frontier_def interior_open open_halfspace_gt)
qed
subsection‹Some more convenient intermediate-value theorem formulations›
lemma connected_ivt_hyperplane:
assumes "connected S" and xy: "x ∈ S" "y ∈ S" and b: "inner a x ≤ b" "b ≤ inner a y"
shows "∃z ∈ S. inner a z = b"
proof (rule ccontr)
assume as:"¬ (∃z∈S. inner a z = b)"
let ?A = "{x. inner a x < b}"
let ?B = "{x. inner a x > b}"
have "open ?A" "open ?B"
using open_halfspace_lt and open_halfspace_gt by auto
moreover have "?A ∩ ?B = {}" by auto
moreover have "S ⊆ ?A ∪ ?B" using as by auto
ultimately show False
using ‹connected S› unfolding connected_def
by (smt (verit, del_insts) as b disjoint_iff empty_iff mem_Collect_eq xy)
qed
lemma connected_ivt_component:
fixes x::"'a::euclidean_space"
shows "connected S ⟹ x ∈ S ⟹ y ∈ S ⟹ x∙k ≤ a ⟹ a ≤ y∙k ⟹ (∃z∈S. z∙k = a)"
using connected_ivt_hyperplane[of S x y "k::'a" a]
by (auto simp: inner_commute)
subsection ‹Limit Component Bounds›
lemma Lim_component_le:
fixes f :: "'a ⇒ 'b::euclidean_space"
assumes "(f ⤏ l) net"
and "¬ (trivial_limit net)"
and "eventually (λx. f(x)∙i ≤ b) net"
shows "l∙i ≤ b"
by (rule tendsto_le[OF assms(2) tendsto_const tendsto_inner[OF assms(1) tendsto_const] assms(3)])
lemma Lim_component_ge:
fixes f :: "'a ⇒ 'b::euclidean_space"
assumes "(f ⤏ l) net"
and "¬ (trivial_limit net)"
and "eventually (λx. b ≤ (f x)∙i) net"
shows "b ≤ l∙i"
by (rule tendsto_le[OF assms(2) tendsto_inner[OF assms(1) tendsto_const] tendsto_const assms(3)])
lemma Lim_component_eq:
fixes f :: "'a ⇒ 'b::euclidean_space"
assumes net: "(f ⤏ l) net" "¬ trivial_limit net"
and ev:"eventually (λx. f(x)∙i = b) net"
shows "l∙i = b"
using ev[unfolded order_eq_iff eventually_conj_iff]
using Lim_component_ge[OF net, of b i]
using Lim_component_le[OF net, of i b]
by auto
lemma open_box[intro]: "open (box a b)"
proof -
have "open (⋂i∈Basis. ((∙) i) -` {a ∙ i <..< b ∙ i})"
by (auto intro!: continuous_open_vimage continuous_inner continuous_ident continuous_const)
also have "(⋂i∈Basis. ((∙) i) -` {a ∙ i <..< b ∙ i}) = box a b"
by (auto simp: box_def inner_commute)
finally show ?thesis .
qed
lemma closed_cbox[intro]:
fixes a b :: "'a::euclidean_space"
shows "closed (cbox a b)"
proof -
have "closed (⋂i∈Basis. (λx. x∙i) -` {a∙i .. b∙i})"
by (intro closed_INT ballI continuous_closed_vimage allI
linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
also have "(⋂i∈Basis. (λx. x∙i) -` {a∙i .. b∙i}) = cbox a b"
by (auto simp: cbox_def)
finally show "closed (cbox a b)" .
qed
lemma interior_cbox [simp]:
fixes a b :: "'a::euclidean_space"
shows "interior (cbox a b) = box a b" (is "?L = ?R")
proof(rule subset_antisym)
show "?R ⊆ ?L"
using box_subset_cbox open_box
by (rule interior_maximal)
{
fix x
assume "x ∈ interior (cbox a b)"
then obtain s where s: "open s" "x ∈ s" "s ⊆ cbox a b" ..
then obtain e where "e>0" and e:"∀x'. dist x' x < e ⟶ x' ∈ cbox a b"
unfolding open_dist and subset_eq by auto
{
fix i :: 'a
assume i: "i ∈ Basis"
have "dist (x - (e / 2) *⇩R i) x < e"
and "dist (x + (e / 2) *⇩R i) x < e"
using norm_Basis[OF i] ‹e>0› by (auto simp: dist_norm)
then have "a ∙ i ≤ (x - (e / 2) *⇩R i) ∙ i" and "(x + (e / 2) *⇩R i) ∙ i ≤ b ∙ i"
using e[THEN spec[where x="x - (e/2) *⇩R i"]]
and e[THEN spec[where x="x + (e/2) *⇩R i"]]
unfolding mem_box using i by blast+
then have "a ∙ i < x ∙ i" and "x ∙ i < b ∙ i"
using ‹e>0› i
by (auto simp: inner_diff_left inner_Basis inner_add_left)
}
then have "x ∈ box a b"
unfolding mem_box by auto
}
then show "?L ⊆ ?R" ..
qed
lemma bounded_cbox [simp]:
fixes a :: "'a::euclidean_space"
shows "bounded (cbox a b)"
proof -
let ?b = "∑i∈Basis. ¦a∙i¦ + ¦b∙i¦"
{
fix x :: "'a"
assume "⋀i. i∈Basis ⟹ a ∙ i ≤ x ∙ i ∧ x ∙ i ≤ b ∙ i"
then have "(∑i∈Basis. ¦x ∙ i¦) ≤ ?b"
by (force simp: intro!: sum_mono)
then have "norm x ≤ ?b"
using norm_le_l1[of x] by auto
}
then show ?thesis
unfolding cbox_def bounded_iff by force
qed
lemma bounded_box [simp]:
fixes a :: "'a::euclidean_space"
shows "bounded (box a b)"
by (metis bounded_cbox bounded_interior interior_cbox)
lemma not_interval_UNIV [simp]:
fixes a :: "'a::euclidean_space"
shows "cbox a b ≠ UNIV" "box a b ≠ UNIV"
using bounded_box[of a b] bounded_cbox[of a b] by force+
lemma not_interval_UNIV2 [simp]:
fixes a :: "'a::euclidean_space"
shows "UNIV ≠ cbox a b" "UNIV ≠ box a b"
using bounded_box[of a b] bounded_cbox[of a b] by force+
lemma box_midpoint:
fixes a :: "'a::euclidean_space"
assumes "box a b ≠ {}"
shows "((1/2) *⇩R (a + b)) ∈ box a b"
proof -
have "a ∙ i < ((1 / 2) *⇩R (a + b)) ∙ i ∧ ((1 / 2) *⇩R (a + b)) ∙ i < b ∙ i" if "i ∈ Basis" for i
using assms that by (auto simp: inner_add_left box_ne_empty)
then show ?thesis unfolding mem_box by auto
qed
lemma open_cbox_convex:
fixes x :: "'a::euclidean_space"
assumes x: "x ∈ box a b"
and y: "y ∈ cbox a b"
and e: "0 < e" "e ≤ 1"
shows "(e *⇩R x + (1 - e) *⇩R y) ∈ box a b"
proof -
{
fix i :: 'a
assume i: "i ∈ Basis"
have "a ∙ i = e * (a ∙ i) + (1 - e) * (a ∙ i)"
unfolding left_diff_distrib by simp
also have "… < e * (x ∙ i) + (1 - e) * (y ∙ i)"
by (smt (verit, best) e i mem_box mult_le_cancel_left_pos mult_left_mono x y)
finally have "a ∙ i < (e *⇩R x + (1 - e) *⇩R y) ∙ i"
unfolding inner_simps by auto
moreover
{
have "b ∙ i = e * (b∙i) + (1 - e) * (b∙i)"
unfolding left_diff_distrib by simp
also have "… > e * (x ∙ i) + (1 - e) * (y ∙ i)"
by (smt (verit, best) e i mem_box mult_le_cancel_left_pos mult_left_mono x y)
finally have "(e *⇩R x + (1 - e) *⇩R y) ∙ i < b ∙ i"
unfolding inner_simps by auto
}
ultimately have "a ∙ i < (e *⇩R x + (1 - e) *⇩R y) ∙ i ∧ (e *⇩R x + (1 - e) *⇩R y) ∙ i < b ∙ i"
by auto
}
then show ?thesis
unfolding mem_box by auto
qed
lemma closure_cbox [simp]: "closure (cbox a b) = cbox a b"
by (simp add: closed_cbox)
lemma closure_box [simp]:
fixes a :: "'a::euclidean_space"
assumes "box a b ≠ {}"
shows "closure (box a b) = cbox a b"
proof -
have ab: "a <e b"
using assms by (simp add: eucl_less_def box_ne_empty)
let ?c = "(1 / 2) *⇩R (a + b)"
{
fix x
assume as: "x ∈ cbox a b"
define f where [abs_def]: "f n = x + (inverse (real n + 1)) *⇩R (?c - x)" for n
{
fix n
assume fn: "f n <e b ⟶ a <e f n ⟶ f n = x" and xc: "x ≠ ?c"
have *: "0 < inverse (real n + 1)" "inverse (real n + 1) ≤ 1"
unfolding inverse_le_1_iff by auto
have "(inverse (real n + 1)) *⇩R ((1 / 2) *⇩R (a + b)) + (1 - inverse (real n + 1)) *⇩R x =
x + (inverse (real n + 1)) *⇩R (((1 / 2) *⇩R (a + b)) - x)"
by (auto simp: algebra_simps)
then have "f n <e b" and "a <e f n"
using open_cbox_convex[OF box_midpoint[OF assms] as *]
unfolding f_def by (auto simp: box_def eucl_less_def)
then have False
using fn unfolding f_def using xc by auto
}
moreover
{
have "∃N::nat. ∀n≥N. inverse (real n + 1) < ε" if "ε > 0" for ε
using reals_Archimedean [of ε] that
by (metis inverse_inverse_eq inverse_less_imp_less nat_le_real_less order_less_trans
reals_Archimedean2)
then have "(λn. inverse (real n + 1)) ⇢ 0"
unfolding lim_sequentially by(auto simp: dist_norm)
then have "f ⇢ x"
unfolding f_def
using tendsto_add[OF tendsto_const, of "λn. (inverse (real n + 1)) *⇩R ((1 / 2) *⇩R (a + b) - x)" 0 sequentially x]
using tendsto_scaleR [OF _ tendsto_const, of "λn. inverse (real n + 1)" 0 sequentially "((1 / 2) *⇩R (a + b) - x)"]
by auto
}
ultimately have "x ∈ closure (box a b)"
using as box_midpoint[OF assms]
unfolding closure_def islimpt_sequential
by (cases "x=?c") (auto simp: in_box_eucl_less)
}
then show ?thesis
using closure_minimal[OF box_subset_cbox, of a b] by blast
qed
lemma bounded_subset_box_symmetric:
fixes S :: "('a::euclidean_space) set"
assumes "bounded S"
obtains a where "S ⊆ box (-a) a"
proof -
obtain b where "b>0" and b: "∀x∈S. norm x ≤ b"
using assms[unfolded bounded_pos] by auto
define a :: 'a where "a = (∑i∈Basis. (b + 1) *⇩R i)"
have "(-a)∙i < x∙i" and "x∙i < a∙i" if "x ∈ S" and i: "i ∈ Basis" for x i
using b Basis_le_norm[OF i, of x] that by (auto simp: a_def)
then have "S ⊆ box (-a) a"
by (auto simp: simp add: box_def)
then show ?thesis ..
qed
lemma bounded_subset_cbox_symmetric:
fixes S :: "('a::euclidean_space) set"
assumes "bounded S"
obtains a where "S ⊆ cbox (-a) a"
by (meson assms bounded_subset_box_symmetric box_subset_cbox order.trans)
lemma frontier_cbox:
fixes a b :: "'a::euclidean_space"
shows "frontier (cbox a b) = cbox a b - box a b"
unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] ..
lemma frontier_box:
fixes a b :: "'a::euclidean_space"
shows "frontier (box a b) = (if box a b = {} then {} else cbox a b - box a b)"
by (simp add: frontier_def interior_open open_box)
lemma Int_interval_mixed_eq_empty:
fixes a :: "'a::euclidean_space"
assumes "box c d ≠ {}"
shows "box a b ∩ cbox c d = {} ⟷ box a b ∩ box c d = {}"
unfolding closure_box[OF assms, symmetric]
unfolding open_Int_closure_eq_empty[OF open_box] ..
subsection ‹Class Instances›
lemma compact_lemma:
fixes f :: "nat ⇒ 'a::euclidean_space"
assumes "bounded (range f)"
shows "∀d⊆Basis. ∃l::'a. ∃ r.
strict_mono r ∧ (∀e>0. eventually (λn. ∀i∈d. dist (f (r n) ∙ i) (l ∙ i) < e) sequentially)"
by (rule compact_lemma_general[where unproj="λe. ∑i∈Basis. e i *⇩R i"])
(auto intro!: assms bounded_linear_inner_left bounded_linear_image
simp: euclidean_representation)
instance euclidean_space ⊆ heine_borel
proof
fix f :: "nat ⇒ 'a"
assume f: "bounded (range f)"
then obtain l::'a and r where r: "strict_mono r"
and l: "∀e>0. eventually (λn. ∀i∈Basis. dist (f (r n) ∙ i) (l ∙ i) < e) sequentially"
using compact_lemma [OF f] by blast
{
fix e::real
assume "e > 0"
hence "e / real_of_nat DIM('a) > 0" by (simp)
with l have "eventually (λn. ∀i∈Basis. dist (f (r n) ∙ i) (l ∙ i) < e / (real_of_nat DIM('a))) sequentially"
by simp
moreover
{ fix n
assume n: "∀i∈Basis. dist (f (r n) ∙ i) (l ∙ i) < e / (real_of_nat DIM('a))"
have "dist (f (r n)) l ≤ (∑i∈Basis. dist (f (r n) ∙ i) (l ∙ i))"
using L2_set_le_sum [OF zero_le_dist] by (subst euclidean_dist_l2)
also have "… < (∑i∈(Basis::'a set). e / (real_of_nat DIM('a)))"
by (meson eucl.finite_Basis n nonempty_Basis sum_strict_mono)
finally have "dist (f (r n)) l < e"
by auto
}
ultimately have "∀⇩F n in sequentially. dist (f (r n)) l < e"
by (rule eventually_mono)
}
then have *: "(f ∘ r) ⇢ l"
unfolding o_def tendsto_iff by simp
with r show "∃l r. strict_mono r ∧ (f ∘ r) ⇢ l"
by auto
qed
instance euclidean_space ⊆ banach ..
instance euclidean_space ⊆ second_countable_topology
proof
define a where "a f = (∑i∈Basis. fst (f i) *⇩R i)" for f :: "'a ⇒ real × real"
then have a: "⋀f. (∑i∈Basis. fst (f i) *⇩R i) = a f"
by simp
define b where "b f = (∑i∈Basis. snd (f i) *⇩R i)" for f :: "'a ⇒ real × real"
then have b: "⋀f. (∑i∈Basis. snd (f i) *⇩R i) = b f"
by simp
define B where "B = (λf. box (a f) (b f)) ` (Basis →⇩E (ℚ × ℚ))"
have "Ball B open" by (simp add: B_def open_box)
moreover have "(∀A. open A ⟶ (∃B'⊆B. ⋃B' = A))"
proof safe
fix A::"'a set"
assume "open A"
show "∃B'⊆B. ⋃B' = A"
using open_UNION_box[OF ‹open A›]
by (smt (verit, ccfv_threshold) B_def a b image_iff mem_Collect_eq subsetI)
qed
ultimately
have "topological_basis B"
unfolding topological_basis_def by blast
moreover
have "countable B"
unfolding B_def
by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
ultimately show "∃B::'a set set. countable B ∧ open = generate_topology B"
by (blast intro: topological_basis_imp_subbasis)
qed
instance euclidean_space ⊆ polish_space ..
subsection ‹Compact Boxes›
lemma compact_cbox [simp]:
fixes a :: "'a::euclidean_space"
shows "compact (cbox a b)"
using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
by (auto simp: compact_eq_seq_compact_metric)
proposition is_interval_compact:
"is_interval S ∧ compact S ⟷ (∃a b. S = cbox a b)" (is "?lhs = ?rhs")
proof (cases "S = {}")
case True
with empty_as_interval show ?thesis by auto
next
case False
show ?thesis
proof
assume L: ?lhs
then have "is_interval S" "compact S" by auto
define a where "a ≡ ∑i∈Basis. (INF x∈S. x ∙ i) *⇩R i"
define b where "b ≡ ∑i∈Basis. (SUP x∈S. x ∙ i) *⇩R i"
have 1: "⋀x i. ⟦x ∈ S; i ∈ Basis⟧ ⟹ (INF x∈S. x ∙ i) ≤ x ∙ i"
by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
have 2: "⋀x i. ⟦x ∈ S; i ∈ Basis⟧ ⟹ x ∙ i ≤ (SUP x∈S. x ∙ i)"
by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
have 3: "x ∈ S" if inf: "⋀i. i ∈ Basis ⟹ (INF x∈S. x ∙ i) ≤ x ∙ i"
and sup: "⋀i. i ∈ Basis ⟹ x ∙ i ≤ (SUP x∈S. x ∙ i)" for x
proof (rule mem_box_componentwiseI [OF ‹is_interval S›])
fix i::'a
assume i: "i ∈ Basis"
have cont: "continuous_on S (λx. x ∙ i)"
by (intro continuous_intros)
obtain a where "a ∈ S" and a: "⋀y. y∈S ⟹ a ∙ i ≤ y ∙ i"
using continuous_attains_inf [OF ‹compact S› False cont] by blast
obtain b where "b ∈ S" and b: "⋀y. y∈S ⟹ y ∙ i ≤ b ∙ i"
using continuous_attains_sup [OF ‹compact S› False cont] by blast
have "a ∙ i ≤ (INF x∈S. x ∙ i)"
by (simp add: False a cINF_greatest)
also have "… ≤ x ∙ i"
by (simp add: i inf)
finally have ai: "a ∙ i ≤ x ∙ i" .
have "x ∙ i ≤ (SUP x∈S. x ∙ i)"
by (simp add: i sup)
also have "(SUP x∈S. x ∙ i) ≤ b ∙ i"
by (simp add: False b cSUP_least)
finally have bi: "x ∙ i ≤ b ∙ i" .
show "x ∙ i ∈ (λx. x ∙ i) ` S"
apply (rule_tac x="∑j∈Basis. (((∙)a)(i := x ∙ j))j *⇩R j" in image_eqI)
apply (simp add: i)
apply (rule mem_is_intervalI [OF ‹is_interval S› ‹a ∈ S› ‹b ∈ S›])
using i ai bi
apply force
done
qed
have "S = cbox a b"
by (auto simp: a_def b_def mem_box intro: 1 2 3)
then show ?rhs
by blast
next
assume R: ?rhs
then show ?lhs
using compact_cbox is_interval_cbox by blast
qed
qed
subsection‹Componentwise limits and continuity›
text‹But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}›
lemma Euclidean_dist_upper: "i ∈ Basis ⟹ dist (x ∙ i) (y ∙ i) ≤ dist x y"
by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis)
text‹But is the premise \<^term>‹i ∈ Basis› really necessary?›
lemma open_preimage_inner:
assumes "open S" "i ∈ Basis"
shows "open {x. x ∙ i ∈ S}"
proof (rule openI, simp)
fix x
assume x: "x ∙ i ∈ S"
with assms obtain e where "0 < e" and e: "ball (x ∙ i) e ⊆ S"
by (auto simp: open_contains_ball_eq)
have "∃e>0. ball (y ∙ i) e ⊆ S" if dxy: "dist x y < e / 2" for y
proof (intro exI conjI)
have "dist (x ∙ i) (y ∙ i) < e / 2"
by (meson ‹i ∈ Basis› dual_order.trans Euclidean_dist_upper not_le that)
then have "dist (x ∙ i) z < e" if "dist (y ∙ i) z < e / 2" for z
by (metis dist_commute dist_triangle_half_l that)
then have "ball (y ∙ i) (e / 2) ⊆ ball (x ∙ i) e"
using mem_ball by blast
with e show "ball (y ∙ i) (e / 2) ⊆ S"
by (metis order_trans)
qed (simp add: ‹0 < e›)
then show "∃e>0. ball x e ⊆ {s. s ∙ i ∈ S}"
by (metis (no_types, lifting) ‹0 < e› ‹open S› half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI)
qed
proposition tendsto_componentwise_iff:
fixes f :: "_ ⇒ 'b::euclidean_space"
shows "(f ⤏ l) F ⟷ (∀i ∈ Basis. ((λx. (f x ∙ i)) ⤏ (l ∙ i)) F)"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
unfolding tendsto_def
by (smt (verit) eventually_elim2 mem_Collect_eq open_preimage_inner)
next
assume R: ?rhs
then have "⋀e. e > 0 ⟹ ∀i∈Basis. ∀⇩F x in F. dist (f x ∙ i) (l ∙ i) < e"
unfolding tendsto_iff by blast
then have R': "⋀e. e > 0 ⟹ ∀⇩F x in F. ∀i∈Basis. dist (f x ∙ i) (l ∙ i) < e"
by (simp add: eventually_ball_finite_distrib [symmetric])
show ?lhs
unfolding tendsto_iff
proof clarify
fix e::real
assume "0 < e"
have *: "L2_set (λi. dist (f x ∙ i) (l ∙ i)) Basis < e"
if "∀i∈Basis. dist (f x ∙ i) (l ∙ i) < e / real DIM('b)" for x
proof -
have "L2_set (λi. dist (f x ∙ i) (l ∙ i)) Basis ≤ sum (λi. dist (f x ∙ i) (l ∙ i)) Basis"
by (simp add: L2_set_le_sum)
also have "... < DIM('b) * (e / real DIM('b))"
by (meson DIM_positive sum_bounded_above_strict that)
also have "... = e"
by (simp add: field_simps)
finally show "L2_set (λi. dist (f x ∙ i) (l ∙ i)) Basis < e" .
qed
have "∀⇩F x in F. ∀i∈Basis. dist (f x ∙ i) (l ∙ i) < e / DIM('b)"
by (simp add: R' ‹0 < e›)
then show "∀⇩F x in F. dist (f x) l < e"
by eventually_elim (metis (full_types) "*" euclidean_dist_l2)
qed
qed
corollary continuous_componentwise:
"continuous F f ⟷ (∀i ∈ Basis. continuous F (λx. (f x ∙ i)))"
by (simp add: continuous_def tendsto_componentwise_iff [symmetric])
corollary continuous_on_componentwise:
fixes S :: "'a :: t2_space set"
shows "continuous_on S f ⟷ (∀i ∈ Basis. continuous_on S (λx. (f x ∙ i)))"
by (metis continuous_componentwise continuous_on_eq_continuous_within)
lemma linear_componentwise_iff:
"linear f' ⟷ (∀i∈Basis. linear (λx. f' x ∙ i))" (is "?lhs ⟷ ?rhs")
proof
show "?lhs ⟹ ?rhs"
by (simp add: Real_Vector_Spaces.linear_iff inner_left_distrib)
show "?rhs ⟹ ?lhs"
by (simp add: linear_iff) (metis euclidean_eqI inner_left_distrib inner_scaleR_left)
qed
lemma bounded_linear_componentwise_iff:
"(bounded_linear f') ⟷ (∀i∈Basis. bounded_linear (λx. f' x ∙ i))"
(is "?lhs = ?rhs")
proof
assume ?rhs
then have "(∀i∈Basis. ∃K. ∀x. ¦f' x ∙ i¦ ≤ norm x * K)" "linear f'"
by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_componentwise_iff [symmetric] ball_conj_distrib)
then obtain F where F: "⋀i x. i ∈ Basis ⟹ ¦f' x ∙ i¦ ≤ norm x * F i"
by metis
have "norm (f' x) ≤ norm x * sum F Basis" for x
proof -
have "norm (f' x) ≤ (∑i∈Basis. ¦f' x ∙ i¦)"
by (rule norm_le_l1)
also have "... ≤ (∑i∈Basis. norm x * F i)"
by (metis F sum_mono)
also have "... = norm x * sum F Basis"
by (simp add: sum_distrib_left)
finally show ?thesis .
qed
then show ?lhs
by (force simp: bounded_linear_def bounded_linear_axioms_def ‹linear f'›)
qed (simp add: bounded_linear_inner_left_comp)
subsection ‹Continuous Extension›
definition clamp :: "'a::euclidean_space ⇒ 'a ⇒ 'a ⇒ 'a" where
"clamp a b x = (if (∀i∈Basis. a ∙ i ≤ b ∙ i)
then (∑i∈Basis. (if x∙i < a∙i then a∙i else if x∙i ≤ b∙i then x∙i else b∙i) *⇩R i)
else a)"
lemma clamp_in_interval[simp]:
assumes "⋀i. i ∈ Basis ⟹ a ∙ i ≤ b ∙ i"
shows "clamp a b x ∈ cbox a b"
unfolding clamp_def
using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
lemma clamp_cancel_cbox[simp]:
fixes x a b :: "'a::euclidean_space"
assumes x: "x ∈ cbox a b"
shows "clamp a b x = x"
using assms
by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a])
lemma clamp_empty_interval:
assumes "i ∈ Basis" "a ∙ i > b ∙ i"
shows "clamp a b = (λ_. a)"
using assms
by (force simp: clamp_def[abs_def] split: if_splits intro!: ext)
lemma dist_clamps_le_dist_args:
fixes x :: "'a::euclidean_space"
shows "dist (clamp a b y) (clamp a b x) ≤ dist y x"
proof cases
assume le: "(∀i∈Basis. a ∙ i ≤ b ∙ i)"
then have "(∑i∈Basis. (dist (clamp a b y ∙ i) (clamp a b x ∙ i))⇧2) ≤
(∑i∈Basis. (dist (y ∙ i) (x ∙ i))⇧2)"
by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
then show ?thesis
by (auto intro: real_sqrt_le_mono
simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def)
qed (auto simp: clamp_def)
lemma clamp_continuous_at:
fixes f :: "'a::euclidean_space ⇒ 'b::metric_space"
and x :: 'a
assumes f_cont: "continuous_on (cbox a b) f"
shows "continuous (at x) (λx. f (clamp a b x))"
proof cases
assume le: "(∀i∈Basis. a ∙ i ≤ b ∙ i)"
show ?thesis
unfolding continuous_at_eps_delta
proof safe
fix x :: 'a
fix e :: real
assume "e > 0"
moreover have "clamp a b x ∈ cbox a b"
by (simp add: le)
moreover note f_cont[simplified continuous_on_iff]
ultimately
obtain d where d: "0 < d"
"⋀x'. x' ∈ cbox a b ⟹ dist x' (clamp a b x) < d ⟹ dist (f x') (f (clamp a b x)) < e"
by force
show "∃d>0. ∀x'. dist x' x < d ⟶ dist (f (clamp a b x')) (f (clamp a b x)) < e"
using le
by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans])
qed
qed (auto simp: clamp_empty_interval)
lemma clamp_continuous_on:
fixes f :: "'a::euclidean_space ⇒ 'b::metric_space"
assumes f_cont: "continuous_on (cbox a b) f"
shows "continuous_on S (λx. f (clamp a b x))"
using assms
by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
lemma clamp_bounded:
fixes f :: "'a::euclidean_space ⇒ 'b::metric_space"
assumes bounded: "bounded (f ` (cbox a b))"
shows "bounded (range (λx. f (clamp a b x)))"
proof cases
assume le: "(∀i∈Basis. a ∙ i ≤ b ∙ i)"
from bounded obtain c where f_bound: "∀x∈f ` cbox a b. dist undefined x ≤ c"
by (auto simp: bounded_any_center[where a=undefined])
then show ?thesis
by (metis bounded bounded_subset clamp_in_interval image_mono image_subsetI le range_composition)
qed (auto simp: clamp_empty_interval image_def)
definition ext_cont :: "('a::euclidean_space ⇒ 'b::metric_space) ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'b"
where "ext_cont f a b = (λx. f (clamp a b x))"
lemma ext_cont_cancel_cbox[simp]:
fixes x a b :: "'a::euclidean_space"
assumes x: "x ∈ cbox a b"
shows "ext_cont f a b x = f x"
using assms by (simp add: ext_cont_def)
lemma continuous_on_ext_cont[continuous_intros]:
"continuous_on (cbox a b) f ⟹ continuous_on S (ext_cont f a b)"
by (auto intro!: clamp_continuous_on simp: ext_cont_def)
subsection ‹Separability›
lemma univ_second_countable_sequence:
obtains B :: "nat ⇒ 'a::euclidean_space set"
where "inj B" "⋀n. open(B n)" "⋀S. open S ⟹ ∃k. S = ⋃{B n |n. n ∈ k}"
proof -
obtain ℬ :: "'a set set"
where "countable ℬ"
and opn: "⋀C. C ∈ ℬ ⟹ open C"
and Un: "⋀S. open S ⟹ ∃U. U ⊆ ℬ ∧ S = ⋃U"
using univ_second_countable by blast
have *: "infinite (range (λn. ball (0::'a) (inverse(Suc n))))"
by (simp add: inj_on_def ball_eq_ball_iff Infinite_Set.range_inj_infinite)
have "infinite ℬ"
proof
assume "finite ℬ"
then have "finite (Union ` (Pow ℬ))"
by simp
moreover have "range (λn. ball 0 (inverse (real (Suc n)))) ⊆ ⋃ ` Pow ℬ"
by (metis (no_types, lifting) PowI image_eqI image_subset_iff Un [OF open_ball])
ultimately show False
by (metis finite_subset *)
qed
obtain f :: "nat ⇒ 'a set" where "ℬ = range f" "inj f"
by (blast intro: countable_as_injective_image [OF ‹countable ℬ› ‹infinite ℬ›])
have *: "∃k. S = ⋃{f n |n. n ∈ k}" if "open S" for S
using Un [OF that]
apply clarify
apply (rule_tac x="f-`U" in exI)
using ‹inj f› ‹ℬ = range f› apply force
done
show ?thesis
using "*" ‹ℬ = range f› ‹inj f› opn that by force
qed
proposition separable:
fixes S :: "'a::{metric_space, second_countable_topology} set"
obtains T where "countable T" "T ⊆ S" "S ⊆ closure T"
proof -
obtain ℬ :: "'a set set"
where "countable ℬ"
and "{} ∉ ℬ"
and ope: "⋀C. C ∈ ℬ ⟹ openin(top_of_set S) C"
and if_ope: "⋀T. openin(top_of_set S) T ⟹ ∃𝒰. 𝒰 ⊆ ℬ ∧ T = ⋃𝒰"
by (meson subset_second_countable)
then obtain f where f: "⋀C. C ∈ ℬ ⟹ f C ∈ C"
by (metis equals0I)
show ?thesis
proof
show "countable (f ` ℬ)"
by (simp add: ‹countable ℬ›)
show "f ` ℬ ⊆ S"
using ope f openin_imp_subset by blast
show "S ⊆ closure (f ` ℬ)"
proof (clarsimp simp: closure_approachable)
fix x and e::real
assume "x ∈ S" "0 < e"
have "openin (top_of_set S) (S ∩ ball x e)"
by (simp add: openin_Int_open)
with if_ope obtain 𝒰 where 𝒰: "𝒰 ⊆ ℬ" "S ∩ ball x e = ⋃𝒰"
by meson
show "∃C ∈ ℬ. dist (f C) x < e"
proof (cases "𝒰 = {}")
case True
then show ?thesis
using ‹0 < e› 𝒰 ‹x ∈ S› by auto
next
case False
then show ?thesis
by (metis IntI Union_iff 𝒰 ‹0 < e› ‹x ∈ S› dist_commute dist_self f inf_le2 mem_ball subset_eq)
qed
qed
qed
qed
subsection ‹Diameter›
lemma diameter_cball [simp]:
fixes a :: "'a::euclidean_space"
shows "diameter(cball a r) = (if r < 0 then 0 else 2*r)"
proof -
have "diameter(cball a r) = 2*r" if "r ≥ 0"
proof (rule order_antisym)
show "diameter (cball a r) ≤ 2*r"
proof (rule diameter_le)
fix x y assume "x ∈ cball a r" "y ∈ cball a r"
then have "norm (x - a) ≤ r" "norm (a - y) ≤ r"
by (auto simp: dist_norm norm_minus_commute)
then have "norm (x - y) ≤ r+r"
using norm_diff_triangle_le by blast
then show "norm (x - y) ≤ 2*r" by simp
qed (simp add: that)
have "2*r = dist (a + r *⇩R (SOME i. i ∈ Basis)) (a - r *⇩R (SOME i. i ∈ Basis))"
using ‹0 ≤ r› that by (simp add: dist_norm flip: scaleR_2)
also have "... ≤ diameter (cball a r)"
apply (rule diameter_bounded_bound)
using that by (auto simp: dist_norm)
finally show "2*r ≤ diameter (cball a r)" .
qed
then show ?thesis by simp
qed
lemma diameter_ball [simp]:
fixes a :: "'a::euclidean_space"
shows "diameter(ball a r) = (if r < 0 then 0 else 2*r)"
proof -
have "diameter(ball a r) = 2*r" if "r > 0"
by (metis bounded_ball diameter_closure closure_ball diameter_cball less_eq_real_def linorder_not_less that)
then show ?thesis
by (simp add: diameter_def)
qed
lemma diameter_closed_interval [simp]: "diameter {a..b} = (if b < a then 0 else b-a)"
proof -
have "{a..b} = cball ((a+b)/2) ((b-a)/2)"
using atLeastAtMost_eq_cball by blast
then show ?thesis
by simp
qed
lemma diameter_open_interval [simp]: "diameter {a<..<b} = (if b < a then 0 else b-a)"
proof -
have "{a <..< b} = ball ((a+b)/2) ((b-a)/2)"
using greaterThanLessThan_eq_ball by blast
then show ?thesis
by simp
qed
lemma diameter_cbox:
fixes a b::"'a::euclidean_space"
shows "(∀i ∈ Basis. a ∙ i ≤ b ∙ i) ⟹ diameter (cbox a b) = dist a b"
by (force simp: diameter_def intro!: cSup_eq_maximum L2_set_mono
simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
subsection‹Relating linear images to open/closed/interior/closure/connected›
proposition open_surjective_linear_image:
fixes f :: "'a::real_normed_vector ⇒ 'b::euclidean_space"
assumes "open A" "linear f" "surj f"
shows "open(f ` A)"
unfolding open_dist
proof clarify
fix x
assume "x ∈ A"
have "bounded (inv f ` Basis)"
by (simp add: finite_imp_bounded)
with bounded_pos obtain B where "B > 0" and B: "⋀x. x ∈ inv f ` Basis ⟹ norm x ≤ B"
by metis
obtain e where "e > 0" and e: "⋀z. dist z x < e ⟹ z ∈ A"
by (metis open_dist ‹x ∈ A› ‹open A›)
define δ where "δ ≡ e / B / DIM('b)"
show "∃e>0. ∀y. dist y (f x) < e ⟶ y ∈ f ` A"
proof (intro exI conjI)
show "δ > 0"
using ‹e > 0› ‹B > 0› by (simp add: δ_def field_split_simps)
have "y ∈ f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y
proof -
define u where "u ≡ y - f x"
show ?thesis
proof (rule image_eqI)
show "y = f (x + (∑i∈Basis. (u ∙ i) *⇩R inv f i))"
apply (simp add: linear_add linear_sum linear.scaleR ‹linear f› surj_f_inv_f ‹surj f›)
apply (simp add: euclidean_representation u_def)
done
have "dist (x + (∑i∈Basis. (u ∙ i) *⇩R inv f i)) x ≤ (∑i∈Basis. norm ((u ∙ i) *⇩R inv f i))"
by (simp add: dist_norm sum_norm_le)
also have "... = (∑i∈Basis. ¦u ∙ i¦ * norm (inv f i))"
by simp
also have "... ≤ (∑i∈Basis. ¦u ∙ i¦) * B"
by (simp add: B sum_distrib_right sum_mono mult_left_mono)
also have "... ≤ DIM('b) * dist y (f x) * B"
apply (rule mult_right_mono [OF sum_bounded_above])
using ‹0 < B› by (auto simp: Basis_le_norm dist_norm u_def)
also have "... < e"
by (metis mult.commute mult.left_commute that)
finally show "x + (∑i∈Basis. (u ∙ i) *⇩R inv f i) ∈ A"
by (rule e)
qed
qed
then show "∀y. dist y (f x) < δ ⟶ y ∈ f ` A"
using ‹e > 0› ‹B > 0›
by (auto simp: δ_def field_split_simps)
qed
qed
corollary open_bijective_linear_image_eq:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes "linear f" "bij f"
shows "open(f ` A) ⟷ open A"
proof
assume "open(f ` A)"
then show "open A"
by (metis assms bij_is_inj continuous_open_vimage inj_vimage_image_eq linear_continuous_at linear_linear)
next
assume "open A"
then show "open(f ` A)"
by (simp add: assms bij_is_surj open_surjective_linear_image)
qed
corollary interior_bijective_linear_image:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes "linear f" "bij f"
shows "interior (f ` S) = f ` interior S"
by (smt (verit) assms bij_is_inj inj_image_subset_iff interior_maximal interior_subset
open_bijective_linear_image_eq open_interior subset_antisym subset_imageE)
lemma interior_injective_linear_image:
fixes f :: "'a::euclidean_space ⇒ 'a::euclidean_space"
assumes "linear f" "inj f"
shows "interior(f ` S) = f ` (interior S)"
by (simp add: linear_injective_imp_surjective assms bijI interior_bijective_linear_image)
lemma interior_surjective_linear_image:
fixes f :: "'a::euclidean_space ⇒ 'a::euclidean_space"
assumes "linear f" "surj f"
shows "interior(f ` S) = f ` (interior S)"
by (simp add: assms interior_injective_linear_image linear_surjective_imp_injective)
lemma interior_negations:
fixes S :: "'a::euclidean_space set"
shows "interior(uminus ` S) = image uminus (interior S)"
by (simp add: bij_uminus interior_bijective_linear_image linear_uminus)
lemma connected_linear_image:
fixes f :: "'a::euclidean_space ⇒ 'b::real_normed_vector"
assumes "linear f" and "connected s"
shows "connected (f ` s)"
using connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear by blast
subsection ‹"Isometry" (up to constant bounds) of Injective Linear Map›
proposition injective_imp_isometric:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes s: "closed s" "subspace s"
and f: "bounded_linear f" "∀x∈s. f x = 0 ⟶ x = 0"
shows "∃e>0. ∀x∈s. norm (f x) ≥ e * norm x"
proof (cases "s ⊆ {0::'a}")
case True
have "norm x ≤ norm (f x)" if "x ∈ s" for x
proof -
from True that have "x = 0" by auto
then show ?thesis by simp
qed
then show ?thesis
by (auto intro!: exI[where x=1])
next
case False
interpret f: bounded_linear f by fact
from False obtain a where a: "a ≠ 0" "a ∈ s"
by auto
from False have "s ≠ {}"
by auto
let ?S = "{f x| x. x ∈ s ∧ norm x = norm a}"
let ?S' = "{x::'a. x∈s ∧ norm x = norm a}"
let ?S'' = "{x::'a. norm x = norm a}"
have "?S'' = frontier (cball 0 (norm a))"
by (simp add: sphere_def dist_norm)
then have "compact ?S''" by (metis compact_cball compact_frontier)
moreover have "?S' = s ∩ ?S''" by auto
ultimately have "compact ?S'"
using closed_Int_compact[of s ?S''] using s(1) by auto
moreover have *:"f ` ?S' = ?S" by auto
ultimately have "compact ?S"
using compact_continuous_image[OF linear_continuous_on[OF f(1)], of ?S'] by auto
then have "closed ?S"
using compact_imp_closed by auto
moreover from a have "?S ≠ {}" by auto
ultimately obtain b' where "b'∈?S" "∀y∈?S. norm b' ≤ norm y"
using distance_attains_inf[of ?S 0] unfolding dist_0_norm by auto
then obtain b where "b∈s"
and ba: "norm b = norm a"
and b: "∀x∈{x ∈ s. norm x = norm a}. norm (f b) ≤ norm (f x)"
unfolding *[symmetric] unfolding image_iff by auto
let ?e = "norm (f b) / norm b"
have "norm b > 0"
using ba and a and norm_ge_zero by auto
moreover have "norm (f b) > 0"
using f(2)[THEN bspec[where x=b], OF ‹b∈s›]
using ‹norm b >0› by simp
ultimately have "0 < norm (f b) / norm b" by simp
moreover
have "norm (f b) / norm b * norm x ≤ norm (f x)" if "x∈s" for x
proof (cases "x = 0")
case True
then show "norm (f b) / norm b * norm x ≤ norm (f x)"
by auto
next
case False
with ‹a ≠ 0› have *: "0 < norm a / norm x"
unfolding zero_less_norm_iff[symmetric] by simp
have "∀x∈s. c *⇩R x ∈ s" for c
using s[unfolded subspace_def] by simp
with ‹x ∈ s› ‹x ≠ 0› have "(norm a / norm x) *⇩R x ∈ {x ∈ s. norm x = norm a}"
by simp
with ‹x ≠ 0› ‹a ≠ 0› show "norm (f b) / norm b * norm x ≤ norm (f x)"
using b[THEN bspec[where x="(norm a / norm x) *⇩R x"]]
unfolding f.scaleR and ba
by (auto simp: mult.commute pos_le_divide_eq pos_divide_le_eq)
qed
ultimately show ?thesis by auto
qed
proposition closed_injective_image_subspace:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes "subspace s" "bounded_linear f" "∀x∈s. f x = 0 ⟶ x = 0" "closed s"
shows "closed(f ` s)"
proof -
obtain e where "e > 0" and e: "∀x∈s. e * norm x ≤ norm (f x)"
using assms injective_imp_isometric by blast
with assms show ?thesis
by (meson complete_eq_closed complete_isometric_image)
qed
lemma closure_bounded_linear_image_subset:
assumes f: "bounded_linear f"
shows "f ` closure S ⊆ closure (f ` S)"
using linear_continuous_on [OF f] closed_closure closure_subset
by (rule image_closure_subset)
lemma closure_linear_image_subset:
fixes f :: "'m::euclidean_space ⇒ 'n::real_normed_vector"
assumes "linear f"
shows "f ` (closure S) ⊆ closure (f ` S)"
using assms unfolding linear_conv_bounded_linear
by (rule closure_bounded_linear_image_subset)
lemma closed_injective_linear_image:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes S: "closed S" and f: "linear f" "inj f"
shows "closed (f ` S)"
proof -
obtain g where g: "linear g" "g ∘ f = id"
using linear_injective_left_inverse [OF f] by blast
then have confg: "continuous_on (range f) g"
using linear_continuous_on linear_conv_bounded_linear by blast
have [simp]: "g ` f ` S = S"
using g by (simp add: image_comp)
have cgf: "closed (g ` f ` S)"
by (simp add: ‹g ∘ f = id› S image_comp)
have [simp]: "(range f ∩ g -` S) = f ` S"
using g unfolding o_def id_def image_def by auto metis+
show ?thesis
proof (rule closedin_closed_trans [of "range f"])
show "closedin (top_of_set (range f)) (f ` S)"
using continuous_closedin_preimage [OF confg cgf] by simp
show "closed (range f)"
using closed_injective_image_subspace f linear_conv_bounded_linear
linear_injective_0 subspace_UNIV by blast
qed
qed
lemma closed_injective_linear_image_eq:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes f: "linear f" "inj f"
shows "(closed(image f s) ⟷ closed s)"
by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff)
lemma closure_injective_linear_image:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
shows "⟦linear f; inj f⟧ ⟹ f ` (closure S) = closure (f ` S)"
by (simp add: closed_injective_linear_image closure_linear_image_subset
closure_minimal closure_subset image_mono subset_antisym)
lemma closure_bounded_linear_image:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes "linear f" "bounded S"
shows "f ` (closure S) = closure (f ` S)" (is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
using assms closure_linear_image_subset by blast
show "?rhs ⊆ ?lhs"
using assms by (meson closure_minimal closure_subset compact_closure compact_eq_bounded_closed
compact_continuous_image image_mono linear_continuous_on linear_linear)
qed
lemma closure_scaleR:
fixes S :: "'a::real_normed_vector set"
shows "((*⇩R) c) ` (closure S) = closure (((*⇩R) c) ` S)" (is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
using bounded_linear_scaleR_right by (rule closure_bounded_linear_image_subset)
show "?rhs ⊆ ?lhs"
by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
qed
subsection ‹Some properties of a canonical subspace›
lemma closed_substandard: "closed {x::'a::euclidean_space. ∀i∈Basis. P i ⟶ x∙i = 0}"
(is "closed ?A")
proof -
let ?D = "{i∈Basis. P i}"
have "closed (⋂i∈?D. {x::'a. x∙i = 0})"
by (simp add: closed_INT closed_Collect_eq continuous_on_inner)
also have "(⋂i∈?D. {x::'a. x∙i = 0}) = ?A"
by auto
finally show "closed ?A" .
qed
lemma closed_subspace:
fixes S :: "'a::euclidean_space set"
assumes "subspace S"
shows "closed S"
proof -
have "dim S ≤ card (Basis :: 'a set)"
using dim_subset_UNIV by auto
with obtain_subset_with_card_n
obtain d :: "'a set" where cd: "card d = dim S" and d: "d ⊆ Basis"
by metis
let ?t = "{x::'a. ∀i∈Basis. i ∉ d ⟶ x∙i = 0}"
have "∃f. linear f ∧ f ` {x::'a. ∀i∈Basis. i ∉ d ⟶ x ∙ i = 0} = S ∧
inj_on f {x::'a. ∀i∈Basis. i ∉ d ⟶ x ∙ i = 0}"
using dim_substandard[of d] cd d assms
by (intro subspace_isomorphism[OF subspace_substandard[of "λi. i ∉ d"]]) (auto simp: inner_Basis)
then obtain f where f:
"linear f"
"f ` {x. ∀i∈Basis. i ∉ d ⟶ x ∙ i = 0} = S"
"inj_on f {x. ∀i∈Basis. i ∉ d ⟶ x ∙ i = 0}"
by blast
interpret f: bounded_linear f
using f by (simp add: linear_conv_bounded_linear)
have "x ∈ ?t ⟹ f x = 0 ⟹ x = 0" for x
using f.zero d f(3)[THEN inj_onD, of x 0] by auto
then show ?thesis
using closed_injective_image_subspace[of ?t f] closed_substandard subspace_substandard
using f(2) f.bounded_linear_axioms by force
qed
lemma complete_subspace: "subspace S ⟹ complete S"
for S :: "'a::euclidean_space set"
using complete_eq_closed closed_subspace by auto
lemma closed_span [iff]: "closed (span S)"
for S :: "'a::euclidean_space set"
by (simp add: closed_subspace)
lemma dim_closure [simp]: "dim (closure S) = dim S" (is "?dc = ?d")
for S :: "'a::euclidean_space set"
by (metis closed_span closure_minimal closure_subset dim_eq_span span_eq_dim span_superset subset_le_dim)
subsection ‹Set Distance›
lemma setdist_compact_closed:
fixes A :: "'a::heine_borel set"
assumes "compact A" "closed B"
and "A ≠ {}" "B ≠ {}"
shows "∃x ∈ A. ∃y ∈ B. dist x y = setdist A B"
by (metis assms infdist_attains_inf setdist_attains_inf setdist_sym)
lemma setdist_closed_compact:
fixes S :: "'a::heine_borel set"
assumes S: "closed S" and T: "compact T"
and "S ≠ {}" "T ≠ {}"
shows "∃x ∈ S. ∃y ∈ T. dist x y = setdist S T"
using setdist_compact_closed [OF T S ‹T ≠ {}› ‹S ≠ {}›]
by (metis dist_commute setdist_sym)
lemma setdist_eq_0_compact_closed:
assumes S: "compact S" and T: "closed T"
shows "setdist S T = 0 ⟷ S = {} ∨ T = {} ∨ S ∩ T ≠ {}"
proof (cases "S = {} ∨ T = {}")
case False
then show ?thesis
by (metis S T disjoint_iff in_closed_iff_infdist_zero setdist_attains_inf setdist_eq_0I setdist_sym)
qed auto
corollary setdist_gt_0_compact_closed:
assumes S: "compact S" and T: "closed T"
shows "setdist S T > 0 ⟷ (S ≠ {} ∧ T ≠ {} ∧ S ∩ T = {})"
using setdist_pos_le [of S T] setdist_eq_0_compact_closed [OF assms] by linarith
lemma setdist_eq_0_closed_compact:
assumes S: "closed S" and T: "compact T"
shows "setdist S T = 0 ⟷ S = {} ∨ T = {} ∨ S ∩ T ≠ {}"
using setdist_eq_0_compact_closed [OF T S]
by (metis Int_commute setdist_sym)
lemma setdist_eq_0_bounded:
fixes S :: "'a::heine_borel set"
assumes "bounded S ∨ bounded T"
shows "setdist S T = 0 ⟷ S = {} ∨ T = {} ∨ closure S ∩ closure T ≠ {}"
proof (cases "S = {} ∨ T = {}")
case False
then show ?thesis
using setdist_eq_0_compact_closed [of "closure S" "closure T"]
setdist_eq_0_closed_compact [of "closure S" "closure T"] assms
by (force simp: bounded_closure compact_eq_bounded_closed)
qed force
lemma setdist_eq_0_sing_1:
"setdist {x} S = 0 ⟷ S = {} ∨ x ∈ closure S"
by (metis in_closure_iff_infdist_zero infdist_def infdist_eq_setdist)
lemma setdist_eq_0_sing_2:
"setdist S {x} = 0 ⟷ S = {} ∨ x ∈ closure S"
by (metis setdist_eq_0_sing_1 setdist_sym)
lemma setdist_neq_0_sing_1:
"⟦setdist {x} S = a; a ≠ 0⟧ ⟹ S ≠ {} ∧ x ∉ closure S"
by (metis setdist_closure_2 setdist_empty2 setdist_eq_0I singletonI)
lemma setdist_neq_0_sing_2:
"⟦setdist S {x} = a; a ≠ 0⟧ ⟹ S ≠ {} ∧ x ∉ closure S"
by (simp add: setdist_neq_0_sing_1 setdist_sym)
lemma setdist_sing_in_set:
"x ∈ S ⟹ setdist {x} S = 0"
by (simp add: setdist_eq_0I)
lemma setdist_eq_0_closed:
"closed S ⟹ (setdist {x} S = 0 ⟷ S = {} ∨ x ∈ S)"
by (simp add: setdist_eq_0_sing_1)
lemma setdist_eq_0_closedin:
shows "⟦closedin (top_of_set U) S; x ∈ U⟧
⟹ (setdist {x} S = 0 ⟷ S = {} ∨ x ∈ S)"
by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
lemma setdist_gt_0_closedin:
shows "⟦closedin (top_of_set U) S; x ∈ U; S ≠ {}; x ∉ S⟧
⟹ setdist {x} S > 0"
using less_eq_real_def setdist_eq_0_closedin by fastforce
text ‹A consequence of the results above›
lemma compact_minkowski_sum_cball:
fixes A :: "'a :: heine_borel set"
assumes "compact A"
shows "compact (⋃x∈A. cball x r)"
proof (cases "A = {}")
case False
show ?thesis
unfolding compact_eq_bounded_closed
proof safe
have "open (-(⋃x∈A. cball x r))"
unfolding open_dist
proof safe
fix x assume x: "x ∉ (⋃x∈A. cball x r)"
have "∃x'∈{x}. ∃y∈A. dist x' y = setdist {x} A"
using ‹A ≠ {}› assms
by (intro setdist_compact_closed) (auto simp: compact_imp_closed)
then obtain y where y: "y ∈ A" "dist x y = setdist {x} A"
by blast
with x have "setdist {x} A > r"
by (auto simp: dist_commute)
moreover have "False" if "dist z x < setdist {x} A - r" "u ∈ A" "z ∈ cball u r" for z u
by (smt (verit, del_insts) mem_cball setdist_Lipschitz setdist_sing_in_set that)
ultimately
show "∃e>0. ∀y. dist y x < e ⟶ y ∈ - (⋃x∈A. cball x r)"
by (force intro!: exI[of _ "setdist {x} A - r"])
qed
thus "closed (⋃x∈A. cball x r)"
using closed_open by blast
next
from assms have "bounded A"
by (simp add: compact_imp_bounded)
then obtain x c where c: "⋀y. y ∈ A ⟹ dist x y ≤ c"
unfolding bounded_def by blast
have "∀y∈(⋃x∈A. cball x r). dist x y ≤ c + r"
proof safe
fix y z assume *: "y ∈ A" "z ∈ cball y r"
thus "dist x z ≤ c + r"
using * c[of y] cball_trans mem_cball by blast
qed
thus "bounded (⋃x∈A. cball x r)"
unfolding bounded_def by blast
qed
qed auto
no_notation
eucl_less (infix "<e" 50)
end