diff --git a/src/HOL/Analysis/Elementary_Topology.thy b/src/HOL/Analysis/Elementary_Topology.thy --- a/src/HOL/Analysis/Elementary_Topology.thy +++ b/src/HOL/Analysis/Elementary_Topology.thy @@ -1,2755 +1,2666 @@ (* 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 \Topology\ theory Elementary_Topology imports "HOL-Library.Set_Idioms" "HOL-Library.Disjoint_Sets" Product_Vector begin section \Elementary Topology\ subsection \TODO: move?\ lemma open_subopen: "open S \ (\x\S. \T. open T \ x \ T \ T \ S)" using openI by auto -subsubsection\<^marker>\tag unimportant\ \Archimedean properties and useful consequences\ - -text\Bernoulli's inequality\ -proposition Bernoulli_inequality: - fixes x :: real - assumes "-1 \ x" - shows "1 + n * x \ (1 + x) ^ n" -proof (induct n) - case 0 - then show ?case by simp -next - case (Suc n) - have "1 + Suc n * x \ 1 + (Suc n)*x + n * x^2" - by (simp add: algebra_simps) - also have "... = (1 + x) * (1 + n*x)" - by (auto simp: power2_eq_square algebra_simps of_nat_Suc) - also have "... \ (1 + x) ^ Suc n" - using Suc.hyps assms mult_left_mono by fastforce - finally show ?case . -qed - -corollary Bernoulli_inequality_even: - fixes x :: real - assumes "even n" - shows "1 + n * x \ (1 + x) ^ n" -proof (cases "-1 \ x \ n=0") - case True - then show ?thesis - by (auto simp: Bernoulli_inequality) -next - case False - then have "real n \ 1" - by simp - with False have "n * x \ -1" - by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one) - then have "1 + n * x \ 0" - by auto - also have "... \ (1 + x) ^ n" - using assms - using zero_le_even_power by blast - finally show ?thesis . -qed - -corollary real_arch_pow: - fixes x :: real - assumes x: "1 < x" - shows "\n. y < x^n" -proof - - from x have x0: "x - 1 > 0" - by arith - from reals_Archimedean3[OF x0, rule_format, of y] - obtain n :: nat where n: "y < real n * (x - 1)" by metis - from x0 have x00: "x- 1 \ -1" by arith - from Bernoulli_inequality[OF x00, of n] n - have "y < x^n" by auto - then show ?thesis by metis -qed - -corollary real_arch_pow_inv: - fixes x y :: real - assumes y: "y > 0" - and x1: "x < 1" - shows "\n. x^n < y" -proof (cases "x > 0") - case True - with x1 have ix: "1 < 1/x" by (simp add: field_simps) - from real_arch_pow[OF ix, of "1/y"] - obtain n where n: "1/y < (1/x)^n" by blast - then show ?thesis using y \x > 0\ - by (auto simp add: field_simps) -next - case False - with y x1 show ?thesis - by (metis less_le_trans not_less power_one_right) -qed - -lemma forall_pos_mono: - "(\d e::real. d < e \ P d \ P e) \ - (\n::nat. n \ 0 \ P (inverse (real n))) \ (\e. 0 < e \ P e)" - by (metis real_arch_inverse) - -lemma forall_pos_mono_1: - "(\d e::real. d < e \ P d \ P e) \ - (\n. P (inverse (real (Suc n)))) \ 0 < e \ P e" - apply (rule forall_pos_mono) - apply auto - apply (metis Suc_pred of_nat_Suc) - done - subsubsection\<^marker>\tag unimportant\ \Affine transformations of intervals\ lemma real_affinity_le: "0 < m \ m * x + c \ y \ x \ inverse m * y + - (c / m)" for m :: "'a::linordered_field" by (simp add: field_simps) lemma real_le_affinity: "0 < m \ y \ m * x + c \ inverse m * y + - (c / m) \ x" for m :: "'a::linordered_field" by (simp add: field_simps) lemma real_affinity_lt: "0 < m \ m * x + c < y \ x < inverse m * y + - (c / m)" for m :: "'a::linordered_field" by (simp add: field_simps) lemma real_lt_affinity: "0 < m \ y < m * x + c \ inverse m * y + - (c / m) < x" for m :: "'a::linordered_field" by (simp add: field_simps) lemma real_affinity_eq: "m \ 0 \ m * x + c = y \ x = inverse m * y + - (c / m)" for m :: "'a::linordered_field" by (simp add: field_simps) lemma real_eq_affinity: "m \ 0 \ y = m * x + c \ inverse m * y + - (c / m) = x" for m :: "'a::linordered_field" by (simp add: field_simps) subsection \Topological Basis\ context topological_space begin definition\<^marker>\tag important\ "topological_basis B \ (\b\B. open b) \ (\x. open x \ (\B'. B' \ B \ \B' = x))" lemma topological_basis: "topological_basis B \ (\x. open x \ (\B'. B' \ B \ \B' = x))" unfolding topological_basis_def apply safe apply fastforce apply fastforce apply (erule_tac x=x in allE, simp) apply (rule_tac x="{x}" in exI, auto) done lemma topological_basis_iff: assumes "\B'. B' \ B \ open B'" shows "topological_basis B \ (\O'. open O' \ (\x\O'. \B'\B. x \ B' \ B' \ O'))" (is "_ \ ?rhs") proof safe fix O' and x::'a assume H: "topological_basis B" "open O'" "x \ O'" then have "(\B'\B. \B' = O')" by (simp add: topological_basis_def) then obtain B' where "B' \ B" "O' = \B'" by auto then show "\B'\B. x \ B' \ B' \ O'" using H by auto next assume H: ?rhs show "topological_basis B" using assms unfolding topological_basis_def proof safe fix O' :: "'a set" assume "open O'" with H obtain f where "\x\O'. f x \ B \ x \ f x \ f x \ O'" by (force intro: bchoice simp: Bex_def) then show "\B'\B. \B' = O'" by (auto intro: exI[where x="{f x |x. x \ O'}"]) qed qed lemma topological_basisI: assumes "\B'. B' \ B \ open B'" and "\O' x. open O' \ x \ O' \ \B'\B. x \ B' \ B' \ O'" shows "topological_basis B" using assms by (subst topological_basis_iff) auto lemma topological_basisE: fixes O' assumes "topological_basis B" and "open O'" and "x \ O'" obtains B' where "B' \ B" "x \ B'" "B' \ O'" proof atomize_elim from assms have "\B'. B'\B \ open B'" by (simp add: topological_basis_def) with topological_basis_iff assms show "\B'. B' \ B \ x \ B' \ B' \ O'" using assms by (simp add: Bex_def) qed lemma topological_basis_open: assumes "topological_basis B" and "X \ B" shows "open X" using assms by (simp add: topological_basis_def) lemma topological_basis_imp_subbasis: assumes B: "topological_basis B" shows "open = generate_topology B" proof (intro ext iffI) fix S :: "'a set" assume "open S" with B obtain B' where "B' \ B" "S = \B'" unfolding topological_basis_def by blast then show "generate_topology B S" by (auto intro: generate_topology.intros dest: topological_basis_open) next fix S :: "'a set" assume "generate_topology B S" then show "open S" by induct (auto dest: topological_basis_open[OF B]) qed lemma basis_dense: fixes B :: "'a set set" and f :: "'a set \ 'a" assumes "topological_basis B" and choosefrom_basis: "\B'. B' \ {} \ f B' \ B'" shows "\X. open X \ X \ {} \ (\B' \ B. f B' \ X)" proof (intro allI impI) fix X :: "'a set" assume "open X" and "X \ {}" from topological_basisE[OF \topological_basis B\ \open X\ choosefrom_basis[OF \X \ {}\]] obtain B' where "B' \ B" "f X \ B'" "B' \ X" . then show "\B'\B. f B' \ X" by (auto intro!: choosefrom_basis) qed end lemma topological_basis_prod: assumes A: "topological_basis A" and B: "topological_basis B" shows "topological_basis ((\(a, b). a \ b) ` (A \ B))" unfolding topological_basis_def proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric]) fix S :: "('a \ 'b) set" assume "open S" then show "\X\A \ B. (\(a,b)\X. a \ b) = S" proof (safe intro!: exI[of _ "{x\A \ B. fst x \ snd x \ S}"]) fix x y assume "(x, y) \ S" from open_prod_elim[OF \open S\ this] obtain a b where a: "open a""x \ a" and b: "open b" "y \ b" and "a \ b \ S" by (metis mem_Sigma_iff) moreover from A a obtain A0 where "A0 \ A" "x \ A0" "A0 \ a" by (rule topological_basisE) moreover from B b obtain B0 where "B0 \ B" "y \ B0" "B0 \ b" by (rule topological_basisE) ultimately show "(x, y) \ (\(a, b)\{X \ A \ B. fst X \ snd X \ S}. a \ b)" by (intro UN_I[of "(A0, B0)"]) auto qed auto qed (metis A B topological_basis_open open_Times) subsection \Countable Basis\ locale\<^marker>\tag important\ countable_basis = topological_space p for p::"'a set \ bool" + fixes B :: "'a set set" assumes is_basis: "topological_basis B" and countable_basis: "countable B" begin lemma open_countable_basis_ex: assumes "p X" shows "\B' \ B. X = \B'" using assms countable_basis is_basis unfolding topological_basis_def by blast lemma open_countable_basisE: assumes "p X" obtains B' where "B' \ B" "X = \B'" using assms open_countable_basis_ex by atomize_elim simp lemma countable_dense_exists: "\D::'a set. countable D \ (\X. p X \ X \ {} \ (\d \ D. d \ X))" proof - let ?f = "(\B'. SOME x. x \ B')" have "countable (?f ` B)" using countable_basis by simp with basis_dense[OF is_basis, of ?f] show ?thesis by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI) qed lemma countable_dense_setE: obtains D :: "'a set" where "countable D" "\X. p X \ X \ {} \ \d \ D. d \ X" using countable_dense_exists by blast end lemma countable_basis_openI: "countable_basis open B" if "countable B" "topological_basis B" using that by unfold_locales (simp_all add: topological_basis topological_space.topological_basis topological_space_axioms) lemma (in first_countable_topology) first_countable_basisE: fixes x :: 'a obtains \ where "countable \" "\A. A \ \ \ x \ A" "\A. A \ \ \ open A" "\S. open S \ x \ S \ (\A\\. A \ S)" proof - obtain \ where \: "(\i::nat. x \ \ i \ open (\ i))" "(\S. open S \ x \ S \ (\i. \ i \ S))" using first_countable_basis[of x] by metis show thesis proof show "countable (range \)" by simp qed (use \ in auto) qed lemma (in first_countable_topology) first_countable_basis_Int_stableE: obtains \ where "countable \" "\A. A \ \ \ x \ A" "\A. A \ \ \ open A" "\S. open S \ x \ S \ (\A\\. A \ S)" "\A B. A \ \ \ B \ \ \ A \ B \ \" proof atomize_elim obtain \ where \: "countable \" "\B. B \ \ \ x \ B" "\B. B \ \ \ open B" "\S. open S \ x \ S \ \B\\. B \ S" by (rule first_countable_basisE) blast define \ where [abs_def]: "\ = (\N. \((\n. from_nat_into \ n) ` N)) ` (Collect finite::nat set set)" then show "\\. countable \ \ (\A. A \ \ \ x \ A) \ (\A. A \ \ \ open A) \ (\S. open S \ x \ S \ (\A\\. A \ S)) \ (\A B. A \ \ \ B \ \ \ A \ B \ \)" proof (safe intro!: exI[where x=\]) show "countable \" unfolding \_def by (intro countable_image countable_Collect_finite) fix A assume "A \ \" then show "x \ A" "open A" using \(4)[OF open_UNIV] by (auto simp: \_def intro: \ from_nat_into) next let ?int = "\N. \(from_nat_into \ ` N)" fix A B assume "A \ \" "B \ \" then obtain N M where "A = ?int N" "B = ?int M" "finite (N \ M)" by (auto simp: \_def) then show "A \ B \ \" by (auto simp: \_def intro!: image_eqI[where x="N \ M"]) next fix S assume "open S" "x \ S" then obtain a where a: "a\\" "a \ S" using \ by blast then show "\a\\. a \ S" using a \ by (intro bexI[where x=a]) (auto simp: \_def intro: image_eqI[where x="{to_nat_on \ a}"]) qed qed lemma (in topological_space) first_countableI: assumes "countable \" and 1: "\A. A \ \ \ x \ A" "\A. A \ \ \ open A" and 2: "\S. open S \ x \ S \ \A\\. A \ S" shows "\\::nat \ 'a set. (\i. x \ \ i \ open (\ i)) \ (\S. open S \ x \ S \ (\i. \ i \ S))" proof (safe intro!: exI[of _ "from_nat_into \"]) fix i have "\ \ {}" using 2[of UNIV] by auto show "x \ from_nat_into \ i" "open (from_nat_into \ i)" using range_from_nat_into_subset[OF \\ \ {}\] 1 by auto next fix S assume "open S" "x\S" from 2[OF this] show "\i. from_nat_into \ i \ S" using subset_range_from_nat_into[OF \countable \\] by auto qed instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology proof fix x :: "'a \ 'b" obtain \ where \: "countable \" "\a. a \ \ \ fst x \ a" "\a. a \ \ \ open a" "\S. open S \ fst x \ S \ \a\\. a \ S" by (rule first_countable_basisE[of "fst x"]) blast obtain B where B: "countable B" "\a. a \ B \ snd x \ a" "\a. a \ B \ open a" "\S. open S \ snd x \ S \ \a\B. a \ S" by (rule first_countable_basisE[of "snd x"]) blast show "\\::nat \ ('a \ 'b) set. (\i. x \ \ i \ open (\ i)) \ (\S. open S \ x \ S \ (\i. \ i \ S))" proof (rule first_countableI[of "(\(a, b). a \ b) ` (\ \ B)"], safe) fix a b assume x: "a \ \" "b \ B" show "x \ a \ b" by (simp add: \(2) B(2) mem_Times_iff x) show "open (a \ b)" by (simp add: \(3) B(3) open_Times x) next fix S assume "open S" "x \ S" then obtain a' b' where a'b': "open a'" "open b'" "x \ a' \ b'" "a' \ b' \ S" by (rule open_prod_elim) moreover from a'b' \(4)[of a'] B(4)[of b'] obtain a b where "a \ \" "a \ a'" "b \ B" "b \ b'" by auto ultimately show "\a\(\(a, b). a \ b) ` (\ \ B). a \ S" by (auto intro!: bexI[of _ "a \ b"] bexI[of _ a] bexI[of _ b]) qed (simp add: \ B) qed class second_countable_topology = topological_space + assumes ex_countable_subbasis: "\B::'a set set. countable B \ open = generate_topology B" begin lemma ex_countable_basis: "\B::'a set set. countable B \ topological_basis B" proof - from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B" by blast let ?B = "Inter ` {b. finite b \ b \ B }" show ?thesis proof (intro exI conjI) show "countable ?B" by (intro countable_image countable_Collect_finite_subset B) { fix S assume "open S" then have "\B'\{b. finite b \ b \ B}. (\b\B'. \b) = S" unfolding B proof induct case UNIV show ?case by (intro exI[of _ "{{}}"]) simp next case (Int a b) then obtain x y where x: "a = \(Inter ` x)" "\i. i \ x \ finite i \ i \ B" and y: "b = \(Inter ` y)" "\i. i \ y \ finite i \ i \ B" by blast show ?case unfolding x y Int_UN_distrib2 by (intro exI[of _ "{i \ j| i j. i \ x \ j \ y}"]) (auto dest: x(2) y(2)) next case (UN K) then have "\k\K. \B'\{b. finite b \ b \ B}. \ (Inter ` B') = k" by auto then obtain k where "\ka\K. k ka \ {b. finite b \ b \ B} \ \(Inter ` (k ka)) = ka" unfolding bchoice_iff .. then show "\B'\{b. finite b \ b \ B}. \ (Inter ` B') = \K" by (intro exI[of _ "\(k ` K)"]) auto next case (Basis S) then show ?case by (intro exI[of _ "{{S}}"]) auto qed then have "(\B'\Inter ` {b. finite b \ b \ B}. \B' = S)" unfolding subset_image_iff by blast } then show "topological_basis ?B" unfolding topological_basis_def by (safe intro!: open_Inter) (simp_all add: B generate_topology.Basis subset_eq) qed qed end lemma univ_second_countable: obtains \ :: "'a::second_countable_topology set set" where "countable \" "\C. C \ \ \ open C" "\S. open S \ \U. U \ \ \ S = \U" by (metis ex_countable_basis topological_basis_def) proposition Lindelof: fixes \ :: "'a::second_countable_topology set set" assumes \: "\S. S \ \ \ open S" obtains \' where "\' \ \" "countable \'" "\\' = \\" proof - obtain \ :: "'a set set" where "countable \" "\C. C \ \ \ open C" and \: "\S. open S \ \U. U \ \ \ S = \U" using univ_second_countable by blast define \ where "\ \ {S. S \ \ \ (\U. U \ \ \ S \ U)}" have "countable \" apply (rule countable_subset [OF _ \countable \\]) apply (force simp: \_def) done have "\S. \U. S \ \ \ U \ \ \ S \ U" by (simp add: \_def) then obtain G where G: "\S. S \ \ \ G S \ \ \ S \ G S" by metis have "\\ \ \\" unfolding \_def by (blast dest: \ \) moreover have "\\ \ \\" using \_def by blast ultimately have eq1: "\\ = \\" .. have eq2: "\\ = \ (G ` \)" using G eq1 by auto show ?thesis apply (rule_tac \' = "G ` \" in that) using G \countable \\ by (auto simp: eq1 eq2) qed lemma countable_disjoint_open_subsets: fixes \ :: "'a::second_countable_topology set set" assumes "\S. S \ \ \ open S" and pw: "pairwise disjnt \" shows "countable \" proof - obtain \' where "\' \ \" "countable \'" "\\' = \\" by (meson assms Lindelof) with pw have "\ \ insert {} \'" by (fastforce simp add: pairwise_def disjnt_iff) then show ?thesis by (simp add: \countable \'\ countable_subset) qed sublocale second_countable_topology < countable_basis "open" "SOME B. countable B \ topological_basis B" using someI_ex[OF ex_countable_basis] by unfold_locales safe instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology proof obtain A :: "'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto moreover obtain B :: "'b set set" where "countable B" "topological_basis B" using ex_countable_basis by auto ultimately show "\B::('a \ 'b) set set. countable B \ open = generate_topology B" by (auto intro!: exI[of _ "(\(a, b). a \ b) ` (A \ B)"] topological_basis_prod topological_basis_imp_subbasis) qed instance second_countable_topology \ first_countable_topology proof fix x :: 'a define B :: "'a set set" where "B = (SOME B. countable B \ topological_basis B)" then have B: "countable B" "topological_basis B" using countable_basis is_basis by (auto simp: countable_basis is_basis) then show "\A::nat \ 'a set. (\i. x \ A i \ open (A i)) \ (\S. open S \ x \ S \ (\i. A i \ S))" by (intro first_countableI[of "{b\B. x \ b}"]) (fastforce simp: topological_space_class.topological_basis_def)+ qed instance nat :: second_countable_topology proof show "\B::nat set set. countable B \ open = generate_topology B" by (intro exI[of _ "range lessThan \ range greaterThan"]) (auto simp: open_nat_def) qed lemma countable_separating_set_linorder1: shows "\B::('a::{linorder_topology, second_countable_topology} set). countable B \ (\x y. x < y \ (\b \ B. x < b \ b \ y))" proof - obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto define B1 where "B1 = {(LEAST x. x \ U)| U. U \ A}" then have "countable B1" using \countable A\ by (simp add: Setcompr_eq_image) define B2 where "B2 = {(SOME x. x \ U)| U. U \ A}" then have "countable B2" using \countable A\ by (simp add: Setcompr_eq_image) have "\b \ B1 \ B2. x < b \ b \ y" if "x < y" for x y proof (cases) assume "\z. x < z \ z < y" then obtain z where z: "x < z \ z < y" by auto define U where "U = {x<.. U" using z U_def by simp ultimately obtain V where "V \ A" "z \ V" "V \ U" using topological_basisE[OF \topological_basis A\] by auto define w where "w = (SOME x. x \ V)" then have "w \ V" using \z \ V\ by (metis someI2) then have "x < w \ w \ y" using \w \ V\ \V \ U\ U_def by fastforce moreover have "w \ B1 \ B2" using w_def B2_def \V \ A\ by auto ultimately show ?thesis by auto next assume "\(\z. x < z \ z < y)" then have *: "\z. z > x \ z \ y" by auto define U where "U = {x<..}" then have "open U" by simp moreover have "y \ U" using \x < y\ U_def by simp ultimately obtain "V" where "V \ A" "y \ V" "V \ U" using topological_basisE[OF \topological_basis A\] by auto have "U = {y..}" unfolding U_def using * \x < y\ by auto then have "V \ {y..}" using \V \ U\ by simp then have "(LEAST w. w \ V) = y" using \y \ V\ by (meson Least_equality atLeast_iff subsetCE) then have "y \ B1 \ B2" using \V \ A\ B1_def by auto moreover have "x < y \ y \ y" using \x < y\ by simp ultimately show ?thesis by auto qed moreover have "countable (B1 \ B2)" using \countable B1\ \countable B2\ by simp ultimately show ?thesis by auto qed lemma countable_separating_set_linorder2: shows "\B::('a::{linorder_topology, second_countable_topology} set). countable B \ (\x y. x < y \ (\b \ B. x \ b \ b < y))" proof - obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto define B1 where "B1 = {(GREATEST x. x \ U) | U. U \ A}" then have "countable B1" using \countable A\ by (simp add: Setcompr_eq_image) define B2 where "B2 = {(SOME x. x \ U)| U. U \ A}" then have "countable B2" using \countable A\ by (simp add: Setcompr_eq_image) have "\b \ B1 \ B2. x \ b \ b < y" if "x < y" for x y proof (cases) assume "\z. x < z \ z < y" then obtain z where z: "x < z \ z < y" by auto define U where "U = {x<.. U" using z U_def by simp ultimately obtain "V" where "V \ A" "z \ V" "V \ U" using topological_basisE[OF \topological_basis A\] by auto define w where "w = (SOME x. x \ V)" then have "w \ V" using \z \ V\ by (metis someI2) then have "x \ w \ w < y" using \w \ V\ \V \ U\ U_def by fastforce moreover have "w \ B1 \ B2" using w_def B2_def \V \ A\ by auto ultimately show ?thesis by auto next assume "\(\z. x < z \ z < y)" then have *: "\z. z < y \ z \ x" using leI by blast define U where "U = {.. U" using \x < y\ U_def by simp ultimately obtain "V" where "V \ A" "x \ V" "V \ U" using topological_basisE[OF \topological_basis A\] by auto have "U = {..x}" unfolding U_def using * \x < y\ by auto then have "V \ {..x}" using \V \ U\ by simp then have "(GREATEST x. x \ V) = x" using \x \ V\ by (meson Greatest_equality atMost_iff subsetCE) then have "x \ B1 \ B2" using \V \ A\ B1_def by auto moreover have "x \ x \ x < y" using \x < y\ by simp ultimately show ?thesis by auto qed moreover have "countable (B1 \ B2)" using \countable B1\ \countable B2\ by simp ultimately show ?thesis by auto qed lemma countable_separating_set_dense_linorder: shows "\B::('a::{linorder_topology, dense_linorder, second_countable_topology} set). countable B \ (\x y. x < y \ (\b \ B. x < b \ b < y))" proof - obtain B::"'a set" where B: "countable B" "\x y. x < y \ (\b \ B. x < b \ b \ y)" using countable_separating_set_linorder1 by auto have "\b \ B. x < b \ b < y" if "x < y" for x y proof - obtain z where "x < z" "z < y" using \x < y\ dense by blast then obtain b where "b \ B" "x < b \ b \ z" using B(2) by auto then have "x < b \ b < y" using \z < y\ by auto then show ?thesis using \b \ B\ by auto qed then show ?thesis using B(1) by auto qed subsection \Polish spaces\ text \Textbooks define Polish spaces as completely metrizable. We assume the topology to be complete for a given metric.\ class polish_space = complete_space + second_countable_topology subsection \Limit Points\ definition\<^marker>\tag important\ (in topological_space) islimpt:: "'a \ 'a set \ bool" (infixr "islimpt" 60) where "x islimpt S \ (\T. x\T \ open T \ (\y\S. y\T \ y\x))" lemma islimptI: assumes "\T. x \ T \ open T \ \y\S. y \ T \ y \ x" shows "x islimpt S" using assms unfolding islimpt_def by auto lemma islimptE: assumes "x islimpt S" and "x \ T" and "open T" obtains y where "y \ S" and "y \ T" and "y \ x" using assms unfolding islimpt_def by auto lemma islimpt_iff_eventually: "x islimpt S \ \ eventually (\y. y \ S) (at x)" unfolding islimpt_def eventually_at_topological by auto lemma islimpt_subset: "x islimpt S \ S \ T \ x islimpt T" unfolding islimpt_def by fast lemma islimpt_UNIV_iff: "x islimpt UNIV \ \ open {x}" unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast) lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})" unfolding islimpt_def by blast text \A perfect space has no isolated points.\ lemma islimpt_UNIV [simp, intro]: "x islimpt UNIV" for x :: "'a::perfect_space" unfolding islimpt_UNIV_iff by (rule not_open_singleton) lemma closed_limpt: "closed S \ (\x. x islimpt S \ x \ S)" unfolding closed_def apply (subst open_subopen) apply (simp add: islimpt_def subset_eq) apply (metis ComplE ComplI) done lemma islimpt_EMPTY[simp]: "\ x islimpt {}" by (auto simp: islimpt_def) lemma islimpt_Un: "x islimpt (S \ T) \ x islimpt S \ x islimpt T" by (simp add: islimpt_iff_eventually eventually_conj_iff) lemma islimpt_insert: fixes x :: "'a::t1_space" shows "x islimpt (insert a s) \ x islimpt s" proof assume *: "x islimpt (insert a s)" show "x islimpt s" proof (rule islimptI) fix t assume t: "x \ t" "open t" show "\y\s. y \ t \ y \ x" proof (cases "x = a") case True obtain y where "y \ insert a s" "y \ t" "y \ x" using * t by (rule islimptE) with \x = a\ show ?thesis by auto next case False with t have t': "x \ t - {a}" "open (t - {a})" by (simp_all add: open_Diff) obtain y where "y \ insert a s" "y \ t - {a}" "y \ x" using * t' by (rule islimptE) then show ?thesis by auto qed qed next assume "x islimpt s" then show "x islimpt (insert a s)" by (rule islimpt_subset) auto qed lemma islimpt_finite: fixes x :: "'a::t1_space" shows "finite s \ \ x islimpt s" by (induct set: finite) (simp_all add: islimpt_insert) lemma islimpt_Un_finite: fixes x :: "'a::t1_space" shows "finite s \ x islimpt (s \ t) \ x islimpt t" by (simp add: islimpt_Un islimpt_finite) lemma islimpt_eq_acc_point: fixes l :: "'a :: t1_space" shows "l islimpt S \ (\U. l\U \ open U \ infinite (U \ S))" proof (safe intro!: islimptI) fix U assume "l islimpt S" "l \ U" "open U" "finite (U \ S)" then have "l islimpt S" "l \ (U - (U \ S - {l}))" "open (U - (U \ S - {l}))" by (auto intro: finite_imp_closed) then show False by (rule islimptE) auto next fix T assume *: "\U. l\U \ open U \ infinite (U \ S)" "l \ T" "open T" then have "infinite (T \ S - {l})" by auto then have "\x. x \ (T \ S - {l})" unfolding ex_in_conv by (intro notI) simp then show "\y\S. y \ T \ y \ l" by auto qed lemma acc_point_range_imp_convergent_subsequence: fixes l :: "'a :: first_countable_topology" assumes l: "\U. l\U \ open U \ infinite (U \ range f)" shows "\r::nat\nat. strict_mono r \ (f \ r) \ l" proof - from countable_basis_at_decseq[of l] obtain A where A: "\i. open (A i)" "\i. l \ A i" "\S. open S \ l \ S \ eventually (\i. A i \ S) sequentially" by blast define s where "s n i = (SOME j. i < j \ f j \ A (Suc n))" for n i { fix n i have "infinite (A (Suc n) \ range f - f`{.. i})" using l A by auto then have "\x. x \ A (Suc n) \ range f - f`{.. i}" unfolding ex_in_conv by (intro notI) simp then have "\j. f j \ A (Suc n) \ j \ {.. i}" by auto then have "\a. i < a \ f a \ A (Suc n)" by (auto simp: not_le) then have "i < s n i" "f (s n i) \ A (Suc n)" unfolding s_def by (auto intro: someI2_ex) } note s = this define r where "r = rec_nat (s 0 0) s" have "strict_mono r" by (auto simp: r_def s strict_mono_Suc_iff) moreover have "(\n. f (r n)) \ l" proof (rule topological_tendstoI) fix S assume "open S" "l \ S" with A(3) have "eventually (\i. A i \ S) sequentially" by auto moreover { fix i assume "Suc 0 \ i" then have "f (r i) \ A i" by (cases i) (simp_all add: r_def s) } then have "eventually (\i. f (r i) \ A i) sequentially" by (auto simp: eventually_sequentially) ultimately show "eventually (\i. f (r i) \ S) sequentially" by eventually_elim auto qed ultimately show "\r::nat\nat. strict_mono r \ (f \ r) \ l" by (auto simp: convergent_def comp_def) qed lemma islimpt_range_imp_convergent_subsequence: fixes l :: "'a :: {t1_space, first_countable_topology}" assumes l: "l islimpt (range f)" shows "\r::nat\nat. strict_mono r \ (f \ r) \ l" using l unfolding islimpt_eq_acc_point by (rule acc_point_range_imp_convergent_subsequence) lemma sequence_unique_limpt: fixes f :: "nat \ 'a::t2_space" assumes "(f \ l) sequentially" and "l' islimpt (range f)" shows "l' = l" proof (rule ccontr) assume "l' \ l" obtain s t where "open s" "open t" "l' \ s" "l \ t" "s \ t = {}" using hausdorff [OF \l' \ l\] by auto have "eventually (\n. f n \ t) sequentially" using assms(1) \open t\ \l \ t\ by (rule topological_tendstoD) then obtain N where "\n\N. f n \ t" unfolding eventually_sequentially by auto have "UNIV = {.. {N..}" by auto then have "l' islimpt (f ` ({.. {N..}))" using assms(2) by simp then have "l' islimpt (f ` {.. f ` {N..})" by (simp add: image_Un) then have "l' islimpt (f ` {N..})" by (simp add: islimpt_Un_finite) then obtain y where "y \ f ` {N..}" "y \ s" "y \ l'" using \l' \ s\ \open s\ by (rule islimptE) then obtain n where "N \ n" "f n \ s" "f n \ l'" by auto with \\n\N. f n \ t\ have "f n \ s \ t" by simp with \s \ t = {}\ show False by simp qed subsection \Interior of a Set\ definition\<^marker>\tag important\ interior :: "('a::topological_space) set \ 'a set" where "interior S = \{T. open T \ T \ S}" lemma interiorI [intro?]: assumes "open T" and "x \ T" and "T \ S" shows "x \ interior S" using assms unfolding interior_def by fast lemma interiorE [elim?]: assumes "x \ interior S" obtains T where "open T" and "x \ T" and "T \ S" using assms unfolding interior_def by fast lemma open_interior [simp, intro]: "open (interior S)" by (simp add: interior_def open_Union) lemma interior_subset: "interior S \ S" by (auto simp: interior_def) lemma interior_maximal: "T \ S \ open T \ T \ interior S" by (auto simp: interior_def) lemma interior_open: "open S \ interior S = S" by (intro equalityI interior_subset interior_maximal subset_refl) lemma interior_eq: "interior S = S \ open S" by (metis open_interior interior_open) lemma open_subset_interior: "open S \ S \ interior T \ S \ T" by (metis interior_maximal interior_subset subset_trans) lemma interior_empty [simp]: "interior {} = {}" using open_empty by (rule interior_open) lemma interior_UNIV [simp]: "interior UNIV = UNIV" using open_UNIV by (rule interior_open) lemma interior_interior [simp]: "interior (interior S) = interior S" using open_interior by (rule interior_open) lemma interior_mono: "S \ T \ interior S \ interior T" by (auto simp: interior_def) lemma interior_unique: assumes "T \ S" and "open T" assumes "\T'. T' \ S \ open T' \ T' \ T" shows "interior S = T" by (intro equalityI assms interior_subset open_interior interior_maximal) lemma interior_singleton [simp]: "interior {a} = {}" for a :: "'a::perfect_space" apply (rule interior_unique, simp_all) using not_open_singleton subset_singletonD apply fastforce done lemma interior_Int [simp]: "interior (S \ T) = interior S \ interior T" by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1 Int_lower2 interior_maximal interior_subset open_Int open_interior) lemma eventually_nhds_in_nhd: "x \ interior s \ eventually (\y. y \ s) (nhds x)" using interior_subset[of s] by (subst eventually_nhds) blast lemma interior_limit_point [intro]: fixes x :: "'a::perfect_space" assumes x: "x \ interior S" shows "x islimpt S" using x islimpt_UNIV [of x] unfolding interior_def islimpt_def apply (clarsimp, rename_tac T T') apply (drule_tac x="T \ T'" in spec) apply (auto simp: open_Int) done lemma interior_closed_Un_empty_interior: assumes cS: "closed S" and iT: "interior T = {}" shows "interior (S \ T) = interior S" proof show "interior S \ interior (S \ T)" by (rule interior_mono) (rule Un_upper1) show "interior (S \ T) \ interior S" proof fix x assume "x \ interior (S \ T)" then obtain R where "open R" "x \ R" "R \ S \ T" .. show "x \ interior S" proof (rule ccontr) assume "x \ interior S" with \x \ R\ \open R\ obtain y where "y \ R - S" unfolding interior_def by fast from \open R\ \closed S\ have "open (R - S)" by (rule open_Diff) from \R \ S \ T\ have "R - S \ T" by fast from \y \ R - S\ \open (R - S)\ \R - S \ T\ \interior T = {}\ show False unfolding interior_def by fast qed qed qed lemma interior_Times: "interior (A \ B) = interior A \ interior B" proof (rule interior_unique) show "interior A \ interior B \ A \ B" by (intro Sigma_mono interior_subset) show "open (interior A \ interior B)" by (intro open_Times open_interior) fix T assume "T \ A \ B" and "open T" then show "T \ interior A \ interior B" proof safe fix x y assume "(x, y) \ T" then obtain C D where "open C" "open D" "C \ D \ T" "x \ C" "y \ D" using \open T\ unfolding open_prod_def by fast then have "open C" "open D" "C \ A" "D \ B" "x \ C" "y \ D" using \T \ A \ B\ by auto then show "x \ interior A" and "y \ interior B" by (auto intro: interiorI) qed qed lemma interior_Ici: fixes x :: "'a :: {dense_linorder,linorder_topology}" assumes "b < x" shows "interior {x ..} = {x <..}" proof (rule interior_unique) fix T assume "T \ {x ..}" "open T" moreover have "x \ T" proof assume "x \ T" obtain y where "y < x" "{y <.. x} \ T" using open_left[OF \open T\ \x \ T\ \b < x\] by auto with dense[OF \y < x\] obtain z where "z \ T" "z < x" by (auto simp: subset_eq Ball_def) with \T \ {x ..}\ show False by auto qed ultimately show "T \ {x <..}" by (auto simp: subset_eq less_le) qed auto lemma interior_Iic: fixes x :: "'a ::{dense_linorder,linorder_topology}" assumes "x < b" shows "interior {.. x} = {..< x}" proof (rule interior_unique) fix T assume "T \ {.. x}" "open T" moreover have "x \ T" proof assume "x \ T" obtain y where "x < y" "{x ..< y} \ T" using open_right[OF \open T\ \x \ T\ \x < b\] by auto with dense[OF \x < y\] obtain z where "z \ T" "x < z" by (auto simp: subset_eq Ball_def less_le) with \T \ {.. x}\ show False by auto qed ultimately show "T \ {..< x}" by (auto simp: subset_eq less_le) qed auto lemma countable_disjoint_nonempty_interior_subsets: fixes \ :: "'a::second_countable_topology set set" assumes pw: "pairwise disjnt \" and int: "\S. \S \ \; interior S = {}\ \ S = {}" shows "countable \" proof (rule countable_image_inj_on) have "disjoint (interior ` \)" using pw by (simp add: disjoint_image_subset interior_subset) then show "countable (interior ` \)" by (auto intro: countable_disjoint_open_subsets) show "inj_on interior \" using pw apply (clarsimp simp: inj_on_def pairwise_def) apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset) done qed subsection \Closure of a Set\ definition\<^marker>\tag important\ closure :: "('a::topological_space) set \ 'a set" where "closure S = S \ {x . x islimpt S}" lemma interior_closure: "interior S = - (closure (- S))" by (auto simp: interior_def closure_def islimpt_def) lemma closure_interior: "closure S = - interior (- S)" by (simp add: interior_closure) lemma closed_closure[simp, intro]: "closed (closure S)" by (simp add: closure_interior closed_Compl) lemma closure_subset: "S \ closure S" by (simp add: closure_def) lemma closure_hull: "closure S = closed hull S" by (auto simp: hull_def closure_interior interior_def) lemma closure_eq: "closure S = S \ closed S" unfolding closure_hull using closed_Inter by (rule hull_eq) lemma closure_closed [simp]: "closed S \ closure S = S" by (simp only: closure_eq) lemma closure_closure [simp]: "closure (closure S) = closure S" unfolding closure_hull by (rule hull_hull) lemma closure_mono: "S \ T \ closure S \ closure T" unfolding closure_hull by (rule hull_mono) lemma closure_minimal: "S \ T \ closed T \ closure S \ T" unfolding closure_hull by (rule hull_minimal) lemma closure_unique: assumes "S \ T" and "closed T" and "\T'. S \ T' \ closed T' \ T \ T'" shows "closure S = T" using assms unfolding closure_hull by (rule hull_unique) lemma closure_empty [simp]: "closure {} = {}" using closed_empty by (rule closure_closed) lemma closure_UNIV [simp]: "closure UNIV = UNIV" using closed_UNIV by (rule closure_closed) lemma closure_Un [simp]: "closure (S \ T) = closure S \ closure T" by (simp add: closure_interior) lemma closure_eq_empty [iff]: "closure S = {} \ S = {}" using closure_empty closure_subset[of S] by blast lemma closure_subset_eq: "closure S \ S \ closed S" using closure_eq[of S] closure_subset[of S] by simp lemma open_Int_closure_eq_empty: "open S \ (S \ closure T) = {} \ S \ T = {}" using open_subset_interior[of S "- T"] using interior_subset[of "- T"] by (auto simp: closure_interior) lemma open_Int_closure_subset: "open S \ S \ closure T \ closure (S \ T)" proof fix x assume *: "open S" "x \ S \ closure T" have "x islimpt (S \ T)" if **: "x islimpt T" proof (rule islimptI) fix A assume "x \ A" "open A" with * have "x \ A \ S" "open (A \ S)" by (simp_all add: open_Int) with ** obtain y where "y \ T" "y \ A \ S" "y \ x" by (rule islimptE) then have "y \ S \ T" "y \ A \ y \ x" by simp_all then show "\y\(S \ T). y \ A \ y \ x" .. qed with * show "x \ closure (S \ T)" unfolding closure_def by blast qed lemma closure_complement: "closure (- S) = - interior S" by (simp add: closure_interior) lemma interior_complement: "interior (- S) = - closure S" by (simp add: closure_interior) lemma interior_diff: "interior(S - T) = interior S - closure T" by (simp add: Diff_eq interior_complement) lemma closure_Times: "closure (A \ B) = closure A \ closure B" proof (rule closure_unique) show "A \ B \ closure A \ closure B" by (intro Sigma_mono closure_subset) show "closed (closure A \ closure B)" by (intro closed_Times closed_closure) fix T assume "A \ B \ T" and "closed T" then show "closure A \ closure B \ T" apply (simp add: closed_def open_prod_def, clarify) apply (rule ccontr) apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D) apply (simp add: closure_interior interior_def) apply (drule_tac x=C in spec) apply (drule_tac x=D in spec, auto) done qed lemma islimpt_in_closure: "(x islimpt S) = (x\closure(S-{x}))" unfolding closure_def using islimpt_punctured by blast lemma connected_imp_connected_closure: "connected S \ connected (closure S)" by (rule connectedI) (meson closure_subset open_Int open_Int_closure_eq_empty subset_trans connectedD) lemma bdd_below_closure: fixes A :: "real set" assumes "bdd_below A" shows "bdd_below (closure A)" proof - from assms obtain m where "\x. x \ A \ m \ x" by (auto simp: bdd_below_def) then have "A \ {m..}" by auto then have "closure A \ {m..}" using closed_real_atLeast by (rule closure_minimal) then show ?thesis by (auto simp: bdd_below_def) qed subsection \Frontier (also known as boundary)\ definition\<^marker>\tag important\ frontier :: "('a::topological_space) set \ 'a set" where "frontier S = closure S - interior S" lemma frontier_closed [iff]: "closed (frontier S)" by (simp add: frontier_def closed_Diff) lemma frontier_closures: "frontier S = closure S \ closure (- S)" by (auto simp: frontier_def interior_closure) lemma frontier_Int: "frontier(S \ T) = closure(S \ T) \ (frontier S \ frontier T)" proof - have "closure (S \ T) \ closure S" "closure (S \ T) \ closure T" by (simp_all add: closure_mono) then show ?thesis by (auto simp: frontier_closures) qed lemma frontier_Int_subset: "frontier(S \ T) \ frontier S \ frontier T" by (auto simp: frontier_Int) lemma frontier_Int_closed: assumes "closed S" "closed T" shows "frontier(S \ T) = (frontier S \ T) \ (S \ frontier T)" proof - have "closure (S \ T) = T \ S" using assms by (simp add: Int_commute closed_Int) moreover have "T \ (closure S \ closure (- S)) = frontier S \ T" by (simp add: Int_commute frontier_closures) ultimately show ?thesis by (simp add: Int_Un_distrib Int_assoc Int_left_commute assms frontier_closures) qed lemma frontier_subset_closed: "closed S \ frontier S \ S" by (metis frontier_def closure_closed Diff_subset) lemma frontier_empty [simp]: "frontier {} = {}" by (simp add: frontier_def) lemma frontier_subset_eq: "frontier S \ S \ closed S" proof - { assume "frontier S \ S" then have "closure S \ S" using interior_subset unfolding frontier_def by auto then have "closed S" using closure_subset_eq by auto } then show ?thesis using frontier_subset_closed[of S] .. qed lemma frontier_complement [simp]: "frontier (- S) = frontier S" by (auto simp: frontier_def closure_complement interior_complement) lemma frontier_Un_subset: "frontier(S \ T) \ frontier S \ frontier T" by (metis compl_sup frontier_Int_subset frontier_complement) lemma frontier_disjoint_eq: "frontier S \ S = {} \ open S" using frontier_complement frontier_subset_eq[of "- S"] unfolding open_closed by auto lemma frontier_UNIV [simp]: "frontier UNIV = {}" using frontier_complement frontier_empty by fastforce lemma frontier_interiors: "frontier s = - interior(s) - interior(-s)" by (simp add: Int_commute frontier_def interior_closure) lemma frontier_interior_subset: "frontier(interior S) \ frontier S" by (simp add: Diff_mono frontier_interiors interior_mono interior_subset) lemma closure_Un_frontier: "closure S = S \ frontier S" proof - have "S \ interior S = S" using interior_subset by auto then show ?thesis using closure_subset by (auto simp: frontier_def) qed subsection\<^marker>\tag unimportant\ \Filters and the ``eventually true'' quantifier\ text \Identify Trivial limits, where we can't approach arbitrarily closely.\ lemma trivial_limit_within: "trivial_limit (at a within S) \ \ a islimpt S" proof assume "trivial_limit (at a within S)" then show "\ a islimpt S" unfolding trivial_limit_def unfolding eventually_at_topological unfolding islimpt_def apply (clarsimp simp add: set_eq_iff) apply (rename_tac T, rule_tac x=T in exI) apply (clarsimp, drule_tac x=y in bspec, simp_all) done next assume "\ a islimpt S" then show "trivial_limit (at a within S)" unfolding trivial_limit_def eventually_at_topological islimpt_def by metis qed lemma trivial_limit_at_iff: "trivial_limit (at a) \ \ a islimpt UNIV" using trivial_limit_within [of a UNIV] by simp lemma trivial_limit_at: "\ trivial_limit (at a)" for a :: "'a::perfect_space" by (rule at_neq_bot) lemma not_trivial_limit_within: "\ trivial_limit (at x within S) = (x \ closure (S - {x}))" using islimpt_in_closure by (metis trivial_limit_within) lemma not_in_closure_trivial_limitI: "x \ closure s \ trivial_limit (at x within s)" using not_trivial_limit_within[of x s] by safe (metis Diff_empty Diff_insert0 closure_subset contra_subsetD) lemma filterlim_at_within_closure_implies_filterlim: "filterlim f l (at x within s)" if "x \ closure s \ filterlim f l (at x within s)" by (metis bot.extremum filterlim_filtercomap filterlim_mono not_in_closure_trivial_limitI that) lemma at_within_eq_bot_iff: "at c within A = bot \ c \ closure (A - {c})" using not_trivial_limit_within[of c A] by blast text \Some property holds "sufficiently close" to the limit point.\ lemma trivial_limit_eventually: "trivial_limit net \ eventually P net" by simp lemma trivial_limit_eq: "trivial_limit net \ (\P. eventually P net)" by (simp add: filter_eq_iff) lemma Lim_topological: "(f \ l) net \ trivial_limit net \ (\S. open S \ l \ S \ eventually (\x. f x \ S) net)" unfolding tendsto_def trivial_limit_eq by auto lemma eventually_within_Un: "eventually P (at x within (s \ t)) \ eventually P (at x within s) \ eventually P (at x within t)" unfolding eventually_at_filter by (auto elim!: eventually_rev_mp) lemma Lim_within_union: "(f \ l) (at x within (s \ t)) \ (f \ l) (at x within s) \ (f \ l) (at x within t)" unfolding tendsto_def by (auto simp: eventually_within_Un) subsection \Limits\ text \The expected monotonicity property.\ lemma Lim_Un: assumes "(f \ l) (at x within S)" "(f \ l) (at x within T)" shows "(f \ l) (at x within (S \ T))" using assms unfolding at_within_union by (rule filterlim_sup) lemma Lim_Un_univ: "(f \ l) (at x within S) \ (f \ l) (at x within T) \ S \ T = UNIV \ (f \ l) (at x)" by (metis Lim_Un) text \Interrelations between restricted and unrestricted limits.\ lemma Lim_at_imp_Lim_at_within: "(f \ l) (at x) \ (f \ l) (at x within S)" by (metis order_refl filterlim_mono subset_UNIV at_le) lemma eventually_within_interior: assumes "x \ interior S" shows "eventually P (at x within S) \ eventually P (at x)" (is "?lhs = ?rhs") proof from assms obtain T where T: "open T" "x \ T" "T \ S" .. { assume ?lhs then obtain A where "open A" and "x \ A" and "\y\A. y \ x \ y \ S \ P y" by (auto simp: eventually_at_topological) with T have "open (A \ T)" and "x \ A \ T" and "\y \ A \ T. y \ x \ P y" by auto then show ?rhs by (auto simp: eventually_at_topological) next assume ?rhs then show ?lhs by (auto elim: eventually_mono simp: eventually_at_filter) } qed lemma at_within_interior: "x \ interior S \ at x within S = at x" unfolding filter_eq_iff by (intro allI eventually_within_interior) lemma Lim_within_LIMSEQ: fixes a :: "'a::first_countable_topology" assumes "\S. (\n. S n \ a \ S n \ T) \ S \ a \ (\n. X (S n)) \ L" shows "(X \ L) (at a within T)" using assms unfolding tendsto_def [where l=L] by (simp add: sequentially_imp_eventually_within) lemma Lim_right_bound: fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \ 'b::{linorder_topology, conditionally_complete_linorder}" assumes mono: "\a b. a \ I \ b \ I \ x < a \ a \ b \ f a \ f b" and bnd: "\a. a \ I \ x < a \ K \ f a" shows "(f \ Inf (f ` ({x<..} \ I))) (at x within ({x<..} \ I))" proof (cases "{x<..} \ I = {}") case True then show ?thesis by simp next case False show ?thesis proof (rule order_tendstoI) fix a assume a: "a < Inf (f ` ({x<..} \ I))" { fix y assume "y \ {x<..} \ I" with False bnd have "Inf (f ` ({x<..} \ I)) \ f y" by (auto intro!: cInf_lower bdd_belowI2) with a have "a < f y" by (blast intro: less_le_trans) } then show "eventually (\x. a < f x) (at x within ({x<..} \ I))" by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one) next fix a assume "Inf (f ` ({x<..} \ I)) < a" from cInf_lessD[OF _ this] False obtain y where y: "x < y" "y \ I" "f y < a" by auto then have "eventually (\x. x \ I \ f x < a) (at_right x)" unfolding eventually_at_right[OF \x < y\] by (metis less_imp_le le_less_trans mono) then show "eventually (\x. f x < a) (at x within ({x<..} \ I))" unfolding eventually_at_filter by eventually_elim simp qed qed (*could prove directly from islimpt_sequential_inj, but only for metric spaces*) lemma islimpt_sequential: fixes x :: "'a::first_countable_topology" shows "x islimpt S \ (\f. (\n::nat. f n \ S - {x}) \ (f \ x) sequentially)" (is "?lhs = ?rhs") proof assume ?lhs from countable_basis_at_decseq[of x] obtain A where A: "\i. open (A i)" "\i. x \ A i" "\S. open S \ x \ S \ eventually (\i. A i \ S) sequentially" by blast define f where "f n = (SOME y. y \ S \ y \ A n \ x \ y)" for n { fix n from \?lhs\ have "\y. y \ S \ y \ A n \ x \ y" unfolding islimpt_def using A(1,2)[of n] by auto then have "f n \ S \ f n \ A n \ x \ f n" unfolding f_def by (rule someI_ex) then have "f n \ S" "f n \ A n" "x \ f n" by auto } then have "\n. f n \ S - {x}" by auto moreover have "(\n. f n) \ x" proof (rule topological_tendstoI) fix S assume "open S" "x \ S" from A(3)[OF this] \\n. f n \ A n\ show "eventually (\x. f x \ S) sequentially" by (auto elim!: eventually_mono) qed ultimately show ?rhs by fast next assume ?rhs then obtain f :: "nat \ 'a" where f: "\n. f n \ S - {x}" and lim: "f \ x" by auto show ?lhs unfolding islimpt_def proof safe fix T assume "open T" "x \ T" from lim[THEN topological_tendstoD, OF this] f show "\y\S. y \ T \ y \ x" unfolding eventually_sequentially by auto qed qed text\These are special for limits out of the same topological space.\ lemma Lim_within_id: "(id \ a) (at a within s)" unfolding id_def by (rule tendsto_ident_at) lemma Lim_at_id: "(id \ a) (at a)" unfolding id_def by (rule tendsto_ident_at) text\It's also sometimes useful to extract the limit point from the filter.\ abbreviation netlimit :: "'a::t2_space filter \ 'a" where "netlimit F \ Lim F (\x. x)" lemma netlimit_at [simp]: fixes a :: "'a::{perfect_space,t2_space}" shows "netlimit (at a) = a" using Lim_ident_at [of a UNIV] by simp lemma lim_within_interior: "x \ interior S \ (f \ l) (at x within S) \ (f \ l) (at x)" by (metis at_within_interior) lemma netlimit_within_interior: fixes x :: "'a::{t2_space,perfect_space}" assumes "x \ interior S" shows "netlimit (at x within S) = x" using assms by (metis at_within_interior netlimit_at) text\Useful lemmas on closure and set of possible sequential limits.\ lemma closure_sequential: fixes l :: "'a::first_countable_topology" shows "l \ closure S \ (\x. (\n. x n \ S) \ (x \ l) sequentially)" (is "?lhs = ?rhs") proof assume "?lhs" moreover { assume "l \ S" then have "?rhs" using tendsto_const[of l sequentially] by auto } moreover { assume "l islimpt S" then have "?rhs" unfolding islimpt_sequential by auto } ultimately show "?rhs" unfolding closure_def by auto next assume "?rhs" then show "?lhs" unfolding closure_def islimpt_sequential by auto qed lemma closed_sequential_limits: fixes S :: "'a::first_countable_topology set" shows "closed S \ (\x l. (\n. x n \ S) \ (x \ l) sequentially \ l \ S)" by (metis closure_sequential closure_subset_eq subset_iff) lemma tendsto_If_within_closures: assumes f: "x \ s \ (closure s \ closure t) \ (f \ l x) (at x within s \ (closure s \ closure t))" assumes g: "x \ t \ (closure s \ closure t) \ (g \ l x) (at x within t \ (closure s \ closure t))" assumes "x \ s \ t" shows "((\x. if x \ s then f x else g x) \ l x) (at x within s \ t)" proof - have *: "(s \ t) \ {x. x \ s} = s" "(s \ t) \ {x. x \ s} = t - s" by auto have "(f \ l x) (at x within s)" by (rule filterlim_at_within_closure_implies_filterlim) (use \x \ _\ in \auto simp: inf_commute closure_def intro: tendsto_within_subset[OF f]\) moreover have "(g \ l x) (at x within t - s)" by (rule filterlim_at_within_closure_implies_filterlim) (use \x \ _\ in \auto intro!: tendsto_within_subset[OF g] simp: closure_def intro: islimpt_subset\) ultimately show ?thesis by (intro filterlim_at_within_If) (simp_all only: *) qed subsection \Compactness\ lemma brouwer_compactness_lemma: fixes f :: "'a::topological_space \ 'b::real_normed_vector" assumes "compact s" and "continuous_on s f" and "\ (\x\s. f x = 0)" obtains d where "0 < d" and "\x\s. d \ norm (f x)" proof (cases "s = {}") case True show thesis by (rule that [of 1]) (auto simp: True) next case False have "continuous_on s (norm \ f)" by (rule continuous_intros continuous_on_norm assms(2))+ with False obtain x where x: "x \ s" "\y\s. (norm \ f) x \ (norm \ f) y" using continuous_attains_inf[OF assms(1), of "norm \ f"] unfolding o_def by auto have "(norm \ f) x > 0" using assms(3) and x(1) by auto then show ?thesis by (rule that) (insert x(2), auto simp: o_def) qed subsubsection \Bolzano-Weierstrass property\ proposition Heine_Borel_imp_Bolzano_Weierstrass: assumes "compact s" and "infinite t" and "t \ s" shows "\x \ s. x islimpt t" proof (rule ccontr) assume "\ (\x \ s. x islimpt t)" then obtain f where f: "\x\s. x \ f x \ open (f x) \ (\y\t. y \ f x \ y = x)" unfolding islimpt_def using bchoice[of s "\ x T. x \ T \ open T \ (\y\t. y \ T \ y = x)"] by auto obtain g where g: "g \ {t. \x. x \ s \ t = f x}" "finite g" "s \ \g" using assms(1)[unfolded compact_eq_Heine_Borel, THEN spec[where x="{t. \x. x\s \ t = f x}"]] using f by auto from g(1,3) have g':"\x\g. \xa \ s. x = f xa" by auto { fix x y assume "x \ t" "y \ t" "f x = f y" then have "x \ f x" "y \ f x \ y = x" using f[THEN bspec[where x=x]] and \t \ s\ by auto then have "x = y" using \f x = f y\ and f[THEN bspec[where x=y]] and \y \ t\ and \t \ s\ by auto } then have "inj_on f t" unfolding inj_on_def by simp then have "infinite (f ` t)" using assms(2) using finite_imageD by auto moreover { fix x assume "x \ t" "f x \ g" from g(3) assms(3) \x \ t\ obtain h where "h \ g" and "x \ h" by auto then obtain y where "y \ s" "h = f y" using g'[THEN bspec[where x=h]] by auto then have "y = x" using f[THEN bspec[where x=y]] and \x\t\ and \x\h\[unfolded \h = f y\] by auto then have False using \f x \ g\ \h \ g\ unfolding \h = f y\ by auto } then have "f ` t \ g" by auto ultimately show False using g(2) using finite_subset by auto qed lemma sequence_infinite_lemma: fixes f :: "nat \ 'a::t1_space" assumes "\n. f n \ l" and "(f \ l) sequentially" shows "infinite (range f)" proof assume "finite (range f)" then have "closed (range f)" by (rule finite_imp_closed) then have "open (- range f)" by (rule open_Compl) from assms(1) have "l \ - range f" by auto from assms(2) have "eventually (\n. f n \ - range f) sequentially" using \open (- range f)\ \l \ - range f\ by (rule topological_tendstoD) then show False unfolding eventually_sequentially by auto qed lemma Bolzano_Weierstrass_imp_closed: fixes s :: "'a::{first_countable_topology,t2_space} set" assumes "\t. infinite t \ t \ s --> (\x \ s. x islimpt t)" shows "closed s" proof - { fix x l assume as: "\n::nat. x n \ s" "(x \ l) sequentially" then have "l \ s" proof (cases "\n. x n \ l") case False then show "l\s" using as(1) by auto next case True note cas = this with as(2) have "infinite (range x)" using sequence_infinite_lemma[of x l] by auto then obtain l' where "l'\s" "l' islimpt (range x)" using assms[THEN spec[where x="range x"]] as(1) by auto then show "l\s" using sequence_unique_limpt[of x l l'] using as cas by auto qed } then show ?thesis unfolding closed_sequential_limits by fast qed lemma closure_insert: fixes x :: "'a::t1_space" shows "closure (insert x s) = insert x (closure s)" apply (rule closure_unique) apply (rule insert_mono [OF closure_subset]) apply (rule closed_insert [OF closed_closure]) apply (simp add: closure_minimal) done text\In particular, some common special cases.\ lemma compact_Un [intro]: assumes "compact s" and "compact t" shows " compact (s \ t)" proof (rule compactI) fix f assume *: "Ball f open" "s \ t \ \f" from * \compact s\ obtain s' where "s' \ f \ finite s' \ s \ \s'" unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f]) moreover from * \compact t\ obtain t' where "t' \ f \ finite t' \ t \ \t'" unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f]) ultimately show "\f'\f. finite f' \ s \ t \ \f'" by (auto intro!: exI[of _ "s' \ t'"]) qed lemma compact_Union [intro]: "finite S \ (\T. T \ S \ compact T) \ compact (\S)" by (induct set: finite) auto lemma compact_UN [intro]: "finite A \ (\x. x \ A \ compact (B x)) \ compact (\x\A. B x)" by (rule compact_Union) auto lemma closed_Int_compact [intro]: assumes "closed s" and "compact t" shows "compact (s \ t)" using compact_Int_closed [of t s] assms by (simp add: Int_commute) lemma compact_Int [intro]: fixes s t :: "'a :: t2_space set" assumes "compact s" and "compact t" shows "compact (s \ t)" using assms by (intro compact_Int_closed compact_imp_closed) lemma compact_sing [simp]: "compact {a}" unfolding compact_eq_Heine_Borel by auto lemma compact_insert [simp]: assumes "compact s" shows "compact (insert x s)" proof - have "compact ({x} \ s)" using compact_sing assms by (rule compact_Un) then show ?thesis by simp qed lemma finite_imp_compact: "finite s \ compact s" by (induct set: finite) simp_all lemma open_delete: fixes s :: "'a::t1_space set" shows "open s \ open (s - {x})" by (simp add: open_Diff) text\Compactness expressed with filters\ lemma closure_iff_nhds_not_empty: "x \ closure X \ (\A. \S\A. open S \ x \ S \ X \ A \ {})" proof safe assume x: "x \ closure X" fix S A assume "open S" "x \ S" "X \ A = {}" "S \ A" then have "x \ closure (-S)" by (auto simp: closure_complement subset_eq[symmetric] intro: interiorI) with x have "x \ closure X - closure (-S)" by auto also have "\ \ closure (X \ S)" using \open S\ open_Int_closure_subset[of S X] by (simp add: closed_Compl ac_simps) finally have "X \ S \ {}" by auto then show False using \X \ A = {}\ \S \ A\ by auto next assume "\A S. S \ A \ open S \ x \ S \ X \ A \ {}" from this[THEN spec, of "- X", THEN spec, of "- closure X"] show "x \ closure X" by (simp add: closure_subset open_Compl) qed lemma compact_filter: "compact U \ (\F. F \ bot \ eventually (\x. x \ U) F \ (\x\U. inf (nhds x) F \ bot))" proof (intro allI iffI impI compact_fip[THEN iffD2] notI) fix F assume "compact U" assume F: "F \ bot" "eventually (\x. x \ U) F" then have "U \ {}" by (auto simp: eventually_False) define Z where "Z = closure ` {A. eventually (\x. x \ A) F}" then have "\z\Z. closed z" by auto moreover have ev_Z: "\z. z \ Z \ eventually (\x. x \ z) F" unfolding Z_def by (auto elim: eventually_mono intro: subsetD[OF closure_subset]) have "(\B \ Z. finite B \ U \ \B \ {})" proof (intro allI impI) fix B assume "finite B" "B \ Z" with \finite B\ ev_Z F(2) have "eventually (\x. x \ U \ (\B)) F" by (auto simp: eventually_ball_finite_distrib eventually_conj_iff) with F show "U \ \B \ {}" by (intro notI) (simp add: eventually_False) qed ultimately have "U \ \Z \ {}" using \compact U\ unfolding compact_fip by blast then obtain x where "x \ U" and x: "\z. z \ Z \ x \ z" by auto have "\P. eventually P (inf (nhds x) F) \ P \ bot" unfolding eventually_inf eventually_nhds proof safe fix P Q R S assume "eventually R F" "open S" "x \ S" with open_Int_closure_eq_empty[of S "{x. R x}"] x[of "closure {x. R x}"] have "S \ {x. R x} \ {}" by (auto simp: Z_def) moreover assume "Ball S Q" "\x. Q x \ R x \ bot x" ultimately show False by (auto simp: set_eq_iff) qed with \x \ U\ show "\x\U. inf (nhds x) F \ bot" by (metis eventually_bot) next fix A assume A: "\a\A. closed a" "\B\A. finite B \ U \ \B \ {}" "U \ \A = {}" define F where "F = (INF a\insert U A. principal a)" have "F \ bot" unfolding F_def proof (rule INF_filter_not_bot) fix X assume X: "X \ insert U A" "finite X" with A(2)[THEN spec, of "X - {U}"] have "U \ \(X - {U}) \ {}" by auto with X show "(INF a\X. principal a) \ bot" by (auto simp: INF_principal_finite principal_eq_bot_iff) qed moreover have "F \ principal U" unfolding F_def by auto then have "eventually (\x. x \ U) F" by (auto simp: le_filter_def eventually_principal) moreover assume "\F. F \ bot \ eventually (\x. x \ U) F \ (\x\U. inf (nhds x) F \ bot)" ultimately obtain x where "x \ U" and x: "inf (nhds x) F \ bot" by auto { fix V assume "V \ A" then have "F \ principal V" unfolding F_def by (intro INF_lower2[of V]) auto then have V: "eventually (\x. x \ V) F" by (auto simp: le_filter_def eventually_principal) have "x \ closure V" unfolding closure_iff_nhds_not_empty proof (intro impI allI) fix S A assume "open S" "x \ S" "S \ A" then have "eventually (\x. x \ A) (nhds x)" by (auto simp: eventually_nhds) with V have "eventually (\x. x \ V \ A) (inf (nhds x) F)" by (auto simp: eventually_inf) with x show "V \ A \ {}" by (auto simp del: Int_iff simp add: trivial_limit_def) qed then have "x \ V" using \V \ A\ A(1) by simp } with \x\U\ have "x \ U \ \A" by auto with \U \ \A = {}\ show False by auto qed definition\<^marker>\tag important\ countably_compact :: "('a::topological_space) set \ bool" where "countably_compact U \ (\A. countable A \ (\a\A. open a) \ U \ \A \ (\T\A. finite T \ U \ \T))" lemma countably_compactE: assumes "countably_compact s" and "\t\C. open t" and "s \ \C" "countable C" obtains C' where "C' \ C" and "finite C'" and "s \ \C'" using assms unfolding countably_compact_def by metis lemma countably_compactI: assumes "\C. \t\C. open t \ s \ \C \ countable C \ (\C'\C. finite C' \ s \ \C')" shows "countably_compact s" using assms unfolding countably_compact_def by metis lemma compact_imp_countably_compact: "compact U \ countably_compact U" by (auto simp: compact_eq_Heine_Borel countably_compact_def) lemma countably_compact_imp_compact: assumes "countably_compact U" and ccover: "countable B" "\b\B. open b" and basis: "\T x. open T \ x \ T \ x \ U \ \b\B. x \ b \ b \ U \ T" shows "compact U" using \countably_compact U\ unfolding compact_eq_Heine_Borel countably_compact_def proof safe fix A assume A: "\a\A. open a" "U \ \A" assume *: "\A. countable A \ (\a\A. open a) \ U \ \A \ (\T\A. finite T \ U \ \T)" moreover define C where "C = {b\B. \a\A. b \ U \ a}" ultimately have "countable C" "\a\C. open a" unfolding C_def using ccover by auto moreover have "\A \ U \ \C" proof safe fix x a assume "x \ U" "x \ a" "a \ A" with basis[of a x] A obtain b where "b \ B" "x \ b" "b \ U \ a" by blast with \a \ A\ show "x \ \C" unfolding C_def by auto qed then have "U \ \C" using \U \ \A\ by auto ultimately obtain T where T: "T\C" "finite T" "U \ \T" using * by metis then have "\t\T. \a\A. t \ U \ a" by (auto simp: C_def) then obtain f where "\t\T. f t \ A \ t \ U \ f t" unfolding bchoice_iff Bex_def .. with T show "\T\A. finite T \ U \ \T" unfolding C_def by (intro exI[of _ "f`T"]) fastforce qed proposition countably_compact_imp_compact_second_countable: "countably_compact U \ compact (U :: 'a :: second_countable_topology set)" proof (rule countably_compact_imp_compact) fix T and x :: 'a assume "open T" "x \ T" from topological_basisE[OF is_basis this] obtain b where "b \ (SOME B. countable B \ topological_basis B)" "x \ b" "b \ T" . then show "\b\SOME B. countable B \ topological_basis B. x \ b \ b \ U \ T" by blast qed (insert countable_basis topological_basis_open[OF is_basis], auto) lemma countably_compact_eq_compact: "countably_compact U \ compact (U :: 'a :: second_countable_topology set)" using countably_compact_imp_compact_second_countable compact_imp_countably_compact by blast subsubsection\Sequential compactness\ definition\<^marker>\tag important\ seq_compact :: "'a::topological_space set \ bool" where "seq_compact S \ (\f. (\n. f n \ S) \ (\l\S. \r::nat\nat. strict_mono r \ ((f \ r) \ l) sequentially))" lemma seq_compactI: assumes "\f. \n. f n \ S \ \l\S. \r::nat\nat. strict_mono r \ ((f \ r) \ l) sequentially" shows "seq_compact S" unfolding seq_compact_def using assms by fast lemma seq_compactE: assumes "seq_compact S" "\n. f n \ S" obtains l r where "l \ S" "strict_mono (r :: nat \ nat)" "((f \ r) \ l) sequentially" using assms unfolding seq_compact_def by fast lemma closed_sequentially: (* TODO: move upwards *) assumes "closed s" and "\n. f n \ s" and "f \ l" shows "l \ s" proof (rule ccontr) assume "l \ s" with \closed s\ and \f \ l\ have "eventually (\n. f n \ - s) sequentially" by (fast intro: topological_tendstoD) with \\n. f n \ s\ show "False" by simp qed lemma seq_compact_Int_closed: assumes "seq_compact s" and "closed t" shows "seq_compact (s \ t)" proof (rule seq_compactI) fix f assume "\n::nat. f n \ s \ t" hence "\n. f n \ s" and "\n. f n \ t" by simp_all from \seq_compact s\ and \\n. f n \ s\ obtain l r where "l \ s" and r: "strict_mono r" and l: "(f \ r) \ l" by (rule seq_compactE) from \\n. f n \ t\ have "\n. (f \ r) n \ t" by simp from \closed t\ and this and l have "l \ t" by (rule closed_sequentially) with \l \ s\ and r and l show "\l\s \ t. \r. strict_mono r \ (f \ r) \ l" by fast qed lemma seq_compact_closed_subset: assumes "closed s" and "s \ t" and "seq_compact t" shows "seq_compact s" using assms seq_compact_Int_closed [of t s] by (simp add: Int_absorb1) lemma seq_compact_imp_countably_compact: fixes U :: "'a :: first_countable_topology set" assumes "seq_compact U" shows "countably_compact U" proof (safe intro!: countably_compactI) fix A assume A: "\a\A. open a" "U \ \A" "countable A" have subseq: "\X. range X \ U \ \r x. x \ U \ strict_mono (r :: nat \ nat) \ (X \ r) \ x" using \seq_compact U\ by (fastforce simp: seq_compact_def subset_eq) show "\T\A. finite T \ U \ \T" proof cases assume "finite A" with A show ?thesis by auto next assume "infinite A" then have "A \ {}" by auto show ?thesis proof (rule ccontr) assume "\ (\T\A. finite T \ U \ \T)" then have "\T. \x. T \ A \ finite T \ (x \ U - \T)" by auto then obtain X' where T: "\T. T \ A \ finite T \ X' T \ U - \T" by metis define X where "X n = X' (from_nat_into A ` {.. n})" for n have X: "\n. X n \ U - (\i\n. from_nat_into A i)" using \A \ {}\ unfolding X_def by (intro T) (auto intro: from_nat_into) then have "range X \ U" by auto with subseq[of X] obtain r x where "x \ U" and r: "strict_mono r" "(X \ r) \ x" by auto from \x\U\ \U \ \A\ from_nat_into_surj[OF \countable A\] obtain n where "x \ from_nat_into A n" by auto with r(2) A(1) from_nat_into[OF \A \ {}\, of n] have "eventually (\i. X (r i) \ from_nat_into A n) sequentially" unfolding tendsto_def by (auto simp: comp_def) then obtain N where "\i. N \ i \ X (r i) \ from_nat_into A n" by (auto simp: eventually_sequentially) moreover from X have "\i. n \ r i \ X (r i) \ from_nat_into A n" by auto moreover from \strict_mono r\[THEN seq_suble, of "max n N"] have "\i. n \ r i \ N \ i" by (auto intro!: exI[of _ "max n N"]) ultimately show False by auto qed qed qed lemma compact_imp_seq_compact: fixes U :: "'a :: first_countable_topology set" assumes "compact U" shows "seq_compact U" unfolding seq_compact_def proof safe fix X :: "nat \ 'a" assume "\n. X n \ U" then have "eventually (\x. x \ U) (filtermap X sequentially)" by (auto simp: eventually_filtermap) moreover have "filtermap X sequentially \ bot" by (simp add: trivial_limit_def eventually_filtermap) ultimately obtain x where "x \ U" and x: "inf (nhds x) (filtermap X sequentially) \ bot" (is "?F \ _") using \compact U\ by (auto simp: compact_filter) from countable_basis_at_decseq[of x] obtain A where A: "\i. open (A i)" "\i. x \ A i" "\S. open S \ x \ S \ eventually (\i. A i \ S) sequentially" by blast define s where "s n i = (SOME j. i < j \ X j \ A (Suc n))" for n i { fix n i have "\a. i < a \ X a \ A (Suc n)" proof (rule ccontr) assume "\ (\a>i. X a \ A (Suc n))" then have "\a. Suc i \ a \ X a \ A (Suc n)" by auto then have "eventually (\x. x \ A (Suc n)) (filtermap X sequentially)" by (auto simp: eventually_filtermap eventually_sequentially) moreover have "eventually (\x. x \ A (Suc n)) (nhds x)" using A(1,2)[of "Suc n"] by (auto simp: eventually_nhds) ultimately have "eventually (\x. False) ?F" by (auto simp: eventually_inf) with x show False by (simp add: eventually_False) qed then have "i < s n i" "X (s n i) \ A (Suc n)" unfolding s_def by (auto intro: someI2_ex) } note s = this define r where "r = rec_nat (s 0 0) s" have "strict_mono r" by (auto simp: r_def s strict_mono_Suc_iff) moreover have "(\n. X (r n)) \ x" proof (rule topological_tendstoI) fix S assume "open S" "x \ S" with A(3) have "eventually (\i. A i \ S) sequentially" by auto moreover { fix i assume "Suc 0 \ i" then have "X (r i) \ A i" by (cases i) (simp_all add: r_def s) } then have "eventually (\i. X (r i) \ A i) sequentially" by (auto simp: eventually_sequentially) ultimately show "eventually (\i. X (r i) \ S) sequentially" by eventually_elim auto qed ultimately show "\x \ U. \r. strict_mono r \ (X \ r) \ x" using \x \ U\ by (auto simp: convergent_def comp_def) qed lemma countably_compact_imp_acc_point: assumes "countably_compact s" and "countable t" and "infinite t" and "t \ s" shows "\x\s. \U. x\U \ open U \ infinite (U \ t)" proof (rule ccontr) define C where "C = (\F. interior (F \ (- t))) ` {F. finite F \ F \ t }" note \countably_compact s\ moreover have "\t\C. open t" by (auto simp: C_def) moreover assume "\ (\x\s. \U. x\U \ open U \ infinite (U \ t))" then have s: "\x. x \ s \ \U. x\U \ open U \ finite (U \ t)" by metis have "s \ \C" using \t \ s\ unfolding C_def apply (safe dest!: s) apply (rule_tac a="U \ t" in UN_I) apply (auto intro!: interiorI simp add: finite_subset) done moreover from \countable t\ have "countable C" unfolding C_def by (auto intro: countable_Collect_finite_subset) ultimately obtain D where "D \ C" "finite D" "s \ \D" by (rule countably_compactE) then obtain E where E: "E \ {F. finite F \ F \ t }" "finite E" and s: "s \ (\F\E. interior (F \ (- t)))" by (metis (lifting) finite_subset_image C_def) from s \t \ s\ have "t \ \E" using interior_subset by blast moreover have "finite (\E)" using E by auto ultimately show False using \infinite t\ by (auto simp: finite_subset) qed lemma countable_acc_point_imp_seq_compact: fixes s :: "'a::first_countable_topology set" assumes "\t. infinite t \ countable t \ t \ s \ (\x\s. \U. x\U \ open U \ infinite (U \ t))" shows "seq_compact s" proof - { fix f :: "nat \ 'a" assume f: "\n. f n \ s" have "\l\s. \r. strict_mono r \ ((f \ r) \ l) sequentially" proof (cases "finite (range f)") case True obtain l where "infinite {n. f n = f l}" using pigeonhole_infinite[OF _ True] by auto then obtain r :: "nat \ nat" where "strict_mono r" and fr: "\n. f (r n) = f l" using infinite_enumerate by blast then have "strict_mono r \ (f \ r) \ f l" by (simp add: fr o_def) with f show "\l\s. \r. strict_mono r \ (f \ r) \ l" by auto next case False with f assms have "\x\s. \U. x\U \ open U \ infinite (U \ range f)" by auto then obtain l where "l \ s" "\U. l\U \ open U \ infinite (U \ range f)" .. from this(2) have "\r. strict_mono r \ ((f \ r) \ l) sequentially" using acc_point_range_imp_convergent_subsequence[of l f] by auto with \l \ s\ show "\l\s. \r. strict_mono r \ ((f \ r) \ l) sequentially" .. qed } then show ?thesis unfolding seq_compact_def by auto qed lemma seq_compact_eq_countably_compact: fixes U :: "'a :: first_countable_topology set" shows "seq_compact U \ countably_compact U" using countable_acc_point_imp_seq_compact countably_compact_imp_acc_point seq_compact_imp_countably_compact by metis lemma seq_compact_eq_acc_point: fixes s :: "'a :: first_countable_topology set" shows "seq_compact s \ (\t. infinite t \ countable t \ t \ s --> (\x\s. \U. x\U \ open U \ infinite (U \ t)))" using countable_acc_point_imp_seq_compact[of s] countably_compact_imp_acc_point[of s] seq_compact_imp_countably_compact[of s] by metis lemma seq_compact_eq_compact: fixes U :: "'a :: second_countable_topology set" shows "seq_compact U \ compact U" using seq_compact_eq_countably_compact countably_compact_eq_compact by blast proposition Bolzano_Weierstrass_imp_seq_compact: fixes s :: "'a::{t1_space, first_countable_topology} set" shows "\t. infinite t \ t \ s \ (\x \ s. x islimpt t) \ seq_compact s" by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point) subsection\<^marker>\tag unimportant\ \Cartesian products\ lemma seq_compact_Times: "seq_compact s \ seq_compact t \ seq_compact (s \ t)" unfolding seq_compact_def apply clarify apply (drule_tac x="fst \ f" in spec) apply (drule mp, simp add: mem_Times_iff) apply (clarify, rename_tac l1 r1) apply (drule_tac x="snd \ f \ r1" in spec) apply (drule mp, simp add: mem_Times_iff) apply (clarify, rename_tac l2 r2) apply (rule_tac x="(l1, l2)" in rev_bexI, simp) apply (rule_tac x="r1 \ r2" in exI) apply (rule conjI, simp add: strict_mono_def) apply (drule_tac f=r2 in LIMSEQ_subseq_LIMSEQ, assumption) apply (drule (1) tendsto_Pair) back apply (simp add: o_def) done lemma compact_Times: assumes "compact s" "compact t" shows "compact (s \ t)" proof (rule compactI) fix C assume C: "\t\C. open t" "s \ t \ \C" have "\x\s. \a. open a \ x \ a \ (\d\C. finite d \ a \ t \ \d)" proof fix x assume "x \ s" have "\y\t. \a b c. c \ C \ open a \ open b \ x \ a \ y \ b \ a \ b \ c" (is "\y\t. ?P y") proof fix y assume "y \ t" with \x \ s\ C obtain c where "c \ C" "(x, y) \ c" "open c" by auto then show "?P y" by (auto elim!: open_prod_elim) qed then obtain a b c where b: "\y. y \ t \ open (b y)" and c: "\y. y \ t \ c y \ C \ open (a y) \ open (b y) \ x \ a y \ y \ b y \ a y \ b y \ c y" by metis then have "\y\t. open (b y)" "t \ (\y\t. b y)" by auto with compactE_image[OF \compact t\] obtain D where D: "D \ t" "finite D" "t \ (\y\D. b y)" by metis moreover from D c have "(\y\D. a y) \ t \ (\y\D. c y)" by (fastforce simp: subset_eq) ultimately show "\a. open a \ x \ a \ (\d\C. finite d \ a \ t \ \d)" using c by (intro exI[of _ "c`D"] exI[of _ "\(a`D)"] conjI) (auto intro!: open_INT) qed then obtain a d where a: "\x. x\s \ open (a x)" "s \ (\x\s. a x)" and d: "\x. x \ s \ d x \ C \ finite (d x) \ a x \ t \ \(d x)" unfolding subset_eq UN_iff by metis moreover from compactE_image[OF \compact s\ a] obtain e where e: "e \ s" "finite e" and s: "s \ (\x\e. a x)" by auto moreover { from s have "s \ t \ (\x\e. a x \ t)" by auto also have "\ \ (\x\e. \(d x))" using d \e \ s\ by (intro UN_mono) auto finally have "s \ t \ (\x\e. \(d x))" . } ultimately show "\C'\C. finite C' \ s \ t \ \C'" by (intro exI[of _ "(\x\e. d x)"]) (auto simp: subset_eq) qed lemma tube_lemma: assumes "compact K" assumes "open W" assumes "{x0} \ K \ W" shows "\X0. x0 \ X0 \ open X0 \ X0 \ K \ W" proof - { fix y assume "y \ K" then have "(x0, y) \ W" using assms by auto with \open W\ have "\X0 Y. open X0 \ open Y \ x0 \ X0 \ y \ Y \ X0 \ Y \ W" by (rule open_prod_elim) blast } then obtain X0 Y where *: "\y \ K. open (X0 y) \ open (Y y) \ x0 \ X0 y \ y \ Y y \ X0 y \ Y y \ W" by metis from * have "\t\Y ` K. open t" "K \ \(Y ` K)" by auto with \compact K\ obtain CC where CC: "CC \ Y ` K" "finite CC" "K \ \CC" by (meson compactE) then obtain c where c: "\C. C \ CC \ c C \ K \ C = Y (c C)" by (force intro!: choice) with * CC show ?thesis by (force intro!: exI[where x="\C\CC. X0 (c C)"]) (* SLOW *) qed lemma continuous_on_prod_compactE: fixes fx::"'a::topological_space \ 'b::topological_space \ 'c::metric_space" and e::real assumes cont_fx: "continuous_on (U \ C) fx" assumes "compact C" assumes [intro]: "x0 \ U" notes [continuous_intros] = continuous_on_compose2[OF cont_fx] assumes "e > 0" obtains X0 where "x0 \ X0" "open X0" "\x\X0 \ U. \t \ C. dist (fx (x, t)) (fx (x0, t)) \ e" proof - define psi where "psi = (\(x, t). dist (fx (x, t)) (fx (x0, t)))" define W0 where "W0 = {(x, t) \ U \ C. psi (x, t) < e}" have W0_eq: "W0 = psi -` {.. U \ C" by (auto simp: vimage_def W0_def) have "open {.. C) psi" by (auto intro!: continuous_intros simp: psi_def split_beta') from this[unfolded continuous_on_open_invariant, rule_format, OF \open {..] obtain W where W: "open W" "W \ U \ C = W0 \ U \ C" unfolding W0_eq by blast have "{x0} \ C \ W \ U \ C" unfolding W by (auto simp: W0_def psi_def \0 < e\) then have "{x0} \ C \ W" by blast from tube_lemma[OF \compact C\ \open W\ this] obtain X0 where X0: "x0 \ X0" "open X0" "X0 \ C \ W" by blast have "\x\X0 \ U. \t \ C. dist (fx (x, t)) (fx (x0, t)) \ e" proof safe fix x assume x: "x \ X0" "x \ U" fix t assume t: "t \ C" have "dist (fx (x, t)) (fx (x0, t)) = psi (x, t)" by (auto simp: psi_def) also { have "(x, t) \ X0 \ C" using t x by auto also note \\ \ W\ finally have "(x, t) \ W" . with t x have "(x, t) \ W \ U \ C" by blast also note \W \ U \ C = W0 \ U \ C\ finally have "psi (x, t) < e" by (auto simp: W0_def) } finally show "dist (fx (x, t)) (fx (x0, t)) \ e" by simp qed from X0(1,2) this show ?thesis .. qed subsection \Continuity\ lemma continuous_at_imp_continuous_within: "continuous (at x) f \ continuous (at x within s) f" unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto lemma Lim_trivial_limit: "trivial_limit net \ (f \ l) net" by simp lemmas continuous_on = continuous_on_def \ \legacy theorem name\ lemma continuous_within_subset: "continuous (at x within s) f \ t \ s \ continuous (at x within t) f" unfolding continuous_within by(metis tendsto_within_subset) lemma continuous_on_interior: "continuous_on s f \ x \ interior s \ continuous (at x) f" by (metis continuous_on_eq_continuous_at continuous_on_subset interiorE) lemma continuous_on_eq: "\continuous_on s f; \x. x \ s \ f x = g x\ \ continuous_on s g" unfolding continuous_on_def tendsto_def eventually_at_topological by simp text \Characterization of various kinds of continuity in terms of sequences.\ lemma continuous_within_sequentiallyI: fixes f :: "'a::{first_countable_topology, t2_space} \ 'b::topological_space" assumes "\u::nat \ 'a. u \ a \ (\n. u n \ s) \ (\n. f (u n)) \ f a" shows "continuous (at a within s) f" using assms unfolding continuous_within tendsto_def[where l = "f a"] by (auto intro!: sequentially_imp_eventually_within) lemma continuous_within_tendsto_compose: fixes f::"'a::t2_space \ 'b::topological_space" assumes "continuous (at a within s) f" "eventually (\n. x n \ s) F" "(x \ a) F " shows "((\n. f (x n)) \ f a) F" proof - have *: "filterlim x (inf (nhds a) (principal s)) F" using assms(2) assms(3) unfolding at_within_def filterlim_inf by (auto simp: filterlim_principal eventually_mono) show ?thesis by (auto simp: assms(1) continuous_within[symmetric] tendsto_at_within_iff_tendsto_nhds[symmetric] intro!: filterlim_compose[OF _ *]) qed lemma continuous_within_tendsto_compose': fixes f::"'a::t2_space \ 'b::topological_space" assumes "continuous (at a within s) f" "\n. x n \ s" "(x \ a) F " shows "((\n. f (x n)) \ f a) F" by (auto intro!: continuous_within_tendsto_compose[OF assms(1)] simp add: assms) lemma continuous_within_sequentially: fixes f :: "'a::{first_countable_topology, t2_space} \ 'b::topological_space" shows "continuous (at a within s) f \ (\x. (\n::nat. x n \ s) \ (x \ a) sequentially \ ((f \ x) \ f a) sequentially)" using continuous_within_tendsto_compose'[of a s f _ sequentially] continuous_within_sequentiallyI[of a s f] by (auto simp: o_def) lemma continuous_at_sequentiallyI: fixes f :: "'a::{first_countable_topology, t2_space} \ 'b::topological_space" assumes "\u. u \ a \ (\n. f (u n)) \ f a" shows "continuous (at a) f" using continuous_within_sequentiallyI[of a UNIV f] assms by auto lemma continuous_at_sequentially: fixes f :: "'a::metric_space \ 'b::topological_space" shows "continuous (at a) f \ (\x. (x \ a) sequentially --> ((f \ x) \ f a) sequentially)" using continuous_within_sequentially[of a UNIV f] by simp lemma continuous_on_sequentiallyI: fixes f :: "'a::{first_countable_topology, t2_space} \ 'b::topological_space" assumes "\u a. (\n. u n \ s) \ a \ s \ u \ a \ (\n. f (u n)) \ f a" shows "continuous_on s f" using assms unfolding continuous_on_eq_continuous_within using continuous_within_sequentiallyI[of _ s f] by auto lemma continuous_on_sequentially: fixes f :: "'a::{first_countable_topology, t2_space} \ 'b::topological_space" shows "continuous_on s f \ (\x. \a \ s. (\n. x(n) \ s) \ (x \ a) sequentially --> ((f \ x) \ f a) sequentially)" (is "?lhs = ?rhs") proof assume ?rhs then show ?lhs using continuous_within_sequentially[of _ s f] unfolding continuous_on_eq_continuous_within by auto next assume ?lhs then show ?rhs unfolding continuous_on_eq_continuous_within using continuous_within_sequentially[of _ s f] by auto qed text \Continuity in terms of open preimages.\ lemma continuous_at_open: "continuous (at x) f \ (\t. open t \ f x \ t --> (\s. open s \ x \ s \ (\x' \ s. (f x') \ t)))" unfolding continuous_within_topological [of x UNIV f] unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto lemma continuous_imp_tendsto: assumes "continuous (at x0) f" and "x \ x0" shows "(f \ x) \ (f x0)" proof (rule topological_tendstoI) fix S assume "open S" "f x0 \ S" then obtain T where T_def: "open T" "x0 \ T" "\x\T. f x \ S" using assms continuous_at_open by metis then have "eventually (\n. x n \ T) sequentially" using assms T_def by (auto simp: tendsto_def) then show "eventually (\n. (f \ x) n \ S) sequentially" using T_def by (auto elim!: eventually_mono) qed subsection \Homeomorphisms\ definition\<^marker>\tag important\ "homeomorphism s t f g \ (\x\s. (g(f x) = x)) \ (f ` s = t) \ continuous_on s f \ (\y\t. (f(g y) = y)) \ (g ` t = s) \ continuous_on t g" lemma homeomorphismI [intro?]: assumes "continuous_on S f" "continuous_on T g" "f ` S \ T" "g ` T \ S" "\x. x \ S \ g(f x) = x" "\y. y \ T \ f(g y) = y" shows "homeomorphism S T f g" using assms by (force simp: homeomorphism_def) lemma homeomorphism_translation: fixes a :: "'a :: real_normed_vector" shows "homeomorphism ((+) a ` S) S ((+) (- a)) ((+) a)" unfolding homeomorphism_def by (auto simp: algebra_simps continuous_intros) lemma homeomorphism_ident: "homeomorphism T T (\a. a) (\a. a)" by (rule homeomorphismI) auto lemma homeomorphism_compose: assumes "homeomorphism S T f g" "homeomorphism T U h k" shows "homeomorphism S U (h o f) (g o k)" using assms unfolding homeomorphism_def by (intro conjI ballI continuous_on_compose) (auto simp: image_iff) lemma homeomorphism_cong: "homeomorphism X' Y' f' g'" if "homeomorphism X Y f g" "X' = X" "Y' = Y" "\x. x \ X \ f' x = f x" "\y. y \ Y \ g' y = g y" using that by (auto simp add: homeomorphism_def) lemma homeomorphism_empty [simp]: "homeomorphism {} {} f g" unfolding homeomorphism_def by auto lemma homeomorphism_symD: "homeomorphism S t f g \ homeomorphism t S g f" by (simp add: homeomorphism_def) lemma homeomorphism_sym: "homeomorphism S t f g = homeomorphism t S g f" by (force simp: homeomorphism_def) definition\<^marker>\tag important\ homeomorphic :: "'a::topological_space set \ 'b::topological_space set \ bool" (infixr "homeomorphic" 60) where "s homeomorphic t \ (\f g. homeomorphism s t f g)" lemma homeomorphic_empty [iff]: "S homeomorphic {} \ S = {}" "{} homeomorphic S \ S = {}" by (auto simp: homeomorphic_def homeomorphism_def) lemma homeomorphic_refl: "s homeomorphic s" unfolding homeomorphic_def homeomorphism_def using continuous_on_id apply (rule_tac x = "(\x. x)" in exI) apply (rule_tac x = "(\x. x)" in exI) apply blast done lemma homeomorphic_sym: "s homeomorphic t \ t homeomorphic s" unfolding homeomorphic_def homeomorphism_def by blast lemma homeomorphic_trans [trans]: assumes "S homeomorphic T" and "T homeomorphic U" shows "S homeomorphic U" using assms unfolding homeomorphic_def by (metis homeomorphism_compose) lemma homeomorphic_minimal: "s homeomorphic t \ (\f g. (\x\s. f(x) \ t \ (g(f(x)) = x)) \ (\y\t. g(y) \ s \ (f(g(y)) = y)) \ continuous_on s f \ continuous_on t g)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (fastforce simp: homeomorphic_def homeomorphism_def) next assume ?rhs then show ?lhs apply clarify unfolding homeomorphic_def homeomorphism_def by (metis equalityI image_subset_iff subsetI) qed lemma homeomorphicI [intro?]: "\f ` S = T; g ` T = S; continuous_on S f; continuous_on T g; \x. x \ S \ g(f(x)) = x; \y. y \ T \ f(g(y)) = y\ \ S homeomorphic T" unfolding homeomorphic_def homeomorphism_def by metis lemma homeomorphism_of_subsets: "\homeomorphism S T f g; S' \ S; T'' \ T; f ` S' = T'\ \ homeomorphism S' T' f g" apply (auto simp: homeomorphism_def elim!: continuous_on_subset) by (metis subsetD imageI) lemma homeomorphism_apply1: "\homeomorphism S T f g; x \ S\ \ g(f x) = x" by (simp add: homeomorphism_def) lemma homeomorphism_apply2: "\homeomorphism S T f g; x \ T\ \ f(g x) = x" by (simp add: homeomorphism_def) lemma homeomorphism_image1: "homeomorphism S T f g \ f ` S = T" by (simp add: homeomorphism_def) lemma homeomorphism_image2: "homeomorphism S T f g \ g ` T = S" by (simp add: homeomorphism_def) lemma homeomorphism_cont1: "homeomorphism S T f g \ continuous_on S f" by (simp add: homeomorphism_def) lemma homeomorphism_cont2: "homeomorphism S T f g \ continuous_on T g" by (simp add: homeomorphism_def) lemma continuous_on_no_limpt: "(\x. \ x islimpt S) \ continuous_on S f" unfolding continuous_on_def by (metis UNIV_I empty_iff eventually_at_topological islimptE open_UNIV tendsto_def trivial_limit_within) lemma continuous_on_finite: fixes S :: "'a::t1_space set" shows "finite S \ continuous_on S f" by (metis continuous_on_no_limpt islimpt_finite) lemma homeomorphic_finite: fixes S :: "'a::t1_space set" and T :: "'b::t1_space set" assumes "finite T" shows "S homeomorphic T \ finite S \ finite T \ card S = card T" (is "?lhs = ?rhs") proof assume "S homeomorphic T" with assms show ?rhs apply (auto simp: homeomorphic_def homeomorphism_def) apply (metis finite_imageI) by (metis card_image_le finite_imageI le_antisym) next assume R: ?rhs with finite_same_card_bij obtain h where "bij_betw h S T" by auto with R show ?lhs apply (auto simp: homeomorphic_def homeomorphism_def continuous_on_finite) apply (rule_tac x=h in exI) apply (rule_tac x="inv_into S h" in exI) apply (auto simp: bij_betw_inv_into_left bij_betw_inv_into_right bij_betw_imp_surj_on inv_into_into bij_betwE) apply (metis bij_betw_def bij_betw_inv_into) done qed text \Relatively weak hypotheses if a set is compact.\ lemma homeomorphism_compact: fixes f :: "'a::topological_space \ 'b::t2_space" assumes "compact s" "continuous_on s f" "f ` s = t" "inj_on f s" shows "\g. homeomorphism s t f g" proof - define g where "g x = (SOME y. y\s \ f y = x)" for x have g: "\x\s. g (f x) = x" using assms(3) assms(4)[unfolded inj_on_def] unfolding g_def by auto { fix y assume "y \ t" then obtain x where x:"f x = y" "x\s" using assms(3) by auto then have "g (f x) = x" using g by auto then have "f (g y) = y" unfolding x(1)[symmetric] by auto } then have g':"\x\t. f (g x) = x" by auto moreover { fix x have "x\s \ x \ g ` t" using g[THEN bspec[where x=x]] unfolding image_iff using assms(3) by (auto intro!: bexI[where x="f x"]) moreover { assume "x\g ` t" then obtain y where y:"y\t" "g y = x" by auto then obtain x' where x':"x'\s" "f x' = y" using assms(3) by auto then have "x \ s" unfolding g_def using someI2[of "\b. b\s \ f b = y" x' "\x. x\s"] unfolding y(2)[symmetric] and g_def by auto } ultimately have "x\s \ x \ g ` t" .. } then have "g ` t = s" by auto ultimately show ?thesis unfolding homeomorphism_def homeomorphic_def apply (rule_tac x=g in exI) using g and assms(3) and continuous_on_inv[OF assms(2,1), of g, unfolded assms(3)] and assms(2) apply auto done qed lemma homeomorphic_compact: fixes f :: "'a::topological_space \ 'b::t2_space" shows "compact s \ continuous_on s f \ (f ` s = t) \ inj_on f s \ s homeomorphic t" unfolding homeomorphic_def by (metis homeomorphism_compact) text\Preservation of topological properties.\ lemma homeomorphic_compactness: "s homeomorphic t \ (compact s \ compact t)" unfolding homeomorphic_def homeomorphism_def by (metis compact_continuous_image) subsection\<^marker>\tag unimportant\ \On Linorder Topologies\ lemma islimpt_greaterThanLessThan1: fixes a b::"'a::{linorder_topology, dense_order}" assumes "a < b" shows "a islimpt {a<.. T" from open_right[OF this \a < b\] obtain c where c: "a < c" "{a.. T" by auto with assms dense[of a "min c b"] show "\y\{a<.. T \ y \ a" by (metis atLeastLessThan_iff greaterThanLessThan_iff min_less_iff_conj not_le order.strict_implies_order subset_eq) qed lemma islimpt_greaterThanLessThan2: fixes a b::"'a::{linorder_topology, dense_order}" assumes "a < b" shows "b islimpt {a<.. T" from open_left[OF this \a < b\] obtain c where c: "c < b" "{c<..b} \ T" by auto with assms dense[of "max a c" b] show "\y\{a<.. T \ y \ b" by (metis greaterThanAtMost_iff greaterThanLessThan_iff max_less_iff_conj not_le order.strict_implies_order subset_eq) qed lemma closure_greaterThanLessThan[simp]: fixes a b::"'a::{linorder_topology, dense_order}" shows "a < b \ closure {a <..< b} = {a .. b}" (is "_ \ ?l = ?r") proof have "?l \ closure ?r" by (rule closure_mono) auto thus "closure {a<.. {a..b}" by simp qed (auto simp: closure_def order.order_iff_strict islimpt_greaterThanLessThan1 islimpt_greaterThanLessThan2) lemma closure_greaterThan[simp]: fixes a b::"'a::{no_top, linorder_topology, dense_order}" shows "closure {a<..} = {a..}" proof - from gt_ex obtain b where "a < b" by auto hence "{a<..} = {a<.. {b..}" by auto also have "closure \ = {a..}" using \a < b\ unfolding closure_Un by auto finally show ?thesis . qed lemma closure_lessThan[simp]: fixes b::"'a::{no_bot, linorder_topology, dense_order}" shows "closure {.. {..a}" by auto also have "closure \ = {..b}" using \a < b\ unfolding closure_Un by auto finally show ?thesis . qed lemma closure_atLeastLessThan[simp]: fixes a b::"'a::{linorder_topology, dense_order}" assumes "a < b" shows "closure {a ..< b} = {a .. b}" proof - from assms have "{a ..< b} = {a} \ {a <..< b}" by auto also have "closure \ = {a .. b}" unfolding closure_Un by (auto simp: assms less_imp_le) finally show ?thesis . qed lemma closure_greaterThanAtMost[simp]: fixes a b::"'a::{linorder_topology, dense_order}" assumes "a < b" shows "closure {a <.. b} = {a .. b}" proof - from assms have "{a <.. b} = {b} \ {a <..< b}" by auto also have "closure \ = {a .. b}" unfolding closure_Un by (auto simp: assms less_imp_le) finally show ?thesis . qed end \ No newline at end of file diff --git a/src/HOL/Analysis/Linear_Algebra.thy b/src/HOL/Analysis/Linear_Algebra.thy --- a/src/HOL/Analysis/Linear_Algebra.thy +++ b/src/HOL/Analysis/Linear_Algebra.thy @@ -1,1972 +1,1882 @@ (* Title: HOL/Analysis/Linear_Algebra.thy Author: Amine Chaieb, University of Cambridge *) section \Elementary Linear Algebra on Euclidean Spaces\ theory Linear_Algebra imports Euclidean_Space "HOL-Library.Infinite_Set" begin lemma linear_simps: assumes "bounded_linear f" shows "f (a + b) = f a + f b" "f (a - b) = f a - f b" "f 0 = 0" "f (- a) = - f a" "f (s *\<^sub>R v) = s *\<^sub>R (f v)" proof - interpret f: bounded_linear f by fact show "f (a + b) = f a + f b" by (rule f.add) show "f (a - b) = f a - f b" by (rule f.diff) show "f 0 = 0" by (rule f.zero) show "f (- a) = - f a" by (rule f.neg) show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scale) qed lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x \ (UNIV::'a::finite set)}" using finite finite_image_set by blast lemma substdbasis_expansion_unique: includes inner_syntax assumes d: "d \ Basis" shows "(\i\d. f i *\<^sub>R i) = (x::'a::euclidean_space) \ (\i\Basis. (i \ d \ f i = x \ i) \ (i \ d \ x \ i = 0))" proof - have *: "\x a b P. x * (if P then a else b) = (if P then x * a else x * b)" by auto have **: "finite d" by (auto intro: finite_subset[OF assms]) have ***: "\i. i \ Basis \ (\i\d. f i *\<^sub>R i) \ i = (\x\d. if x = i then f x else 0)" using d by (auto intro!: sum.cong simp: inner_Basis inner_sum_left) show ?thesis unfolding euclidean_eq_iff[where 'a='a] by (auto simp: sum.delta[OF **] ***) qed lemma independent_substdbasis: "d \ Basis \ independent d" by (rule independent_mono[OF independent_Basis]) lemma subset_translation_eq [simp]: fixes a :: "'a::real_vector" shows "(+) a ` s \ (+) a ` t \ s \ t" by auto lemma translate_inj_on: fixes A :: "'a::ab_group_add set" shows "inj_on (\x. a + x) A" unfolding inj_on_def by auto lemma translation_assoc: fixes a b :: "'a::ab_group_add" shows "(\x. b + x) ` ((\x. a + x) ` S) = (\x. (a + b) + x) ` S" by auto lemma translation_invert: fixes a :: "'a::ab_group_add" assumes "(\x. a + x) ` A = (\x. a + x) ` B" shows "A = B" proof - have "(\x. -a + x) ` ((\x. a + x) ` A) = (\x. - a + x) ` ((\x. a + x) ` B)" using assms by auto then show ?thesis using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto qed lemma translation_galois: fixes a :: "'a::ab_group_add" shows "T = ((\x. a + x) ` S) \ S = ((\x. (- a) + x) ` T)" using translation_assoc[of "-a" a S] apply auto using translation_assoc[of a "-a" T] apply auto done lemma translation_inverse_subset: assumes "((\x. - a + x) ` V) \ (S :: 'n::ab_group_add set)" shows "V \ ((\x. a + x) ` S)" proof - { fix x assume "x \ V" then have "x-a \ S" using assms by auto then have "x \ {a + v |v. v \ S}" apply auto apply (rule exI[of _ "x-a"], simp) done then have "x \ ((\x. a+x) ` S)" by auto } then show ?thesis by auto qed subsection\<^marker>\tag unimportant\ \More interesting properties of the norm\ unbundle inner_syntax text\Equality of vectors in terms of \<^term>\(\)\ products.\ lemma linear_componentwise: fixes f:: "'a::euclidean_space \ 'b::real_inner" assumes lf: "linear f" shows "(f x) \ j = (\i\Basis. (x\i) * (f i\j))" (is "?lhs = ?rhs") proof - interpret linear f by fact have "?rhs = (\i\Basis. (x\i) *\<^sub>R (f i))\j" by (simp add: inner_sum_left) then show ?thesis by (simp add: euclidean_representation sum[symmetric] scale[symmetric]) qed lemma vector_eq: "x = y \ x \ x = x \ y \ y \ y = x \ x" (is "?lhs \ ?rhs") proof assume ?lhs then show ?rhs by simp next assume ?rhs then have "x \ x - x \ y = 0 \ x \ y - y \ y = 0" by simp then have "x \ (x - y) = 0 \ y \ (x - y) = 0" by (simp add: inner_diff inner_commute) then have "(x - y) \ (x - y) = 0" by (simp add: field_simps inner_diff inner_commute) then show "x = y" by simp qed lemma norm_triangle_half_r: "norm (y - x1) < e / 2 \ norm (y - x2) < e / 2 \ norm (x1 - x2) < e" using dist_triangle_half_r unfolding dist_norm[symmetric] by auto lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" and "norm (x' - y) < e / 2" shows "norm (x - x') < e" using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]] unfolding dist_norm[symmetric] . lemma abs_triangle_half_r: fixes y :: "'a::linordered_field" shows "abs (y - x1) < e / 2 \ abs (y - x2) < e / 2 \ abs (x1 - x2) < e" by linarith lemma abs_triangle_half_l: fixes y :: "'a::linordered_field" assumes "abs (x - y) < e / 2" and "abs (x' - y) < e / 2" shows "abs (x - x') < e" using assms by linarith lemma sum_clauses: shows "sum f {} = 0" and "finite S \ sum f (insert x S) = (if x \ S then sum f S else f x + sum f S)" by (auto simp add: insert_absorb) lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = z" proof assume "\x. x \ y = x \ z" then have "\x. x \ (y - z) = 0" by (simp add: inner_diff) then have "(y - z) \ (y - z) = 0" .. then show "y = z" by simp qed simp lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = y" proof assume "\z. x \ z = y \ z" then have "\z. (x - y) \ z = 0" by (simp add: inner_diff) then have "(x - y) \ (x - y) = 0" .. then show "x = y" by simp qed simp subsection \Substandard Basis\ lemma ex_card: assumes "n \ card A" shows "\S\A. card S = n" proof (cases "finite A") case True from ex_bij_betw_nat_finite[OF this] obtain f where f: "bij_betw f {0..n \ card A\ have "{..< n} \ {..< card A}" "inj_on f {..< n}" by (auto simp: bij_betw_def intro: subset_inj_on) ultimately have "f ` {..< n} \ A" "card (f ` {..< n}) = n" by (auto simp: bij_betw_def card_image) then show ?thesis by blast next case False with \n \ card A\ show ?thesis by force qed lemma subspace_substandard: "subspace {x::'a::euclidean_space. (\i\Basis. P i \ x\i = 0)}" by (auto simp: subspace_def inner_add_left) lemma dim_substandard: assumes d: "d \ Basis" shows "dim {x::'a::euclidean_space. \i\Basis. i \ d \ x\i = 0} = card d" (is "dim ?A = _") proof (rule dim_unique) from d show "d \ ?A" by (auto simp: inner_Basis) from d show "independent d" by (rule independent_mono [OF independent_Basis]) have "x \ span d" if "\i\Basis. i \ d \ x \ i = 0" for x proof - have "finite d" by (rule finite_subset [OF d finite_Basis]) then have "(\i\d. (x \ i) *\<^sub>R i) \ span d" by (simp add: span_sum span_clauses) also have "(\i\d. (x \ i) *\<^sub>R i) = (\i\Basis. (x \ i) *\<^sub>R i)" by (rule sum.mono_neutral_cong_left [OF finite_Basis d]) (auto simp: that) finally show "x \ span d" by (simp only: euclidean_representation) qed then show "?A \ span d" by auto qed simp subsection \Orthogonality\ definition\<^marker>\tag important\ (in real_inner) "orthogonal x y \ x \ y = 0" context real_inner begin lemma orthogonal_self: "orthogonal x x \ x = 0" by (simp add: orthogonal_def) lemma orthogonal_clauses: "orthogonal a 0" "orthogonal a x \ orthogonal a (c *\<^sub>R x)" "orthogonal a x \ orthogonal a (- x)" "orthogonal a x \ orthogonal a y \ orthogonal a (x + y)" "orthogonal a x \ orthogonal a y \ orthogonal a (x - y)" "orthogonal 0 a" "orthogonal x a \ orthogonal (c *\<^sub>R x) a" "orthogonal x a \ orthogonal (- x) a" "orthogonal x a \ orthogonal y a \ orthogonal (x + y) a" "orthogonal x a \ orthogonal y a \ orthogonal (x - y) a" unfolding orthogonal_def inner_add inner_diff by auto end lemma orthogonal_commute: "orthogonal x y \ orthogonal y x" by (simp add: orthogonal_def inner_commute) lemma orthogonal_scaleR [simp]: "c \ 0 \ orthogonal (c *\<^sub>R x) = orthogonal x" by (rule ext) (simp add: orthogonal_def) lemma pairwise_ortho_scaleR: "pairwise (\i j. orthogonal (f i) (g j)) B \ pairwise (\i j. orthogonal (a i *\<^sub>R f i) (a j *\<^sub>R g j)) B" by (auto simp: pairwise_def orthogonal_clauses) lemma orthogonal_rvsum: "\finite s; \y. y \ s \ orthogonal x (f y)\ \ orthogonal x (sum f s)" by (induction s rule: finite_induct) (auto simp: orthogonal_clauses) lemma orthogonal_lvsum: "\finite s; \x. x \ s \ orthogonal (f x) y\ \ orthogonal (sum f s) y" by (induction s rule: finite_induct) (auto simp: orthogonal_clauses) lemma norm_add_Pythagorean: assumes "orthogonal a b" shows "norm(a + b) ^ 2 = norm a ^ 2 + norm b ^ 2" proof - from assms have "(a - (0 - b)) \ (a - (0 - b)) = a \ a - (0 - b \ b)" by (simp add: algebra_simps orthogonal_def inner_commute) then show ?thesis by (simp add: power2_norm_eq_inner) qed lemma norm_sum_Pythagorean: assumes "finite I" "pairwise (\i j. orthogonal (f i) (f j)) I" shows "(norm (sum f I))\<^sup>2 = (\i\I. (norm (f i))\<^sup>2)" using assms proof (induction I rule: finite_induct) case empty then show ?case by simp next case (insert x I) then have "orthogonal (f x) (sum f I)" by (metis pairwise_insert orthogonal_rvsum) with insert show ?case by (simp add: pairwise_insert norm_add_Pythagorean) qed subsection \Orthogonality of a transformation\ definition\<^marker>\tag important\ "orthogonal_transformation f \ linear f \ (\v w. f v \ f w = v \ w)" lemma\<^marker>\tag unimportant\ orthogonal_transformation: "orthogonal_transformation f \ linear f \ (\v. norm (f v) = norm v)" unfolding orthogonal_transformation_def apply auto apply (erule_tac x=v in allE)+ apply (simp add: norm_eq_sqrt_inner) apply (simp add: dot_norm linear_add[symmetric]) done lemma\<^marker>\tag unimportant\ orthogonal_transformation_id [simp]: "orthogonal_transformation (\x. x)" by (simp add: linear_iff orthogonal_transformation_def) lemma\<^marker>\tag unimportant\ orthogonal_orthogonal_transformation: "orthogonal_transformation f \ orthogonal (f x) (f y) \ orthogonal x y" by (simp add: orthogonal_def orthogonal_transformation_def) lemma\<^marker>\tag unimportant\ orthogonal_transformation_compose: "\orthogonal_transformation f; orthogonal_transformation g\ \ orthogonal_transformation(f \ g)" by (auto simp: orthogonal_transformation_def linear_compose) lemma\<^marker>\tag unimportant\ orthogonal_transformation_neg: "orthogonal_transformation(\x. -(f x)) \ orthogonal_transformation f" by (auto simp: orthogonal_transformation_def dest: linear_compose_neg) lemma\<^marker>\tag unimportant\ orthogonal_transformation_scaleR: "orthogonal_transformation f \ f (c *\<^sub>R v) = c *\<^sub>R f v" by (simp add: linear_iff orthogonal_transformation_def) lemma\<^marker>\tag unimportant\ orthogonal_transformation_linear: "orthogonal_transformation f \ linear f" by (simp add: orthogonal_transformation_def) lemma\<^marker>\tag unimportant\ orthogonal_transformation_inj: "orthogonal_transformation f \ inj f" unfolding orthogonal_transformation_def inj_on_def by (metis vector_eq) lemma\<^marker>\tag unimportant\ orthogonal_transformation_surj: "orthogonal_transformation f \ surj f" for f :: "'a::euclidean_space \ 'a::euclidean_space" by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear) lemma\<^marker>\tag unimportant\ orthogonal_transformation_bij: "orthogonal_transformation f \ bij f" for f :: "'a::euclidean_space \ 'a::euclidean_space" by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj) lemma\<^marker>\tag unimportant\ orthogonal_transformation_inv: "orthogonal_transformation f \ orthogonal_transformation (inv f)" for f :: "'a::euclidean_space \ 'a::euclidean_space" by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj) lemma\<^marker>\tag unimportant\ orthogonal_transformation_norm: "orthogonal_transformation f \ norm (f x) = norm x" by (metis orthogonal_transformation) subsection \Bilinear functions\ definition\<^marker>\tag important\ bilinear :: "('a::real_vector \ 'b::real_vector \ 'c::real_vector) \ bool" where "bilinear f \ (\x. linear (\y. f x y)) \ (\y. linear (\x. f x y))" lemma bilinear_ladd: "bilinear h \ h (x + y) z = h x z + h y z" by (simp add: bilinear_def linear_iff) lemma bilinear_radd: "bilinear h \ h x (y + z) = h x y + h x z" by (simp add: bilinear_def linear_iff) lemma bilinear_times: fixes c::"'a::real_algebra" shows "bilinear (\x y::'a. x*y)" by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI) lemma bilinear_lmul: "bilinear h \ h (c *\<^sub>R x) y = c *\<^sub>R h x y" by (simp add: bilinear_def linear_iff) lemma bilinear_rmul: "bilinear h \ h x (c *\<^sub>R y) = c *\<^sub>R h x y" by (simp add: bilinear_def linear_iff) lemma bilinear_lneg: "bilinear h \ h (- x) y = - h x y" by (drule bilinear_lmul [of _ "- 1"]) simp lemma bilinear_rneg: "bilinear h \ h x (- y) = - h x y" by (drule bilinear_rmul [of _ _ "- 1"]) simp lemma (in ab_group_add) eq_add_iff: "x = x + y \ y = 0" using add_left_imp_eq[of x y 0] by auto lemma bilinear_lzero: assumes "bilinear h" shows "h 0 x = 0" using bilinear_ladd [OF assms, of 0 0 x] by (simp add: eq_add_iff field_simps) lemma bilinear_rzero: assumes "bilinear h" shows "h x 0 = 0" using bilinear_radd [OF assms, of x 0 0 ] by (simp add: eq_add_iff field_simps) lemma bilinear_lsub: "bilinear h \ h (x - y) z = h x z - h y z" using bilinear_ladd [of h x "- y"] by (simp add: bilinear_lneg) lemma bilinear_rsub: "bilinear h \ h z (x - y) = h z x - h z y" using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg) lemma bilinear_sum: assumes "bilinear h" shows "h (sum f S) (sum g T) = sum (\(i,j). h (f i) (g j)) (S \ T) " proof - interpret l: linear "\x. h x y" for y using assms by (simp add: bilinear_def) interpret r: linear "\y. h x y" for x using assms by (simp add: bilinear_def) have "h (sum f S) (sum g T) = sum (\x. h (f x) (sum g T)) S" by (simp add: l.sum) also have "\ = sum (\x. sum (\y. h (f x) (g y)) T) S" by (rule sum.cong) (simp_all add: r.sum) finally show ?thesis unfolding sum.cartesian_product . qed subsection \Adjoints\ definition\<^marker>\tag important\ adjoint :: "(('a::real_inner) \ ('b::real_inner)) \ 'b \ 'a" where "adjoint f = (SOME f'. \x y. f x \ y = x \ f' y)" lemma adjoint_unique: assumes "\x y. inner (f x) y = inner x (g y)" shows "adjoint f = g" unfolding adjoint_def proof (rule some_equality) show "\x y. inner (f x) y = inner x (g y)" by (rule assms) next fix h assume "\x y. inner (f x) y = inner x (h y)" then have "\x y. inner x (g y) = inner x (h y)" using assms by simp then have "\x y. inner x (g y - h y) = 0" by (simp add: inner_diff_right) then have "\y. inner (g y - h y) (g y - h y) = 0" by simp then have "\y. h y = g y" by simp then show "h = g" by (simp add: ext) qed text \TODO: The following lemmas about adjoints should hold for any Hilbert space (i.e. complete inner product space). (see \<^url>\https://en.wikipedia.org/wiki/Hermitian_adjoint\) \ lemma adjoint_works: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes lf: "linear f" shows "x \ adjoint f y = f x \ y" proof - interpret linear f by fact have "\y. \w. \x. f x \ y = x \ w" proof (intro allI exI) fix y :: "'m" and x let ?w = "(\i\Basis. (f i \ y) *\<^sub>R i) :: 'n" have "f x \ y = f (\i\Basis. (x \ i) *\<^sub>R i) \ y" by (simp add: euclidean_representation) also have "\ = (\i\Basis. (x \ i) *\<^sub>R f i) \ y" by (simp add: sum scale) finally show "f x \ y = x \ ?w" by (simp add: inner_sum_left inner_sum_right mult.commute) qed then show ?thesis unfolding adjoint_def choice_iff by (intro someI2_ex[where Q="\f'. x \ f' y = f x \ y"]) auto qed lemma adjoint_clauses: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes lf: "linear f" shows "x \ adjoint f y = f x \ y" and "adjoint f y \ x = y \ f x" by (simp_all add: adjoint_works[OF lf] inner_commute) lemma adjoint_linear: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes lf: "linear f" shows "linear (adjoint f)" by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m] adjoint_clauses[OF lf] inner_distrib) lemma adjoint_adjoint: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes lf: "linear f" shows "adjoint (adjoint f) = f" by (rule adjoint_unique, simp add: adjoint_clauses [OF lf]) -subsection \Archimedean properties and useful consequences\ - -text\Bernoulli's inequality\ -proposition Bernoulli_inequality: - fixes x :: real - assumes "-1 \ x" - shows "1 + n * x \ (1 + x) ^ n" -proof (induct n) - case 0 - then show ?case by simp -next - case (Suc n) - have "1 + Suc n * x \ 1 + (Suc n)*x + n * x^2" - by (simp add: algebra_simps) - also have "... = (1 + x) * (1 + n*x)" - by (auto simp: power2_eq_square algebra_simps of_nat_Suc) - also have "... \ (1 + x) ^ Suc n" - using Suc.hyps assms mult_left_mono by fastforce - finally show ?case . -qed - -corollary Bernoulli_inequality_even: - fixes x :: real - assumes "even n" - shows "1 + n * x \ (1 + x) ^ n" -proof (cases "-1 \ x \ n=0") - case True - then show ?thesis - by (auto simp: Bernoulli_inequality) -next - case False - then have "real n \ 1" - by simp - with False have "n * x \ -1" - by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one) - then have "1 + n * x \ 0" - by auto - also have "... \ (1 + x) ^ n" - using assms - using zero_le_even_power by blast - finally show ?thesis . -qed - -corollary real_arch_pow: - fixes x :: real - assumes x: "1 < x" - shows "\n. y < x^n" -proof - - from x have x0: "x - 1 > 0" - by arith - from reals_Archimedean3[OF x0, rule_format, of y] - obtain n :: nat where n: "y < real n * (x - 1)" by metis - from x0 have x00: "x- 1 \ -1" by arith - from Bernoulli_inequality[OF x00, of n] n - have "y < x^n" by auto - then show ?thesis by metis -qed - -corollary real_arch_pow_inv: - fixes x y :: real - assumes y: "y > 0" - and x1: "x < 1" - shows "\n. x^n < y" -proof (cases "x > 0") - case True - with x1 have ix: "1 < 1/x" by (simp add: field_simps) - from real_arch_pow[OF ix, of "1/y"] - obtain n where n: "1/y < (1/x)^n" by blast - then show ?thesis using y \x > 0\ - by (auto simp add: field_simps) -next - case False - with y x1 show ?thesis - by (metis less_le_trans not_less power_one_right) -qed - -lemma forall_pos_mono: - "(\d e::real. d < e \ P d \ P e) \ - (\n::nat. n \ 0 \ P (inverse (real n))) \ (\e. 0 < e \ P e)" - by (metis real_arch_inverse) - -lemma forall_pos_mono_1: - "(\d e::real. d < e \ P d \ P e) \ - (\n. P (inverse (real (Suc n)))) \ 0 < e \ P e" - apply (rule forall_pos_mono) - apply auto - apply (metis Suc_pred of_nat_Suc) - done - - subsection\<^marker>\tag unimportant\ \Euclidean Spaces as Typeclass\ lemma independent_Basis: "independent Basis" by (rule independent_Basis) lemma span_Basis [simp]: "span Basis = UNIV" by (rule span_Basis) lemma in_span_Basis: "x \ span Basis" unfolding span_Basis .. subsection\<^marker>\tag unimportant\ \Linearity and Bilinearity continued\ lemma linear_bounded: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" assumes lf: "linear f" shows "\B. \x. norm (f x) \ B * norm x" proof interpret linear f by fact let ?B = "\b\Basis. norm (f b)" show "\x. norm (f x) \ ?B * norm x" proof fix x :: 'a let ?g = "\b. (x \ b) *\<^sub>R f b" have "norm (f x) = norm (f (\b\Basis. (x \ b) *\<^sub>R b))" unfolding euclidean_representation .. also have "\ = norm (sum ?g Basis)" by (simp add: sum scale) finally have th0: "norm (f x) = norm (sum ?g Basis)" . have th: "norm (?g i) \ norm (f i) * norm x" if "i \ Basis" for i proof - from Basis_le_norm[OF that, of x] show "norm (?g i) \ norm (f i) * norm x" unfolding norm_scaleR by (metis mult.commute mult_left_mono norm_ge_zero) qed from sum_norm_le[of _ ?g, OF th] show "norm (f x) \ ?B * norm x" unfolding th0 sum_distrib_right by metis qed qed lemma linear_conv_bounded_linear: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" shows "linear f \ bounded_linear f" proof assume "linear f" then interpret f: linear f . show "bounded_linear f" proof have "\B. \x. norm (f x) \ B * norm x" using \linear f\ by (rule linear_bounded) then show "\K. \x. norm (f x) \ norm x * K" by (simp add: mult.commute) qed next assume "bounded_linear f" then interpret f: bounded_linear f . show "linear f" .. qed lemmas linear_linear = linear_conv_bounded_linear[symmetric] lemma inj_linear_imp_inv_bounded_linear: fixes f::"'a::euclidean_space \ 'a" shows "\bounded_linear f; inj f\ \ bounded_linear (inv f)" by (simp add: inj_linear_imp_inv_linear linear_linear) lemma linear_bounded_pos: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" assumes lf: "linear f" obtains B where "B > 0" "\x. norm (f x) \ B * norm x" proof - have "\B > 0. \x. norm (f x) \ norm x * B" using lf unfolding linear_conv_bounded_linear by (rule bounded_linear.pos_bounded) with that show ?thesis by (auto simp: mult.commute) qed lemma linear_invertible_bounded_below_pos: fixes f :: "'a::real_normed_vector \ 'b::euclidean_space" assumes "linear f" "linear g" "g \ f = id" obtains B where "B > 0" "\x. B * norm x \ norm(f x)" proof - obtain B where "B > 0" and B: "\x. norm (g x) \ B * norm x" using linear_bounded_pos [OF \linear g\] by blast show thesis proof show "0 < 1/B" by (simp add: \B > 0\) show "1/B * norm x \ norm (f x)" for x proof - have "1/B * norm x = 1/B * norm (g (f x))" using assms by (simp add: pointfree_idE) also have "\ \ norm (f x)" using B [of "f x"] by (simp add: \B > 0\ mult.commute pos_divide_le_eq) finally show ?thesis . qed qed qed lemma linear_inj_bounded_below_pos: fixes f :: "'a::real_normed_vector \ 'b::euclidean_space" assumes "linear f" "inj f" obtains B where "B > 0" "\x. B * norm x \ norm(f x)" using linear_injective_left_inverse [OF assms] linear_invertible_bounded_below_pos assms by blast lemma bounded_linearI': fixes f ::"'a::euclidean_space \ 'b::real_normed_vector" assumes "\x y. f (x + y) = f x + f y" and "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" shows "bounded_linear f" using assms linearI linear_conv_bounded_linear by blast lemma bilinear_bounded: fixes h :: "'m::euclidean_space \ 'n::euclidean_space \ 'k::real_normed_vector" assumes bh: "bilinear h" shows "\B. \x y. norm (h x y) \ B * norm x * norm y" proof (clarify intro!: exI[of _ "\i\Basis. \j\Basis. norm (h i j)"]) fix x :: 'm fix y :: 'n have "norm (h x y) = norm (h (sum (\i. (x \ i) *\<^sub>R i) Basis) (sum (\i. (y \ i) *\<^sub>R i) Basis))" by (simp add: euclidean_representation) also have "\ = norm (sum (\ (i,j). h ((x \ i) *\<^sub>R i) ((y \ j) *\<^sub>R j)) (Basis \ Basis))" unfolding bilinear_sum[OF bh] .. finally have th: "norm (h x y) = \" . have "\i j. \i \ Basis; j \ Basis\ \ \x \ i\ * (\y \ j\ * norm (h i j)) \ norm x * (norm y * norm (h i j))" by (auto simp add: zero_le_mult_iff Basis_le_norm mult_mono) then show "norm (h x y) \ (\i\Basis. \j\Basis. norm (h i j)) * norm x * norm y" unfolding sum_distrib_right th sum.cartesian_product by (clarsimp simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps simp del: scaleR_scaleR intro!: sum_norm_le) qed lemma bilinear_conv_bounded_bilinear: fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" shows "bilinear h \ bounded_bilinear h" proof assume "bilinear h" show "bounded_bilinear h" proof fix x y z show "h (x + y) z = h x z + h y z" using \bilinear h\ unfolding bilinear_def linear_iff by simp next fix x y z show "h x (y + z) = h x y + h x z" using \bilinear h\ unfolding bilinear_def linear_iff by simp next show "h (scaleR r x) y = scaleR r (h x y)" "h x (scaleR r y) = scaleR r (h x y)" for r x y using \bilinear h\ unfolding bilinear_def linear_iff by simp_all next have "\B. \x y. norm (h x y) \ B * norm x * norm y" using \bilinear h\ by (rule bilinear_bounded) then show "\K. \x y. norm (h x y) \ norm x * norm y * K" by (simp add: ac_simps) qed next assume "bounded_bilinear h" then interpret h: bounded_bilinear h . show "bilinear h" unfolding bilinear_def linear_conv_bounded_linear using h.bounded_linear_left h.bounded_linear_right by simp qed lemma bilinear_bounded_pos: fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" assumes bh: "bilinear h" shows "\B > 0. \x y. norm (h x y) \ B * norm x * norm y" proof - have "\B > 0. \x y. norm (h x y) \ norm x * norm y * B" using bh [unfolded bilinear_conv_bounded_bilinear] by (rule bounded_bilinear.pos_bounded) then show ?thesis by (simp only: ac_simps) qed lemma bounded_linear_imp_has_derivative: "bounded_linear f \ (f has_derivative f) net" by (auto simp add: has_derivative_def linear_diff linear_linear linear_def dest: bounded_linear.linear) lemma linear_imp_has_derivative: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" shows "linear f \ (f has_derivative f) net" by (simp add: bounded_linear_imp_has_derivative linear_conv_bounded_linear) lemma bounded_linear_imp_differentiable: "bounded_linear f \ f differentiable net" using bounded_linear_imp_has_derivative differentiable_def by blast lemma linear_imp_differentiable: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" shows "linear f \ f differentiable net" by (metis linear_imp_has_derivative differentiable_def) subsection\<^marker>\tag unimportant\ \We continue\ lemma independent_bound: fixes S :: "'a::euclidean_space set" shows "independent S \ finite S \ card S \ DIM('a)" by (metis dim_subset_UNIV finiteI_independent dim_span_eq_card_independent) lemmas independent_imp_finite = finiteI_independent corollary fixes S :: "'a::euclidean_space set" assumes "independent S" shows independent_card_le:"card S \ DIM('a)" using assms independent_bound by auto lemma dependent_biggerset: fixes S :: "'a::euclidean_space set" shows "(finite S \ card S > DIM('a)) \ dependent S" by (metis independent_bound not_less) text \Picking an orthogonal replacement for a spanning set.\ lemma vector_sub_project_orthogonal: fixes b x :: "'a::euclidean_space" shows "b \ (x - ((b \ x) / (b \ b)) *\<^sub>R b) = 0" unfolding inner_simps by auto lemma pairwise_orthogonal_insert: assumes "pairwise orthogonal S" and "\y. y \ S \ orthogonal x y" shows "pairwise orthogonal (insert x S)" using assms unfolding pairwise_def by (auto simp add: orthogonal_commute) lemma basis_orthogonal: fixes B :: "'a::real_inner set" assumes fB: "finite B" shows "\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C" (is " \C. ?P B C") using fB proof (induct rule: finite_induct) case empty then show ?case apply (rule exI[where x="{}"]) apply (auto simp add: pairwise_def) done next case (insert a B) note fB = \finite B\ and aB = \a \ B\ from \\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C\ obtain C where C: "finite C" "card C \ card B" "span C = span B" "pairwise orthogonal C" by blast let ?a = "a - sum (\x. (x \ a / (x \ x)) *\<^sub>R x) C" let ?C = "insert ?a C" from C(1) have fC: "finite ?C" by simp from fB aB C(1,2) have cC: "card ?C \ card (insert a B)" by (simp add: card_insert_if) { fix x k have th0: "\(a::'a) b c. a - (b - c) = c + (a - b)" by (simp add: field_simps) have "x - k *\<^sub>R (a - (\x\C. (x \ a / (x \ x)) *\<^sub>R x)) \ span C \ x - k *\<^sub>R a \ span C" apply (simp only: scaleR_right_diff_distrib th0) apply (rule span_add_eq) apply (rule span_scale) apply (rule span_sum) apply (rule span_scale) apply (rule span_base) apply assumption done } then have SC: "span ?C = span (insert a B)" unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto { fix y assume yC: "y \ C" then have Cy: "C = insert y (C - {y})" by blast have fth: "finite (C - {y})" using C by simp have "orthogonal ?a y" unfolding orthogonal_def unfolding inner_diff inner_sum_left right_minus_eq unfolding sum.remove [OF \finite C\ \y \ C\] apply (clarsimp simp add: inner_commute[of y a]) apply (rule sum.neutral) apply clarsimp apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) using \y \ C\ by auto } with \pairwise orthogonal C\ have CPO: "pairwise orthogonal ?C" by (rule pairwise_orthogonal_insert) from fC cC SC CPO have "?P (insert a B) ?C" by blast then show ?case by blast qed lemma orthogonal_basis_exists: fixes V :: "('a::euclidean_space) set" shows "\B. independent B \ B \ span V \ V \ span B \ (card B = dim V) \ pairwise orthogonal B" proof - from basis_exists[of V] obtain B where B: "B \ V" "independent B" "V \ span B" "card B = dim V" by force from B have fB: "finite B" "card B = dim V" using independent_bound by auto from basis_orthogonal[OF fB(1)] obtain C where C: "finite C" "card C \ card B" "span C = span B" "pairwise orthogonal C" by blast from C B have CSV: "C \ span V" by (metis span_superset span_mono subset_trans) from span_mono[OF B(3)] C have SVC: "span V \ span C" by (simp add: span_span) from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB have iC: "independent C" by (simp add: dim_span) from C fB have "card C \ dim V" by simp moreover have "dim V \ card C" using span_card_ge_dim[OF CSV SVC C(1)] by simp ultimately have CdV: "card C = dim V" using C(1) by simp from C B CSV CdV iC show ?thesis by auto qed text \Low-dimensional subset is in a hyperplane (weak orthogonal complement).\ lemma span_not_univ_orthogonal: fixes S :: "'a::euclidean_space set" assumes sU: "span S \ UNIV" shows "\a::'a. a \ 0 \ (\x \ span S. a \ x = 0)" proof - from sU obtain a where a: "a \ span S" by blast from orthogonal_basis_exists obtain B where B: "independent B" "B \ span S" "S \ span B" "card B = dim S" "pairwise orthogonal B" by blast from B have fB: "finite B" "card B = dim S" using independent_bound by auto from span_mono[OF B(2)] span_mono[OF B(3)] have sSB: "span S = span B" by (simp add: span_span) let ?a = "a - sum (\b. (a \ b / (b \ b)) *\<^sub>R b) B" have "sum (\b. (a \ b / (b \ b)) *\<^sub>R b) B \ span S" unfolding sSB apply (rule span_sum) apply (rule span_scale) apply (rule span_base) apply assumption done with a have a0:"?a \ 0" by auto have "?a \ x = 0" if "x\span B" for x proof (rule span_induct [OF that]) show "subspace {x. ?a \ x = 0}" by (auto simp add: subspace_def inner_add) next { fix x assume x: "x \ B" from x have B': "B = insert x (B - {x})" by blast have fth: "finite (B - {x})" using fB by simp have "?a \ x = 0" apply (subst B') using fB fth unfolding sum_clauses(2)[OF fth] apply simp unfolding inner_simps apply (clarsimp simp add: inner_add inner_sum_left) apply (rule sum.neutral, rule ballI) apply (simp only: inner_commute) apply (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format]) done } then show "?a \ x = 0" if "x \ B" for x using that by blast qed with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"]) qed lemma span_not_univ_subset_hyperplane: fixes S :: "'a::euclidean_space set" assumes SU: "span S \ UNIV" shows "\ a. a \0 \ span S \ {x. a \ x = 0}" using span_not_univ_orthogonal[OF SU] by auto lemma lowdim_subset_hyperplane: fixes S :: "'a::euclidean_space set" assumes d: "dim S < DIM('a)" shows "\a::'a. a \ 0 \ span S \ {x. a \ x = 0}" proof - { assume "span S = UNIV" then have "dim (span S) = dim (UNIV :: ('a) set)" by simp then have "dim S = DIM('a)" by (metis Euclidean_Space.dim_UNIV dim_span) with d have False by arith } then have th: "span S \ UNIV" by blast from span_not_univ_subset_hyperplane[OF th] show ?thesis . qed lemma linear_eq_stdbasis: fixes f :: "'a::euclidean_space \ _" assumes lf: "linear f" and lg: "linear g" and fg: "\b. b \ Basis \ f b = g b" shows "f = g" using linear_eq_on_span[OF lf lg, of Basis] fg by auto text \Similar results for bilinear functions.\ lemma bilinear_eq: assumes bf: "bilinear f" and bg: "bilinear g" and SB: "S \ span B" and TC: "T \ span C" and "x\S" "y\T" and fg: "\x y. \x \ B; y\ C\ \ f x y = g x y" shows "f x y = g x y" proof - let ?P = "{x. \y\ span C. f x y = g x y}" from bf bg have sp: "subspace ?P" unfolding bilinear_def linear_iff subspace_def bf bg by (auto simp add: span_zero bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf]) have sfg: "\x. x \ B \ subspace {a. f x a = g x a}" apply (auto simp add: subspace_def) using bf bg unfolding bilinear_def linear_iff apply (auto simp add: span_zero bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf]) done have "\y\ span C. f x y = g x y" if "x \ span B" for x apply (rule span_induct [OF that sp]) using fg sfg span_induct by blast then show ?thesis using SB TC assms by auto qed lemma bilinear_eq_stdbasis: fixes f :: "'a::euclidean_space \ 'b::euclidean_space \ _" assumes bf: "bilinear f" and bg: "bilinear g" and fg: "\i j. i \ Basis \ j \ Basis \ f i j = g i j" shows "f = g" using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg by blast subsection \Infinity norm\ definition\<^marker>\tag important\ "infnorm (x::'a::euclidean_space) = Sup {\x \ b\ |b. b \ Basis}" lemma infnorm_set_image: fixes x :: "'a::euclidean_space" shows "{\x \ i\ |i. i \ Basis} = (\i. \x \ i\) ` Basis" by blast lemma infnorm_Max: fixes x :: "'a::euclidean_space" shows "infnorm x = Max ((\i. \x \ i\) ` Basis)" by (simp add: infnorm_def infnorm_set_image cSup_eq_Max) lemma infnorm_set_lemma: fixes x :: "'a::euclidean_space" shows "finite {\x \ i\ |i. i \ Basis}" and "{\x \ i\ |i. i \ Basis} \ {}" unfolding infnorm_set_image by auto lemma infnorm_pos_le: fixes x :: "'a::euclidean_space" shows "0 \ infnorm x" by (simp add: infnorm_Max Max_ge_iff ex_in_conv) lemma infnorm_triangle: fixes x :: "'a::euclidean_space" shows "infnorm (x + y) \ infnorm x + infnorm y" proof - have *: "\a b c d :: real. \a\ \ c \ \b\ \ d \ \a + b\ \ c + d" by simp show ?thesis by (auto simp: infnorm_Max inner_add_left intro!: *) qed lemma infnorm_eq_0: fixes x :: "'a::euclidean_space" shows "infnorm x = 0 \ x = 0" proof - have "infnorm x \ 0 \ x = 0" unfolding infnorm_Max by (simp add: euclidean_all_zero_iff) then show ?thesis using infnorm_pos_le[of x] by simp qed lemma infnorm_0: "infnorm 0 = 0" by (simp add: infnorm_eq_0) lemma infnorm_neg: "infnorm (- x) = infnorm x" unfolding infnorm_def by simp lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)" by (metis infnorm_neg minus_diff_eq) lemma absdiff_infnorm: "\infnorm x - infnorm y\ \ infnorm (x - y)" proof - have *: "\(nx::real) n ny. nx \ n + ny \ ny \ n + nx \ \nx - ny\ \ n" by arith show ?thesis proof (rule *) from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"] show "infnorm x \ infnorm (x - y) + infnorm y" "infnorm y \ infnorm (x - y) + infnorm x" by (simp_all add: field_simps infnorm_neg) qed qed lemma real_abs_infnorm: "\infnorm x\ = infnorm x" using infnorm_pos_le[of x] by arith lemma Basis_le_infnorm: fixes x :: "'a::euclidean_space" shows "b \ Basis \ \x \ b\ \ infnorm x" by (simp add: infnorm_Max) lemma infnorm_mul: "infnorm (a *\<^sub>R x) = \a\ * infnorm x" unfolding infnorm_Max proof (safe intro!: Max_eqI) let ?B = "(\i. \x \ i\) ` Basis" { fix b :: 'a assume "b \ Basis" then show "\a *\<^sub>R x \ b\ \ \a\ * Max ?B" by (simp add: abs_mult mult_left_mono) next from Max_in[of ?B] obtain b where "b \ Basis" "Max ?B = \x \ b\" by (auto simp del: Max_in) then show "\a\ * Max ((\i. \x \ i\) ` Basis) \ (\i. \a *\<^sub>R x \ i\) ` Basis" by (intro image_eqI[where x=b]) (auto simp: abs_mult) } qed simp lemma infnorm_mul_lemma: "infnorm (a *\<^sub>R x) \ \a\ * infnorm x" unfolding infnorm_mul .. lemma infnorm_pos_lt: "infnorm x > 0 \ x \ 0" using infnorm_pos_le[of x] infnorm_eq_0[of x] by arith text \Prove that it differs only up to a bound from Euclidean norm.\ lemma infnorm_le_norm: "infnorm x \ norm x" by (simp add: Basis_le_norm infnorm_Max) lemma norm_le_infnorm: fixes x :: "'a::euclidean_space" shows "norm x \ sqrt DIM('a) * infnorm x" unfolding norm_eq_sqrt_inner id_def proof (rule real_le_lsqrt[OF inner_ge_zero]) show "sqrt DIM('a) * infnorm x \ 0" by (simp add: zero_le_mult_iff infnorm_pos_le) have "x \ x \ (\b\Basis. x \ b * (x \ b))" by (metis euclidean_inner order_refl) also have "... \ DIM('a) * \infnorm x\\<^sup>2" by (rule sum_bounded_above) (metis Basis_le_infnorm abs_le_square_iff power2_eq_square real_abs_infnorm) also have "... \ (sqrt DIM('a) * infnorm x)\<^sup>2" by (simp add: power_mult_distrib) finally show "x \ x \ (sqrt DIM('a) * infnorm x)\<^sup>2" . qed lemma tendsto_infnorm [tendsto_intros]: assumes "(f \ a) F" shows "((\x. infnorm (f x)) \ infnorm a) F" proof (rule tendsto_compose [OF LIM_I assms]) fix r :: real assume "r > 0" then show "\s>0. \x. x \ a \ norm (x - a) < s \ norm (infnorm x - infnorm a) < r" by (metis real_norm_def le_less_trans absdiff_infnorm infnorm_le_norm) qed text \Equality in Cauchy-Schwarz and triangle inequalities.\ lemma norm_cauchy_schwarz_eq: "x \ y = norm x * norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" (is "?lhs \ ?rhs") proof (cases "x=0") case True then show ?thesis by auto next case False from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"] have "?rhs \ (norm y * (norm y * norm x * norm x - norm x * (x \ y)) - norm x * (norm y * (y \ x) - norm x * norm y * norm y) = 0)" using False unfolding inner_simps by (auto simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps) also have "\ \ (2 * norm x * norm y * (norm x * norm y - x \ y) = 0)" using False by (simp add: field_simps inner_commute) also have "\ \ ?lhs" using False by auto finally show ?thesis by metis qed lemma norm_cauchy_schwarz_abs_eq: "\x \ y\ = norm x * norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x \ norm x *\<^sub>R y = - norm y *\<^sub>R x" (is "?lhs \ ?rhs") proof - have th: "\(x::real) a. a \ 0 \ \x\ = a \ x = a \ x = - a" by arith have "?rhs \ norm x *\<^sub>R y = norm y *\<^sub>R x \ norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)" by simp also have "\ \ (x \ y = norm x * norm y \ (- x) \ y = norm x * norm y)" unfolding norm_cauchy_schwarz_eq[symmetric] unfolding norm_minus_cancel norm_scaleR .. also have "\ \ ?lhs" unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] inner_simps by auto finally show ?thesis .. qed lemma norm_triangle_eq: fixes x y :: "'a::real_inner" shows "norm (x + y) = norm x + norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" proof (cases "x = 0 \ y = 0") case True then show ?thesis by force next case False then have n: "norm x > 0" "norm y > 0" by auto have "norm (x + y) = norm x + norm y \ (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2" by simp also have "\ \ norm x *\<^sub>R y = norm y *\<^sub>R x" unfolding norm_cauchy_schwarz_eq[symmetric] unfolding power2_norm_eq_inner inner_simps by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps) finally show ?thesis . qed subsection \Collinearity\ definition\<^marker>\tag important\ collinear :: "'a::real_vector set \ bool" where "collinear S \ (\u. \x \ S. \ y \ S. \c. x - y = c *\<^sub>R u)" lemma collinear_alt: "collinear S \ (\u v. \x \ S. \c. x = u + c *\<^sub>R v)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs unfolding collinear_def by (metis Groups.add_ac(2) diff_add_cancel) next assume ?rhs then obtain u v where *: "\x. x \ S \ \c. x = u + c *\<^sub>R v" by (auto simp: ) have "\c. x - y = c *\<^sub>R v" if "x \ S" "y \ S" for x y by (metis *[OF \x \ S\] *[OF \y \ S\] scaleR_left.diff add_diff_cancel_left) then show ?lhs using collinear_def by blast qed lemma collinear: fixes S :: "'a::{perfect_space,real_vector} set" shows "collinear S \ (\u. u \ 0 \ (\x \ S. \ y \ S. \c. x - y = c *\<^sub>R u))" proof - have "\v. v \ 0 \ (\x\S. \y\S. \c. x - y = c *\<^sub>R v)" if "\x\S. \y\S. \c. x - y = c *\<^sub>R u" "u=0" for u proof - have "\x\S. \y\S. x = y" using that by auto moreover obtain v::'a where "v \ 0" using UNIV_not_singleton [of 0] by auto ultimately have "\x\S. \y\S. \c. x - y = c *\<^sub>R v" by auto then show ?thesis using \v \ 0\ by blast qed then show ?thesis apply (clarsimp simp: collinear_def) by (metis scaleR_zero_right vector_fraction_eq_iff) qed lemma collinear_subset: "\collinear T; S \ T\ \ collinear S" by (meson collinear_def subsetCE) lemma collinear_empty [iff]: "collinear {}" by (simp add: collinear_def) lemma collinear_sing [iff]: "collinear {x}" by (simp add: collinear_def) lemma collinear_2 [iff]: "collinear {x, y}" apply (simp add: collinear_def) apply (rule exI[where x="x - y"]) by (metis minus_diff_eq scaleR_left.minus scaleR_one) lemma collinear_lemma: "collinear {0, x, y} \ x = 0 \ y = 0 \ (\c. y = c *\<^sub>R x)" (is "?lhs \ ?rhs") proof (cases "x = 0 \ y = 0") case True then show ?thesis by (auto simp: insert_commute) next case False show ?thesis proof assume h: "?lhs" then obtain u where u: "\ x\ {0,x,y}. \y\ {0,x,y}. \c. x - y = c *\<^sub>R u" unfolding collinear_def by blast from u[rule_format, of x 0] u[rule_format, of y 0] obtain cx and cy where cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u" by auto from cx cy False have cx0: "cx \ 0" and cy0: "cy \ 0" by auto let ?d = "cy / cx" from cx cy cx0 have "y = ?d *\<^sub>R x" by simp then show ?rhs using False by blast next assume h: "?rhs" then obtain c where c: "y = c *\<^sub>R x" using False by blast show ?lhs unfolding collinear_def c apply (rule exI[where x=x]) apply auto apply (rule exI[where x="- 1"], simp) apply (rule exI[where x= "-c"], simp) apply (rule exI[where x=1], simp) apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib) apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib) done qed qed lemma norm_cauchy_schwarz_equal: "\x \ y\ = norm x * norm y \ collinear {0, x, y}" proof (cases "x=0") case True then show ?thesis by (auto simp: insert_commute) next case False then have nnz: "norm x \ 0" by auto show ?thesis proof assume "\x \ y\ = norm x * norm y" then show "collinear {0, x, y}" unfolding norm_cauchy_schwarz_abs_eq collinear_lemma by (meson eq_vector_fraction_iff nnz) next assume "collinear {0, x, y}" with False show "\x \ y\ = norm x * norm y" unfolding norm_cauchy_schwarz_abs_eq collinear_lemma by (auto simp: abs_if) qed qed subsection\Properties of special hyperplanes\ lemma subspace_hyperplane: "subspace {x. a \ x = 0}" by (simp add: subspace_def inner_right_distrib) lemma subspace_hyperplane2: "subspace {x. x \ a = 0}" by (simp add: inner_commute inner_right_distrib subspace_def) lemma special_hyperplane_span: fixes S :: "'n::euclidean_space set" assumes "k \ Basis" shows "{x. k \ x = 0} = span (Basis - {k})" proof - have *: "x \ span (Basis - {k})" if "k \ x = 0" for x proof - have "x = (\b\Basis. (x \ b) *\<^sub>R b)" by (simp add: euclidean_representation) also have "... = (\b \ Basis - {k}. (x \ b) *\<^sub>R b)" by (auto simp: sum.remove [of _ k] inner_commute assms that) finally have "x = (\b\Basis - {k}. (x \ b) *\<^sub>R b)" . then show ?thesis by (simp add: span_finite) qed show ?thesis apply (rule span_subspace [symmetric]) using assms apply (auto simp: inner_not_same_Basis intro: * subspace_hyperplane) done qed lemma dim_special_hyperplane: fixes k :: "'n::euclidean_space" shows "k \ Basis \ dim {x. k \ x = 0} = DIM('n) - 1" apply (simp add: special_hyperplane_span) apply (rule dim_unique [OF subset_refl]) apply (auto simp: independent_substdbasis) apply (metis member_remove remove_def span_base) done proposition dim_hyperplane: fixes a :: "'a::euclidean_space" assumes "a \ 0" shows "dim {x. a \ x = 0} = DIM('a) - 1" proof - have span0: "span {x. a \ x = 0} = {x. a \ x = 0}" by (rule span_unique) (auto simp: subspace_hyperplane) then obtain B where "independent B" and Bsub: "B \ {x. a \ x = 0}" and subspB: "{x. a \ x = 0} \ span B" and card0: "(card B = dim {x. a \ x = 0})" and ortho: "pairwise orthogonal B" using orthogonal_basis_exists by metis with assms have "a \ span B" by (metis (mono_tags, lifting) span_eq inner_eq_zero_iff mem_Collect_eq span0) then have ind: "independent (insert a B)" by (simp add: \independent B\ independent_insert) have "finite B" using \independent B\ independent_bound by blast have "UNIV \ span (insert a B)" proof fix y::'a obtain r z where z: "y = r *\<^sub>R a + z" "a \ z = 0" apply (rule_tac r="(a \ y) / (a \ a)" and z = "y - ((a \ y) / (a \ a)) *\<^sub>R a" in that) using assms by (auto simp: algebra_simps) show "y \ span (insert a B)" by (metis (mono_tags, lifting) z Bsub span_eq_iff add_diff_cancel_left' mem_Collect_eq span0 span_breakdown_eq span_subspace subspB) qed then have dima: "DIM('a) = dim(insert a B)" by (metis independent_Basis span_Basis dim_eq_card top.extremum_uniqueI) then show ?thesis by (metis (mono_tags, lifting) Bsub Diff_insert_absorb \a \ span B\ ind card0 card_Diff_singleton dim_span indep_card_eq_dim_span insertI1 subsetCE subspB) qed lemma lowdim_eq_hyperplane: fixes S :: "'a::euclidean_space set" assumes "dim S = DIM('a) - 1" obtains a where "a \ 0" and "span S = {x. a \ x = 0}" proof - have dimS: "dim S < DIM('a)" by (simp add: assms) then obtain b where b: "b \ 0" "span S \ {a. b \ a = 0}" using lowdim_subset_hyperplane [of S] by fastforce show ?thesis apply (rule that[OF b(1)]) apply (rule subspace_dim_equal) by (auto simp: assms b dim_hyperplane dim_span subspace_hyperplane subspace_span) qed lemma dim_eq_hyperplane: fixes S :: "'n::euclidean_space set" shows "dim S = DIM('n) - 1 \ (\a. a \ 0 \ span S = {x. a \ x = 0})" by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane) subsection\ Orthogonal bases, Gram-Schmidt process, and related theorems\ lemma pairwise_orthogonal_independent: assumes "pairwise orthogonal S" and "0 \ S" shows "independent S" proof - have 0: "\x y. \x \ y; x \ S; y \ S\ \ x \ y = 0" using assms by (simp add: pairwise_def orthogonal_def) have "False" if "a \ S" and a: "a \ span (S - {a})" for a proof - obtain T U where "T \ S - {a}" "a = (\v\T. U v *\<^sub>R v)" using a by (force simp: span_explicit) then have "a \ a = a \ (\v\T. U v *\<^sub>R v)" by simp also have "... = 0" apply (simp add: inner_sum_right) apply (rule comm_monoid_add_class.sum.neutral) by (metis "0" DiffE \T \ S - {a}\ mult_not_zero singletonI subsetCE \a \ S\) finally show ?thesis using \0 \ S\ \a \ S\ by auto qed then show ?thesis by (force simp: dependent_def) qed lemma pairwise_orthogonal_imp_finite: fixes S :: "'a::euclidean_space set" assumes "pairwise orthogonal S" shows "finite S" proof - have "independent (S - {0})" apply (rule pairwise_orthogonal_independent) apply (metis Diff_iff assms pairwise_def) by blast then show ?thesis by (meson independent_imp_finite infinite_remove) qed lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}" by (simp add: subspace_def orthogonal_clauses) lemma subspace_orthogonal_to_vectors: "subspace {y. \x \ S. orthogonal x y}" by (simp add: subspace_def orthogonal_clauses) lemma orthogonal_to_span: assumes a: "a \ span S" and x: "\y. y \ S \ orthogonal x y" shows "orthogonal x a" by (metis a orthogonal_clauses(1,2,4) span_induct_alt x) proposition Gram_Schmidt_step: fixes S :: "'a::euclidean_space set" assumes S: "pairwise orthogonal S" and x: "x \ span S" shows "orthogonal x (a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b))" proof - have "finite S" by (simp add: S pairwise_orthogonal_imp_finite) have "orthogonal (a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b)) x" if "x \ S" for x proof - have "a \ x = (\y\S. if y = x then y \ a else 0)" by (simp add: \finite S\ inner_commute sum.delta that) also have "... = (\b\S. b \ a * (b \ x) / (b \ b))" apply (rule sum.cong [OF refl], simp) by (meson S orthogonal_def pairwise_def that) finally show ?thesis by (simp add: orthogonal_def algebra_simps inner_sum_left) qed then show ?thesis using orthogonal_to_span orthogonal_commute x by blast qed lemma orthogonal_extension_aux: fixes S :: "'a::euclidean_space set" assumes "finite T" "finite S" "pairwise orthogonal S" shows "\U. pairwise orthogonal (S \ U) \ span (S \ U) = span (S \ T)" using assms proof (induction arbitrary: S) case empty then show ?case by simp (metis sup_bot_right) next case (insert a T) have 0: "\x y. \x \ y; x \ S; y \ S\ \ x \ y = 0" using insert by (simp add: pairwise_def orthogonal_def) define a' where "a' = a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b)" obtain U where orthU: "pairwise orthogonal (S \ insert a' U)" and spanU: "span (insert a' S \ U) = span (insert a' S \ T)" by (rule exE [OF insert.IH [of "insert a' S"]]) (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute pairwise_orthogonal_insert span_clauses) have orthS: "\x. x \ S \ a' \ x = 0" apply (simp add: a'_def) using Gram_Schmidt_step [OF \pairwise orthogonal S\] apply (force simp: orthogonal_def inner_commute span_superset [THEN subsetD]) done have "span (S \ insert a' U) = span (insert a' (S \ T))" using spanU by simp also have "... = span (insert a (S \ T))" apply (rule eq_span_insert_eq) apply (simp add: a'_def span_neg span_sum span_base span_mul) done also have "... = span (S \ insert a T)" by simp finally show ?case by (rule_tac x="insert a' U" in exI) (use orthU in auto) qed proposition orthogonal_extension: fixes S :: "'a::euclidean_space set" assumes S: "pairwise orthogonal S" obtains U where "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ T)" proof - obtain B where "finite B" "span B = span T" using basis_subspace_exists [of "span T"] subspace_span by metis with orthogonal_extension_aux [of B S] obtain U where "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ B)" using assms pairwise_orthogonal_imp_finite by auto with \span B = span T\ show ?thesis by (rule_tac U=U in that) (auto simp: span_Un) qed corollary\<^marker>\tag unimportant\ orthogonal_extension_strong: fixes S :: "'a::euclidean_space set" assumes S: "pairwise orthogonal S" obtains U where "U \ (insert 0 S) = {}" "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ T)" proof - obtain U where "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ T)" using orthogonal_extension assms by blast then show ?thesis apply (rule_tac U = "U - (insert 0 S)" in that) apply blast apply (force simp: pairwise_def) apply (metis Un_Diff_cancel Un_insert_left span_redundant span_zero) done qed subsection\Decomposing a vector into parts in orthogonal subspaces\ text\existence of orthonormal basis for a subspace.\ lemma orthogonal_spanningset_subspace: fixes S :: "'a :: euclidean_space set" assumes "subspace S" obtains B where "B \ S" "pairwise orthogonal B" "span B = S" proof - obtain B where "B \ S" "independent B" "S \ span B" "card B = dim S" using basis_exists by blast with orthogonal_extension [of "{}" B] show ?thesis by (metis Un_empty_left assms pairwise_empty span_superset span_subspace that) qed lemma orthogonal_basis_subspace: fixes S :: "'a :: euclidean_space set" assumes "subspace S" obtains B where "0 \ B" "B \ S" "pairwise orthogonal B" "independent B" "card B = dim S" "span B = S" proof - obtain B where "B \ S" "pairwise orthogonal B" "span B = S" using assms orthogonal_spanningset_subspace by blast then show ?thesis apply (rule_tac B = "B - {0}" in that) apply (auto simp: indep_card_eq_dim_span pairwise_subset pairwise_orthogonal_independent elim: pairwise_subset) done qed proposition orthonormal_basis_subspace: fixes S :: "'a :: euclidean_space set" assumes "subspace S" obtains B where "B \ S" "pairwise orthogonal B" and "\x. x \ B \ norm x = 1" and "independent B" "card B = dim S" "span B = S" proof - obtain B where "0 \ B" "B \ S" and orth: "pairwise orthogonal B" and "independent B" "card B = dim S" "span B = S" by (blast intro: orthogonal_basis_subspace [OF assms]) have 1: "(\x. x /\<^sub>R norm x) ` B \ S" using \span B = S\ span_superset span_mul by fastforce have 2: "pairwise orthogonal ((\x. x /\<^sub>R norm x) ` B)" using orth by (force simp: pairwise_def orthogonal_clauses) have 3: "\x. x \ (\x. x /\<^sub>R norm x) ` B \ norm x = 1" by (metis (no_types, lifting) \0 \ B\ image_iff norm_sgn sgn_div_norm) have 4: "independent ((\x. x /\<^sub>R norm x) ` B)" by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one) have "inj_on (\x. x /\<^sub>R norm x) B" proof fix x y assume "x \ B" "y \ B" "x /\<^sub>R norm x = y /\<^sub>R norm y" moreover have "\i. i \ B \ norm (i /\<^sub>R norm i) = 1" using 3 by blast ultimately show "x = y" by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one) qed then have 5: "card ((\x. x /\<^sub>R norm x) ` B) = dim S" by (metis \card B = dim S\ card_image) have 6: "span ((\x. x /\<^sub>R norm x) ` B) = S" by (metis "1" "4" "5" assms card_eq_dim independent_imp_finite span_subspace) show ?thesis by (rule that [OF 1 2 3 4 5 6]) qed proposition\<^marker>\tag unimportant\ orthogonal_to_subspace_exists_gen: fixes S :: "'a :: euclidean_space set" assumes "span S \ span T" obtains x where "x \ 0" "x \ span T" "\y. y \ span S \ orthogonal x y" proof - obtain B where "B \ span S" and orthB: "pairwise orthogonal B" and "\x. x \ B \ norm x = 1" and "independent B" "card B = dim S" "span B = span S" by (rule orthonormal_basis_subspace [of "span S", OF subspace_span]) (auto simp: dim_span) with assms obtain u where spanBT: "span B \ span T" and "u \ span B" "u \ span T" by auto obtain C where orthBC: "pairwise orthogonal (B \ C)" and spanBC: "span (B \ C) = span (B \ {u})" by (blast intro: orthogonal_extension [OF orthB]) show thesis proof (cases "C \ insert 0 B") case True then have "C \ span B" using span_eq by (metis span_insert_0 subset_trans) moreover have "u \ span (B \ C)" using \span (B \ C) = span (B \ {u})\ span_superset by force ultimately show ?thesis using True \u \ span B\ by (metis Un_insert_left span_insert_0 sup.orderE) next case False then obtain x where "x \ C" "x \ 0" "x \ B" by blast then have "x \ span T" by (metis (no_types, lifting) Un_insert_right Un_upper2 \u \ span T\ spanBT spanBC \u \ span T\ insert_subset span_superset span_mono span_span subsetCE subset_trans sup_bot.comm_neutral) moreover have "orthogonal x y" if "y \ span B" for y using that proof (rule span_induct) show "subspace {a. orthogonal x a}" by (simp add: subspace_orthogonal_to_vector) show "\b. b \ B \ orthogonal x b" by (metis Un_iff \x \ C\ \x \ B\ orthBC pairwise_def) qed ultimately show ?thesis using \x \ 0\ that \span B = span S\ by auto qed qed corollary\<^marker>\tag unimportant\ orthogonal_to_subspace_exists: fixes S :: "'a :: euclidean_space set" assumes "dim S < DIM('a)" obtains x where "x \ 0" "\y. y \ span S \ orthogonal x y" proof - have "span S \ UNIV" by (metis (mono_tags) UNIV_I assms inner_eq_zero_iff less_le lowdim_subset_hyperplane mem_Collect_eq top.extremum_strict top.not_eq_extremum) with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis by (auto simp: span_UNIV) qed corollary\<^marker>\tag unimportant\ orthogonal_to_vector_exists: fixes x :: "'a :: euclidean_space" assumes "2 \ DIM('a)" obtains y where "y \ 0" "orthogonal x y" proof - have "dim {x} < DIM('a)" using assms by auto then show thesis by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that) qed proposition\<^marker>\tag unimportant\ orthogonal_subspace_decomp_exists: fixes S :: "'a :: euclidean_space set" obtains y z where "y \ span S" and "\w. w \ span S \ orthogonal z w" and "x = y + z" proof - obtain T where "0 \ T" "T \ span S" "pairwise orthogonal T" "independent T" "card T = dim (span S)" "span T = span S" using orthogonal_basis_subspace subspace_span by blast let ?a = "\b\T. (b \ x / (b \ b)) *\<^sub>R b" have orth: "orthogonal (x - ?a) w" if "w \ span S" for w by (simp add: Gram_Schmidt_step \pairwise orthogonal T\ \span T = span S\ orthogonal_commute that) show ?thesis apply (rule_tac y = "?a" and z = "x - ?a" in that) apply (meson \T \ span S\ span_scale span_sum subsetCE) apply (fact orth, simp) done qed lemma orthogonal_subspace_decomp_unique: fixes S :: "'a :: euclidean_space set" assumes "x + y = x' + y'" and ST: "x \ span S" "x' \ span S" "y \ span T" "y' \ span T" and orth: "\a b. \a \ S; b \ T\ \ orthogonal a b" shows "x = x' \ y = y'" proof - have "x + y - y' = x'" by (simp add: assms) moreover have "\a b. \a \ span S; b \ span T\ \ orthogonal a b" by (meson orth orthogonal_commute orthogonal_to_span) ultimately have "0 = x' - x" by (metis (full_types) add_diff_cancel_left' ST diff_right_commute orthogonal_clauses(10) orthogonal_clauses(5) orthogonal_self) with assms show ?thesis by auto qed lemma vector_in_orthogonal_spanningset: fixes a :: "'a::euclidean_space" obtains S where "a \ S" "pairwise orthogonal S" "span S = UNIV" by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def pairwise_orthogonal_insert span_UNIV subsetI subset_antisym) lemma vector_in_orthogonal_basis: fixes a :: "'a::euclidean_space" assumes "a \ 0" obtains S where "a \ S" "0 \ S" "pairwise orthogonal S" "independent S" "finite S" "span S = UNIV" "card S = DIM('a)" proof - obtain S where S: "a \ S" "pairwise orthogonal S" "span S = UNIV" using vector_in_orthogonal_spanningset . show thesis proof show "pairwise orthogonal (S - {0})" using pairwise_mono S(2) by blast show "independent (S - {0})" by (simp add: \pairwise orthogonal (S - {0})\ pairwise_orthogonal_independent) show "finite (S - {0})" using \independent (S - {0})\ independent_imp_finite by blast show "card (S - {0}) = DIM('a)" using span_delete_0 [of S] S by (simp add: \independent (S - {0})\ indep_card_eq_dim_span dim_UNIV) qed (use S \a \ 0\ in auto) qed lemma vector_in_orthonormal_basis: fixes a :: "'a::euclidean_space" assumes "norm a = 1" obtains S where "a \ S" "pairwise orthogonal S" "\x. x \ S \ norm x = 1" "independent S" "card S = DIM('a)" "span S = UNIV" proof - have "a \ 0" using assms by auto then obtain S where "a \ S" "0 \ S" "finite S" and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)" by (metis vector_in_orthogonal_basis) let ?S = "(\x. x /\<^sub>R norm x) ` S" show thesis proof show "a \ ?S" using \a \ S\ assms image_iff by fastforce next show "pairwise orthogonal ?S" using \pairwise orthogonal S\ by (auto simp: pairwise_def orthogonal_def) show "\x. x \ (\x. x /\<^sub>R norm x) ` S \ norm x = 1" using \0 \ S\ by (auto simp: field_split_simps) then show "independent ?S" by (metis \pairwise orthogonal ((\x. x /\<^sub>R norm x) ` S)\ norm_zero pairwise_orthogonal_independent zero_neq_one) have "inj_on (\x. x /\<^sub>R norm x) S" unfolding inj_on_def by (metis (full_types) S(1) \0 \ S\ inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def) then show "card ?S = DIM('a)" by (simp add: card_image S) show "span ?S = UNIV" by (metis (no_types) \0 \ S\ \finite S\ \span S = UNIV\ field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale zero_less_norm_iff) qed qed proposition dim_orthogonal_sum: fixes A :: "'a::euclidean_space set" assumes "\x y. \x \ A; y \ B\ \ x \ y = 0" shows "dim(A \ B) = dim A + dim B" proof - have 1: "\x y. \x \ span A; y \ B\ \ x \ y = 0" by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms) have "\x y. \x \ span A; y \ span B\ \ x \ y = 0" using 1 by (simp add: span_induct [OF _ subspace_hyperplane]) then have 0: "\x y. \x \ span A; y \ span B\ \ x \ y = 0" by simp have "dim(A \ B) = dim (span (A \ B))" by (simp add: dim_span) also have "span (A \ B) = ((\(a, b). a + b) ` (span A \ span B))" by (auto simp add: span_Un image_def) also have "dim \ = dim {x + y |x y. x \ span A \ y \ span B}" by (auto intro!: arg_cong [where f=dim]) also have "... = dim {x + y |x y. x \ span A \ y \ span B} + dim(span A \ span B)" by (auto simp: dest: 0) also have "... = dim (span A) + dim (span B)" by (rule dim_sums_Int) (auto simp: subspace_span) also have "... = dim A + dim B" by (simp add: dim_span) finally show ?thesis . qed lemma dim_subspace_orthogonal_to_vectors: fixes A :: "'a::euclidean_space set" assumes "subspace A" "subspace B" "A \ B" shows "dim {y \ B. \x \ A. orthogonal x y} + dim A = dim B" proof - have "dim (span ({y \ B. \x\A. orthogonal x y} \ A)) = dim (span B)" proof (rule arg_cong [where f=dim, OF subset_antisym]) show "span ({y \ B. \x\A. orthogonal x y} \ A) \ span B" by (simp add: \A \ B\ Collect_restrict span_mono) next have *: "x \ span ({y \ B. \x\A. orthogonal x y} \ A)" if "x \ B" for x proof - obtain y z where "x = y + z" "y \ span A" and orth: "\w. w \ span A \ orthogonal z w" using orthogonal_subspace_decomp_exists [of A x] that by auto have "y \ span B" using \y \ span A\ assms(3) span_mono by blast then have "z \ {a \ B. \x. x \ A \ orthogonal x a}" apply simp using \x = y + z\ assms(1) assms(2) orth orthogonal_commute span_add_eq span_eq_iff that by blast then have z: "z \ span {y \ B. \x\A. orthogonal x y}" by (meson span_superset subset_iff) then show ?thesis apply (auto simp: span_Un image_def \x = y + z\ \y \ span A\) using \y \ span A\ add.commute by blast qed show "span B \ span ({y \ B. \x\A. orthogonal x y} \ A)" by (rule span_minimal) (auto intro: * span_minimal simp: subspace_span) qed then show ?thesis by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq orthogonal_commute orthogonal_def) qed subsection\Linear functions are (uniformly) continuous on any set\ subsection\<^marker>\tag unimportant\ \Topological properties of linear functions\ lemma linear_lim_0: assumes "bounded_linear f" shows "(f \ 0) (at (0))" proof - interpret f: bounded_linear f by fact have "(f \ f 0) (at 0)" using tendsto_ident_at by (rule f.tendsto) then show ?thesis unfolding f.zero . qed lemma linear_continuous_at: assumes "bounded_linear f" shows "continuous (at a) f" unfolding continuous_at using assms apply (rule bounded_linear.tendsto) apply (rule tendsto_ident_at) done lemma linear_continuous_within: "bounded_linear f \ continuous (at x within s) f" using continuous_at_imp_continuous_at_within linear_continuous_at by blast lemma linear_continuous_on: "bounded_linear f \ continuous_on s f" using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto lemma Lim_linear: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" and h :: "'b \ 'c::real_normed_vector" assumes "(f \ l) F" "linear h" shows "((\x. h(f x)) \ h l) F" proof - obtain B where B: "B > 0" "\x. norm (h x) \ B * norm x" using linear_bounded_pos [OF \linear h\] by blast show ?thesis unfolding tendsto_iff proof (intro allI impI) show "\\<^sub>F x in F. dist (h (f x)) (h l) < e" if "e > 0" for e proof - have "\\<^sub>F x in F. dist (f x) l < e/B" by (simp add: \0 < B\ assms(1) tendstoD that) then show ?thesis unfolding dist_norm proof (rule eventually_mono) show "norm (h (f x) - h l) < e" if "norm (f x - l) < e / B" for x using that B apply (simp add: field_split_simps) by (metis \linear h\ le_less_trans linear_diff mult.commute) qed qed qed qed lemma linear_continuous_compose: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" and g :: "'b \ 'c::real_normed_vector" assumes "continuous F f" "linear g" shows "continuous F (\x. g(f x))" using assms unfolding continuous_def by (rule Lim_linear) lemma linear_continuous_on_compose: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" and g :: "'b \ 'c::real_normed_vector" assumes "continuous_on S f" "linear g" shows "continuous_on S (\x. g(f x))" using assms by (simp add: continuous_on_eq_continuous_within linear_continuous_compose) text\Also bilinear functions, in composition form\ lemma bilinear_continuous_compose: fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" assumes "continuous F f" "continuous F g" "bilinear h" shows "continuous F (\x. h (f x) (g x))" using assms bilinear_conv_bounded_bilinear bounded_bilinear.continuous by blast lemma bilinear_continuous_on_compose: fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" and f :: "'d::t2_space \ 'a" assumes "continuous_on S f" "continuous_on S g" "bilinear h" shows "continuous_on S (\x. h (f x) (g x))" using assms by (simp add: continuous_on_eq_continuous_within bilinear_continuous_compose) end diff --git a/src/HOL/Real.thy b/src/HOL/Real.thy --- a/src/HOL/Real.thy +++ b/src/HOL/Real.thy @@ -1,1656 +1,1746 @@ (* Title: HOL/Real.thy Author: Jacques D. Fleuriot, University of Edinburgh, 1998 Author: Larry Paulson, University of Cambridge Author: Jeremy Avigad, Carnegie Mellon University Author: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 Construction of Cauchy Reals by Brian Huffman, 2010 *) section \Development of the Reals using Cauchy Sequences\ theory Real imports Rat begin text \ This theory contains a formalization of the real numbers as equivalence classes of Cauchy sequences of rationals. See \<^file>\~~/src/HOL/ex/Dedekind_Real.thy\ for an alternative construction using Dedekind cuts. \ subsection \Preliminary lemmas\ text\Useful in convergence arguments\ lemma inverse_of_nat_le: fixes n::nat shows "\n \ m; n\0\ \ 1 / of_nat m \ (1::'a::linordered_field) / of_nat n" by (simp add: frac_le) lemma add_diff_add: "(a + c) - (b + d) = (a - b) + (c - d)" for a b c d :: "'a::ab_group_add" by simp lemma minus_diff_minus: "- a - - b = - (a - b)" for a b :: "'a::ab_group_add" by simp lemma mult_diff_mult: "(x * y - a * b) = x * (y - b) + (x - a) * b" for x y a b :: "'a::ring" by (simp add: algebra_simps) lemma inverse_diff_inverse: fixes a b :: "'a::division_ring" assumes "a \ 0" and "b \ 0" shows "inverse a - inverse b = - (inverse a * (a - b) * inverse b)" using assms by (simp add: algebra_simps) lemma obtain_pos_sum: fixes r :: rat assumes r: "0 < r" obtains s t where "0 < s" and "0 < t" and "r = s + t" proof from r show "0 < r/2" by simp from r show "0 < r/2" by simp show "r = r/2 + r/2" by simp qed subsection \Sequences that converge to zero\ definition vanishes :: "(nat \ rat) \ bool" where "vanishes X \ (\r>0. \k. \n\k. \X n\ < r)" lemma vanishesI: "(\r. 0 < r \ \k. \n\k. \X n\ < r) \ vanishes X" unfolding vanishes_def by simp lemma vanishesD: "vanishes X \ 0 < r \ \k. \n\k. \X n\ < r" unfolding vanishes_def by simp lemma vanishes_const [simp]: "vanishes (\n. c) \ c = 0" proof (cases "c = 0") case True then show ?thesis by (simp add: vanishesI) next case False then show ?thesis unfolding vanishes_def using zero_less_abs_iff by blast qed lemma vanishes_minus: "vanishes X \ vanishes (\n. - X n)" unfolding vanishes_def by simp lemma vanishes_add: assumes X: "vanishes X" and Y: "vanishes Y" shows "vanishes (\n. X n + Y n)" proof (rule vanishesI) fix r :: rat assume "0 < r" then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" by (rule obtain_pos_sum) obtain i where i: "\n\i. \X n\ < s" using vanishesD [OF X s] .. obtain j where j: "\n\j. \Y n\ < t" using vanishesD [OF Y t] .. have "\n\max i j. \X n + Y n\ < r" proof clarsimp fix n assume n: "i \ n" "j \ n" have "\X n + Y n\ \ \X n\ + \Y n\" by (rule abs_triangle_ineq) also have "\ < s + t" by (simp add: add_strict_mono i j n) finally show "\X n + Y n\ < r" by (simp only: r) qed then show "\k. \n\k. \X n + Y n\ < r" .. qed lemma vanishes_diff: assumes "vanishes X" "vanishes Y" shows "vanishes (\n. X n - Y n)" unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus assms) lemma vanishes_mult_bounded: assumes X: "\a>0. \n. \X n\ < a" assumes Y: "vanishes (\n. Y n)" shows "vanishes (\n. X n * Y n)" proof (rule vanishesI) fix r :: rat assume r: "0 < r" obtain a where a: "0 < a" "\n. \X n\ < a" using X by blast obtain b where b: "0 < b" "r = a * b" proof show "0 < r / a" using r a by simp show "r = a * (r / a)" using a by simp qed obtain k where k: "\n\k. \Y n\ < b" using vanishesD [OF Y b(1)] .. have "\n\k. \X n * Y n\ < r" by (simp add: b(2) abs_mult mult_strict_mono' a k) then show "\k. \n\k. \X n * Y n\ < r" .. qed subsection \Cauchy sequences\ definition cauchy :: "(nat \ rat) \ bool" where "cauchy X \ (\r>0. \k. \m\k. \n\k. \X m - X n\ < r)" lemma cauchyI: "(\r. 0 < r \ \k. \m\k. \n\k. \X m - X n\ < r) \ cauchy X" unfolding cauchy_def by simp lemma cauchyD: "cauchy X \ 0 < r \ \k. \m\k. \n\k. \X m - X n\ < r" unfolding cauchy_def by simp lemma cauchy_const [simp]: "cauchy (\n. x)" unfolding cauchy_def by simp lemma cauchy_add [simp]: assumes X: "cauchy X" and Y: "cauchy Y" shows "cauchy (\n. X n + Y n)" proof (rule cauchyI) fix r :: rat assume "0 < r" then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" by (rule obtain_pos_sum) obtain i where i: "\m\i. \n\i. \X m - X n\ < s" using cauchyD [OF X s] .. obtain j where j: "\m\j. \n\j. \Y m - Y n\ < t" using cauchyD [OF Y t] .. have "\m\max i j. \n\max i j. \(X m + Y m) - (X n + Y n)\ < r" proof clarsimp fix m n assume *: "i \ m" "j \ m" "i \ n" "j \ n" have "\(X m + Y m) - (X n + Y n)\ \ \X m - X n\ + \Y m - Y n\" unfolding add_diff_add by (rule abs_triangle_ineq) also have "\ < s + t" by (rule add_strict_mono) (simp_all add: i j *) finally show "\(X m + Y m) - (X n + Y n)\ < r" by (simp only: r) qed then show "\k. \m\k. \n\k. \(X m + Y m) - (X n + Y n)\ < r" .. qed lemma cauchy_minus [simp]: assumes X: "cauchy X" shows "cauchy (\n. - X n)" using assms unfolding cauchy_def unfolding minus_diff_minus abs_minus_cancel . lemma cauchy_diff [simp]: assumes "cauchy X" "cauchy Y" shows "cauchy (\n. X n - Y n)" using assms unfolding diff_conv_add_uminus by (simp del: add_uminus_conv_diff) lemma cauchy_imp_bounded: assumes "cauchy X" shows "\b>0. \n. \X n\ < b" proof - obtain k where k: "\m\k. \n\k. \X m - X n\ < 1" using cauchyD [OF assms zero_less_one] .. show "\b>0. \n. \X n\ < b" proof (intro exI conjI allI) have "0 \ \X 0\" by simp also have "\X 0\ \ Max (abs ` X ` {..k})" by simp finally have "0 \ Max (abs ` X ` {..k})" . then show "0 < Max (abs ` X ` {..k}) + 1" by simp next fix n :: nat show "\X n\ < Max (abs ` X ` {..k}) + 1" proof (rule linorder_le_cases) assume "n \ k" then have "\X n\ \ Max (abs ` X ` {..k})" by simp then show "\X n\ < Max (abs ` X ` {..k}) + 1" by simp next assume "k \ n" have "\X n\ = \X k + (X n - X k)\" by simp also have "\X k + (X n - X k)\ \ \X k\ + \X n - X k\" by (rule abs_triangle_ineq) also have "\ < Max (abs ` X ` {..k}) + 1" by (rule add_le_less_mono) (simp_all add: k \k \ n\) finally show "\X n\ < Max (abs ` X ` {..k}) + 1" . qed qed qed lemma cauchy_mult [simp]: assumes X: "cauchy X" and Y: "cauchy Y" shows "cauchy (\n. X n * Y n)" proof (rule cauchyI) fix r :: rat assume "0 < r" then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v" by (rule obtain_pos_sum) obtain a where a: "0 < a" "\n. \X n\ < a" using cauchy_imp_bounded [OF X] by blast obtain b where b: "0 < b" "\n. \Y n\ < b" using cauchy_imp_bounded [OF Y] by blast obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b" proof show "0 < v/b" using v b(1) by simp show "0 < u/a" using u a(1) by simp show "r = a * (u/a) + (v/b) * b" using a(1) b(1) \r = u + v\ by simp qed obtain i where i: "\m\i. \n\i. \X m - X n\ < s" using cauchyD [OF X s] .. obtain j where j: "\m\j. \n\j. \Y m - Y n\ < t" using cauchyD [OF Y t] .. have "\m\max i j. \n\max i j. \X m * Y m - X n * Y n\ < r" proof clarsimp fix m n assume *: "i \ m" "j \ m" "i \ n" "j \ n" have "\X m * Y m - X n * Y n\ = \X m * (Y m - Y n) + (X m - X n) * Y n\" unfolding mult_diff_mult .. also have "\ \ \X m * (Y m - Y n)\ + \(X m - X n) * Y n\" by (rule abs_triangle_ineq) also have "\ = \X m\ * \Y m - Y n\ + \X m - X n\ * \Y n\" unfolding abs_mult .. also have "\ < a * t + s * b" by (simp_all add: add_strict_mono mult_strict_mono' a b i j *) finally show "\X m * Y m - X n * Y n\ < r" by (simp only: r) qed then show "\k. \m\k. \n\k. \X m * Y m - X n * Y n\ < r" .. qed lemma cauchy_not_vanishes_cases: assumes X: "cauchy X" assumes nz: "\ vanishes X" shows "\b>0. \k. (\n\k. b < - X n) \ (\n\k. b < X n)" proof - obtain r where "0 < r" and r: "\k. \n\k. r \ \X n\" using nz unfolding vanishes_def by (auto simp add: not_less) obtain s t where s: "0 < s" and t: "0 < t" and "r = s + t" using \0 < r\ by (rule obtain_pos_sum) obtain i where i: "\m\i. \n\i. \X m - X n\ < s" using cauchyD [OF X s] .. obtain k where "i \ k" and "r \ \X k\" using r by blast have k: "\n\k. \X n - X k\ < s" using i \i \ k\ by auto have "X k \ - r \ r \ X k" using \r \ \X k\\ by auto then have "(\n\k. t < - X n) \ (\n\k. t < X n)" unfolding \r = s + t\ using k by auto then have "\k. (\n\k. t < - X n) \ (\n\k. t < X n)" .. then show "\t>0. \k. (\n\k. t < - X n) \ (\n\k. t < X n)" using t by auto qed lemma cauchy_not_vanishes: assumes X: "cauchy X" and nz: "\ vanishes X" shows "\b>0. \k. \n\k. b < \X n\" using cauchy_not_vanishes_cases [OF assms] by (elim ex_forward conj_forward asm_rl) auto lemma cauchy_inverse [simp]: assumes X: "cauchy X" and nz: "\ vanishes X" shows "cauchy (\n. inverse (X n))" proof (rule cauchyI) fix r :: rat assume "0 < r" obtain b i where b: "0 < b" and i: "\n\i. b < \X n\" using cauchy_not_vanishes [OF X nz] by blast from b i have nz: "\n\i. X n \ 0" by auto obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b" proof show "0 < b * r * b" by (simp add: \0 < r\ b) show "r = inverse b * (b * r * b) * inverse b" using b by simp qed obtain j where j: "\m\j. \n\j. \X m - X n\ < s" using cauchyD [OF X s] .. have "\m\max i j. \n\max i j. \inverse (X m) - inverse (X n)\ < r" proof clarsimp fix m n assume *: "i \ m" "j \ m" "i \ n" "j \ n" have "\inverse (X m) - inverse (X n)\ = inverse \X m\ * \X m - X n\ * inverse \X n\" by (simp add: inverse_diff_inverse nz * abs_mult) also have "\ < inverse b * s * inverse b" by (simp add: mult_strict_mono less_imp_inverse_less i j b * s) finally show "\inverse (X m) - inverse (X n)\ < r" by (simp only: r) qed then show "\k. \m\k. \n\k. \inverse (X m) - inverse (X n)\ < r" .. qed lemma vanishes_diff_inverse: assumes X: "cauchy X" "\ vanishes X" and Y: "cauchy Y" "\ vanishes Y" and XY: "vanishes (\n. X n - Y n)" shows "vanishes (\n. inverse (X n) - inverse (Y n))" proof (rule vanishesI) fix r :: rat assume r: "0 < r" obtain a i where a: "0 < a" and i: "\n\i. a < \X n\" using cauchy_not_vanishes [OF X] by blast obtain b j where b: "0 < b" and j: "\n\j. b < \Y n\" using cauchy_not_vanishes [OF Y] by blast obtain s where s: "0 < s" and "inverse a * s * inverse b = r" proof show "0 < a * r * b" using a r b by simp show "inverse a * (a * r * b) * inverse b = r" using a r b by simp qed obtain k where k: "\n\k. \X n - Y n\ < s" using vanishesD [OF XY s] .. have "\n\max (max i j) k. \inverse (X n) - inverse (Y n)\ < r" proof clarsimp fix n assume n: "i \ n" "j \ n" "k \ n" with i j a b have "X n \ 0" and "Y n \ 0" by auto then have "\inverse (X n) - inverse (Y n)\ = inverse \X n\ * \X n - Y n\ * inverse \Y n\" by (simp add: inverse_diff_inverse abs_mult) also have "\ < inverse a * s * inverse b" by (intro mult_strict_mono' less_imp_inverse_less) (simp_all add: a b i j k n) also note \inverse a * s * inverse b = r\ finally show "\inverse (X n) - inverse (Y n)\ < r" . qed then show "\k. \n\k. \inverse (X n) - inverse (Y n)\ < r" .. qed subsection \Equivalence relation on Cauchy sequences\ definition realrel :: "(nat \ rat) \ (nat \ rat) \ bool" where "realrel = (\X Y. cauchy X \ cauchy Y \ vanishes (\n. X n - Y n))" lemma realrelI [intro?]: "cauchy X \ cauchy Y \ vanishes (\n. X n - Y n) \ realrel X Y" by (simp add: realrel_def) lemma realrel_refl: "cauchy X \ realrel X X" by (simp add: realrel_def) lemma symp_realrel: "symp realrel" by (simp add: abs_minus_commute realrel_def symp_def vanishes_def) lemma transp_realrel: "transp realrel" unfolding realrel_def by (rule transpI) (force simp add: dest: vanishes_add) lemma part_equivp_realrel: "part_equivp realrel" by (blast intro: part_equivpI symp_realrel transp_realrel realrel_refl cauchy_const) subsection \The field of real numbers\ quotient_type real = "nat \ rat" / partial: realrel morphisms rep_real Real by (rule part_equivp_realrel) lemma cr_real_eq: "pcr_real = (\x y. cauchy x \ Real x = y)" unfolding real.pcr_cr_eq cr_real_def realrel_def by auto lemma Real_induct [induct type: real]: (* TODO: generate automatically *) assumes "\X. cauchy X \ P (Real X)" shows "P x" proof (induct x) case (1 X) then have "cauchy X" by (simp add: realrel_def) then show "P (Real X)" by (rule assms) qed lemma eq_Real: "cauchy X \ cauchy Y \ Real X = Real Y \ vanishes (\n. X n - Y n)" using real.rel_eq_transfer unfolding real.pcr_cr_eq cr_real_def rel_fun_def realrel_def by simp lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy" by (simp add: real.domain_eq realrel_def) instantiation real :: field begin lift_definition zero_real :: "real" is "\n. 0" by (simp add: realrel_refl) lift_definition one_real :: "real" is "\n. 1" by (simp add: realrel_refl) lift_definition plus_real :: "real \ real \ real" is "\X Y n. X n + Y n" unfolding realrel_def add_diff_add by (simp only: cauchy_add vanishes_add simp_thms) lift_definition uminus_real :: "real \ real" is "\X n. - X n" unfolding realrel_def minus_diff_minus by (simp only: cauchy_minus vanishes_minus simp_thms) lift_definition times_real :: "real \ real \ real" is "\X Y n. X n * Y n" proof - fix f1 f2 f3 f4 have "\cauchy f1; cauchy f4; vanishes (\n. f1 n - f2 n); vanishes (\n. f3 n - f4 n)\ \ vanishes (\n. f1 n * (f3 n - f4 n) + f4 n * (f1 n - f2 n))" by (simp add: vanishes_add vanishes_mult_bounded cauchy_imp_bounded) then show "\realrel f1 f2; realrel f3 f4\ \ realrel (\n. f1 n * f3 n) (\n. f2 n * f4 n)" by (simp add: mult.commute realrel_def mult_diff_mult) qed lift_definition inverse_real :: "real \ real" is "\X. if vanishes X then (\n. 0) else (\n. inverse (X n))" proof - fix X Y assume "realrel X Y" then have X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\n. X n - Y n)" by (simp_all add: realrel_def) have "vanishes X \ vanishes Y" proof assume "vanishes X" from vanishes_diff [OF this XY] show "vanishes Y" by simp next assume "vanishes Y" from vanishes_add [OF this XY] show "vanishes X" by simp qed then show "?thesis X Y" by (simp add: vanishes_diff_inverse X Y XY realrel_def) qed definition "x - y = x + - y" for x y :: real definition "x div y = x * inverse y" for x y :: real lemma add_Real: "cauchy X \ cauchy Y \ Real X + Real Y = Real (\n. X n + Y n)" using plus_real.transfer by (simp add: cr_real_eq rel_fun_def) lemma minus_Real: "cauchy X \ - Real X = Real (\n. - X n)" using uminus_real.transfer by (simp add: cr_real_eq rel_fun_def) lemma diff_Real: "cauchy X \ cauchy Y \ Real X - Real Y = Real (\n. X n - Y n)" by (simp add: minus_Real add_Real minus_real_def) lemma mult_Real: "cauchy X \ cauchy Y \ Real X * Real Y = Real (\n. X n * Y n)" using times_real.transfer by (simp add: cr_real_eq rel_fun_def) lemma inverse_Real: "cauchy X \ inverse (Real X) = (if vanishes X then 0 else Real (\n. inverse (X n)))" using inverse_real.transfer zero_real.transfer unfolding cr_real_eq rel_fun_def by (simp split: if_split_asm, metis) instance proof fix a b c :: real show "a + b = b + a" by transfer (simp add: ac_simps realrel_def) show "(a + b) + c = a + (b + c)" by transfer (simp add: ac_simps realrel_def) show "0 + a = a" by transfer (simp add: realrel_def) show "- a + a = 0" by transfer (simp add: realrel_def) show "a - b = a + - b" by (rule minus_real_def) show "(a * b) * c = a * (b * c)" by transfer (simp add: ac_simps realrel_def) show "a * b = b * a" by transfer (simp add: ac_simps realrel_def) show "1 * a = a" by transfer (simp add: ac_simps realrel_def) show "(a + b) * c = a * c + b * c" by transfer (simp add: distrib_right realrel_def) show "(0::real) \ (1::real)" by transfer (simp add: realrel_def) have "vanishes (\n. inverse (X n) * X n - 1)" if X: "cauchy X" "\ vanishes X" for X proof (rule vanishesI) fix r::rat assume "0 < r" obtain b k where "b>0" "\n\k. b < \X n\" using X cauchy_not_vanishes by blast then show "\k. \n\k. \inverse (X n) * X n - 1\ < r" using \0 < r\ by force qed then show "a \ 0 \ inverse a * a = 1" by transfer (simp add: realrel_def) show "a div b = a * inverse b" by (rule divide_real_def) show "inverse (0::real) = 0" by transfer (simp add: realrel_def) qed end subsection \Positive reals\ lift_definition positive :: "real \ bool" is "\X. \r>0. \k. \n\k. r < X n" proof - have 1: "\r>0. \k. \n\k. r < Y n" if *: "realrel X Y" and **: "\r>0. \k. \n\k. r < X n" for X Y proof - from * have XY: "vanishes (\n. X n - Y n)" by (simp_all add: realrel_def) from ** obtain r i where "0 < r" and i: "\n\i. r < X n" by blast obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" using \0 < r\ by (rule obtain_pos_sum) obtain j where j: "\n\j. \X n - Y n\ < s" using vanishesD [OF XY s] .. have "\n\max i j. t < Y n" proof clarsimp fix n assume n: "i \ n" "j \ n" have "\X n - Y n\ < s" and "r < X n" using i j n by simp_all then show "t < Y n" by (simp add: r) qed then show ?thesis using t by blast qed fix X Y assume "realrel X Y" then have "realrel X Y" and "realrel Y X" using symp_realrel by (auto simp: symp_def) then show "?thesis X Y" by (safe elim!: 1) qed lemma positive_Real: "cauchy X \ positive (Real X) \ (\r>0. \k. \n\k. r < X n)" using positive.transfer by (simp add: cr_real_eq rel_fun_def) lemma positive_zero: "\ positive 0" by transfer auto lemma positive_add: assumes "positive x" "positive y" shows "positive (x + y)" proof - have *: "\\n\i. a < x n; \n\j. b < y n; 0 < a; 0 < b; n \ max i j\ \ a+b < x n + y n" for x y and a b::rat and i j n::nat by (simp add: add_strict_mono) show ?thesis using assms by transfer (blast intro: * pos_add_strict) qed lemma positive_mult: assumes "positive x" "positive y" shows "positive (x * y)" proof - have *: "\\n\i. a < x n; \n\j. b < y n; 0 < a; 0 < b; n \ max i j\ \ a*b < x n * y n" for x y and a b::rat and i j n::nat by (simp add: mult_strict_mono') show ?thesis using assms by transfer (blast intro: * mult_pos_pos) qed lemma positive_minus: "\ positive x \ x \ 0 \ positive (- x)" apply transfer apply (simp add: realrel_def) apply (blast dest: cauchy_not_vanishes_cases) done instantiation real :: linordered_field begin definition "x < y \ positive (y - x)" definition "x \ y \ x < y \ x = y" for x y :: real definition "\a\ = (if a < 0 then - a else a)" for a :: real definition "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" for a :: real instance proof fix a b c :: real show "\a\ = (if a < 0 then - a else a)" by (rule abs_real_def) show "a < b \ a \ b \ \ b \ a" "a \ b \ b \ c \ a \ c" "a \ a" "a \ b \ b \ a \ a = b" "a \ b \ c + a \ c + b" unfolding less_eq_real_def less_real_def by (force simp add: positive_zero dest: positive_add)+ show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" by (rule sgn_real_def) show "a \ b \ b \ a" by (auto dest!: positive_minus simp: less_eq_real_def less_real_def) show "a < b \ 0 < c \ c * a < c * b" unfolding less_real_def by (force simp add: algebra_simps dest: positive_mult) qed end instantiation real :: distrib_lattice begin definition "(inf :: real \ real \ real) = min" definition "(sup :: real \ real \ real) = max" instance by standard (auto simp add: inf_real_def sup_real_def max_min_distrib2) end lemma of_nat_Real: "of_nat x = Real (\n. of_nat x)" by (induct x) (simp_all add: zero_real_def one_real_def add_Real) lemma of_int_Real: "of_int x = Real (\n. of_int x)" by (cases x rule: int_diff_cases) (simp add: of_nat_Real diff_Real) lemma of_rat_Real: "of_rat x = Real (\n. x)" proof (induct x) case (Fract a b) then show ?case apply (simp add: Fract_of_int_quotient of_rat_divide) apply (simp add: of_int_Real divide_inverse inverse_Real mult_Real) done qed instance real :: archimedean_field proof show "\z. x \ of_int z" for x :: real proof (induct x) case (1 X) then obtain b where "0 < b" and b: "\n. \X n\ < b" by (blast dest: cauchy_imp_bounded) then have "Real X < of_int (\b\ + 1)" using 1 apply (simp add: of_int_Real less_real_def diff_Real positive_Real) apply (rule_tac x=1 in exI) apply (simp add: algebra_simps) by (metis abs_ge_self le_less_trans le_of_int_ceiling less_le) then show ?case using less_eq_real_def by blast qed qed instantiation real :: floor_ceiling begin definition [code del]: "\x::real\ = (THE z. of_int z \ x \ x < of_int (z + 1))" instance proof show "of_int \x\ \ x \ x < of_int (\x\ + 1)" for x :: real unfolding floor_real_def using floor_exists1 by (rule theI') qed end subsection \Completeness\ lemma not_positive_Real: assumes "cauchy X" shows "\ positive (Real X) \ (\r>0. \k. \n\k. X n \ r)" (is "?lhs = ?rhs") unfolding positive_Real [OF assms] proof (intro iffI allI notI impI) show "\k. \n\k. X n \ r" if r: "\ (\r>0. \k. \n\k. r < X n)" and "0 < r" for r proof - obtain s t where "s > 0" "t > 0" "r = s+t" using \r > 0\ obtain_pos_sum by blast obtain k where k: "\m n. \m\k; n\k\ \ \X m - X n\ < t" using cauchyD [OF assms \t > 0\] by blast obtain n where "n \ k" "X n \ s" by (meson r \0 < s\ not_less) then have "X l \ r" if "l \ n" for l using k [OF \n \ k\, of l] that \r = s+t\ by linarith then show ?thesis by blast qed qed (meson le_cases not_le) lemma le_Real: assumes "cauchy X" "cauchy Y" shows "Real X \ Real Y = (\r>0. \k. \n\k. X n \ Y n + r)" unfolding not_less [symmetric, where 'a=real] less_real_def apply (simp add: diff_Real not_positive_Real assms) apply (simp add: diff_le_eq ac_simps) done lemma le_RealI: assumes Y: "cauchy Y" shows "\n. x \ of_rat (Y n) \ x \ Real Y" proof (induct x) fix X assume X: "cauchy X" and "\n. Real X \ of_rat (Y n)" then have le: "\m r. 0 < r \ \k. \n\k. X n \ Y m + r" by (simp add: of_rat_Real le_Real) then have "\k. \n\k. X n \ Y n + r" if "0 < r" for r :: rat proof - from that obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" by (rule obtain_pos_sum) obtain i where i: "\m\i. \n\i. \Y m - Y n\ < s" using cauchyD [OF Y s] .. obtain j where j: "\n\j. X n \ Y i + t" using le [OF t] .. have "\n\max i j. X n \ Y n + r" proof clarsimp fix n assume n: "i \ n" "j \ n" have "X n \ Y i + t" using n j by simp moreover have "\Y i - Y n\ < s" using n i by simp ultimately show "X n \ Y n + r" unfolding r by simp qed then show ?thesis .. qed then show "Real X \ Real Y" by (simp add: of_rat_Real le_Real X Y) qed lemma Real_leI: assumes X: "cauchy X" assumes le: "\n. of_rat (X n) \ y" shows "Real X \ y" proof - have "- y \ - Real X" by (simp add: minus_Real X le_RealI of_rat_minus le) then show ?thesis by simp qed lemma less_RealD: assumes "cauchy Y" shows "x < Real Y \ \n. x < of_rat (Y n)" apply (erule contrapos_pp) apply (simp add: not_less) apply (erule Real_leI [OF assms]) done lemma of_nat_less_two_power [simp]: "of_nat n < (2::'a::linordered_idom) ^ n" apply (induct n) apply simp apply (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc) done lemma complete_real: fixes S :: "real set" assumes "\x. x \ S" and "\z. \x\S. x \ z" shows "\y. (\x\S. x \ y) \ (\z. (\x\S. x \ z) \ y \ z)" proof - obtain x where x: "x \ S" using assms(1) .. obtain z where z: "\x\S. x \ z" using assms(2) .. define P where "P x \ (\y\S. y \ of_rat x)" for x obtain a where a: "\ P a" proof have "of_int \x - 1\ \ x - 1" by (rule of_int_floor_le) also have "x - 1 < x" by simp finally have "of_int \x - 1\ < x" . then have "\ x \ of_int \x - 1\" by (simp only: not_le) then show "\ P (of_int \x - 1\)" unfolding P_def of_rat_of_int_eq using x by blast qed obtain b where b: "P b" proof show "P (of_int \z\)" unfolding P_def of_rat_of_int_eq proof fix y assume "y \ S" then have "y \ z" using z by simp also have "z \ of_int \z\" by (rule le_of_int_ceiling) finally show "y \ of_int \z\" . qed qed define avg where "avg x y = x/2 + y/2" for x y :: rat define bisect where "bisect = (\(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y))" define A where "A n = fst ((bisect ^^ n) (a, b))" for n define B where "B n = snd ((bisect ^^ n) (a, b))" for n define C where "C n = avg (A n) (B n)" for n have A_0 [simp]: "A 0 = a" unfolding A_def by simp have B_0 [simp]: "B 0 = b" unfolding B_def by simp have A_Suc [simp]: "\n. A (Suc n) = (if P (C n) then A n else C n)" unfolding A_def B_def C_def bisect_def split_def by simp have B_Suc [simp]: "\n. B (Suc n) = (if P (C n) then C n else B n)" unfolding A_def B_def C_def bisect_def split_def by simp have width: "B n - A n = (b - a) / 2^n" for n proof (induct n) case (Suc n) then show ?case by (simp add: C_def eq_divide_eq avg_def algebra_simps) qed simp have twos: "\n. y / 2 ^ n < r" if "0 < r" for y r :: rat proof - obtain n where "y / r < rat_of_nat n" using \0 < r\ reals_Archimedean2 by blast then have "\n. y < r * 2 ^ n" by (metis divide_less_eq less_trans mult.commute of_nat_less_two_power that) then show ?thesis by (simp add: field_split_simps) qed have PA: "\ P (A n)" for n by (induct n) (simp_all add: a) have PB: "P (B n)" for n by (induct n) (simp_all add: b) have ab: "a < b" using a b unfolding P_def by (meson leI less_le_trans of_rat_less) have AB: "A n < B n" for n by (induct n) (simp_all add: ab C_def avg_def) have "A i \ A j \ B j \ B i" if "i < j" for i j using that proof (induction rule: less_Suc_induct) case (1 i) then show ?case apply (clarsimp simp add: C_def avg_def add_divide_distrib [symmetric]) apply (rule AB [THEN less_imp_le]) done qed simp then have A_mono: "A i \ A j" and B_mono: "B j \ B i" if "i \ j" for i j by (metis eq_refl le_neq_implies_less that)+ have cauchy_lemma: "cauchy X" if *: "\n i. i\n \ A n \ X i \ X i \ B n" for X proof (rule cauchyI) fix r::rat assume "0 < r" then obtain k where k: "(b - a) / 2 ^ k < r" using twos by blast have "\X m - X n\ < r" if "m\k" "n\k" for m n proof - have "\X m - X n\ \ B k - A k" by (simp add: * abs_rat_def diff_mono that) also have "... < r" by (simp add: k width) finally show ?thesis . qed then show "\k. \m\k. \n\k. \X m - X n\ < r" by blast qed have "cauchy A" by (rule cauchy_lemma) (meson AB A_mono B_mono dual_order.strict_implies_order less_le_trans) have "cauchy B" by (rule cauchy_lemma) (meson AB A_mono B_mono dual_order.strict_implies_order le_less_trans) have "\x\S. x \ Real B" proof fix x assume "x \ S" then show "x \ Real B" using PB [unfolded P_def] \cauchy B\ by (simp add: le_RealI) qed moreover have "\z. (\x\S. x \ z) \ Real A \ z" by (meson PA Real_leI P_def \cauchy A\ le_cases order.trans) moreover have "vanishes (\n. (b - a) / 2 ^ n)" proof (rule vanishesI) fix r :: rat assume "0 < r" then obtain k where k: "\b - a\ / 2 ^ k < r" using twos by blast have "\n\k. \(b - a) / 2 ^ n\ < r" proof clarify fix n assume n: "k \ n" have "\(b - a) / 2 ^ n\ = \b - a\ / 2 ^ n" by simp also have "\ \ \b - a\ / 2 ^ k" using n by (simp add: divide_left_mono) also note k finally show "\(b - a) / 2 ^ n\ < r" . qed then show "\k. \n\k. \(b - a) / 2 ^ n\ < r" .. qed then have "Real B = Real A" by (simp add: eq_Real \cauchy A\ \cauchy B\ width) ultimately show "\y. (\x\S. x \ y) \ (\z. (\x\S. x \ z) \ y \ z)" by force qed instantiation real :: linear_continuum begin subsection \Supremum of a set of reals\ definition "Sup X = (LEAST z::real. \x\X. x \ z)" definition "Inf X = - Sup (uminus ` X)" for X :: "real set" instance proof show Sup_upper: "x \ Sup X" if "x \ X" "bdd_above X" for x :: real and X :: "real set" proof - from that obtain s where s: "\y\X. y \ s" "\z. \y\X. y \ z \ s \ z" using complete_real[of X] unfolding bdd_above_def by blast then show ?thesis unfolding Sup_real_def by (rule LeastI2_order) (auto simp: that) qed show Sup_least: "Sup X \ z" if "X \ {}" and z: "\x. x \ X \ x \ z" for z :: real and X :: "real set" proof - from that obtain s where s: "\y\X. y \ s" "\z. \y\X. y \ z \ s \ z" using complete_real [of X] by blast then have "Sup X = s" unfolding Sup_real_def by (best intro: Least_equality) also from s z have "\ \ z" by blast finally show ?thesis . qed show "Inf X \ x" if "x \ X" "bdd_below X" for x :: real and X :: "real set" using Sup_upper [of "-x" "uminus ` X"] by (auto simp: Inf_real_def that) show "z \ Inf X" if "X \ {}" "\x. x \ X \ z \ x" for z :: real and X :: "real set" using Sup_least [of "uminus ` X" "- z"] by (force simp: Inf_real_def that) show "\a b::real. a \ b" using zero_neq_one by blast qed end subsection \Hiding implementation details\ hide_const (open) vanishes cauchy positive Real declare Real_induct [induct del] declare Abs_real_induct [induct del] declare Abs_real_cases [cases del] lifting_update real.lifting lifting_forget real.lifting subsection \More Lemmas\ text \BH: These lemmas should not be necessary; they should be covered by existing simp rules and simplification procedures.\ lemma real_mult_less_iff1 [simp]: "0 < z \ x * z < y * z \ x < y" for x y z :: real by simp (* solved by linordered_ring_less_cancel_factor simproc *) lemma real_mult_le_cancel_iff1 [simp]: "0 < z \ x * z \ y * z \ x \ y" for x y z :: real by simp (* solved by linordered_ring_le_cancel_factor simproc *) lemma real_mult_le_cancel_iff2 [simp]: "0 < z \ z * x \ z * y \ x \ y" for x y z :: real by simp (* solved by linordered_ring_le_cancel_factor simproc *) subsection \Embedding numbers into the Reals\ abbreviation real_of_nat :: "nat \ real" where "real_of_nat \ of_nat" abbreviation real :: "nat \ real" where "real \ of_nat" abbreviation real_of_int :: "int \ real" where "real_of_int \ of_int" abbreviation real_of_rat :: "rat \ real" where "real_of_rat \ of_rat" declare [[coercion_enabled]] declare [[coercion "of_nat :: nat \ int"]] declare [[coercion "of_nat :: nat \ real"]] declare [[coercion "of_int :: int \ real"]] (* We do not add rat to the coerced types, this has often unpleasant side effects when writing inverse (Suc n) which sometimes gets two coercions: of_rat (inverse (of_nat (Suc n))) *) declare [[coercion_map map]] declare [[coercion_map "\f g h x. g (h (f x))"]] declare [[coercion_map "\f g (x,y). (f x, g y)"]] declare of_int_eq_0_iff [algebra, presburger] declare of_int_eq_1_iff [algebra, presburger] declare of_int_eq_iff [algebra, presburger] declare of_int_less_0_iff [algebra, presburger] declare of_int_less_1_iff [algebra, presburger] declare of_int_less_iff [algebra, presburger] declare of_int_le_0_iff [algebra, presburger] declare of_int_le_1_iff [algebra, presburger] declare of_int_le_iff [algebra, presburger] declare of_int_0_less_iff [algebra, presburger] declare of_int_0_le_iff [algebra, presburger] declare of_int_1_less_iff [algebra, presburger] declare of_int_1_le_iff [algebra, presburger] lemma int_less_real_le: "n < m \ real_of_int n + 1 \ real_of_int m" proof - have "(0::real) \ 1" by (metis less_eq_real_def zero_less_one) then show ?thesis by (metis floor_of_int less_floor_iff) qed lemma int_le_real_less: "n \ m \ real_of_int n < real_of_int m + 1" by (meson int_less_real_le not_le) lemma real_of_int_div_aux: "(real_of_int x) / (real_of_int d) = real_of_int (x div d) + (real_of_int (x mod d)) / (real_of_int d)" proof - have "x = (x div d) * d + x mod d" by auto then have "real_of_int x = real_of_int (x div d) * real_of_int d + real_of_int(x mod d)" by (metis of_int_add of_int_mult) then have "real_of_int x / real_of_int d = \ / real_of_int d" by simp then show ?thesis by (auto simp add: add_divide_distrib algebra_simps) qed lemma real_of_int_div: "d dvd n \ real_of_int (n div d) = real_of_int n / real_of_int d" for d n :: int by (simp add: real_of_int_div_aux) lemma real_of_int_div2: "0 \ real_of_int n / real_of_int x - real_of_int (n div x)" proof (cases "x = 0") case False then show ?thesis by (metis diff_ge_0_iff_ge floor_divide_of_int_eq of_int_floor_le) qed simp lemma real_of_int_div3: "real_of_int n / real_of_int x - real_of_int (n div x) \ 1" apply (simp add: algebra_simps) by (metis add.commute floor_correct floor_divide_of_int_eq less_eq_real_def of_int_1 of_int_add) lemma real_of_int_div4: "real_of_int (n div x) \ real_of_int n / real_of_int x" using real_of_int_div2 [of n x] by simp subsection \Embedding the Naturals into the Reals\ lemma real_of_card: "real (card A) = sum (\x. 1) A" by simp lemma nat_less_real_le: "n < m \ real n + 1 \ real m" by (metis discrete of_nat_1 of_nat_add of_nat_le_iff) lemma nat_le_real_less: "n \ m \ real n < real m + 1" for m n :: nat by (meson nat_less_real_le not_le) lemma real_of_nat_div_aux: "real x / real d = real (x div d) + real (x mod d) / real d" proof - have "x = (x div d) * d + x mod d" by auto then have "real x = real (x div d) * real d + real(x mod d)" by (metis of_nat_add of_nat_mult) then have "real x / real d = \ / real d" by simp then show ?thesis by (auto simp add: add_divide_distrib algebra_simps) qed lemma real_of_nat_div: "d dvd n \ real(n div d) = real n / real d" by (subst real_of_nat_div_aux) (auto simp add: dvd_eq_mod_eq_0 [symmetric]) lemma real_of_nat_div2: "0 \ real n / real x - real (n div x)" for n x :: nat apply (simp add: algebra_simps) by (metis floor_divide_of_nat_eq of_int_floor_le of_int_of_nat_eq) lemma real_of_nat_div3: "real n / real x - real (n div x) \ 1" for n x :: nat proof (cases "x = 0") case False then show ?thesis by (metis of_int_of_nat_eq real_of_int_div3 zdiv_int) qed auto lemma real_of_nat_div4: "real (n div x) \ real n / real x" for n x :: nat using real_of_nat_div2 [of n x] by simp subsection \The Archimedean Property of the Reals\ lemma real_arch_inverse: "0 < e \ (\n::nat. n \ 0 \ 0 < inverse (real n) \ inverse (real n) < e)" using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat] by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc) lemma reals_Archimedean3: "0 < x \ \y. \n. y < real n * x" by (auto intro: ex_less_of_nat_mult) lemma real_archimedian_rdiv_eq_0: assumes x0: "x \ 0" and c: "c \ 0" and xc: "\m::nat. m > 0 \ real m * x \ c" shows "x = 0" by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc) subsection \Rationals\ lemma Rats_abs_iff[simp]: "\(x::real)\ \ \ \ x \ \" by(simp add: abs_real_def split: if_splits) lemma Rats_eq_int_div_int: "\ = {real_of_int i / real_of_int j | i j. j \ 0}" (is "_ = ?S") proof show "\ \ ?S" proof fix x :: real assume "x \ \" then obtain r where "x = of_rat r" unfolding Rats_def .. have "of_rat r \ ?S" by (cases r) (auto simp add: of_rat_rat) then show "x \ ?S" using \x = of_rat r\ by simp qed next show "?S \ \" proof (auto simp: Rats_def) fix i j :: int assume "j \ 0" then have "real_of_int i / real_of_int j = of_rat (Fract i j)" by (simp add: of_rat_rat) then show "real_of_int i / real_of_int j \ range of_rat" by blast qed qed lemma Rats_eq_int_div_nat: "\ = { real_of_int i / real n | i n. n \ 0}" proof (auto simp: Rats_eq_int_div_int) fix i j :: int assume "j \ 0" show "\(i'::int) (n::nat). real_of_int i / real_of_int j = real_of_int i' / real n \ 0 < n" proof (cases "j > 0") case True then have "real_of_int i / real_of_int j = real_of_int i / real (nat j) \ 0 < nat j" by simp then show ?thesis by blast next case False with \j \ 0\ have "real_of_int i / real_of_int j = real_of_int (- i) / real (nat (- j)) \ 0 < nat (- j)" by simp then show ?thesis by blast qed next fix i :: int and n :: nat assume "0 < n" then have "real_of_int i / real n = real_of_int i / real_of_int(int n) \ int n \ 0" by simp then show "\i' j. real_of_int i / real n = real_of_int i' / real_of_int j \ j \ 0" by blast qed lemma Rats_abs_nat_div_natE: assumes "x \ \" obtains m n :: nat where "n \ 0" and "\x\ = real m / real n" and "coprime m n" proof - from \x \ \\ obtain i :: int and n :: nat where "n \ 0" and "x = real_of_int i / real n" by (auto simp add: Rats_eq_int_div_nat) then have "\x\ = real (nat \i\) / real n" by simp then obtain m :: nat where x_rat: "\x\ = real m / real n" by blast let ?gcd = "gcd m n" from \n \ 0\ have gcd: "?gcd \ 0" by simp let ?k = "m div ?gcd" let ?l = "n div ?gcd" let ?gcd' = "gcd ?k ?l" have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m" by (rule dvd_mult_div_cancel) have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n" by (rule dvd_mult_div_cancel) from \n \ 0\ and gcd_l have "?gcd * ?l \ 0" by simp then have "?l \ 0" by (blast dest!: mult_not_zero) moreover have "\x\ = real ?k / real ?l" proof - from gcd have "real ?k / real ?l = real (?gcd * ?k) / real (?gcd * ?l)" by (simp add: real_of_nat_div) also from gcd_k and gcd_l have "\ = real m / real n" by simp also from x_rat have "\ = \x\" .. finally show ?thesis .. qed moreover have "?gcd' = 1" proof - have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)" by (rule gcd_mult_distrib_nat) with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp with gcd show ?thesis by auto qed then have "coprime ?k ?l" by (simp only: coprime_iff_gcd_eq_1) ultimately show ?thesis .. qed subsection \Density of the Rational Reals in the Reals\ text \ This density proof is due to Stefan Richter and was ported by TN. The original source is \<^emph>\Real Analysis\ by H.L. Royden. It employs the Archimedean property of the reals.\ lemma Rats_dense_in_real: fixes x :: real assumes "x < y" shows "\r\\. x < r \ r < y" proof - from \x < y\ have "0 < y - x" by simp with reals_Archimedean obtain q :: nat where q: "inverse (real q) < y - x" and "0 < q" by blast define p where "p = \y * real q\ - 1" define r where "r = of_int p / real q" from q have "x < y - inverse (real q)" by simp also from \0 < q\ have "y - inverse (real q) \ r" by (simp add: r_def p_def le_divide_eq left_diff_distrib) finally have "x < r" . moreover from \0 < q\ have "r < y" by (simp add: r_def p_def divide_less_eq diff_less_eq less_ceiling_iff [symmetric]) moreover have "r \ \" by (simp add: r_def) ultimately show ?thesis by blast qed lemma of_rat_dense: fixes x y :: real assumes "x < y" shows "\q :: rat. x < of_rat q \ of_rat q < y" using Rats_dense_in_real [OF \x < y\] by (auto elim: Rats_cases) subsection \Numerals and Arithmetic\ declaration \ K (Lin_Arith.add_inj_const (\<^const_name>\of_nat\, \<^typ>\nat \ real\) #> Lin_Arith.add_inj_const (\<^const_name>\of_int\, \<^typ>\int \ real\)) \ subsection \Simprules combining \x + y\ and \0\\ (* FIXME ARE THEY NEEDED? *) lemma real_add_minus_iff [simp]: "x + - a = 0 \ x = a" for x a :: real by arith lemma real_add_less_0_iff: "x + y < 0 \ y < - x" for x y :: real by auto lemma real_0_less_add_iff: "0 < x + y \ - x < y" for x y :: real by auto lemma real_add_le_0_iff: "x + y \ 0 \ y \ - x" for x y :: real by auto lemma real_0_le_add_iff: "0 \ x + y \ - x \ y" for x y :: real by auto subsection \Lemmas about powers\ lemma two_realpow_ge_one: "(1::real) \ 2 ^ n" by simp (* FIXME: declare this [simp] for all types, or not at all *) declare sum_squares_eq_zero_iff [simp] sum_power2_eq_zero_iff [simp] lemma real_minus_mult_self_le [simp]: "- (u * u) \ x * x" for u x :: real by (rule order_trans [where y = 0]) auto lemma realpow_square_minus_le [simp]: "- u\<^sup>2 \ x\<^sup>2" for u x :: real by (auto simp add: power2_eq_square) subsection \Density of the Reals\ lemma field_lbound_gt_zero: "0 < d1 \ 0 < d2 \ \e. 0 < e \ e < d1 \ e < d2" for d1 d2 :: "'a::linordered_field" by (rule exI [where x = "min d1 d2 / 2"]) (simp add: min_def) lemma field_less_half_sum: "x < y \ x < (x + y) / 2" for x y :: "'a::linordered_field" by auto lemma field_sum_of_halves: "x / 2 + x / 2 = x" for x :: "'a::linordered_field" by simp +subsection \Archimedean properties and useful consequences\ + +text\Bernoulli's inequality\ +proposition Bernoulli_inequality: + fixes x :: real + assumes "-1 \ x" + shows "1 + n * x \ (1 + x) ^ n" +proof (induct n) + case 0 + then show ?case by simp +next + case (Suc n) + have "1 + Suc n * x \ 1 + (Suc n)*x + n * x^2" + by (simp add: algebra_simps) + also have "... = (1 + x) * (1 + n*x)" + by (auto simp: power2_eq_square algebra_simps) + also have "... \ (1 + x) ^ Suc n" + using Suc.hyps assms mult_left_mono by fastforce + finally show ?case . +qed + +corollary Bernoulli_inequality_even: + fixes x :: real + assumes "even n" + shows "1 + n * x \ (1 + x) ^ n" +proof (cases "-1 \ x \ n=0") + case True + then show ?thesis + by (auto simp: Bernoulli_inequality) +next + case False + then have "real n \ 1" + by simp + with False have "n * x \ -1" + by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one) + then have "1 + n * x \ 0" + by auto + also have "... \ (1 + x) ^ n" + using assms + using zero_le_even_power by blast + finally show ?thesis . +qed + +corollary real_arch_pow: + fixes x :: real + assumes x: "1 < x" + shows "\n. y < x^n" +proof - + from x have x0: "x - 1 > 0" + by arith + from reals_Archimedean3[OF x0, rule_format, of y] + obtain n :: nat where n: "y < real n * (x - 1)" by metis + from x0 have x00: "x- 1 \ -1" by arith + from Bernoulli_inequality[OF x00, of n] n + have "y < x^n" by auto + then show ?thesis by metis +qed + +corollary real_arch_pow_inv: + fixes x y :: real + assumes y: "y > 0" + and x1: "x < 1" + shows "\n. x^n < y" +proof (cases "x > 0") + case True + with x1 have ix: "1 < 1/x" by (simp add: field_simps) + from real_arch_pow[OF ix, of "1/y"] + obtain n where n: "1/y < (1/x)^n" by blast + then show ?thesis using y \x > 0\ + by (auto simp add: field_simps) +next + case False + with y x1 show ?thesis + by (metis less_le_trans not_less power_one_right) +qed + +lemma forall_pos_mono: + "(\d e::real. d < e \ P d \ P e) \ + (\n::nat. n \ 0 \ P (inverse (real n))) \ (\e. 0 < e \ P e)" + by (metis real_arch_inverse) + +lemma forall_pos_mono_1: + "(\d e::real. d < e \ P d \ P e) \ + (\n. P (inverse (real (Suc n)))) \ 0 < e \ P e" + apply (rule forall_pos_mono) + apply auto + apply (metis Suc_pred of_nat_Suc) + done + + subsection \Floor and Ceiling Functions from the Reals to the Integers\ (* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *) lemma real_of_nat_less_numeral_iff [simp]: "real n < numeral w \ n < numeral w" for n :: nat by (metis of_nat_less_iff of_nat_numeral) lemma numeral_less_real_of_nat_iff [simp]: "numeral w < real n \ numeral w < n" for n :: nat by (metis of_nat_less_iff of_nat_numeral) lemma numeral_le_real_of_nat_iff [simp]: "numeral n \ real m \ numeral n \ m" for m :: nat by (metis not_le real_of_nat_less_numeral_iff) lemma of_int_floor_cancel [simp]: "of_int \x\ = x \ (\n::int. x = of_int n)" by (metis floor_of_int) lemma floor_eq: "real_of_int n < x \ x < real_of_int n + 1 \ \x\ = n" by linarith lemma floor_eq2: "real_of_int n \ x \ x < real_of_int n + 1 \ \x\ = n" by (fact floor_unique) lemma floor_eq3: "real n < x \ x < real (Suc n) \ nat \x\ = n" by linarith lemma floor_eq4: "real n \ x \ x < real (Suc n) \ nat \x\ = n" by linarith lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \ real_of_int \r\" by linarith lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real_of_int \r\" by linarith lemma real_of_int_floor_add_one_ge [simp]: "r \ real_of_int \r\ + 1" by linarith lemma real_of_int_floor_add_one_gt [simp]: "r < real_of_int \r\ + 1" by linarith lemma floor_divide_real_eq_div: assumes "0 \ b" shows "\a / real_of_int b\ = \a\ div b" proof (cases "b = 0") case True then show ?thesis by simp next case False with assms have b: "b > 0" by simp have "j = i div b" if "real_of_int i \ a" "a < 1 + real_of_int i" "real_of_int j * real_of_int b \ a" "a < real_of_int b + real_of_int j * real_of_int b" for i j :: int proof - from that have "i < b + j * b" by (metis le_less_trans of_int_add of_int_less_iff of_int_mult) moreover have "j * b < 1 + i" proof - have "real_of_int (j * b) < real_of_int i + 1" using \a < 1 + real_of_int i\ \real_of_int j * real_of_int b \ a\ by force then show "j * b < 1 + i" by linarith qed ultimately have "(j - i div b) * b \ i mod b" "i mod b < ((j - i div b) + 1) * b" by (auto simp: field_simps) then have "(j - i div b) * b < 1 * b" "0 * b < ((j - i div b) + 1) * b" using pos_mod_bound [OF b, of i] pos_mod_sign [OF b, of i] by linarith+ then show ?thesis using b unfolding mult_less_cancel_right by auto qed with b show ?thesis by (auto split: floor_split simp: field_simps) qed lemma floor_one_divide_eq_div_numeral [simp]: "\1 / numeral b::real\ = 1 div numeral b" by (metis floor_divide_of_int_eq of_int_1 of_int_numeral) lemma floor_minus_one_divide_eq_div_numeral [simp]: "\- (1 / numeral b)::real\ = - 1 div numeral b" by (metis (mono_tags, hide_lams) div_minus_right minus_divide_right floor_divide_of_int_eq of_int_neg_numeral of_int_1) lemma floor_divide_eq_div_numeral [simp]: "\numeral a / numeral b::real\ = numeral a div numeral b" by (metis floor_divide_of_int_eq of_int_numeral) lemma floor_minus_divide_eq_div_numeral [simp]: "\- (numeral a / numeral b)::real\ = - numeral a div numeral b" by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral) lemma of_int_ceiling_cancel [simp]: "of_int \x\ = x \ (\n::int. x = of_int n)" using ceiling_of_int by metis lemma ceiling_eq: "of_int n < x \ x \ of_int n + 1 \ \x\ = n + 1" by (simp add: ceiling_unique) lemma of_int_ceiling_diff_one_le [simp]: "of_int \r\ - 1 \ r" by linarith lemma of_int_ceiling_le_add_one [simp]: "of_int \r\ \ r + 1" by linarith lemma ceiling_le: "x \ of_int a \ \x\ \ a" by (simp add: ceiling_le_iff) lemma ceiling_divide_eq_div: "\of_int a / of_int b\ = - (- a div b)" by (metis ceiling_def floor_divide_of_int_eq minus_divide_left of_int_minus) lemma ceiling_divide_eq_div_numeral [simp]: "\numeral a / numeral b :: real\ = - (- numeral a div numeral b)" using ceiling_divide_eq_div[of "numeral a" "numeral b"] by simp lemma ceiling_minus_divide_eq_div_numeral [simp]: "\- (numeral a / numeral b :: real)\ = - (numeral a div numeral b)" using ceiling_divide_eq_div[of "- numeral a" "numeral b"] by simp text \ The following lemmas are remnants of the erstwhile functions natfloor and natceiling. \ lemma nat_floor_neg: "x \ 0 \ nat \x\ = 0" for x :: real by linarith lemma le_nat_floor: "real x \ a \ x \ nat \a\" by linarith lemma le_mult_nat_floor: "nat \a\ * nat \b\ \ nat \a * b\" by (cases "0 \ a \ 0 \ b") (auto simp add: nat_mult_distrib[symmetric] nat_mono le_mult_floor) lemma nat_ceiling_le_eq [simp]: "nat \x\ \ a \ x \ real a" by linarith lemma real_nat_ceiling_ge: "x \ real (nat \x\)" by linarith lemma Rats_no_top_le: "\q \ \. x \ q" for x :: real by (auto intro!: bexI[of _ "of_nat (nat \x\)"]) linarith lemma Rats_no_bot_less: "\q \ \. q < x" for x :: real by (auto intro!: bexI[of _ "of_int (\x\ - 1)"]) linarith subsection \Exponentiation with floor\ lemma floor_power: assumes "x = of_int \x\" shows "\x ^ n\ = \x\ ^ n" proof - have "x ^ n = of_int (\x\ ^ n)" using assms by (induct n arbitrary: x) simp_all then show ?thesis by (metis floor_of_int) qed lemma floor_numeral_power [simp]: "\numeral x ^ n\ = numeral x ^ n" by (metis floor_of_int of_int_numeral of_int_power) lemma ceiling_numeral_power [simp]: "\numeral x ^ n\ = numeral x ^ n" by (metis ceiling_of_int of_int_numeral of_int_power) subsection \Implementation of rational real numbers\ text \Formal constructor\ definition Ratreal :: "rat \ real" where [code_abbrev, simp]: "Ratreal = real_of_rat" code_datatype Ratreal text \Quasi-Numerals\ lemma [code_abbrev]: "real_of_rat (numeral k) = numeral k" "real_of_rat (- numeral k) = - numeral k" "real_of_rat (rat_of_int a) = real_of_int a" by simp_all lemma [code_post]: "real_of_rat 0 = 0" "real_of_rat 1 = 1" "real_of_rat (- 1) = - 1" "real_of_rat (1 / numeral k) = 1 / numeral k" "real_of_rat (numeral k / numeral l) = numeral k / numeral l" "real_of_rat (- (1 / numeral k)) = - (1 / numeral k)" "real_of_rat (- (numeral k / numeral l)) = - (numeral k / numeral l)" by (simp_all add: of_rat_divide of_rat_minus) text \Operations\ lemma zero_real_code [code]: "0 = Ratreal 0" by simp lemma one_real_code [code]: "1 = Ratreal 1" by simp instantiation real :: equal begin definition "HOL.equal x y \ x - y = 0" for x :: real instance by standard (simp add: equal_real_def) lemma real_equal_code [code]: "HOL.equal (Ratreal x) (Ratreal y) \ HOL.equal x y" by (simp add: equal_real_def equal) lemma [code nbe]: "HOL.equal x x \ True" for x :: real by (rule equal_refl) end lemma real_less_eq_code [code]: "Ratreal x \ Ratreal y \ x \ y" by (simp add: of_rat_less_eq) lemma real_less_code [code]: "Ratreal x < Ratreal y \ x < y" by (simp add: of_rat_less) lemma real_plus_code [code]: "Ratreal x + Ratreal y = Ratreal (x + y)" by (simp add: of_rat_add) lemma real_times_code [code]: "Ratreal x * Ratreal y = Ratreal (x * y)" by (simp add: of_rat_mult) lemma real_uminus_code [code]: "- Ratreal x = Ratreal (- x)" by (simp add: of_rat_minus) lemma real_minus_code [code]: "Ratreal x - Ratreal y = Ratreal (x - y)" by (simp add: of_rat_diff) lemma real_inverse_code [code]: "inverse (Ratreal x) = Ratreal (inverse x)" by (simp add: of_rat_inverse) lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)" by (simp add: of_rat_divide) lemma real_floor_code [code]: "\Ratreal x\ = \x\" by (metis Ratreal_def floor_le_iff floor_unique le_floor_iff of_int_floor_le of_rat_of_int_eq real_less_eq_code) text \Quickcheck\ definition (in term_syntax) valterm_ratreal :: "rat \ (unit \ Code_Evaluation.term) \ real \ (unit \ Code_Evaluation.term)" where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\} k" notation fcomp (infixl "\>" 60) notation scomp (infixl "\\" 60) instantiation real :: random begin definition "Quickcheck_Random.random i = Quickcheck_Random.random i \\ (\r. Pair (valterm_ratreal r))" instance .. end no_notation fcomp (infixl "\>" 60) no_notation scomp (infixl "\\" 60) instantiation real :: exhaustive begin definition "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (\r. f (Ratreal r)) d" instance .. end instantiation real :: full_exhaustive begin definition "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (\r. f (valterm_ratreal r)) d" instance .. end instantiation real :: narrowing begin definition "narrowing_real = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing" instance .. end subsection \Setup for Nitpick\ declaration \ Nitpick_HOL.register_frac_type \<^type_name>\real\ [(\<^const_name>\zero_real_inst.zero_real\, \<^const_name>\Nitpick.zero_frac\), (\<^const_name>\one_real_inst.one_real\, \<^const_name>\Nitpick.one_frac\), (\<^const_name>\plus_real_inst.plus_real\, \<^const_name>\Nitpick.plus_frac\), (\<^const_name>\times_real_inst.times_real\, \<^const_name>\Nitpick.times_frac\), (\<^const_name>\uminus_real_inst.uminus_real\, \<^const_name>\Nitpick.uminus_frac\), (\<^const_name>\inverse_real_inst.inverse_real\, \<^const_name>\Nitpick.inverse_frac\), (\<^const_name>\ord_real_inst.less_real\, \<^const_name>\Nitpick.less_frac\), (\<^const_name>\ord_real_inst.less_eq_real\, \<^const_name>\Nitpick.less_eq_frac\)] \ lemmas [nitpick_unfold] = inverse_real_inst.inverse_real one_real_inst.one_real ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real times_real_inst.times_real uminus_real_inst.uminus_real zero_real_inst.zero_real subsection \Setup for SMT\ ML_file \Tools/SMT/smt_real.ML\ ML_file \Tools/SMT/z3_real.ML\ lemma [z3_rule]: "0 + x = x" "x + 0 = x" "0 * x = 0" "1 * x = x" "-x = -1 * x" "x + y = y + x" for x y :: real by auto subsection \Setup for Argo\ ML_file \Tools/Argo/argo_real.ML\ end