Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Complex_Analysis.thy Sprache: Isabelle

Original von: 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 (a' - a - (r / norm (a - a')) *\<^sub>R (a - a'))"
 by (simp add: algebra_simps)
 also have "... = 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 (simp add: field_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 (simp split: abs_split)
 (metis \<open>0 \<le> r\<close> \<open>?lhs\<close> centre_in_cball dist_commute dist_norm less_asym mem_ball subset_eq)
 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"
 (is "?lhs = ?rhs")
proof
 assume ?lhs
 then show ?rhs
 proof (cases "d \ 0 \ e \ 0")
 case True
 with \<open>?lhs\<close> show ?rhs
 by safe (simp_all only: ball_eq_empty [of y e, symmetric] ball_eq_empty [of x d, symmetric])
 next
 case False
 with \<open>?lhs\<close> show ?rhs
 apply (auto simp: set_eq_subset ball_subset_ball_iff dist_norm norm_minus_commute algebra_simps)
 apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
 apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
 done
 qed
next
 assume ?rhs then show ?lhs
 by (auto simp: set_eq_subset ball_subset_ball_iff)
qed

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"
 (is "?lhs = ?rhs")
proof
 assume ?lhs
 then show ?rhs
 proof (cases "d < 0 \ e < 0")
 case True
 with \<open>?lhs\<close> show ?rhs
 by safe (simp_all only: cball_eq_empty [of y e, symmetric] cball_eq_empty [of x d, symmetric])
 next
 case False
 with \<open>?lhs\<close> show ?rhs
 apply (auto simp: set_eq_subset cball_subset_cball_iff dist_norm norm_minus_commute algebra_simps)
 apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
 apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
 done
 qed
next
 assume ?rhs then show ?lhs
 by (auto simp: set_eq_subset cball_subset_cball_iff)
qed

lemma ball_eq_cball_iff:
 fixes x :: "'a :: euclidean_space"
 shows "ball x d = cball y e \ d \ 0 \ e < 0" (is "?lhs = ?rhs")
proof
 assume ?lhs
 then show ?rhs
 apply (auto simp: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps)
 apply (metis add_increasing2 add_le_cancel_right add_less_same_cancel1 dist_not_less_zero less_le_trans zero_le_dist)
 apply (metis add_less_same_cancel1 dist_not_less_zero less_le_trans not_le)
 using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
 done
next
 assume ?rhs then show ?lhs by auto
qed

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 \e2>0\ \e1>0\
 apply (rule_tac x="min e1 e2" in exI)
 by 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 "<e" 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)"
 apply (auto simp: cbox_def Basis_complex_def)
 apply (rule_tac x = "(Re x, Im x)" in image_eqI)
 using complex_eq by auto

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 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 "\i. \y. y \ \ \ y < x \ i \ x \ i - y < e'" (is "\i. ?th i")
 proof
 fix i
 from Rats_dense_in_real[of "x \ i - e'" "x \ i"] e
 show "?th i" by auto
 qed
 from choice[OF this] obtain a where
 a: "\xa. a xa \ \ \ a xa < x \ xa \ x \ xa - a xa < e'" ..
 have "\i. \y. y \ \ \ x \ i < y \ y - x \ i < e'" (is "\i. ?th i")
 proof
 fix i
 from Rats_dense_in_real[of "x \ i" "x \ i + e'"] e
 show "?th i" by auto
 qed
 from choice[OF this] obtain b where
 b: "\xa. b xa \ \ \ x \ xa 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'"
 using a by auto
 moreover have "x\i < b i" "b i - x\i < e'"
 using 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 (insert a b, 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) *\<^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 "\i. \y. y \ \ \ y < x \ i \ x \ i - y < e'" (is "\i. ?th i")
 proof
 fix i
 from Rats_dense_in_real[of "x \ i - e'" "x \ i"] e
 show "?th i" by auto
 qed
 from choice[OF this] obtain a where
 a: "\u. a u \ \ \ a u < x \ u \ x \ u - a u < e'" ..
 have "\i. \y. y \ \ \ x \ i < y \ y - x \ i < e'" (is "\i. ?th i")
 proof
 fix i
 from Rats_dense_in_real[of "x \ i" "x \ i + e'"] e
 show "?th i" by auto
 qed
 from choice[OF this] 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'"
 using a by auto
 moreover have "x\i < b i" "b i - x\i < e'"
 using 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 -
 {
 fix i x
 assume i: "i\Basis" and as:"b\i \ a\i" and x:"x\box a b"
 then have "a \ i < x \ i \ x \ i < b \ i"
 unfolding mem_box by (auto simp: box_def)
 then have "a\i < b\i" by auto
 then have False using as by auto
 }
 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[THEN bspec[where x=i]] i by auto
 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 \ {}"
 using mem_box(1)[of "?x" a b] by auto
 }
 ultimately show ?th1 by blast

 {
 fix i x
 assume i: "i \ Basis" and as:"b\i < a\i" and x:"x\cbox a b"
 then have "a \ i \ x \ i \ x \ i \ b \ i"
 unfolding mem_box by auto
 then have "a\i \ b\i" by auto
 then have False using as by auto
 }
 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[THEN bspec[where x=i]] i by auto
 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 "cbox a b \ {}"
 using mem_box(2)[of "?x" a b] by auto
 }
 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_sing [simp]: "cbox a a = {a}"
 and box_sing [simp]: "box a a = {}"
 unfolding set_eq_iff mem_box eq_iff [symmetric]
 by (auto intro!: euclidean_eqI[where 'a='a])
 (metis all_not_in_conv nonempty_Basis)

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)
next
 assume ?rhs
 then show ?lhs
 by force
qed

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
 then show ?rhs
 apply (simp add: subset_box)
 using L box_ne_empty box_sing apply (fastforce simp add:)
 done
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
 apply (simp add: subset_box)
 using box_ne_empty(2) L
 apply auto
 apply (meson euclidean_eqI less_eq_real_def not_less)+
 done
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 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 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 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
 apply (rule ssubst)
 apply (rule continuous_on_compose)
 apply (simp add: split_def)
 apply (rule continuous_intros | simp add: assms)+
 done
qed

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"
 by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)])

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]
 apply (induct bs)
 apply (auto simp: y_def j)
 apply (rule interval_subst[OF assms(1)])
 apply (auto simp: s)
 done
 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 unfolding is_interval_def
 apply (clarsimp simp add: mem_box)
 using that by blast
 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 (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
 (auto simp: algebra_simps)
 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 simp:)
 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 simp:)
 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>[unfolded connected_def not_ex,
 THEN spec[where x="?A"], THEN spec[where x="?B"]]
 using xy b by auto
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"
 unfolding dist_norm
 apply auto
 unfolding norm_minus_cancel
 using norm_Basis[OF i] \<open>e>0\<close>
 apply auto
 done
 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)"
 using bounded_cbox[of a b] box_subset_cbox[of a b] bounded_subset[of "cbox a b" "box a b"]
 by simp

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"
 assumes x: "x \ box a b"
 and y: "y \ cbox a b"
 and e: "0 < e" "e \ 1"
 shows "(e *\<^sub>R x + (1 - e) *\<^sub>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)"
 proof (rule add_less_le_mono)
 show "e * (a \ i) < e * (x \ i)"
 using \<open>0 < e\<close> i mem_box(1) x by auto
 show "(1 - e) * (a \ i) \ (1 - e) * (y \ i)"
 by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
 qed
 finally have "a \ i < (e *\<^sub>R x + (1 - e) *\<^sub>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)"
 proof (rule add_less_le_mono)
 show "e * (x \ i) < e * (b \ i)"
 using \<open>0 < e\<close> i mem_box(1) x by auto
 show "(1 - e) * (y \ i) \ (1 - e) * (b \ i)"
 by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
 qed
 finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i R x + (1 - e) *\<^sub>R y) \ i \ (e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i --------------------

--> maximum size reached

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

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.72Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

Begriffe der Konzeptbildung Was zu einem Entwurf gehört
Begriffe der Konzeptbildung Hier finden Sie eine Liste der Produkte des Unternehmens
Mittel

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Complex_Analysis.thy Sprache: Isabelle

Original von: Isabelle^©

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.72Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

Lebenszyklus

Ziele

Bot Zugriff

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Complex_Analysis.thy Sprache: Isabelle

Original von: Isabelle©

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.72Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

Lebenszyklus

Ziele

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©