src/HOL/Real_Vector_Spaces.thy
 changeset 62101 26c0a70f78a3 parent 62087 44841d07ef1d child 62102 877463945ce9
1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 16:37:56 2016 +0100
1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 17:40:59 2016 +0100
1.3 @@ -191,7 +191,7 @@
1.4    fixes x :: "'a::real_vector"
1.5    shows "scaleR (-1) x = - x"
1.6    using scaleR_minus_left [of 1 x] by simp
1.7 -
1.8 +
1.9  class real_algebra = real_vector + ring +
1.10    assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
1.11    and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
1.12 @@ -662,10 +662,19 @@
1.13  class dist_norm = dist + norm + minus +
1.14    assumes dist_norm: "dist x y = norm (x - y)"
1.16 -class open_dist = "open" + dist +
1.17 -  assumes open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
1.18 +class uniformity_dist = dist + uniformity +
1.19 +  assumes uniformity_dist: "uniformity = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
1.20 +begin
1.22 -class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist +
1.23 +lemma eventually_uniformity_metric:
1.24 +  "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x y. dist x y < e \<longrightarrow> P (x, y))"
1.25 +  unfolding uniformity_dist
1.26 +  by (subst eventually_INF_base)
1.27 +     (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
1.28 +
1.29 +end
1.30 +
1.31 +class real_normed_vector = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
1.32    assumes norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
1.33    and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
1.34    and norm_scaleR [simp]: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
1.35 @@ -686,8 +695,8 @@
1.37  class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra +
1.38    assumes norm_one [simp]: "norm 1 = 1"
1.39 -
1.40 -lemma (in real_normed_algebra_1) scaleR_power [simp]:
1.41 +
1.42 +lemma (in real_normed_algebra_1) scaleR_power [simp]:
1.43    "(scaleR x y) ^ n = scaleR (x^n) (y^n)"
1.44    by (induction n) (simp_all add: scaleR_one scaleR_scaleR mult_ac)
1.46 @@ -1010,7 +1019,7 @@
1.48  subsection \<open>Metric spaces\<close>
1.50 -class metric_space = open_dist +
1.51 +class metric_space = uniformity_dist + open_uniformity +
1.52    assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
1.53    assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
1.54  begin
1.55 @@ -1074,26 +1083,23 @@
1.56    shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
1.57  by (rule dist_triangle_half_l, simp_all add: dist_commute)
1.59 -subclass topological_space
1.60 +subclass uniform_space
1.61  proof
1.62 -  have "\<exists>e::real. 0 < e"
1.63 -    by (blast intro: zero_less_one)
1.64 -  then show "open UNIV"
1.65 -    unfolding open_dist by simp
1.66 -next
1.67 -  fix S T assume "open S" "open T"
1.68 -  then show "open (S \<inter> T)"
1.69 -    unfolding open_dist
1.70 -    apply clarify
1.71 -    apply (drule (1) bspec)+
1.72 -    apply (clarify, rename_tac r s)
1.73 -    apply (rule_tac x="min r s" in exI, simp)
1.74 -    done
1.75 -next
1.76 -  fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
1.77 -    unfolding open_dist by (meson UnionE UnionI)
1.78 +  fix E x assume "eventually E uniformity"
1.79 +  then obtain e where E: "0 < e" "\<And>x y. dist x y < e \<Longrightarrow> E (x, y)"
1.80 +    unfolding eventually_uniformity_metric by auto
1.81 +  then show "E (x, x)" "\<forall>\<^sub>F (x, y) in uniformity. E (y, x)"
1.82 +    unfolding eventually_uniformity_metric by (auto simp: dist_commute)
1.83 +
1.84 +  show "\<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))"
1.85 +    using E dist_triangle_half_l[where e=e] unfolding eventually_uniformity_metric
1.86 +    by (intro exI[of _ "\<lambda>(x, y). dist x y < e / 2"] exI[of _ "e/2"] conjI)
1.87 +       (auto simp: dist_commute)
1.88  qed
1.90 +lemma open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
1.91 +  unfolding open_uniformity eventually_uniformity_metric by (simp add: dist_commute)
1.92 +
1.93  lemma open_ball: "open {y. dist x y < d}"
1.94  proof (unfold open_dist, intro ballI)
1.95    fix y assume *: "y \<in> {y. dist x y < d}"
1.96 @@ -1156,8 +1162,11 @@
1.97  definition dist_real_def:
1.98    "dist x y = \<bar>x - y\<bar>"
1.100 +definition uniformity_real_def [code del]:
1.101 +  "(uniformity :: (real \<times> real) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
1.103  definition open_real_def [code del]:
1.104 -  "open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
1.105 +  "open (U :: real set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
1.107  definition real_norm_def [simp]:
1.108    "norm r = \<bar>r\<bar>"
1.109 @@ -1165,8 +1174,9 @@
1.110  instance
1.111  apply (intro_classes, unfold real_norm_def real_scaleR_def)
1.112  apply (rule dist_real_def)
1.113 +apply (simp add: sgn_real_def)
1.114 +apply (rule uniformity_real_def)
1.115  apply (rule open_real_def)
1.116 -apply (simp add: sgn_real_def)
1.117  apply (rule abs_eq_0)
1.118  apply (rule abs_triangle_ineq)
1.119  apply (rule abs_mult)
1.120 @@ -1188,7 +1198,7 @@
1.121    proof (rule ext, safe)
1.122      fix S :: "real set" assume "open S"
1.123      then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
1.124 -      unfolding open_real_def bchoice_iff ..
1.125 +      unfolding open_dist bchoice_iff ..
1.126      then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
1.127        by (fastforce simp: dist_real_def)
1.128      show "generate_topology (range lessThan \<union> range greaterThan) S"
1.129 @@ -1199,14 +1209,14 @@
1.130    next
1.131      fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S"
1.132      moreover have "\<And>a::real. open {..<a}"
1.133 -      unfolding open_real_def dist_real_def
1.134 +      unfolding open_dist dist_real_def
1.135      proof clarify
1.136        fix x a :: real assume "x < a"
1.137        hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
1.138        thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
1.139      qed
1.140      moreover have "\<And>a::real. open {a <..}"
1.141 -      unfolding open_real_def dist_real_def
1.142 +      unfolding open_dist dist_real_def
1.143      proof clarify
1.144        fix x a :: real assume "a < x"
1.145        hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
1.146 @@ -1233,6 +1243,11 @@
1.148    (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
1.150 +text \<open>Only allow @{term "uniformity"} in class \<open>uniform_space\<close>.\<close>
1.153 +  (@{const_name "uniformity"}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
1.155  text \<open>Only allow @{term dist} in class \<open>metric_space\<close>.\<close>
1.158 @@ -1786,10 +1801,22 @@
1.160  subsection \<open>Cauchy sequences\<close>
1.162 -definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
1.163 -  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
1.164 +lemma (in metric_space) Cauchy_def: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e)"
1.165 +proof -
1.166 +  have *: "eventually P (INF M. principal {(X m, X n) | n m. m \<ge> M \<and> n \<ge> M}) =
1.167 +    (\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. P (X m, X n))" for P
1.168 +  proof (subst eventually_INF_base, goal_cases)
1.169 +    case (2 a b) then show ?case
1.170 +      by (intro bexI[of _ "max a b"]) (auto simp: eventually_principal subset_eq)
1.171 +  qed (auto simp: eventually_principal, blast)
1.172 +  have "Cauchy X \<longleftrightarrow> (INF M. principal {(X m, X n) | n m. m \<ge> M \<and> n \<ge> M}) \<le> uniformity"
1.173 +    unfolding Cauchy_uniform_iff le_filter_def * ..
1.174 +  also have "\<dots> = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e)"
1.175 +    unfolding uniformity_dist le_INF_iff by (auto simp: * le_principal)
1.176 +  finally show ?thesis .
1.177 +qed
1.179 -lemma Cauchy_altdef:
1.180 +lemma (in metric_space) Cauchy_altdef:
1.181    "Cauchy f = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e)"
1.182  proof
1.183    assume A: "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
1.184 @@ -1812,18 +1839,18 @@
1.185    qed
1.186  qed
1.188 -lemma metric_CauchyI:
1.189 +lemma (in metric_space) metric_CauchyI:
1.190    "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
1.191    by (simp add: Cauchy_def)
1.193 -lemma CauchyI': "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
1.194 +lemma (in metric_space) CauchyI': "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
1.195    unfolding Cauchy_altdef by blast
1.197 -lemma metric_CauchyD:
1.198 +lemma (in metric_space) metric_CauchyD:
1.199    "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
1.200    by (simp add: Cauchy_def)
1.202 -lemma metric_Cauchy_iff2:
1.203 +lemma (in metric_space) metric_Cauchy_iff2:
1.204    "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < inverse(real (Suc j))))"
1.205  apply (simp add: Cauchy_def, auto)
1.206  apply (drule reals_Archimedean, safe)
1.207 @@ -1837,40 +1864,118 @@
1.208    "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
1.209    unfolding metric_Cauchy_iff2 dist_real_def ..
1.211 -lemma Cauchy_subseq_Cauchy:
1.212 -  "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)"
1.213 -apply (auto simp add: Cauchy_def)
1.214 -apply (drule_tac x=e in spec, clarify)
1.215 -apply (rule_tac x=M in exI, clarify)
1.216 -apply (blast intro: le_trans [OF _ seq_suble] dest!: spec)
1.217 -done
1.219 -theorem LIMSEQ_imp_Cauchy:
1.220 -  assumes X: "X \<longlonglongrightarrow> a" shows "Cauchy X"
1.221 -proof (rule metric_CauchyI)
1.222 -  fix e::real assume "0 < e"
1.223 -  hence "0 < e/2" by simp
1.224 -  with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D)
1.225 -  then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" ..
1.226 -  show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
1.227 -  proof (intro exI allI impI)
1.228 -    fix m assume "N \<le> m"
1.229 -    hence m: "dist (X m) a < e/2" using N by blast
1.230 -    fix n assume "N \<le> n"
1.231 -    hence n: "dist (X n) a < e/2" using N by blast
1.232 -    have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
1.233 -      by (rule dist_triangle2)
1.234 -    also from m n have "\<dots> < e" by simp
1.235 -    finally show "dist (X m) (X n) < e" .
1.236 -  qed
1.237 +lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
1.238 +proof (subst lim_sequentially, intro allI impI exI)
1.239 +  fix e :: real assume e: "e > 0"
1.240 +  fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
1.241 +  have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
1.242 +  also note n
1.243 +  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
1.244 +    by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
1.245  qed
1.247 -lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
1.248 -unfolding convergent_def
1.249 -by (erule exE, erule LIMSEQ_imp_Cauchy)
1.250 +lemma (in metric_space) complete_def:
1.251 +  shows "complete S = (\<forall>f. (\<forall>n. f n \<in> S) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>S. f \<longlonglongrightarrow> l))"
1.252 +  unfolding complete_uniform
1.253 +proof safe
1.254 +  fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> S" "Cauchy f"
1.255 +    and *: "\<forall>F\<le>principal S. F \<noteq> bot \<longrightarrow> cauchy_filter F \<longrightarrow> (\<exists>x\<in>S. F \<le> nhds x)"
1.256 +  then show "\<exists>l\<in>S. f \<longlonglongrightarrow> l"
1.257 +    unfolding filterlim_def using f
1.258 +    by (intro *[rule_format])
1.259 +       (auto simp: filtermap_sequentually_ne_bot le_principal eventually_filtermap Cauchy_uniform)
1.260 +next
1.261 +  fix F :: "'a filter" assume "F \<le> principal S" "F \<noteq> bot" "cauchy_filter F"
1.262 +  assume seq: "\<forall>f. (\<forall>n. f n \<in> S) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>S. f \<longlonglongrightarrow> l)"
1.264 +  from \<open>F \<le> principal S\<close> \<open>cauchy_filter F\<close> have FF_le: "F \<times>\<^sub>F F \<le> uniformity_on S"
1.265 +    by (simp add: cauchy_filter_def principal_prod_principal[symmetric] prod_filter_mono)
1.267 +  let ?P = "\<lambda>P e. eventually P F \<and> (\<forall>x. P x \<longrightarrow> x \<in> S) \<and> (\<forall>x y. P x \<longrightarrow> P y \<longrightarrow> dist x y < e)"
1.269 +  { fix \<epsilon> :: real assume "0 < \<epsilon>"
1.270 +    then have "eventually (\<lambda>(x, y). x \<in> S \<and> y \<in> S \<and> dist x y < \<epsilon>) (uniformity_on S)"
1.271 +      unfolding eventually_inf_principal eventually_uniformity_metric by auto
1.272 +    from filter_leD[OF FF_le this] have "\<exists>P. ?P P \<epsilon>"
1.273 +      unfolding eventually_prod_same by auto }
1.274 +  note P = this
1.276 +  have "\<exists>P. \<forall>n. ?P (P n) (1 / Suc n) \<and> P (Suc n) \<le> P n"
1.277 +  proof (rule dependent_nat_choice)
1.278 +    show "\<exists>P. ?P P (1 / Suc 0)"
1.279 +      using P[of 1] by auto
1.280 +  next
1.281 +    fix P n assume "?P P (1/Suc n)"
1.282 +    moreover obtain Q where "?P Q (1 / Suc (Suc n))"
1.283 +      using P[of "1/Suc (Suc n)"] by auto
1.284 +    ultimately show "\<exists>Q. ?P Q (1 / Suc (Suc n)) \<and> Q \<le> P"
1.285 +      by (intro exI[of _ "\<lambda>x. P x \<and> Q x"]) (auto simp: eventually_conj_iff)
1.286 +  qed
1.287 +  then obtain P where P: "\<And>n. eventually (P n) F" "\<And>n x. P n x \<Longrightarrow> x \<in> S"
1.288 +    "\<And>n x y. P n x \<Longrightarrow> P n y \<Longrightarrow> dist x y < 1 / Suc n" "\<And>n. P (Suc n) \<le> P n"
1.289 +    by metis
1.290 +  have "antimono P"
1.291 +    using P(4) unfolding decseq_Suc_iff le_fun_def by blast
1.293 +  obtain X where X: "\<And>n. P n (X n)"
1.294 +    using P(1)[THEN eventually_happens'[OF \<open>F \<noteq> bot\<close>]] by metis
1.295 +  have "Cauchy X"
1.296 +    unfolding metric_Cauchy_iff2 inverse_eq_divide
1.297 +  proof (intro exI allI impI)
1.298 +    fix j m n :: nat assume "j \<le> m" "j \<le> n"
1.299 +    with \<open>antimono P\<close> X have "P j (X m)" "P j (X n)"
1.300 +      by (auto simp: antimono_def)
1.301 +    then show "dist (X m) (X n) < 1 / Suc j"
1.302 +      by (rule P)
1.303 +  qed
1.304 +  moreover have "\<forall>n. X n \<in> S"
1.305 +    using P(2) X by auto
1.306 +  ultimately obtain x where "X \<longlonglongrightarrow> x" "x \<in> S"
1.307 +    using seq by blast
1.309 +  show "\<exists>x\<in>S. F \<le> nhds x"
1.310 +  proof (rule bexI)
1.311 +    { fix e :: real assume "0 < e"
1.312 +      then have "(\<lambda>n. 1 / Suc n :: real) \<longlonglongrightarrow> 0 \<and> 0 < e / 2"
1.313 +        by (subst LIMSEQ_Suc_iff) (auto intro!: lim_1_over_n)
1.314 +      then have "\<forall>\<^sub>F n in sequentially. dist (X n) x < e / 2 \<and> 1 / Suc n < e / 2"
1.315 +        using \<open>X \<longlonglongrightarrow> x\<close> unfolding tendsto_iff order_tendsto_iff[where 'a=real] eventually_conj_iff by blast
1.316 +      then obtain n where "dist x (X n) < e / 2" "1 / Suc n < e / 2"
1.317 +        by (auto simp: eventually_sequentially dist_commute)
1.318 +      have "eventually (\<lambda>y. dist y x < e) F"
1.319 +        using \<open>eventually (P n) F\<close>
1.320 +      proof eventually_elim
1.321 +        fix y assume "P n y"
1.322 +        then have "dist y (X n) < 1 / Suc n"
1.323 +          by (intro X P)
1.324 +        also have "\<dots> < e / 2" by fact
1.325 +        finally show "dist y x < e"
1.326 +          by (rule dist_triangle_half_l) fact
1.327 +      qed }
1.328 +    then show "F \<le> nhds x"
1.329 +      unfolding nhds_metric le_INF_iff le_principal by auto
1.330 +  qed fact
1.331 +qed
1.333 +lemma (in metric_space) totally_bounded_metric:
1.334 +  "totally_bounded S \<longleftrightarrow> (\<forall>e>0. \<exists>k. finite k \<and> S \<subseteq> (\<Union>x\<in>k. {y. dist x y < e}))"
1.335 +  unfolding totally_bounded_def eventually_uniformity_metric imp_ex
1.336 +  apply (subst all_comm)
1.337 +  apply (intro arg_cong[where f=All] ext)
1.338 +  apply safe
1.339 +  subgoal for e
1.340 +    apply (erule allE[of _ "\<lambda>(x, y). dist x y < e"])
1.341 +    apply auto
1.342 +    done
1.343 +  subgoal for e P k
1.344 +    apply (intro exI[of _ k])
1.345 +    apply (force simp: subset_eq)
1.346 +    done
1.347 +  done
1.349  subsubsection \<open>Cauchy Sequences are Convergent\<close>
1.351 +(* TODO: update to uniform_space *)
1.352  class complete_space = metric_space +
1.353    assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"