src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 57447 87429bdecad5
parent 57418 6ab1c7cb0b8d
child 57448 159e45728ceb
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 30 15:45:03 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 30 15:45:21 2014 +0200
     1.3 @@ -825,6 +825,9 @@
     1.4  
     1.5  subsection {* Boxes *}
     1.6  
     1.7 +abbreviation One :: "'a::euclidean_space"
     1.8 +  where "One \<equiv> \<Sum>Basis"
     1.9 +
    1.10  definition (in euclidean_space) eucl_less (infix "<e" 50)
    1.11    where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
    1.12  
    1.13 @@ -847,6 +850,12 @@
    1.14    shows "box a b = {a <..< b}" "cbox a b = {a .. b}"
    1.15    by auto
    1.16  
    1.17 +lemma box_Int_box:
    1.18 +  fixes a :: "'a::euclidean_space"
    1.19 +  shows "box a b \<inter> box c d =
    1.20 +    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)"
    1.21 +  unfolding set_eq_iff and Int_iff and mem_box by auto
    1.22 +
    1.23  lemma rational_boxes:
    1.24    fixes x :: "'a\<Colon>euclidean_space"
    1.25    assumes "e > 0"
    1.26 @@ -1142,6 +1151,24 @@
    1.27    show ?th4 unfolding * by (intro **) auto
    1.28  qed
    1.29  
    1.30 +lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV"
    1.31 +proof -
    1.32 +  { fix x b :: 'a assume [simp]: "b \<in> Basis"
    1.33 +    have "\<bar>x \<bullet> b\<bar> \<le> real (natceiling \<bar>x \<bullet> b\<bar>)"
    1.34 +      by (rule real_natceiling_ge)
    1.35 +    also have "\<dots> \<le> real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
    1.36 +      by (auto intro!: natceiling_mono)
    1.37 +    also have "\<dots> < real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
    1.38 +      by simp
    1.39 +    finally have "\<bar>x \<bullet> b\<bar> < real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)" . }
    1.40 +  then have "\<And>x::'a. \<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n"
    1.41 +    by auto
    1.42 +  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"
    1.43 +    by auto
    1.44 +  ultimately show ?thesis
    1.45 +    by (auto simp: box_def inner_setsum_left inner_Basis setsum.If_cases)
    1.46 +qed
    1.47 +
    1.48  text {* Intervals in general, including infinite and mixtures of open and closed. *}
    1.49  
    1.50  definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
    1.51 @@ -4588,6 +4615,43 @@
    1.52    "continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
    1.53    using continuous_within_eps_delta [of x UNIV f] by simp
    1.54  
    1.55 +lemma continuous_at_right_real_increasing:
    1.56 +  assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)"
    1.57 +  shows "(continuous (at_right (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f (a + delta) - f a < e)"
    1.58 +  apply (auto simp add: continuous_within_eps_delta dist_real_def greaterThan_def)
    1.59 +  apply (drule_tac x = e in spec, auto)
    1.60 +  apply (drule_tac x = "a + d / 2" in spec)
    1.61 +  apply (subst (asm) abs_of_nonneg)
    1.62 +  apply (auto intro: nondecF simp add: field_simps)
    1.63 +  apply (rule_tac x = "d / 2" in exI)
    1.64 +  apply (auto simp add: field_simps)
    1.65 +  apply (drule_tac x = e in spec, auto)
    1.66 +  apply (rule_tac x = delta in exI, auto)
    1.67 +  apply (subst abs_of_nonneg)
    1.68 +  apply (auto intro: nondecF simp add: field_simps)
    1.69 +  apply (rule le_less_trans)
    1.70 +  prefer 2 apply assumption
    1.71 +by (rule nondecF, auto)
    1.72 +
    1.73 +lemma continuous_at_left_real_increasing:
    1.74 +  assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)"
    1.75 +  shows "(continuous (at_left (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f a - f (a - delta) < e)"
    1.76 +  apply (auto simp add: continuous_within_eps_delta dist_real_def lessThan_def)
    1.77 +  apply (drule_tac x = e in spec, auto)
    1.78 +  apply (drule_tac x = "a - d / 2" in spec)
    1.79 +  apply (subst (asm) abs_of_nonpos)
    1.80 +  apply (auto intro: nondecF simp add: field_simps)
    1.81 +  apply (rule_tac x = "d / 2" in exI)
    1.82 +  apply (auto simp add: field_simps)
    1.83 +  apply (drule_tac x = e in spec, auto)
    1.84 +  apply (rule_tac x = delta in exI, auto)
    1.85 +  apply (subst abs_of_nonpos)
    1.86 +  apply (auto intro: nondecF simp add: field_simps)
    1.87 +  apply (rule less_le_trans)
    1.88 +  apply assumption
    1.89 +  apply auto
    1.90 +by (rule nondecF, auto)
    1.91 +
    1.92  text{* Versions in terms of open balls. *}
    1.93  
    1.94  lemma continuous_within_ball: