Quelle Topology_Euclidean_Space.thy Sprache: Isabelle

(* Author: L C Paulson, University of Cambridge
 Author: Amine Chaieb, University of Cambridge
 Author: Robert Himmelmann, TU Muenchen
 Author: Brian Huffman, Portland State University
*)

chapter \<open>Vector Analysis\<close>

theory Topology_Euclidean_Space
 imports
 Elementary_Normed_Spaces
 Linear_Algebra
 Norm_Arith
begin

section \<open>Elementary Topology in Euclidean Space\<close>

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)\<^sup>2 = (\i\{i}. (x \ i)\<^sup>2)"
 by simp
 also have "\ \ (\i\Basis. (x \ i)\<^sup>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\<^marker>\<open>tag unimportant\<close> \<open>Continuity of the representation WRT an orthogonal basis\<close>

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 \<open>independent B\<close> \<open>b \<in> B\<close> dependent_zero by blast
 have [simp]: "b \ b' = (if b' = b then (norm b)\<^sup>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 *\<^sub>R b)"
 using real_vector.sum_representation_eq [OF \<open>independent B\<close> x \<open>finite B\<close> order_refl]
 by simp
 also have "\ = sqrt ((\b\B. representation B x b *\<^sub>R b) \ (\b\B. representation B x b *\<^sub>R b))"
 by (simp add: norm_eq_sqrt_inner)
 also have "\ = sqrt (\b\B. (representation B x b *\<^sub>R b) \ (representation B x b *\<^sub>R b))"
 using \<open>finite B\<close>
 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 *\<^sub>R b))\<^sup>2)"
 by (simp add: mult.commute mult.left_commute power2_eq_square)
 also have "\ = sqrt (\b\B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)"
 by (simp add: norm_mult power_mult_distrib)
 finally have "norm x = sqrt (\b\B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)" .
 moreover
 have "sqrt ((representation B x b)\<^sup>2 * (norm b)\<^sup>2) \ sqrt (\b\B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)"
 using \<open>b \<in> B\<close> \<open>finite B\<close> by (auto intro: member_le_sum)
 then have "\representation B x b\ \ (1 / norm b) * sqrt (\b\B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)"
 using \<open>b \<noteq> 0\<close> 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 \<open>independent B\<close> \<open>b \<in> B\<close> 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: \<open>e > 0\<close> \<open>m > 0\<close>)
 show "norm (representation B x' b - representation B x b) \ e"
 if x': "x' \<in> 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"] \<open>x \<in> span B\<close> span_diff x' by blast
 also have "\ < e"
 by (metis \<open>m > 0\<close> less mult.commute pos_less_divide_eq)
 finally have "\representation B (x'-x) b\ \ e" by simp
 then show ?thesis
 by (simp add: \<open>x \<in> span B\<close> \<open>independent B\<close> representation_diff x')
 qed
 qed
 qed
qed

subsection\<^marker>\<open>tag unimportant\<close>\<open>Balls in Euclidean Space\<close>

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 *\<^sub>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')) *\<^sub>R (a - a'))) = norm ((-1 - (r / norm (a - a'))) *\<^sub>R (a - a'))"
 by (simp add: algebra_simps)
 also from \<open>a \<noteq> a'\<close> have "... = \<bar>- norm (a - a') - r\<bar>"
 by (simp add: divide_simps)
 finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = \norm (a - a') + r\"
 by linarith
 from \<open>a \<noteq> a'\<close> show ?thesis
 using subsetD [where c = "a' + (1 + r / norm(a - a')) *\<^sub>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 *\<^sub>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) \<open>0 \<le> r\<close> \<open>?lhs\<close> ball_subset_cball cball_subset_cball_iff dist_norm order_trans)
 then show ?thesis
 using subsetD [where c = "a + (r' / norm(a - a') - 1) *\<^sub>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 \<open>?lhs\<close> 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>open S\<close>] assms by auto
 obtain e2 where "0 < e2" and "\x\X. x \ p \ e2 \ dist p x"
 using finite_set_avoid[OF \<open>finite X\<close>,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 \<open>e2>0\<close> \<open>e1>0\<close> 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 \<open>e1>0\<close> 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) *\<^sub>R x"
 then have "y \ cball 0 e"
 using assms by auto
 moreover have *: "x = (norm x / e) *\<^sub>R y"
 using y_def assms by simp
 moreover from * have "x = (norm x/e) *\<^sub>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 \<open>Boxes\<close>

abbreviation\<^marker>\<open>tag important\<close> 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\<^marker>\<open>tag unimportant\<close> One_neq_0[iff]: "One \<noteq> 0"
 by (metis One_non_0)

corollary\<^marker>\<open>tag unimportant\<close> Zero_neq_One[iff]: "0 \<noteq> One"
 by (metis One_non_0)

definition\<^marker>\<open>tag important\<close> (in euclidean_space) eucl_less (infix \<open><e\<close> 50) where
"eucl_less a b \ (\i\Basis. a \ i \<open>tag important\<close> box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
definition\<^marker>\<open>tag important\<close> "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> 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 x
 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 (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)"
 unfolding set_eq_iff and Int_iff and mem_box by auto

lemma cbox_prod: "cbox a b = cbox (fst a) (fst b) \ cbox (snd a) (snd b)"
 by (cases a; cases b) auto

lemma box_prod: "box a b = box (fst a) (fst b) \ box (snd a) (snd b)"
 by (cases a; cases b) (force simp: box_def Basis_prod_def)

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 R i" and ?b = "\i\Basis. b i *\<^sub>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))\<^sup>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))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
 by (rule power_strict_mono) auto
 then show "(dist (x \ i) (y \ i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
 by (simp add: power_divide)
 qed auto
 also have "\ = e"
 using \<open>0 < e\<close> by simp
 finally show "y \ ball x e"
 by (auto simp: ball_def)
 qed (use a b in \<open>auto simp: box_def\<close>)
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) *\<^sub>R i)"
 defines "b' \ \f :: 'a \ real \ real. (\(i::'a)\Basis. snd (f i) *\<^sub>R i)"
 defines "I \ {f\Basis \\<^sub>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>open M\<close> \<open>x \<in> M\<close>] 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 \<D> where "countable \<D>" "\<D> \<subseteq> Pow S" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = box a b" "\<Union>\<D> = S"
proof -
 let ?a = "\f. (\(i::'a)\Basis. fst (f i) *\<^sub>R i)"
 let ?b = "\f. (\(i::'a)\Basis. snd (f i) *\<^sub>R i)"
 let ?I = "{f\Basis \\<^sub>E \ \ \. box (?a f) (?b f) \ S}"
 let ?\<D> = "(\<lambda>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 R i" and ?b = "\i\Basis. b i *\<^sub>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))\<^sup>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))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
 by (rule power_strict_mono) auto
 then show "(dist (x \ i) (y \ i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
 by (simp add: power_divide)
 qed auto
 also have "\ = e"
 using \<open>0 < e\<close> by simp
 finally show "y \ ball x e"
 by (auto simp: ball_def)
 next
 show "x \ cbox (\i\Basis. a i *\<^sub>R i) (\i\Basis. b i *\<^sub>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) *\<^sub>R i)"
 defines "b' \ \f. (\(i::'a)\Basis. snd (f i) *\<^sub>R i)"
 defines "I \ {f\Basis \\<^sub>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>open M\<close> \<open>x \<in> M\<close>] 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 \<D> where "countable \<D>" "\<D> \<subseteq> Pow S" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = cbox a b" "\<Union>\<D> = S"
proof -
 let ?a = "\f. (\(i::'a)\Basis. fst (f i) *\<^sub>R i)"
 let ?b = "\f. (\(i::'a)\Basis. snd (f i) *\<^sub>R i)"
 let ?I = "{f\Basis \\<^sub>E \ \ \. cbox (?a f) (?b f) \ S}"
 let ?\<D> = "(\<lambda>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) *\<^sub>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) *\<^sub>R (a+b)) \ i" "((1/2) *\<^sub>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) *\<^sub>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) *\<^sub>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 \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
 "cbox a b \ box c d \
 (Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a > Re c \<and> Im a > Im c \<and> Re b < Re d \<and> Im b < Im d"
 "box a b \ cbox c d \
 (Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
 "box a b \ box c d \
 (Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> 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<.. Im x \ {Im a<..
 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 cbox_complex_eq: "cbox a b = {x. Re x \ {Re a..Re b} \ Im x \ {Im a..Im b}}"
 by (auto simp: in_cbox_complex_iff)

lemma box_complex_eq: "box a b = {x. Re x \ {Re a<.. Im x \ {Im a<..
 by (auto simp: in_box_complex_iff)

lemma Int_interval:
 fixes a :: "'a::euclidean_space"
 shows "cbox a b \ cbox c d =
 cbox (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>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) *\<^sub>R i)::'a"
 have **: "\P Q. (\i :: 'a. i \ Basis \ Q ?z i \ P i) \
 (\<And>i x :: 'a. i \<in> Basis \<Longrightarrow> P i \<Longrightarrow> Q x i) \<Longrightarrow> (\<forall>x. \<exists>i\<in>Basis. Q x i) \<longleftrightarrow> (\<exists>i\<in>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 *\<^sub>R One)) (real i *\<^sub>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 cbox_shift: "(+) c ` cbox a b = cbox (a + c) (b + c)"
proof -
 have "bij_betw ((+) c) (cbox a b) (cbox (a + c) (b + c))"
 by (rule bij_betwI[of _ _ _ "\x. x - c"]) (auto simp: cbox_def algebra_simps)
 thus ?thesis
 by (simp add: bij_betw_def)
qed

lemma cbox_shift': "(\x. x + c) ` cbox a b = cbox (a + c) (b + c)"
 using cbox_shift[of c a b] by (simp add: add.commute)

lemma cbox_shift'': "(\x. x - c) ` cbox a b = cbox (a - c) (b - c)"
 using cbox_shift[of "-c" a b] by simp

lemma image_affinity_cbox: fixes m::real
 fixes a b c :: "'a::euclidean_space"
 shows "(\x. m *\<^sub>R x + c) ` cbox a b =
 (if cbox a b = {} then {}
 else (if 0 \<le> m then cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)
 else cbox (m *\<^sub>R b + c) (m *\<^sub>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 *\<^sub>R a + c) (m *\<^sub>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 *\<^sub>R a + c) \ i \ (m *\<^sub>R y + c) \ i"
 and "\i\Basis. (m *\<^sub>R y + c) \ i \ (m *\<^sub>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 *\<^sub>R b + c) \ i \ (m *\<^sub>R y + c) \ i"
 and "\i\Basis. (m *\<^sub>R y + c) \ i \ (m *\<^sub>R a + c) \ i"
 by (auto simp: mult_left_mono_neg inner_distrib)
 }
 moreover
 {
 fix y
 assume "m > 0" and "\i\Basis. (m *\<^sub>R a + c) \ i \ y \ i"
 and "\i\Basis. y \ i \ (m *\<^sub>R b + c) \ i"
 then have "y \ (\x. m *\<^sub>R x + c) ` cbox a b"
 unfolding image_iff Bex_def mem_box
 apply (intro exI[where x="(1 / m) *\<^sub>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 *\<^sub>R b + c) \ i \ y \ i" "\i\Basis. y \ i \ (m *\<^sub>R a + c) \ i" "m < 0"
 then have "y \ (\x. m *\<^sub>R x + c) ` cbox a b"
 unfolding image_iff Bex_def mem_box
 apply (intro exI[where x="(1 / m) *\<^sub>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 *\<^sub>R (x::_::euclidean_space)) ` cbox a b =
 (if cbox a b = {} then {} else if 0 \<le> m then cbox (m *\<^sub>R a) (m *\<^sub>R b) else cbox (m *\<^sub>R b) (m *\<^sub>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 0" "ball x R \ A"
 by (auto simp: open_contains_ball)
 define r :: real where "r = R / (2 * sqrt DIM('a))"
 from \<open>R > 0\<close> have [simp]: "r > 0" by (auto simp: r_def)
 define d :: 'a where "d = r *\<^sub>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))\<^sup>2)"
 by (subst euclidean_dist_l2) (auto simp: L2_set_def)
 also from y have "sqrt (\i\Basis. (dist (x \ i) (y \ i))\<^sup>2) \ sqrt (\i\(Basis::'a set). r\<^sup>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\<^sup>2)" by simp
 also have "DIM('a) * r\<^sup>2 = (R / 2) ^ 2"
 by (simp add: r_def power_divide)
 also have "sqrt \ = R / 2"
 using \<open>R > 0\<close> by simp
 also from \<open>R > 0\<close> have "\<dots> < 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 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) *\<^sub>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 \<open>General Intervals\<close>

definition\<^marker>\<open>tag important\<close> "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
 (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> 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) *\<^sub>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) *\<^sub>R i))"
 have "x = (\i\Basis. (if i \ set bs then s i \ i else s j \ i) *\<^sub>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 \<open>?rhs\<close> 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) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + b) \<bullet> i"
 hence "e - x \ X"
 by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, 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) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> 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\<^marker>\<open>tag unimportant\<close> \<open>Bounded Projections\<close>

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\<^marker>\<open>tag unimportant\<close> \<open>Structural rules for pointwise continuity\<close>

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\<^marker>\<open>tag unimportant\<close> \<open>Structural rules for setwise continuity\<close>

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\<^marker>\<open>tag unimportant\<close> \<open>Openness of halfspaces.\<close>

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 i\Basis. {x. x \ i < a \ i})"
 "{x. a 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 "open {x. a
 by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Closure and Interior of halfspaces and hyperplanes\<close>

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>open S\<close> open_contains_cball x by blast
 then have "x + (e / norm a) *\<^sub>R a \ cball x e"
 by (simp add: dist_norm)
 then have "x + (e / norm a) *\<^sub>R a \ S"
 using e by blast
 then have "x + (e / norm a) *\<^sub>R a \ {x. a \ x \ b}"
 using S by blast
 moreover have "e * (a \ a) / norm a > 0"
 by (simp add: \<open>0 < e\<close> 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\<^marker>\<open>tag unimportant\<close>\<open>Some more convenient intermediate-value theorem formulations\<close>

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 \<open>connected S\<close> 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 \<open>Limit Component Bounds\<close>

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) *\<^sub>R i) x < e"
 and "dist (x + (e / 2) *\<^sub>R i) x < e"
 using norm_Basis[OF i] \<open>e>0\<close> by (auto simp: dist_norm)
 then have "a \ i \ (x - (e / 2) *\<^sub>R i) \ i" and "(x + (e / 2) *\<^sub>R i) \ i \ b \ i"
 using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
 and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
 unfolding mem_box using i by blast+
 then have "a \ i < x \ i" and "x \ i e>0\<close> 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) *\<^sub>R (a + b)) \ box a b"
proof -
 have "a \ i < ((1 / 2) *\<^sub>R (a + b)) \ i \ ((1 / 2) *\<^sub>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"
--> --------------------

--> maximum size reached

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

quality94%

¤ Dauer der Verarbeitung: 0.29 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.