823 by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left) |
823 by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left) |
824 |
824 |
825 |
825 |
826 subsection {* Boxes *} |
826 subsection {* Boxes *} |
827 |
827 |
|
828 abbreviation One :: "'a::euclidean_space" |
|
829 where "One \<equiv> \<Sum>Basis" |
|
830 |
828 definition (in euclidean_space) eucl_less (infix "<e" 50) |
831 definition (in euclidean_space) eucl_less (infix "<e" 50) |
829 where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)" |
832 where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)" |
830 |
833 |
831 definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}" |
834 definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}" |
832 definition "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}" |
835 definition "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}" |
844 |
847 |
845 lemma box_real[simp]: |
848 lemma box_real[simp]: |
846 fixes a b:: real |
849 fixes a b:: real |
847 shows "box a b = {a <..< b}" "cbox a b = {a .. b}" |
850 shows "box a b = {a <..< b}" "cbox a b = {a .. b}" |
848 by auto |
851 by auto |
|
852 |
|
853 lemma box_Int_box: |
|
854 fixes a :: "'a::euclidean_space" |
|
855 shows "box a b \<inter> box c d = |
|
856 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)" |
|
857 unfolding set_eq_iff and Int_iff and mem_box by auto |
849 |
858 |
850 lemma rational_boxes: |
859 lemma rational_boxes: |
851 fixes x :: "'a\<Colon>euclidean_space" |
860 fixes x :: "'a\<Colon>euclidean_space" |
852 assumes "e > 0" |
861 assumes "e > 0" |
853 shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat> ) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e" |
862 shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat> ) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e" |
1138 note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10) |
1147 note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10) |
1139 show ?th1 unfolding * by (intro **) auto |
1148 show ?th1 unfolding * by (intro **) auto |
1140 show ?th2 unfolding * by (intro **) auto |
1149 show ?th2 unfolding * by (intro **) auto |
1141 show ?th3 unfolding * by (intro **) auto |
1150 show ?th3 unfolding * by (intro **) auto |
1142 show ?th4 unfolding * by (intro **) auto |
1151 show ?th4 unfolding * by (intro **) auto |
|
1152 qed |
|
1153 |
|
1154 lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV" |
|
1155 proof - |
|
1156 { fix x b :: 'a assume [simp]: "b \<in> Basis" |
|
1157 have "\<bar>x \<bullet> b\<bar> \<le> real (natceiling \<bar>x \<bullet> b\<bar>)" |
|
1158 by (rule real_natceiling_ge) |
|
1159 also have "\<dots> \<le> real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))" |
|
1160 by (auto intro!: natceiling_mono) |
|
1161 also have "\<dots> < real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)" |
|
1162 by simp |
|
1163 finally have "\<bar>x \<bullet> b\<bar> < real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)" . } |
|
1164 then have "\<And>x::'a. \<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n" |
|
1165 by auto |
|
1166 moreover have "\<And>x b::'a. \<And>n::nat. \<bar>x \<bullet> b\<bar> < real n \<longleftrightarrow> - real n < x \<bullet> b \<and> x \<bullet> b < real n" |
|
1167 by auto |
|
1168 ultimately show ?thesis |
|
1169 by (auto simp: box_def inner_setsum_left inner_Basis setsum.If_cases) |
1143 qed |
1170 qed |
1144 |
1171 |
1145 text {* Intervals in general, including infinite and mixtures of open and closed. *} |
1172 text {* Intervals in general, including infinite and mixtures of open and closed. *} |
1146 |
1173 |
1147 definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow> |
1174 definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow> |
4586 |
4613 |
4587 lemma continuous_at_eps_delta: |
4614 lemma continuous_at_eps_delta: |
4588 "continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)" |
4615 "continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)" |
4589 using continuous_within_eps_delta [of x UNIV f] by simp |
4616 using continuous_within_eps_delta [of x UNIV f] by simp |
4590 |
4617 |
|
4618 lemma continuous_at_right_real_increasing: |
|
4619 assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)" |
|
4620 shows "(continuous (at_right (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f (a + delta) - f a < e)" |
|
4621 apply (auto simp add: continuous_within_eps_delta dist_real_def greaterThan_def) |
|
4622 apply (drule_tac x = e in spec, auto) |
|
4623 apply (drule_tac x = "a + d / 2" in spec) |
|
4624 apply (subst (asm) abs_of_nonneg) |
|
4625 apply (auto intro: nondecF simp add: field_simps) |
|
4626 apply (rule_tac x = "d / 2" in exI) |
|
4627 apply (auto simp add: field_simps) |
|
4628 apply (drule_tac x = e in spec, auto) |
|
4629 apply (rule_tac x = delta in exI, auto) |
|
4630 apply (subst abs_of_nonneg) |
|
4631 apply (auto intro: nondecF simp add: field_simps) |
|
4632 apply (rule le_less_trans) |
|
4633 prefer 2 apply assumption |
|
4634 by (rule nondecF, auto) |
|
4635 |
|
4636 lemma continuous_at_left_real_increasing: |
|
4637 assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)" |
|
4638 shows "(continuous (at_left (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f a - f (a - delta) < e)" |
|
4639 apply (auto simp add: continuous_within_eps_delta dist_real_def lessThan_def) |
|
4640 apply (drule_tac x = e in spec, auto) |
|
4641 apply (drule_tac x = "a - d / 2" in spec) |
|
4642 apply (subst (asm) abs_of_nonpos) |
|
4643 apply (auto intro: nondecF simp add: field_simps) |
|
4644 apply (rule_tac x = "d / 2" in exI) |
|
4645 apply (auto simp add: field_simps) |
|
4646 apply (drule_tac x = e in spec, auto) |
|
4647 apply (rule_tac x = delta in exI, auto) |
|
4648 apply (subst abs_of_nonpos) |
|
4649 apply (auto intro: nondecF simp add: field_simps) |
|
4650 apply (rule less_le_trans) |
|
4651 apply assumption |
|
4652 apply auto |
|
4653 by (rule nondecF, auto) |
|
4654 |
4591 text{* Versions in terms of open balls. *} |
4655 text{* Versions in terms of open balls. *} |
4592 |
4656 |
4593 lemma continuous_within_ball: |
4657 lemma continuous_within_ball: |
4594 "continuous (at x within s) f \<longleftrightarrow> |
4658 "continuous (at x within s) f \<longleftrightarrow> |
4595 (\<forall>e > 0. \<exists>d > 0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e)" |
4659 (\<forall>e > 0. \<exists>d > 0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e)" |