--- a/src/HOL/Analysis/Analysis.thy Wed Jan 25 22:00:21 2023 +0100
+++ b/src/HOL/Analysis/Analysis.thy Thu Jan 26 13:59:51 2023 +0000
@@ -6,6 +6,7 @@
(* Topology *)
Connected
Abstract_Limits
+ Isolated
(* Functional Analysis *)
Elementary_Normed_Spaces
Norm_Arith
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Isolated.thy Thu Jan 26 13:59:51 2023 +0000
@@ -0,0 +1,215 @@
+theory Isolated
+ imports "HOL-Analysis.Elementary_Metric_Spaces"
+
+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)"
+
+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"
+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"
+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:
+ 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)
+
+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:
+ 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)
+
+(*
+TODO.
+Other than
+
+ uniform_discrete S \<longrightarrow> discrete S
+ uniform_discrete S \<longrightarrow> closed S
+
+, we should be able to prove
+
+ discrete S \<and> closed S \<longrightarrow> uniform_discrete S
+
+but the proof (based on Tietze Extension Theorem) seems not very trivial to me. Informal proofs can be found in
+
+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)
+
+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
+
+lemma discrete_subset[elim]: "discrete S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> discrete T"
+ unfolding discrete_def using islimpt_subset isolate_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 uniform_discrete_insert: "uniform_discrete (insert a S) \<longleftrightarrow> 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)
+ moreover have ?thesis when "a\<notin>S" "S\<noteq>{}"
+ 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 asm unfolding uniform_discrete_def by auto
+ define e2 where "e2 \<equiv> min (setdist {a} S) e1"
+ 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
+ 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
+ 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
+ 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)
+qed
+
+lemma uniform_discrete_finite_iff:
+ fixes S :: "'a::heine_borel set"
+ shows "uniform_discrete S \<and> bounded S \<longleftrightarrow> finite S"
+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
+ by auto
+ then show "finite S" using discrete_compact_finite_iff by auto
+next
+ assume asm:"finite S"
+ let ?thesis = "uniform_discrete S \<and> bounded S"
+ have ?thesis when "S={}" using that by auto
+ moreover have ?thesis when "S\<noteq>{}"
+ 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"
+ and f_dist: "\<forall>y\<in>S. y \<noteq> x \<longrightarrow> f x \<le> dist x y"
+ if "x\<in>S" for x
+ by metis
+ define f_min where "f_min \<equiv> Min (f ` S)"
+ have "f_min > 0"
+ 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"
+ 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)"
+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
+ 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>] .
+ 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
+ qed
+ ultimately show ?thesis by auto
+ qed
+ moreover have ?thesis when "S\<noteq>{}" "c>0"
+ 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
+ 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
--- a/src/HOL/Limits.thy Wed Jan 25 22:00:21 2023 +0100
+++ b/src/HOL/Limits.thy Thu Jan 26 13:59:51 2023 +0000
@@ -11,15 +11,6 @@
imports Real_Vector_Spaces
begin
-text \<open>Lemmas related to shifting/scaling\<close>
-lemma range_add [simp]:
- fixes a::"'a::group_add" shows "range ((+) a) = UNIV"
- by simp
-
-lemma range_diff [simp]:
- fixes a::"'a::group_add" shows "range ((-) a) = UNIV"
- by (metis (full_types) add_minus_cancel diff_minus_eq_add surj_def)
-
lemma range_mult [simp]:
fixes a::"real" shows "range ((*) a) = (if a=0 then {0} else UNIV)"
by (simp add: surj_def) (meson dvdE dvd_field_iff)
@@ -2533,6 +2524,147 @@
by (metis B abs_le_iff add.inverse_inverse neg_le_iff_le)
qed
+subsection \<open>More about @{term filterlim} (thanks to Wenda Li)\<close>
+
+lemma filterlim_at_infinity_times:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_field"
+ assumes "filterlim f at_infinity F" "filterlim g at_infinity F"
+ shows "filterlim (\<lambda>x. f x * g x) at_infinity F"
+proof -
+ have "((\<lambda>x. inverse (f x) * inverse (g x)) \<longlongrightarrow> 0 * 0) F"
+ by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0])
+ then have "filterlim (\<lambda>x. inverse (f x) * inverse (g x)) (at 0) F"
+ unfolding filterlim_at using assms
+ by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
+ then show ?thesis
+ by (subst filterlim_inverse_at_iff[symmetric]) simp_all
+qed
+
+lemma filterlim_at_top_at_bot[elim]:
+ fixes f::"'a \<Rightarrow> 'b::unbounded_dense_linorder" and F::"'a filter"
+ assumes top:"filterlim f at_top F" and bot: "filterlim f at_bot F" and "F\<noteq>bot"
+ shows False
+proof -
+ obtain c::'b where True by auto
+ have "\<forall>\<^sub>F x in F. c < f x"
+ using top unfolding filterlim_at_top_dense by auto
+ moreover have "\<forall>\<^sub>F x in F. f x < c"
+ using bot unfolding filterlim_at_bot_dense by auto
+ ultimately have "\<forall>\<^sub>F x in F. c < f x \<and> f x < c"
+ using eventually_conj by auto
+ then have "\<forall>\<^sub>F x in F. False" by (auto elim:eventually_mono)
+ then show False using \<open>F\<noteq>bot\<close> by auto
+qed
+
+lemma filterlim_at_top_nhds[elim]:
+ fixes f::"'a \<Rightarrow> 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter"
+ assumes top:"filterlim f at_top F" and tendsto: "(f \<longlongrightarrow> c) F" and "F\<noteq>bot"
+ shows False
+proof -
+ obtain c'::'b where "c'>c" using gt_ex by blast
+ have "\<forall>\<^sub>F x in F. c' < f x"
+ using top unfolding filterlim_at_top_dense by auto
+ moreover have "\<forall>\<^sub>F x in F. f x < c'"
+ using order_tendstoD[OF tendsto,of c'] \<open>c'>c\<close> by auto
+ ultimately have "\<forall>\<^sub>F x in F. c' < f x \<and> f x < c'"
+ using eventually_conj by auto
+ then have "\<forall>\<^sub>F x in F. False" by (auto elim:eventually_mono)
+ then show False using \<open>F\<noteq>bot\<close> by auto
+qed
+
+lemma filterlim_at_bot_nhds[elim]:
+ fixes f::"'a \<Rightarrow> 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter"
+ assumes top:"filterlim f at_bot F" and tendsto: "(f \<longlongrightarrow> c) F" and "F\<noteq>bot"
+ shows False
+proof -
+ obtain c'::'b where "c'<c" using lt_ex by blast
+ have "\<forall>\<^sub>F x in F. c' > f x"
+ using top unfolding filterlim_at_bot_dense by auto
+ moreover have "\<forall>\<^sub>F x in F. f x > c'"
+ using order_tendstoD[OF tendsto,of c'] \<open>c'<c\<close> by auto
+ ultimately have "\<forall>\<^sub>F x in F. c' < f x \<and> f x < c'"
+ using eventually_conj by auto
+ then have "\<forall>\<^sub>F x in F. False" by (auto elim:eventually_mono)
+ then show False using \<open>F\<noteq>bot\<close> by auto
+qed
+
+lemma eventually_times_inverse_1:
+ fixes f::"'a \<Rightarrow> 'b::{field,t2_space}"
+ assumes "(f \<longlongrightarrow> c) F" "c\<noteq>0"
+ shows "\<forall>\<^sub>F x in F. inverse (f x) * f x = 1"
+ by (smt (verit) assms eventually_mono mult.commute right_inverse tendsto_imp_eventually_ne)
+
+lemma filterlim_at_infinity_divide_iff:
+ fixes f::"'a \<Rightarrow> 'b::real_normed_field"
+ assumes "(f \<longlongrightarrow> c) F" "c\<noteq>0"
+ shows "(LIM x F. f x / g x :> at_infinity) \<longleftrightarrow> (LIM x F. g x :> at 0)"
+proof
+ assume "LIM x F. f x / g x :> at_infinity"
+ then have "LIM x F. inverse (f x) * (f x / g x) :> at_infinity"
+ using assms tendsto_inverse tendsto_mult_filterlim_at_infinity by fastforce
+ then have "LIM x F. inverse (g x) :> at_infinity"
+ apply (elim filterlim_mono_eventually)
+ using eventually_times_inverse_1[OF assms]
+ by (auto elim:eventually_mono simp add:field_simps)
+ then show "filterlim g (at 0) F" using filterlim_inverse_at_iff[symmetric] by force
+next
+ assume "filterlim g (at 0) F"
+ then have "filterlim (\<lambda>x. inverse (g x)) at_infinity F"
+ using filterlim_compose filterlim_inverse_at_infinity by blast
+ then have "LIM x F. f x * inverse (g x) :> at_infinity"
+ using tendsto_mult_filterlim_at_infinity[OF assms, of "\<lambda>x. inverse(g x)"]
+ by simp
+ then show "LIM x F. f x / g x :> at_infinity" by (simp add: divide_inverse)
+qed
+
+lemma filterlim_tendsto_pos_mult_at_top_iff:
+ fixes f::"'a \<Rightarrow> real"
+ assumes "(f \<longlongrightarrow> c) F" and "0 < c"
+ shows "(LIM x F. (f x * g x) :> at_top) \<longleftrightarrow> (LIM x F. g x :> at_top)"
+proof
+ assume "filterlim g at_top F"
+ then show "LIM x F. f x * g x :> at_top"
+ using filterlim_tendsto_pos_mult_at_top[OF assms] by auto
+next
+ assume asm:"LIM x F. f x * g x :> at_top"
+ have "((\<lambda>x. inverse (f x)) \<longlongrightarrow> inverse c) F"
+ using tendsto_inverse[OF assms(1)] \<open>0<c\<close> by auto
+ moreover have "inverse c >0" using assms(2) by auto
+ ultimately have "LIM x F. inverse (f x) * (f x * g x) :> at_top"
+ using filterlim_tendsto_pos_mult_at_top[OF _ _ asm,of "\<lambda>x. inverse (f x)" "inverse c"] by auto
+ then show "LIM x F. g x :> at_top"
+ apply (elim filterlim_mono_eventually)
+ apply simp_all[2]
+ using eventually_times_inverse_1[OF assms(1)] \<open>c>0\<close> eventually_mono by fastforce
+qed
+
+lemma filterlim_tendsto_pos_mult_at_bot_iff:
+ fixes c :: real
+ assumes "(f \<longlongrightarrow> c) F" "0 < c"
+ shows "(LIM x F. f x * g x :> at_bot) \<longleftrightarrow> filterlim g at_bot F"
+ using filterlim_tendsto_pos_mult_at_top_iff[OF assms(1,2), of "\<lambda>x. - g x"]
+ unfolding filterlim_uminus_at_bot by simp
+
+lemma filterlim_tendsto_neg_mult_at_top_iff:
+ fixes f::"'a \<Rightarrow> real"
+ assumes "(f \<longlongrightarrow> c) F" and "c < 0"
+ shows "(LIM x F. (f x * g x) :> at_top) \<longleftrightarrow> (LIM x F. g x :> at_bot)"
+proof -
+ have "(LIM x F. f x * g x :> at_top) = (LIM x F. - g x :> at_top)"
+ apply (rule filterlim_tendsto_pos_mult_at_top_iff[of "\<lambda>x. - f x" "-c" F "\<lambda>x. - g x", simplified])
+ using assms by (auto intro: tendsto_intros )
+ also have "... = (LIM x F. g x :> at_bot)"
+ using filterlim_uminus_at_bot[symmetric] by auto
+ finally show ?thesis .
+qed
+
+lemma filterlim_tendsto_neg_mult_at_bot_iff:
+ fixes c :: real
+ assumes "(f \<longlongrightarrow> c) F" "0 > c"
+ shows "(LIM x F. f x * g x :> at_bot) \<longleftrightarrow> filterlim g at_top F"
+ using filterlim_tendsto_neg_mult_at_top_iff[OF assms(1,2), of "\<lambda>x. - g x"]
+ unfolding filterlim_uminus_at_top by simp
+
subsection \<open>Power Sequences\<close>
lemma Bseq_realpow: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> Bseq (\<lambda>n. x ^ n)"