--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Feb 06 15:41:23 2023 +0000
@@ -6,7 +6,7 @@
text \<open>Definitions of analytic and holomorphic functions, limit theorems, complex differentiation\<close>
theory Complex_Analysis_Basics
- imports Derivative "HOL-Library.Nonpos_Ints"
+ imports Derivative "HOL-Library.Nonpos_Ints" Uncountable_Sets
begin
subsection\<^marker>\<open>tag unimportant\<close>\<open>General lemmas\<close>
@@ -51,6 +51,50 @@
by (intro open_Collect_less closed_Collect_le closed_Collect_eq continuous_on_Re
continuous_on_Im continuous_on_id continuous_on_const)+
+lemma uncountable_halfspace_Im_gt: "uncountable {z. Im z > c}"
+proof -
+ obtain r where r: "r > 0" "ball ((c + 1) *\<^sub>R \<i>) r \<subseteq> {z. Im z > c}"
+ using open_halfspace_Im_gt[of c] unfolding open_contains_ball by force
+ then show ?thesis
+ using countable_subset uncountable_ball by blast
+qed
+
+lemma uncountable_halfspace_Im_lt: "uncountable {z. Im z < c}"
+proof -
+ obtain r where r: "r > 0" "ball ((c - 1) *\<^sub>R \<i>) r \<subseteq> {z. Im z < c}"
+ using open_halfspace_Im_lt[of c] unfolding open_contains_ball by force
+ then show ?thesis
+ using countable_subset uncountable_ball by blast
+qed
+
+lemma uncountable_halfspace_Re_gt: "uncountable {z. Re z > c}"
+proof -
+ obtain r where r: "r > 0" "ball (of_real(c + 1)) r \<subseteq> {z. Re z > c}"
+ using open_halfspace_Re_gt[of c] unfolding open_contains_ball by force
+ then show ?thesis
+ using countable_subset uncountable_ball by blast
+qed
+
+lemma uncountable_halfspace_Re_lt: "uncountable {z. Re z < c}"
+proof -
+ obtain r where r: "r > 0" "ball (of_real(c - 1)) r \<subseteq> {z. Re z < c}"
+ using open_halfspace_Re_lt[of c] unfolding open_contains_ball by force
+ then show ?thesis
+ using countable_subset uncountable_ball by blast
+qed
+
+lemma connected_halfspace_Im_gt [intro]: "connected {z. c < Im z}"
+ by (intro convex_connected convex_halfspace_Im_gt)
+
+lemma connected_halfspace_Im_lt [intro]: "connected {z. c > Im z}"
+ by (intro convex_connected convex_halfspace_Im_lt)
+
+lemma connected_halfspace_Re_gt [intro]: "connected {z. c < Re z}"
+ by (intro convex_connected convex_halfspace_Re_gt)
+
+lemma connected_halfspace_Re_lt [intro]: "connected {z. c > Re z}"
+ by (intro convex_connected convex_halfspace_Re_lt)
+
lemma closed_complex_Reals: "closed (\<real> :: complex set)"
proof -
have "(\<real> :: complex set) = {z. Im z = 0}"
--- a/src/HOL/Analysis/Complex_Transcendental.thy Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Mon Feb 06 15:41:23 2023 +0000
@@ -84,6 +84,41 @@
"f holomorphic_on s \<Longrightarrow> (\<lambda>x. exp (f x)) holomorphic_on s"
using holomorphic_on_compose[OF _ holomorphic_on_exp] by (simp add: o_def)
+lemma exp_analytic_on [analytic_intros]:
+ assumes "f analytic_on A"
+ shows "(\<lambda>z. exp (f z)) analytic_on A"
+ by (metis analytic_on_holomorphic assms holomorphic_on_exp')
+
+lemma
+ assumes "\<And>w. w \<in> A \<Longrightarrow> exp (f w) = w"
+ assumes "f holomorphic_on A" "z \<in> A" "open A"
+ shows deriv_complex_logarithm: "deriv f z = 1 / z"
+ and has_field_derivative_complex_logarithm: "(f has_field_derivative 1 / z) (at z)"
+proof -
+ have [simp]: "z \<noteq> 0"
+ using assms(1)[of z] assms(3) by auto
+ have deriv [derivative_intros]: "(f has_field_derivative deriv f z) (at z)"
+ using assms holomorphic_derivI by blast
+ have "((\<lambda>w. w) has_field_derivative 1) (at z)"
+ by (intro derivative_intros)
+ also have "?this \<longleftrightarrow> ((\<lambda>w. exp (f w)) has_field_derivative 1) (at z)"
+ proof (rule DERIV_cong_ev)
+ have "eventually (\<lambda>w. w \<in> A) (nhds z)"
+ using assms by (intro eventually_nhds_in_open) auto
+ thus "eventually (\<lambda>w. w = exp (f w)) (nhds z)"
+ by eventually_elim (use assms in auto)
+ qed auto
+ finally have "((\<lambda>w. exp (f w)) has_field_derivative 1) (at z)" .
+ moreover have "((\<lambda>w. exp (f w)) has_field_derivative exp (f z) * deriv f z) (at z)"
+ by (rule derivative_eq_intros refl)+
+ ultimately have "exp (f z) * deriv f z = 1"
+ using DERIV_unique by blast
+ with assms show "deriv f z = 1 / z"
+ by (simp add: field_simps)
+ with deriv show "(f has_field_derivative 1 / z) (at z)"
+ by simp
+qed
+
subsection\<open>Euler and de Moivre formulas\<close>
text\<open>The sine series times \<^term>\<open>i\<close>\<close>
@@ -2602,6 +2637,9 @@
lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
using Ln_Reals_eq norm_exp_eq_Re by (auto simp: Im_Ln_eq_0 powr_def norm_complex_def)
+lemma norm_powr_real_powr': "w \<in> \<real> \<Longrightarrow> norm (z powr w) = norm z powr Re w"
+ by (auto simp: powr_def Reals_def)
+
lemma powr_complexpow [simp]:
fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (of_nat n) = x^n"
by (induct n) (auto simp: ac_simps powr_add)
--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy Mon Feb 06 15:41:23 2023 +0000
@@ -176,9 +176,7 @@
qed
lemma uncountable_closed_interval: "uncountable {a..b} \<longleftrightarrow> a < b" for a b :: real
- apply (rule iffI)
- apply (metis atLeastAtMost_singleton atLeastatMost_empty countable_finite finite.emptyI finite_insert linorder_neqE_linordered_idom)
- using real_interval_avoid_countable_set by fastforce
+ using infinite_Icc_iff by (fastforce dest: countable_finite real_interval_avoid_countable_set)
lemma open_minus_countable:
fixes S A :: "real set"
--- a/src/HOL/Analysis/Elementary_Topology.thy Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Mon Feb 06 15:41:23 2023 +0000
@@ -618,31 +618,18 @@
lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
by (simp add: islimpt_iff_eventually eventually_conj_iff)
+lemma islimpt_finite_union_iff:
+ assumes "finite A"
+ shows "z islimpt (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. z islimpt B x)"
+ using assms by (induction rule: finite_induct) (simp_all add: islimpt_Un)
lemma islimpt_insert:
fixes x :: "'a::t1_space"
shows "x islimpt (insert a s) \<longleftrightarrow> x islimpt s"
proof
- assume *: "x islimpt (insert a s)"
- show "x islimpt s"
- proof (rule islimptI)
- fix t
- assume t: "x \<in> t" "open t"
- show "\<exists>y\<in>s. y \<in> t \<and> y \<noteq> x"
- proof (cases "x = a")
- case True
- obtain y where "y \<in> insert a s" "y \<in> t" "y \<noteq> x"
- using * t by (rule islimptE)
- with \<open>x = a\<close> show ?thesis by auto
- next
- case False
- with t have t': "x \<in> t - {a}" "open (t - {a})"
- by (simp_all add: open_Diff)
- obtain y where "y \<in> insert a s" "y \<in> t - {a}" "y \<noteq> x"
- using * t' by (rule islimptE)
- then show ?thesis by auto
- qed
- qed
+ assume "x islimpt (insert a s)"
+ then show "x islimpt s"
+ by (metis closed_limpt closed_singleton empty_iff insert_iff insert_is_Un islimpt_Un islimpt_def)
next
assume "x islimpt s"
then show "x islimpt (insert a s)"
--- a/src/HOL/Analysis/Homeomorphism.thy Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy Mon Feb 06 15:41:23 2023 +0000
@@ -1017,6 +1017,14 @@
pairwise disjnt v \<and>
(\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
+lemma covering_spaceI [intro?]:
+ assumes "continuous_on c p" "p ` c = S"
+ "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> openin (top_of_set S) T \<and>
+ (\<exists>v. \<Union>v = c \<inter> p -` T \<and> (\<forall>u \<in> v. openin (top_of_set c) u) \<and>
+ pairwise disjnt v \<and> (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q))"
+ shows "covering_space c p S"
+ using assms unfolding covering_space_def by auto
+
lemma covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
by (simp add: covering_space_def)
--- a/src/HOL/Analysis/Homotopy.thy Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Homotopy.thy Mon Feb 06 15:41:23 2023 +0000
@@ -5,7 +5,7 @@
section \<open>Homotopy of Maps\<close>
theory Homotopy
- imports Path_Connected Continuum_Not_Denumerable Product_Topology
+ imports Path_Connected Product_Topology Uncountable_Sets
begin
definition\<^marker>\<open>tag important\<close> homotopic_with
@@ -4169,144 +4169,16 @@
by blast
qed
-
-subsection\<^marker>\<open>tag unimportant\<close>\<open>Some Uncountable Sets\<close>
-
-lemma uncountable_closed_segment:
- fixes a :: "'a::real_normed_vector"
- assumes "a \<noteq> b" shows "uncountable (closed_segment a b)"
-unfolding path_image_linepath [symmetric] path_image_def
- using inj_on_linepath [OF assms] uncountable_closed_interval [of 0 1]
- countable_image_inj_on by auto
-
-lemma uncountable_open_segment:
- fixes a :: "'a::real_normed_vector"
- assumes "a \<noteq> b" shows "uncountable (open_segment a b)"
- by (simp add: assms open_segment_def uncountable_closed_segment uncountable_minus_countable)
-
-lemma uncountable_convex:
- fixes a :: "'a::real_normed_vector"
- assumes "convex S" "a \<in> S" "b \<in> S" "a \<noteq> b"
- shows "uncountable S"
-proof -
- have "uncountable (closed_segment a b)"
- by (simp add: uncountable_closed_segment assms)
- then show ?thesis
- by (meson assms convex_contains_segment countable_subset)
-qed
-
-lemma uncountable_ball:
- fixes a :: "'a::euclidean_space"
- assumes "r > 0"
- shows "uncountable (ball a r)"
-proof -
- have "uncountable (open_segment a (a + r *\<^sub>R (SOME i. i \<in> Basis)))"
- by (metis Basis_zero SOME_Basis add_cancel_right_right assms less_le scale_eq_0_iff uncountable_open_segment)
- moreover have "open_segment a (a + r *\<^sub>R (SOME i. i \<in> Basis)) \<subseteq> ball a r"
- using assms by (auto simp: in_segment algebra_simps dist_norm SOME_Basis)
- ultimately show ?thesis
- by (metis countable_subset)
-qed
-
-lemma ball_minus_countable_nonempty:
- assumes "countable (A :: 'a :: euclidean_space set)" "r > 0"
- shows "ball z r - A \<noteq> {}"
-proof
- assume *: "ball z r - A = {}"
- have "uncountable (ball z r - A)"
- by (intro uncountable_minus_countable assms uncountable_ball)
- thus False by (subst (asm) *) auto
-qed
-
-lemma uncountable_cball:
- fixes a :: "'a::euclidean_space"
- assumes "r > 0"
- shows "uncountable (cball a r)"
- using assms countable_subset uncountable_ball by auto
-
-lemma pairwise_disjnt_countable:
- fixes \<N> :: "nat set set"
- assumes "pairwise disjnt \<N>"
- shows "countable \<N>"
-proof -
- have "inj_on (\<lambda>X. SOME n. n \<in> X) (\<N> - {{}})"
- by (clarsimp simp: inj_on_def) (metis assms disjnt_iff pairwiseD some_in_eq)
- then show ?thesis
- by (metis countable_Diff_eq countable_def)
-qed
-
-lemma pairwise_disjnt_countable_Union:
- assumes "countable (\<Union>\<N>)" and pwd: "pairwise disjnt \<N>"
- shows "countable \<N>"
-proof -
- obtain f :: "_ \<Rightarrow> nat" where f: "inj_on f (\<Union>\<N>)"
- using assms by blast
- then have "pairwise disjnt (\<Union> X \<in> \<N>. {f ` X})"
- using assms by (force simp: pairwise_def disjnt_inj_on_iff [OF f])
- then have "countable (\<Union> X \<in> \<N>. {f ` X})"
- using pairwise_disjnt_countable by blast
- then show ?thesis
- by (meson pwd countable_image_inj_on disjoint_image f inj_on_image pairwise_disjnt_countable)
-qed
-
-lemma connected_uncountable:
+lemma connected_card_eq_iff_nontrivial:
fixes S :: "'a::metric_space set"
- assumes "connected S" "a \<in> S" "b \<in> S" "a \<noteq> b" shows "uncountable S"
-proof -
- have "continuous_on S (dist a)"
- by (intro continuous_intros)
- then have "connected (dist a ` S)"
- by (metis connected_continuous_image \<open>connected S\<close>)
- then have "closed_segment 0 (dist a b) \<subseteq> (dist a ` S)"
- by (simp add: assms closed_segment_subset is_interval_connected_1 is_interval_convex)
- then have "uncountable (dist a ` S)"
- by (metis \<open>a \<noteq> b\<close> countable_subset dist_eq_0_iff uncountable_closed_segment)
- then show ?thesis
- by blast
-qed
-
-lemma path_connected_uncountable:
- fixes S :: "'a::metric_space set"
- assumes "path_connected S" "a \<in> S" "b \<in> S" "a \<noteq> b" shows "uncountable S"
- using path_connected_imp_connected assms connected_uncountable by metis
+ shows "connected S \<Longrightarrow> uncountable S \<longleftrightarrow> \<not>(\<exists>a. S \<subseteq> {a})"
+ by (metis connected_uncountable finite.emptyI finite.insertI rev_finite_subset singleton_iff subsetI uncountable_infinite)
lemma connected_finite_iff_sing:
fixes S :: "'a::metric_space set"
assumes "connected S"
- shows "finite S \<longleftrightarrow> S = {} \<or> (\<exists>a. S = {a})" (is "_ = ?rhs")
-proof -
- have "uncountable S" if "\<not> ?rhs"
- using connected_uncountable assms that by blast
- then show ?thesis
- using uncountable_infinite by auto
-qed
-
-lemma connected_card_eq_iff_nontrivial:
- fixes S :: "'a::metric_space set"
- shows "connected S \<Longrightarrow> uncountable S \<longleftrightarrow> \<not>(\<exists>a. S \<subseteq> {a})"
- by (metis connected_uncountable finite.emptyI finite.insertI rev_finite_subset singleton_iff subsetI uncountable_infinite)
-
-lemma simple_path_image_uncountable:
- fixes g :: "real \<Rightarrow> 'a::metric_space"
- assumes "simple_path g"
- shows "uncountable (path_image g)"
-proof -
- have "g 0 \<in> path_image g" "g (1/2) \<in> path_image g"
- by (simp_all add: path_defs)
- moreover have "g 0 \<noteq> g (1/2)"
- using assms by (fastforce simp add: simple_path_def loop_free_def)
- ultimately have "\<forall>a. \<not> path_image g \<subseteq> {a}"
- by blast
- then show ?thesis
- using assms connected_simple_path_image connected_uncountable by blast
-qed
-
-lemma arc_image_uncountable:
- fixes g :: "real \<Rightarrow> 'a::metric_space"
- assumes "arc g"
- shows "uncountable (path_image g)"
- by (simp add: arc_imp_simple_path assms simple_path_image_uncountable)
-
+ shows "finite S \<longleftrightarrow> S = {} \<or> (\<exists>a. S = {a})"
+ using assms connected_uncountable countable_finite by blast
subsection\<^marker>\<open>tag unimportant\<close>\<open> Some simple positive connection theorems\<close>
--- a/src/HOL/Analysis/Isolated.thy Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Analysis/Isolated.thy Mon Feb 06 15:41:23 2023 +0000
@@ -3,49 +3,49 @@
begin
-subsection \<open>Isolate and discrete\<close>
-
-definition (in topological_space) isolate:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "isolate" 60)
- where "x isolate S \<longleftrightarrow> (x\<in>S \<and> (\<exists>T. open T \<and> T \<inter> S = {x}))"
-
-definition (in topological_space) discrete:: "'a set \<Rightarrow> bool"
- where "discrete S \<longleftrightarrow> (\<forall>x\<in>S. x isolate S)"
-
+subsection \<open>Isolate and discrete\<close>
+
+definition (in topological_space) isolated_in:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "isolated'_in" 60)
+ where "x isolated_in S \<longleftrightarrow> (x\<in>S \<and> (\<exists>T. open T \<and> T \<inter> S = {x}))"
+
+definition (in topological_space) discrete:: "'a set \<Rightarrow> bool"
+ where "discrete S \<longleftrightarrow> (\<forall>x\<in>S. x isolated_in S)"
+
definition (in metric_space) uniform_discrete :: "'a set \<Rightarrow> bool" where
"uniform_discrete S \<longleftrightarrow> (\<exists>e>0. \<forall>x\<in>S. \<forall>y\<in>S. dist x y < e \<longrightarrow> x = y)"
-
+
lemma uniformI1:
assumes "e>0" "\<And>x y. \<lbrakk>x\<in>S;y\<in>S;dist x y<e\<rbrakk> \<Longrightarrow> x =y "
- shows "uniform_discrete S"
+ shows "uniform_discrete S"
unfolding uniform_discrete_def using assms by auto
lemma uniformI2:
assumes "e>0" "\<And>x y. \<lbrakk>x\<in>S;y\<in>S;x\<noteq>y\<rbrakk> \<Longrightarrow> dist x y\<ge>e "
- shows "uniform_discrete S"
+ shows "uniform_discrete S"
unfolding uniform_discrete_def using assms not_less by blast
-
-lemma isolate_islimpt_iff:"(x isolate S) \<longleftrightarrow> (\<not> (x islimpt S) \<and> x\<in>S)"
- unfolding isolate_def islimpt_def by auto
-
-lemma isolate_dist_Ex_iff:
+
+lemma isolated_in_islimpt_iff:"(x isolated_in S) \<longleftrightarrow> (\<not> (x islimpt S) \<and> x\<in>S)"
+ unfolding isolated_in_def islimpt_def by auto
+
+lemma isolated_in_dist_Ex_iff:
fixes x::"'a::metric_space"
- shows "x isolate S \<longleftrightarrow> (x\<in>S \<and> (\<exists>e>0. \<forall>y\<in>S. dist x y < e \<longrightarrow> y=x))"
-unfolding isolate_islimpt_iff islimpt_approachable by (metis dist_commute)
-
+ shows "x isolated_in S \<longleftrightarrow> (x\<in>S \<and> (\<exists>e>0. \<forall>y\<in>S. dist x y < e \<longrightarrow> y=x))"
+unfolding isolated_in_islimpt_iff islimpt_approachable by (metis dist_commute)
+
lemma discrete_empty[simp]: "discrete {}"
unfolding discrete_def by auto
lemma uniform_discrete_empty[simp]: "uniform_discrete {}"
unfolding uniform_discrete_def by (simp add: gt_ex)
-
-lemma isolate_insert:
+
+lemma isolated_in_insert:
fixes x :: "'a::t1_space"
- shows "x isolate (insert a S) \<longleftrightarrow> x isolate S \<or> (x=a \<and> \<not> (x islimpt S))"
-by (meson insert_iff islimpt_insert isolate_islimpt_iff)
-
+ shows "x isolated_in (insert a S) \<longleftrightarrow> x isolated_in S \<or> (x=a \<and> \<not> (x islimpt S))"
+by (meson insert_iff islimpt_insert isolated_in_islimpt_iff)
+
(*
-TODO.
-Other than
+TODO.
+Other than
uniform_discrete S \<longrightarrow> discrete S
uniform_discrete S \<longrightarrow> closed S
@@ -58,31 +58,31 @@
http://topology.auburn.edu/tp/reprints/v30/tp30120.pdf
http://msp.org/pjm/1959/9-2/pjm-v9-n2-p19-s.pdf
-*)
-
+*)
+
lemma uniform_discrete_imp_closed:
- "uniform_discrete S \<Longrightarrow> closed S"
- by (meson discrete_imp_closed uniform_discrete_def)
-
+ "uniform_discrete S \<Longrightarrow> closed S"
+ by (meson discrete_imp_closed uniform_discrete_def)
+
lemma uniform_discrete_imp_discrete:
"uniform_discrete S \<Longrightarrow> discrete S"
- by (metis discrete_def isolate_dist_Ex_iff uniform_discrete_def)
-
-lemma isolate_subset:"x isolate S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> x\<in>T \<Longrightarrow> x isolate T"
- unfolding isolate_def by fastforce
+ by (metis discrete_def isolated_in_dist_Ex_iff uniform_discrete_def)
+
+lemma isolated_in_subset:"x isolated_in S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> x\<in>T \<Longrightarrow> x isolated_in T"
+ unfolding isolated_in_def by fastforce
lemma discrete_subset[elim]: "discrete S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> discrete T"
- unfolding discrete_def using islimpt_subset isolate_islimpt_iff by blast
-
+ unfolding discrete_def using islimpt_subset isolated_in_islimpt_iff by blast
+
lemma uniform_discrete_subset[elim]: "uniform_discrete S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> uniform_discrete T"
by (meson subsetD uniform_discrete_def)
-
-lemma continuous_on_discrete: "discrete S \<Longrightarrow> continuous_on S f"
- unfolding continuous_on_topological by (metis discrete_def islimptI isolate_islimpt_iff)
-
+
+lemma continuous_on_discrete: "discrete S \<Longrightarrow> continuous_on S f"
+ unfolding continuous_on_topological by (metis discrete_def islimptI isolated_in_islimpt_iff)
+
lemma uniform_discrete_insert: "uniform_discrete (insert a S) \<longleftrightarrow> uniform_discrete S"
-proof
- assume asm:"uniform_discrete S"
+proof
+ assume asm:"uniform_discrete S"
let ?thesis = "uniform_discrete (insert a S)"
have ?thesis when "a\<in>S" using that asm by (simp add: insert_absorb)
moreover have ?thesis when "S={}" using that asm by (simp add: uniform_discrete_def)
@@ -94,44 +94,38 @@
have "closed S" using asm uniform_discrete_imp_closed by auto
then have "e2>0"
by (smt (verit) \<open>0 < e1\<close> e2_def infdist_eq_setdist infdist_pos_not_in_closed that)
- moreover have "x = y" when "x\<in>insert a S" "y\<in>insert a S" "dist x y < e2 " for x y
- proof -
- have ?thesis when "x=a" "y=a" using that by auto
- moreover have ?thesis when "x=a" "y\<in>S"
- using that setdist_le_dist[of x "{a}" y S] \<open>dist x y < e2\<close> unfolding e2_def
- by fastforce
- moreover have ?thesis when "y=a" "x\<in>S"
- using that setdist_le_dist[of y "{a}" x S] \<open>dist x y < e2\<close> unfolding e2_def
- by (simp add: dist_commute)
- moreover have ?thesis when "x\<in>S" "y\<in>S"
- using e1_dist[rule_format, OF that] \<open>dist x y < e2\<close> unfolding e2_def
- by (simp add: dist_commute)
- ultimately show ?thesis using that by auto
+ moreover have "x = y" if "x\<in>insert a S" "y\<in>insert a S" "dist x y < e2" for x y
+ proof (cases "x=a \<or> y=a")
+ case True then show ?thesis
+ by (smt (verit, best) dist_commute e2_def infdist_eq_setdist infdist_le insertE that)
+ next
+ case False then show ?thesis
+ using e1_dist e2_def that by force
qed
ultimately show ?thesis unfolding uniform_discrete_def by meson
qed
ultimately show ?thesis by auto
qed (simp add: subset_insertI uniform_discrete_subset)
-
+
lemma discrete_compact_finite_iff:
fixes S :: "'a::t1_space set"
shows "discrete S \<and> compact S \<longleftrightarrow> finite S"
-proof
+proof
assume "finite S"
then have "compact S" using finite_imp_compact by auto
moreover have "discrete S"
- unfolding discrete_def using isolate_islimpt_iff islimpt_finite[OF \<open>finite S\<close>] by auto
+ unfolding discrete_def using isolated_in_islimpt_iff islimpt_finite[OF \<open>finite S\<close>] by auto
ultimately show "discrete S \<and> compact S" by auto
next
assume "discrete S \<and> compact S"
- then show "finite S"
- by (meson discrete_def Heine_Borel_imp_Bolzano_Weierstrass isolate_islimpt_iff order_refl)
+ then show "finite S"
+ by (meson discrete_def Heine_Borel_imp_Bolzano_Weierstrass isolated_in_islimpt_iff order_refl)
qed
-
+
lemma uniform_discrete_finite_iff:
fixes S :: "'a::heine_borel set"
shows "uniform_discrete S \<and> bounded S \<longleftrightarrow> finite S"
-proof
+proof
assume "uniform_discrete S \<and> bounded S"
then have "discrete S" "compact S"
using uniform_discrete_imp_discrete uniform_discrete_imp_closed compact_eq_bounded_closed
@@ -145,46 +139,42 @@
proof -
have "\<forall>x. \<exists>d>0. \<forall>y\<in>S. y \<noteq> x \<longrightarrow> d \<le> dist x y"
using finite_set_avoid[OF \<open>finite S\<close>] by auto
- then obtain f where f_pos:"f x>0"
+ then obtain f where f_pos:"f x>0"
and f_dist: "\<forall>y\<in>S. y \<noteq> x \<longrightarrow> f x \<le> dist x y"
- if "x\<in>S" for x
+ if "x\<in>S" for x
by metis
- define f_min where "f_min \<equiv> Min (f ` S)"
+ define f_min where "f_min \<equiv> Min (f ` S)"
have "f_min > 0"
- unfolding f_min_def
+ unfolding f_min_def
by (simp add: asm f_pos that)
moreover have "\<forall>x\<in>S. \<forall>y\<in>S. f_min > dist x y \<longrightarrow> x=y"
- using f_dist unfolding f_min_def
- by (metis Min_gr_iff all_not_in_conv asm dual_order.irrefl eq_iff finite_imageI imageI
- less_eq_real_def)
- ultimately have "uniform_discrete S"
+ using f_dist unfolding f_min_def
+ by (metis Min_le asm finite_imageI imageI le_less_trans linorder_not_less)
+ ultimately have "uniform_discrete S"
unfolding uniform_discrete_def by auto
moreover have "bounded S" using \<open>finite S\<close> by auto
ultimately show ?thesis by auto
qed
ultimately show ?thesis by blast
qed
-
+
lemma uniform_discrete_image_scale:
assumes "uniform_discrete S" and dist:"\<forall>x\<in>S. \<forall>y\<in>S. dist x y = c * dist (f x) (f y)"
- shows "uniform_discrete (f ` S)"
+ shows "uniform_discrete (f ` S)"
proof -
have ?thesis when "S={}" using that by auto
moreover have ?thesis when "S\<noteq>{}" "c\<le>0"
proof -
obtain x1 where "x1\<in>S" using \<open>S\<noteq>{}\<close> by auto
have ?thesis when "S-{x1} = {}"
- proof -
- have "S={x1}" using that \<open>S\<noteq>{}\<close> by auto
- then show ?thesis using uniform_discrete_insert[of "f x1"] by auto
- qed
+ using \<open>x1 \<in> S\<close> subset_antisym that uniform_discrete_insert by fastforce
moreover have ?thesis when "S-{x1} \<noteq> {}"
proof -
obtain x2 where "x2\<in>S-{x1}" using \<open>S-{x1} \<noteq> {}\<close> by auto
then have "x2\<in>S" "x1\<noteq>x2" by auto
then have "dist x1 x2 > 0" by auto
moreover have "dist x1 x2 = c * dist (f x1) (f x2)"
- using dist[rule_format, OF \<open>x1\<in>S\<close> \<open>x2\<in>S\<close>] .
+ by (simp add: \<open>x1 \<in> S\<close> \<open>x2 \<in> S\<close> dist)
moreover have "dist (f x2) (f x2) \<ge> 0" by auto
ultimately have False using \<open>c\<le>0\<close> by (simp add: zero_less_mult_iff)
then show ?thesis by auto
@@ -195,21 +185,13 @@
proof -
obtain e1 where "e1>0" and e1_dist:"\<forall>x\<in>S. \<forall>y\<in>S. dist y x < e1 \<longrightarrow> y = x"
using \<open>uniform_discrete S\<close> unfolding uniform_discrete_def by auto
- define e where "e= e1/c"
- have "x1 = x2" when "x1\<in> f ` S" "x2\<in> f ` S" "dist x1 x2 < e " for x1 x2
- proof -
- obtain y1 where y1:"y1\<in>S" "x1=f y1" using \<open>x1\<in> f ` S\<close> by auto
- obtain y2 where y2:"y2\<in>S" "x2=f y2" using \<open>x2\<in> f ` S\<close> by auto
- have "dist y1 y2 < e1"
- by (smt (verit) \<open>0 < c\<close> dist divide_right_mono e_def nonzero_mult_div_cancel_left that(3) y1 y2)
- then have "y1=y2"
- using e1_dist[rule_format, OF y2(1) y1(1)] by simp
- then show "x1=x2" using y1(2) y2(2) by auto
- qed
+ define e where "e \<equiv> e1/c"
+ have "x1 = x2" when "x1 \<in> f ` S" "x2 \<in> f ` S" and d: "dist x1 x2 < e" for x1 x2
+ by (smt (verit) \<open>0 < c\<close> d dist divide_right_mono e1_dist e_def imageE nonzero_mult_div_cancel_left that)
moreover have "e>0" using \<open>e1>0\<close> \<open>c>0\<close> unfolding e_def by auto
ultimately show ?thesis unfolding uniform_discrete_def by meson
qed
ultimately show ?thesis by fastforce
qed
-
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Uncountable_Sets.thy Mon Feb 06 15:41:23 2023 +0000
@@ -0,0 +1,121 @@
+section \<open>Some Uncountable Sets\<close>
+
+theory Uncountable_Sets
+ imports Path_Connected Continuum_Not_Denumerable
+begin
+
+lemma uncountable_closed_segment:
+ fixes a :: "'a::real_normed_vector"
+ assumes "a \<noteq> b" shows "uncountable (closed_segment a b)"
+unfolding path_image_linepath [symmetric] path_image_def
+ using inj_on_linepath [OF assms] uncountable_closed_interval [of 0 1]
+ countable_image_inj_on by auto
+
+lemma uncountable_open_segment:
+ fixes a :: "'a::real_normed_vector"
+ assumes "a \<noteq> b" shows "uncountable (open_segment a b)"
+ by (simp add: assms open_segment_def uncountable_closed_segment uncountable_minus_countable)
+
+lemma uncountable_convex:
+ fixes a :: "'a::real_normed_vector"
+ assumes "convex S" "a \<in> S" "b \<in> S" "a \<noteq> b"
+ shows "uncountable S"
+proof -
+ have "uncountable (closed_segment a b)"
+ by (simp add: uncountable_closed_segment assms)
+ then show ?thesis
+ by (meson assms convex_contains_segment countable_subset)
+qed
+
+lemma uncountable_ball:
+ fixes a :: "'a::euclidean_space"
+ assumes "r > 0"
+ shows "uncountable (ball a r)"
+proof -
+ have "uncountable (open_segment a (a + r *\<^sub>R (SOME i. i \<in> Basis)))"
+ by (metis Basis_zero SOME_Basis add_cancel_right_right assms less_le scale_eq_0_iff uncountable_open_segment)
+ moreover have "open_segment a (a + r *\<^sub>R (SOME i. i \<in> Basis)) \<subseteq> ball a r"
+ using assms by (auto simp: in_segment algebra_simps dist_norm SOME_Basis)
+ ultimately show ?thesis
+ by (metis countable_subset)
+qed
+
+lemma ball_minus_countable_nonempty:
+ assumes "countable (A :: 'a :: euclidean_space set)" "r > 0"
+ shows "ball z r - A \<noteq> {}"
+proof
+ assume *: "ball z r - A = {}"
+ have "uncountable (ball z r - A)"
+ by (intro uncountable_minus_countable assms uncountable_ball)
+ thus False by (subst (asm) *) auto
+qed
+
+lemma uncountable_cball:
+ fixes a :: "'a::euclidean_space"
+ assumes "r > 0"
+ shows "uncountable (cball a r)"
+ using assms countable_subset uncountable_ball by auto
+
+lemma pairwise_disjnt_countable:
+ fixes \<N> :: "nat set set"
+ assumes "pairwise disjnt \<N>"
+ shows "countable \<N>"
+ by (simp add: assms countable_disjoint_open_subsets open_discrete)
+
+lemma pairwise_disjnt_countable_Union:
+ assumes "countable (\<Union>\<N>)" and pwd: "pairwise disjnt \<N>"
+ shows "countable \<N>"
+proof -
+ obtain f :: "_ \<Rightarrow> nat" where f: "inj_on f (\<Union>\<N>)"
+ using assms by blast
+ then have "pairwise disjnt (\<Union> X \<in> \<N>. {f ` X})"
+ using assms by (force simp: pairwise_def disjnt_inj_on_iff [OF f])
+ then have "countable (\<Union> X \<in> \<N>. {f ` X})"
+ using pairwise_disjnt_countable by blast
+ then show ?thesis
+ by (meson pwd countable_image_inj_on disjoint_image f inj_on_image pairwise_disjnt_countable)
+qed
+
+lemma connected_uncountable:
+ fixes S :: "'a::metric_space set"
+ assumes "connected S" "a \<in> S" "b \<in> S" "a \<noteq> b" shows "uncountable S"
+proof -
+ have "continuous_on S (dist a)"
+ by (intro continuous_intros)
+ then have "connected (dist a ` S)"
+ by (metis connected_continuous_image \<open>connected S\<close>)
+ then have "closed_segment 0 (dist a b) \<subseteq> (dist a ` S)"
+ by (simp add: assms closed_segment_subset is_interval_connected_1 is_interval_convex)
+ then have "uncountable (dist a ` S)"
+ by (metis \<open>a \<noteq> b\<close> countable_subset dist_eq_0_iff uncountable_closed_segment)
+ then show ?thesis
+ by blast
+qed
+
+lemma path_connected_uncountable:
+ fixes S :: "'a::metric_space set"
+ assumes "path_connected S" "a \<in> S" "b \<in> S" "a \<noteq> b" shows "uncountable S"
+ using path_connected_imp_connected assms connected_uncountable by metis
+
+lemma simple_path_image_uncountable:
+ fixes g :: "real \<Rightarrow> 'a::metric_space"
+ assumes "simple_path g"
+ shows "uncountable (path_image g)"
+proof -
+ have "g 0 \<in> path_image g" "g (1/2) \<in> path_image g"
+ by (simp_all add: path_defs)
+ moreover have "g 0 \<noteq> g (1/2)"
+ using assms by (fastforce simp add: simple_path_def loop_free_def)
+ ultimately have "\<forall>a. \<not> path_image g \<subseteq> {a}"
+ by blast
+ then show ?thesis
+ using assms connected_simple_path_image connected_uncountable by blast
+qed
+
+lemma arc_image_uncountable:
+ fixes g :: "real \<Rightarrow> 'a::metric_space"
+ assumes "arc g"
+ shows "uncountable (path_image g)"
+ by (simp add: arc_imp_simple_path assms simple_path_image_uncountable)
+
+end
--- a/src/HOL/Library/Landau_Symbols.thy Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Library/Landau_Symbols.thy Mon Feb 06 15:41:23 2023 +0000
@@ -618,7 +618,48 @@
lemmas mult = big_mult small_big_mult big_small_mult small_mult
+lemma big_power:
+ assumes "f \<in> L F (g)"
+ shows "(\<lambda>x. f x ^ m) \<in> L F (\<lambda>x. g x ^ m)"
+ using assms by (induction m) (auto intro: mult)
+lemma (in landau_pair) small_power:
+ assumes "f \<in> l F (g)" "m > 0"
+ shows "(\<lambda>x. f x ^ m) \<in> l F (\<lambda>x. g x ^ m)"
+proof -
+ have "(\<lambda>x. f x * f x ^ (m - 1)) \<in> l F (\<lambda>x. g x * g x ^ (m - 1))"
+ by (intro small_big_mult assms big_power[OF small_imp_big])
+ thus ?thesis
+ using assms by (cases m) (simp_all add: mult_ac)
+qed
+
+lemma big_power_increasing:
+ assumes "(\<lambda>_. 1) \<in> L F f" "m \<le> n"
+ shows "(\<lambda>x. f x ^ m) \<in> L F (\<lambda>x. f x ^ n)"
+proof -
+ have "(\<lambda>x. f x ^ m * 1 ^ (n - m)) \<in> L F (\<lambda>x. f x ^ m * f x ^ (n - m))"
+ using assms by (intro mult big_power) auto
+ also have "(\<lambda>x. f x ^ m * f x ^ (n - m)) = (\<lambda>x. f x ^ (m + (n - m)))"
+ by (subst power_add [symmetric]) (rule refl)
+ also have "m + (n - m) = n"
+ using assms by simp
+ finally show ?thesis by simp
+qed
+
+lemma small_power_increasing:
+ assumes "(\<lambda>_. 1) \<in> l F f" "m < n"
+ shows "(\<lambda>x. f x ^ m) \<in> l F (\<lambda>x. f x ^ n)"
+proof -
+ note [trans] = small_big_trans
+ have "(\<lambda>x. f x ^ m * 1) \<in> l F (\<lambda>x. f x ^ m * f x)"
+ using assms by (intro big_small_mult) auto
+ also have "(\<lambda>x. f x ^ m * f x) = (\<lambda>x. f x ^ Suc m)"
+ by (simp add: mult_ac)
+ also have "\<dots> \<in> L F (\<lambda>x. f x ^ n)"
+ using assms by (intro big_power_increasing[OF small_imp_big]) auto
+ finally show ?thesis by simp
+qed
+
sublocale big: landau_symbol L L' Lr
proof
have L: "L = bigo \<or> L = bigomega"
@@ -1779,6 +1820,9 @@
by (intro asymp_equivI tendsto_eventually)
(insert assms, auto elim!: eventually_mono)
+lemma asymp_equiv_nhds_iff: "f \<sim>[nhds (z :: 'a :: t1_space)] g \<longleftrightarrow> f \<sim>[at z] g \<and> f z = g z"
+ by (auto simp: asymp_equiv_def tendsto_nhds_iff)
+
lemma asymp_equiv_sandwich:
fixes f g h :: "'a \<Rightarrow> 'b :: {real_normed_field, order_topology, linordered_field}"
assumes "eventually (\<lambda>x. f x \<ge> 0) F"
@@ -2191,8 +2235,6 @@
assumes "l1 \<sim>[F] u1" "u1 \<sim>[F] l2" "l2 \<sim>[F] u2"
"eventually (\<lambda>x. f x \<in> {l1 x..u1 x}) F" "eventually (\<lambda>x. g x \<in> {l2 x..u2 x}) F"
shows "f \<sim>[F] g"
- by (rule asymp_equiv_sandwich_real[OF asymp_equiv_sandwich_real'[OF _ _ assms(5)]
- asymp_equiv_sandwich_real'[OF _ _ assms(5)] assms(4)];
- blast intro: asymp_equiv_trans assms(1,2,3))+
+ by (meson assms asymp_equiv_sandwich_real asymp_equiv_sandwich_real' asymp_equiv_trans)
end
--- a/src/HOL/Transcendental.thy Sun Feb 05 20:09:39 2023 +0100
+++ b/src/HOL/Transcendental.thy Mon Feb 06 15:41:23 2023 +0000
@@ -2521,20 +2521,7 @@
lemma powr_real_of_int':
assumes "x \<ge> 0" "x \<noteq> 0 \<or> n > 0"
shows "x powr real_of_int n = power_int x n"
-proof (cases "x = 0")
- case False
- with assms have "x > 0" by simp
- show ?thesis
- proof (cases n rule: int_cases4)
- case (nonneg n)
- thus ?thesis using \<open>x > 0\<close>
- by (auto simp add: powr_realpow)
- next
- case (neg n)
- thus ?thesis using \<open>x > 0\<close>
- by (auto simp add: powr_realpow powr_minus power_int_minus)
- qed
-qed (use assms in auto)
+ by (metis assms exp_ln_iff exp_power_int nless_le power_int_eq_0_iff powr_def)
lemma log_ln: "ln x = log (exp(1)) x"
by (simp add: log_def)