--- a/src/HOL/Analysis/Complex_Transcendental.thy Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Wed Feb 08 15:05:24 2023 +0000
@@ -2649,7 +2649,7 @@
lemma powr_nat': "(z :: complex) \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> z powr of_nat n = z ^ n"
by (cases "z = 0") (auto simp: powr_nat)
-
+
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)
@@ -2694,12 +2694,15 @@
shows "z powr of_int n = (if n\<ge>0 then z^nat n else inverse (z^nat (-n)))"
by (metis assms not_le of_int_of_nat powr_complexpow powr_minus)
+lemma complex_powr_of_int: "z \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> z powr of_int n = (z :: complex) powi n"
+ by (cases "z = 0 \<or> n = 0")
+ (auto simp: power_int_def powr_minus powr_nat powr_of_int power_0_left power_inverse)
+
lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x \<ge> 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
by (metis of_real_Re powr_of_real)
lemma norm_powr_real_mono:
- "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
- \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
+ "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk> \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)
lemma powr_times_real:
--- a/src/HOL/Analysis/Connected.thy Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Analysis/Connected.thy Wed Feb 08 15:05:24 2023 +0000
@@ -238,10 +238,7 @@
connected_component_set S x \<inter> T \<noteq> {};
connected_component_set S y \<inter> T \<noteq> {}\<rbrakk>
\<Longrightarrow> connected_component_set S x = connected_component_set S y"
-apply (simp add: ex_in_conv [symmetric])
-apply (rule connected_component_eq)
-by (metis (no_types, opaque_lifting) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
-
+ by (metis (full_types) subsetD connected_component_eq connected_component_maximal disjoint_iff_not_equal)
lemma Union_connected_component: "\<Union>(connected_component_set S ` S) = S"
apply (rule subset_antisym)
@@ -260,10 +257,36 @@
lemma connected_component_intermediate_subset:
"\<lbrakk>connected_component_set U a \<subseteq> T; T \<subseteq> U\<rbrakk>
\<Longrightarrow> connected_component_set T a = connected_component_set U a"
- apply (case_tac "a \<in> U")
- apply (simp add: connected_component_maximal connected_component_mono subset_antisym)
- using connected_component_eq_empty by blast
+ by (metis connected_component_idemp connected_component_mono subset_antisym)
+
+lemma connected_component_homeomorphismI:
+ assumes "homeomorphism A B f g" "connected_component A x y"
+ shows "connected_component B (f x) (f y)"
+proof -
+ from assms obtain T where T: "connected T" "T \<subseteq> A" "x \<in> T" "y \<in> T"
+ unfolding connected_component_def by blast
+ have "connected (f ` T)" "f ` T \<subseteq> B" "f x \<in> f ` T" "f y \<in> f ` T"
+ using assms T continuous_on_subset[of A f T]
+ by (auto intro!: connected_continuous_image simp: homeomorphism_def)
+ thus ?thesis
+ unfolding connected_component_def by blast
+qed
+
+lemma connected_component_homeomorphism_iff:
+ assumes "homeomorphism A B f g"
+ shows "connected_component A x y \<longleftrightarrow> x \<in> A \<and> y \<in> A \<and> connected_component B (f x) (f y)"
+ by (metis assms connected_component_homeomorphismI connected_component_in homeomorphism_apply1 homeomorphism_sym)
+
+lemma connected_component_set_homeomorphism:
+ assumes "homeomorphism A B f g" "x \<in> A"
+ shows "connected_component_set B (f x) = f ` connected_component_set A x" (is "?lhs = ?rhs")
+proof -
+ have "y \<in> ?lhs \<longleftrightarrow> y \<in> ?rhs" for y
+ by (smt (verit, best) assms connected_component_homeomorphism_iff homeomorphism_def image_iff mem_Collect_eq)
+ thus ?thesis
+ by blast
+qed
subsection \<open>The set of connected components of a set\<close>
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Feb 08 15:05:24 2023 +0000
@@ -274,6 +274,48 @@
ultimately show ?thesis by blast
qed
+lemma frequently_atE:
+ fixes x :: "'a :: metric_space"
+ assumes "frequently P (at x within s)"
+ shows "\<exists>f. filterlim f (at x within s) sequentially \<and> (\<forall>n. P (f n))"
+proof -
+ have "\<exists>y. y \<in> s \<inter> (ball x (1 / real (Suc n)) - {x}) \<and> P y" for n
+ proof -
+ have "\<exists>z\<in>s. z \<noteq> x \<and> dist z x < (1 / real (Suc n)) \<and> P z"
+ by (metis assms divide_pos_pos frequently_at of_nat_0_less_iff zero_less_Suc zero_less_one)
+ then show ?thesis
+ by (auto simp: dist_commute conj_commute)
+ qed
+ then obtain f where f: "\<And>n. f n \<in> s \<inter> (ball x (1 / real (Suc n)) - {x}) \<and> P (f n)"
+ by metis
+ have "filterlim f (nhds x) sequentially"
+ unfolding tendsto_iff
+ proof clarify
+ fix e :: real
+ assume e: "e > 0"
+ then obtain n where n: "Suc n > 1 / e"
+ by (meson le_nat_floor lessI not_le)
+ have "dist (f k) x < e" if "k \<ge> n" for k
+ proof -
+ have "dist (f k) x < 1 / real (Suc k)"
+ using f[of k] by (auto simp: dist_commute)
+ also have "\<dots> \<le> 1 / real (Suc n)"
+ using that by (intro divide_left_mono) auto
+ also have "\<dots> < e"
+ using n e by (simp add: field_simps)
+ finally show ?thesis .
+ qed
+ thus "\<forall>\<^sub>F k in sequentially. dist (f k) x < e"
+ unfolding eventually_at_top_linorder by blast
+ qed
+ moreover have "f n \<noteq> x" for n
+ using f[of n] by auto
+ ultimately have "filterlim f (at x within s) sequentially"
+ using f by (auto simp: filterlim_at)
+ with f show ?thesis
+ by blast
+qed
+
subsection \<open>Limit Points\<close>
lemma islimpt_approachable:
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Wed Feb 08 15:05:24 2023 +0000
@@ -659,6 +659,16 @@
lemma bounded_pos_less: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x < b)"
by (metis bounded_pos le_less_trans less_imp_le linordered_field_no_ub)
+lemma bounded_normE:
+ assumes "bounded A"
+ obtains B where "B > 0" "\<And>z. z \<in> A \<Longrightarrow> norm z \<le> B"
+ by (meson assms bounded_pos)
+
+lemma bounded_normE_less:
+ assumes "bounded A"
+ obtains B where "B > 0" "\<And>z. z \<in> A \<Longrightarrow> norm z < B"
+ by (meson assms bounded_pos_less)
+
lemma Bseq_eq_bounded:
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
shows "Bseq f \<longleftrightarrow> bounded (range f)"
--- a/src/HOL/Analysis/Elementary_Topology.thy Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Analysis/Elementary_Topology.thy Wed Feb 08 15:05:24 2023 +0000
@@ -758,6 +758,87 @@
by simp
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 \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f \<longlongrightarrow> x) sequentially)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ from countable_basis_at_decseq[of x] obtain A where A:
+ "\<And>i. open (A i)"
+ "\<And>i. x \<in> A i"
+ "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
+ by blast
+ define f where "f n = (SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y)" for n
+ {
+ fix n
+ from \<open>?lhs\<close> have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
+ unfolding islimpt_def using A(1,2)[of n] by auto
+ then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
+ unfolding f_def by (rule someI_ex)
+ then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto
+ }
+ then have "\<forall>n. f n \<in> S - {x}" by auto
+ moreover have "(\<lambda>n. f n) \<longlonglongrightarrow> x"
+ proof (rule topological_tendstoI)
+ fix S
+ assume "open S" "x \<in> S"
+ from A(3)[OF this] \<open>\<And>n. f n \<in> A n\<close>
+ show "eventually (\<lambda>x. f x \<in> S) sequentially"
+ by (auto elim!: eventually_mono)
+ qed
+ ultimately show ?rhs by fast
+next
+ assume ?rhs
+ then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f \<longlonglongrightarrow> x"
+ by auto
+ show ?lhs
+ unfolding islimpt_def
+ proof safe
+ fix T
+ assume "open T" "x \<in> T"
+ from lim[THEN topological_tendstoD, OF this] f
+ show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
+ unfolding eventually_sequentially by auto
+ qed
+qed
+
+lemma islimpt_isCont_image:
+ fixes f :: "'a :: {first_countable_topology, t2_space} \<Rightarrow> 'b :: {first_countable_topology, t2_space}"
+ assumes "x islimpt A" and "isCont f x" and ev: "eventually (\<lambda>y. f y \<noteq> f x) (at x)"
+ shows "f x islimpt f ` A"
+proof -
+ from assms(1) obtain g where g: "g \<longlonglongrightarrow> x" "range g \<subseteq> A - {x}"
+ unfolding islimpt_sequential by blast
+ have "filterlim g (at x) sequentially"
+ using g by (auto simp: filterlim_at intro!: always_eventually)
+ then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> f (g n) \<noteq> f x"
+ by (metis (mono_tags, lifting) ev eventually_at_top_linorder filterlim_iff)
+ have "(\<lambda>x. g (x + N)) \<longlonglongrightarrow> x"
+ using g(1) by (rule LIMSEQ_ignore_initial_segment)
+ hence "(\<lambda>x. f (g (x + N))) \<longlonglongrightarrow> f x"
+ using assms(2) isCont_tendsto_compose by blast
+ moreover have "range (\<lambda>x. f (g (x + N))) \<subseteq> f ` A - {f x}"
+ using g(2) N by auto
+ ultimately show ?thesis
+ unfolding islimpt_sequential by (intro exI[of _ "\<lambda>x. f (g (x + N))"]) auto
+qed
+
+lemma islimpt_image:
+ assumes "z islimpt g -` A \<inter> B" "g z \<notin> A" "z \<in> B" "open B" "continuous_on B g"
+ shows "g z islimpt A"
+ unfolding islimpt_def
+proof clarify
+ fix T assume T: "g z \<in> T" "open T"
+ have "z \<in> g -` T \<inter> B"
+ using T assms by auto
+ moreover have "open (g -` T \<inter> B)"
+ using T continuous_on_open_vimage assms by blast
+ ultimately show "\<exists>y\<in>A. y \<in> T \<and> y \<noteq> g z"
+ using assms by (metis (mono_tags, lifting) IntD1 islimptE vimageE)
+qed
+
subsection \<open>Interior of a Set\<close>
@@ -845,7 +926,12 @@
lemma islimpt_conv_frequently_at:
"x islimpt A \<longleftrightarrow> frequently (\<lambda>y. y \<in> A) (at x)"
- unfolding islimpt_def eventually_at_filter frequently_def eventually_nhds by blast
+ by (simp add: frequently_def islimpt_iff_eventually)
+
+lemma frequently_at_imp_islimpt:
+ assumes "frequently (\<lambda>y. y \<in> A) (at x)"
+ shows "x islimpt A"
+ by (simp add: assms islimpt_conv_frequently_at)
lemma interior_closed_Un_empty_interior:
assumes cS: "closed S"
@@ -1350,52 +1436,6 @@
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 \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f \<longlongrightarrow> x) sequentially)"
- (is "?lhs = ?rhs")
-proof
- assume ?lhs
- from countable_basis_at_decseq[of x] obtain A where A:
- "\<And>i. open (A i)"
- "\<And>i. x \<in> A i"
- "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
- by blast
- define f where "f n = (SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y)" for n
- {
- fix n
- from \<open>?lhs\<close> have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
- unfolding islimpt_def using A(1,2)[of n] by auto
- then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
- unfolding f_def by (rule someI_ex)
- then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto
- }
- then have "\<forall>n. f n \<in> S - {x}" by auto
- moreover have "(\<lambda>n. f n) \<longlonglongrightarrow> x"
- proof (rule topological_tendstoI)
- fix S
- assume "open S" "x \<in> S"
- from A(3)[OF this] \<open>\<And>n. f n \<in> A n\<close>
- show "eventually (\<lambda>x. f x \<in> S) sequentially"
- by (auto elim!: eventually_mono)
- qed
- ultimately show ?rhs by fast
-next
- assume ?rhs
- then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f \<longlonglongrightarrow> x"
- by auto
- show ?lhs
- unfolding islimpt_def
- proof safe
- fix T
- assume "open T" "x \<in> T"
- from lim[THEN topological_tendstoD, OF this] f
- show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
- unfolding eventually_sequentially by auto
- qed
-qed
-
text\<open>These are special for limits out of the same topological space.\<close>
lemma Lim_within_id: "(id \<longlongrightarrow> a) (at a within s)"
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Wed Feb 08 15:05:24 2023 +0000
@@ -26,8 +26,18 @@
lemma is_pole_tendsto:
fixes f::"('a::topological_space \<Rightarrow> 'b::real_normed_div_algebra)"
shows "is_pole f x \<Longrightarrow> ((inverse o f) \<longlongrightarrow> 0) (at x)"
-unfolding is_pole_def
-by (auto simp add:filterlim_inverse_at_iff[symmetric] comp_def filterlim_at)
+ unfolding is_pole_def
+ by (auto simp add:filterlim_inverse_at_iff[symmetric] comp_def filterlim_at)
+
+lemma is_pole_shift_0:
+ fixes f :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector)"
+ shows "is_pole f z \<longleftrightarrow> is_pole (\<lambda>x. f (z + x)) 0"
+ unfolding is_pole_def by (subst at_to_0) (auto simp: filterlim_filtermap add_ac)
+
+lemma is_pole_shift_0':
+ fixes f :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector)"
+ shows "NO_MATCH 0 z \<Longrightarrow> is_pole f z \<longleftrightarrow> is_pole (\<lambda>x. f (z + x)) 0"
+ by (metis is_pole_shift_0)
lemma is_pole_inverse_holomorphic:
assumes "open s"
@@ -71,6 +81,23 @@
by (intro filterlim_compose[OF filterlim_inverse_at_infinity] tendsto_intros)
(auto simp: filterlim_at eventually_at intro!: exI[of _ 1] tendsto_eq_intros)
+lemma is_pole_cmult_iff [simp]:
+ "c \<noteq> 0 \<Longrightarrow> is_pole (\<lambda>z. c * f z :: 'a :: real_normed_field) z \<longleftrightarrow> is_pole f z"
+proof
+ assume *: "c \<noteq> 0" "is_pole (\<lambda>z. c * f z) z"
+ have "is_pole (\<lambda>z. inverse c * (c * f z)) z" unfolding is_pole_def
+ by (rule tendsto_mult_filterlim_at_infinity tendsto_const)+ (use * in \<open>auto simp: is_pole_def\<close>)
+ thus "is_pole f z"
+ using *(1) by (simp add: field_simps)
+next
+ assume *: "c \<noteq> 0" "is_pole f z"
+ show "is_pole (\<lambda>z. c * f z) z" unfolding is_pole_def
+ by (rule tendsto_mult_filterlim_at_infinity tendsto_const)+ (use * in \<open>auto simp: is_pole_def\<close>)
+qed
+
+lemma is_pole_uminus_iff [simp]: "is_pole (\<lambda>z. -f z :: 'a :: real_normed_field) z \<longleftrightarrow> is_pole f z"
+ using is_pole_cmult_iff[of "-1" f] by (simp del: is_pole_cmult_iff)
+
lemma is_pole_inverse: "is_pole (\<lambda>z::complex. 1 / (z - a)) a"
using is_pole_inverse_power[of 1 a] by simp
@@ -80,7 +107,7 @@
shows "is_pole (\<lambda>z. f z / g z) z"
proof -
have "filterlim (\<lambda>z. f z * inverse (g z)) at_infinity (at z)"
- using assms filterlim_compose filterlim_inverse_at_infinity isCont_def
+ using assms filterlim_compose filterlim_inverse_at_infinity isCont_def
tendsto_mult_filterlim_at_infinity by blast
thus ?thesis by (simp add: field_split_simps is_pole_def)
qed
@@ -113,6 +140,62 @@
definition isolated_singularity_at::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where
"isolated_singularity_at f z = (\<exists>r>0. f analytic_on ball z r-{z})"
+lemma removable_singularity:
+ assumes "f holomorphic_on A - {x}" "open A"
+ assumes "f \<midarrow>x\<rightarrow> c"
+ shows "(\<lambda>y. if y = x then c else f y) holomorphic_on A" (is "?g holomorphic_on _")
+proof -
+ have "continuous_on A ?g"
+ unfolding continuous_on_def
+ proof
+ fix y assume y: "y \<in> A"
+ show "(?g \<longlongrightarrow> ?g y) (at y within A)"
+ proof (cases "y = x")
+ case False
+ have "continuous_on (A - {x}) f"
+ using assms(1) by (meson holomorphic_on_imp_continuous_on)
+ hence "(f \<longlongrightarrow> ?g y) (at y within A - {x})"
+ using False y by (auto simp: continuous_on_def)
+ also have "?this \<longleftrightarrow> (?g \<longlongrightarrow> ?g y) (at y within A - {x})"
+ by (intro filterlim_cong refl) (auto simp: eventually_at_filter)
+ also have "at y within A - {x} = at y within A"
+ using y assms False
+ by (intro at_within_nhd[of _ "A - {x}"]) auto
+ finally show ?thesis .
+ next
+ case [simp]: True
+ have "f \<midarrow>x\<rightarrow> c"
+ by fact
+ also have "?this \<longleftrightarrow> (?g \<longlongrightarrow> ?g y) (at y)"
+ by (intro filterlim_cong) (auto simp: eventually_at_filter)
+ finally show ?thesis
+ by (meson Lim_at_imp_Lim_at_within)
+ qed
+ qed
+ moreover {
+ have "?g holomorphic_on A - {x}"
+ using assms(1) holomorphic_transform by fastforce
+ }
+ ultimately show ?thesis
+ by (rule no_isolated_singularity) (use assms in auto)
+qed
+
+lemma removable_singularity':
+ assumes "isolated_singularity_at f z"
+ assumes "f \<midarrow>z\<rightarrow> c"
+ shows "(\<lambda>y. if y = z then c else f y) analytic_on {z}"
+proof -
+ from assms obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
+ by (auto simp: isolated_singularity_at_def)
+ have "(\<lambda>y. if y = z then c else f y) holomorphic_on ball z r"
+ proof (rule removable_singularity)
+ show "f holomorphic_on ball z r - {z}"
+ using r(2) by (subst (asm) analytic_on_open) auto
+ qed (use assms in auto)
+ thus ?thesis
+ using r(1) unfolding analytic_at by (intro exI[of _ "ball z r"]) auto
+qed
+
named_theorems singularity_intros "introduction rules for singularities"
lemma holomorphic_factor_unique:
@@ -137,7 +220,7 @@
define f' where "f' \<equiv> \<lambda>x. (x - z) powr (n-m)"
have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def continuous_def
- using \<open>n>m\<close>
+ using \<open>n>m\<close>
by (auto simp add: Lim_ident_at intro!:tendsto_powr_complex_0 tendsto_eq_intros)
ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
by (simp add: continuous_within)
@@ -165,7 +248,7 @@
define f' where "f' \<equiv>\<lambda>x. (x - z) powr (m-n)"
have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def continuous_def
- using \<open>m>n\<close>
+ using \<open>m>n\<close>
by (auto simp: Lim_ident_at intro!:tendsto_powr_complex_0 tendsto_eq_intros)
ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
by (simp add: continuous_within)
@@ -272,7 +355,7 @@
ultimately show ?thesis by auto
qed
- have ?thesis when "\<exists>x. (f \<longlongrightarrow> x) (at z)"
+ have ?thesis when "\<exists>x. (f \<longlongrightarrow> x) (at z)"
apply (rule_tac imp_unique[unfolded P_def])
using P_exist[OF that(1) f_iso non_zero] unfolding P_def .
moreover have ?thesis when "is_pole f z"
@@ -312,7 +395,7 @@
have "P f (-n) (inverse o g) r"
proof -
have "f w = inverse (g w) * (w - z) powr of_int (- n)" when "w\<in>cball z r - {z}" for w
- by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib of_int_minus
+ by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib of_int_minus
powr_minus that)
then show ?thesis
unfolding P_def comp_def
@@ -398,7 +481,7 @@
have "(\<lambda>w. inverse ((f w) ^ (nat (-n)))) \<midarrow>z\<rightarrow>?xx"
using assms False unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
then have "fp \<midarrow>z\<rightarrow> ?xx"
- by (smt (verit) LIM_cong fp_def inverse_nonzero_iff_nonzero power_eq_0_iff powr_eq_0_iff
+ by (smt (verit) LIM_cong fp_def inverse_nonzero_iff_nonzero power_eq_0_iff powr_eq_0_iff
powr_of_int that zero_less_nat_eq)
then show ?thesis unfolding fp_def not_essential_def by auto
qed
@@ -520,7 +603,7 @@
using that by (auto intro!:tendsto_eq_intros)
then have "fg \<midarrow>z\<rightarrow> 0"
using Lim_transform_within[OF _ \<open>r1>0\<close>]
- by (smt (verit, ccfv_SIG) DiffI dist_commute dist_nz fg_times mem_ball powr_of_int right_minus_eq
+ by (smt (verit, ccfv_SIG) DiffI dist_commute dist_nz fg_times mem_ball powr_of_int right_minus_eq
singletonD that)
then show ?thesis unfolding not_essential_def fg_def by auto
qed
@@ -629,7 +712,7 @@
using f_iso unfolding isolated_singularity_at_def by auto
define d3 where "d3=min d1 d2"
have "d3>0" unfolding d3_def using \<open>d1>0\<close> \<open>d2>0\<close> by auto
- moreover
+ moreover
have "f analytic_on ball z d3 - {z}"
by (smt (verit, best) Diff_iff analytic_on_analytic_at d2 d3_def mem_ball)
then have "vf analytic_on ball z d3 - {z}"
@@ -712,9 +795,114 @@
using assms unfolding isolated_singularity_at_def
by (metis analytic_on_holomorphic centre_in_ball insert_Diff openE open_delete subset_insert_iff)
+lemma isolated_singularity_at_shift:
+ assumes "isolated_singularity_at (\<lambda>x. f (x + w)) z"
+ shows "isolated_singularity_at f (z + w)"
+proof -
+ from assms obtain r where r: "r > 0" and ana: "(\<lambda>x. f (x + w)) analytic_on ball z r - {z}"
+ unfolding isolated_singularity_at_def by blast
+ have "((\<lambda>x. f (x + w)) \<circ> (\<lambda>x. x - w)) analytic_on (ball (z + w) r - {z + w})"
+ by (rule analytic_on_compose_gen[OF _ ana])
+ (auto simp: dist_norm algebra_simps intro!: analytic_intros)
+ hence "f analytic_on (ball (z + w) r - {z + w})"
+ by (simp add: o_def)
+ thus ?thesis using r
+ unfolding isolated_singularity_at_def by blast
+qed
+
+lemma isolated_singularity_at_shift_iff:
+ "isolated_singularity_at f (z + w) \<longleftrightarrow> isolated_singularity_at (\<lambda>x. f (x + w)) z"
+ using isolated_singularity_at_shift[of f w z]
+ isolated_singularity_at_shift[of "\<lambda>x. f (x + w)" "-w" "w + z"]
+ by (auto simp: algebra_simps)
+
+lemma isolated_singularity_at_shift_0:
+ "NO_MATCH 0 z \<Longrightarrow> isolated_singularity_at f z \<longleftrightarrow> isolated_singularity_at (\<lambda>x. f (z + x)) 0"
+ using isolated_singularity_at_shift_iff[of f 0 z] by (simp add: add_ac)
+
+lemma not_essential_shift:
+ assumes "not_essential (\<lambda>x. f (x + w)) z"
+ shows "not_essential f (z + w)"
+proof -
+ from assms consider c where "(\<lambda>x. f (x + w)) \<midarrow>z\<rightarrow> c" | "is_pole (\<lambda>x. f (x + w)) z"
+ unfolding not_essential_def by blast
+ thus ?thesis
+ proof cases
+ case (1 c)
+ hence "f \<midarrow>z + w\<rightarrow> c"
+ by (smt (verit, ccfv_SIG) LIM_cong add.assoc filterlim_at_to_0)
+ thus ?thesis
+ by (auto simp: not_essential_def)
+ next
+ case 2
+ hence "is_pole f (z + w)"
+ by (subst is_pole_shift_iff [symmetric]) (auto simp: o_def add_ac)
+ thus ?thesis
+ by (auto simp: not_essential_def)
+ qed
+qed
+
+lemma not_essential_shift_iff: "not_essential f (z + w) \<longleftrightarrow> not_essential (\<lambda>x. f (x + w)) z"
+ using not_essential_shift[of f w z]
+ not_essential_shift[of "\<lambda>x. f (x + w)" "-w" "w + z"]
+ by (auto simp: algebra_simps)
+
+lemma not_essential_shift_0:
+ "NO_MATCH 0 z \<Longrightarrow> not_essential f z \<longleftrightarrow> not_essential (\<lambda>x. f (z + x)) 0"
+ using not_essential_shift_iff[of f 0 z] by (simp add: add_ac)
+
+lemma not_essential_holomorphic:
+ assumes "f holomorphic_on A" "x \<in> A" "open A"
+ shows "not_essential f x"
+proof -
+ have "continuous_on A f"
+ using assms holomorphic_on_imp_continuous_on by blast
+ hence "f \<midarrow>x\<rightarrow> f x"
+ using assms continuous_on_eq_continuous_at isContD by blast
+ thus ?thesis
+ by (auto simp: not_essential_def)
+qed
+
+lemma eventually_not_pole:
+ assumes "isolated_singularity_at f z"
+ shows "eventually (\<lambda>w. \<not>is_pole f w) (at z)"
+proof -
+ from assms obtain r where "r > 0" and r: "f analytic_on ball z r - {z}"
+ by (auto simp: isolated_singularity_at_def)
+ then have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+ by (intro eventually_at_in_open) auto
+ thus "eventually (\<lambda>w. \<not>is_pole f w) (at z)"
+ proof eventually_elim
+ case (elim w)
+ with r show ?case
+ using analytic_imp_holomorphic not_is_pole_holomorphic open_delete by blast
+ qed
+qed
+
+lemma not_islimpt_poles:
+ assumes "isolated_singularity_at f z"
+ shows "\<not>z islimpt {w. is_pole f w}"
+ using eventually_not_pole [OF assms]
+ by (auto simp: islimpt_conv_frequently_at frequently_def)
+
+lemma analytic_at_imp_no_pole: "f analytic_on {z} \<Longrightarrow> \<not>is_pole f z"
+ using analytic_at not_is_pole_holomorphic by blast
+
+lemma not_essential_const [singularity_intros]: "not_essential (\<lambda>_. c) z"
+ unfolding not_essential_def by (rule exI[of _ c]) auto
+
+lemma not_essential_uminus [singularity_intros]:
+ assumes f_ness: "not_essential f z"
+ assumes f_iso:"isolated_singularity_at f z"
+ shows "not_essential (\<lambda>w. -f w) z"
+proof -
+ have "not_essential (\<lambda>w. -1 * f w) z"
+ by (intro assms singularity_intros)
+ thus ?thesis by simp
+qed
+
subsubsection \<open>The order of non-essential singularities (i.e. removable singularities or poles)\<close>
-
definition\<^marker>\<open>tag important\<close> zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where
"zorder f z = (THE n. (\<exists>h r. r>0 \<and> h holomorphic_on cball z r \<and> h z\<noteq>0
\<and> (\<forall>w\<in>cball z r - {z}. f w = h w * (w-z) powr (of_int n)
@@ -749,6 +937,29 @@
then show ?thesis unfolding P_def by auto
qed
+lemma zorder_shift:
+ shows "zorder f z = zorder (\<lambda>u. f (u + z)) 0"
+ unfolding zorder_def
+ apply (rule arg_cong [of concl: The])
+ apply (auto simp: fun_eq_iff Ball_def dist_norm)
+ subgoal for x h r
+ apply (rule_tac x="h o (+)z" in exI)
+ apply (rule_tac x="r" in exI)
+ apply (intro conjI holomorphic_on_compose holomorphic_intros)
+ apply (simp_all flip: cball_translation)
+ apply (simp add: add.commute)
+ done
+ subgoal for x h r
+ apply (rule_tac x="h o (\<lambda>u. u-z)" in exI)
+ apply (rule_tac x="r" in exI)
+ apply (intro conjI holomorphic_on_compose holomorphic_intros)
+ apply (simp_all add: flip: cball_translation_subtract)
+ by (metis diff_add_cancel eq_iff_diff_eq_0 norm_minus_commute)
+ done
+
+lemma zorder_shift': "NO_MATCH 0 z \<Longrightarrow> zorder f z = zorder (\<lambda>u. f (u + z)) 0"
+ by (rule zorder_shift)
+
lemma
fixes f::"complex \<Rightarrow> complex" and z::complex
assumes f_iso:"isolated_singularity_at f z"
@@ -819,6 +1030,99 @@
by (metis DiffI dist_commute mem_ball singletonD)
qed
+lemma zor_poly_shift:
+ assumes iso1: "isolated_singularity_at f z"
+ and ness1: "not_essential f z"
+ and nzero1: "\<exists>\<^sub>F w in at z. f w \<noteq> 0"
+ shows "\<forall>\<^sub>F w in nhds z. zor_poly f z w = zor_poly (\<lambda>u. f (z + u)) 0 (w-z)"
+proof -
+ obtain r1 where "r1>0" "zor_poly f z z \<noteq> 0" and
+ holo1:"zor_poly f z holomorphic_on cball z r1" and
+ rball1:"\<forall>w\<in>cball z r1 - {z}.
+ f w = zor_poly f z w * (w - z) powr of_int (zorder f z) \<and>
+ zor_poly f z w \<noteq> 0"
+ using zorder_exist[OF iso1 ness1 nzero1] by blast
+
+ define ff where "ff=(\<lambda>u. f (z + u))"
+ have "isolated_singularity_at ff 0"
+ unfolding ff_def
+ using iso1 isolated_singularity_at_shift_iff[of f 0 z]
+ by (simp add:algebra_simps)
+ moreover have "not_essential ff 0"
+ unfolding ff_def
+ using ness1 not_essential_shift_iff[of f 0 z]
+ by (simp add:algebra_simps)
+ moreover have "\<exists>\<^sub>F w in at 0. ff w \<noteq> 0"
+ unfolding ff_def using nzero1
+ by (smt (verit, ccfv_SIG) add.commute eventually_at_to_0
+ eventually_mono not_frequently)
+ ultimately obtain r2 where "r2>0" "zor_poly ff 0 0 \<noteq> 0" and
+ holo2:"zor_poly ff 0 holomorphic_on cball 0 r2" and
+ rball2:"\<forall>w\<in>cball 0 r2 - {0}.
+ ff w = zor_poly ff 0 w * w powr of_int (zorder ff 0) \<and>
+ zor_poly ff 0 w \<noteq> 0"
+ using zorder_exist[of ff 0] by auto
+
+ define r where "r=min r1 r2"
+ have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto
+
+ have "zor_poly f z w = zor_poly ff 0 (w - z)"
+ if "w\<in>ball z r - {z}" for w
+ proof -
+ define n::complex where "n= of_int (zorder f z)"
+
+ have "f w = zor_poly f z w * (w - z) powr n"
+ proof -
+ have "w\<in>cball z r1 - {z}"
+ using r_def that by auto
+ from rball1[rule_format, OF this]
+ show ?thesis unfolding n_def by auto
+ qed
+
+ moreover have "f w = zor_poly ff 0 (w - z) * (w - z) powr n"
+ proof -
+ have "w-z\<in>cball 0 r2 - {0}"
+ using r_def that by (auto simp:dist_complex_def)
+ from rball2[rule_format, OF this]
+ have "ff (w - z) = zor_poly ff 0 (w - z) * (w - z)
+ powr of_int (zorder ff 0)"
+ by simp
+ moreover have "of_int (zorder ff 0) = n"
+ unfolding n_def ff_def by (simp add:zorder_shift' add.commute)
+ ultimately show ?thesis unfolding ff_def by auto
+ qed
+ ultimately have "zor_poly f z w * (w - z) powr n
+ = zor_poly ff 0 (w - z) * (w - z) powr n"
+ by auto
+ moreover have "(w - z) powr n \<noteq>0"
+ using that by auto
+ ultimately show ?thesis
+ apply (subst (asm) mult_cancel_right)
+ by (simp add:ff_def)
+ qed
+ then have "\<forall>\<^sub>F w in at z. zor_poly f z w
+ = zor_poly ff 0 (w - z)"
+ unfolding eventually_at
+ apply (rule_tac x=r in exI)
+ using \<open>r>0\<close> by (auto simp:dist_commute)
+ moreover have "isCont (zor_poly f z) z"
+ using holo1[THEN holomorphic_on_imp_continuous_on]
+ apply (elim continuous_on_interior)
+ using \<open>r1>0\<close> by auto
+ moreover have "isCont (\<lambda>w. zor_poly ff 0 (w - z)) z"
+ proof -
+ have "isCont (zor_poly ff 0) 0"
+ using holo2[THEN holomorphic_on_imp_continuous_on]
+ apply (elim continuous_on_interior)
+ using \<open>r2>0\<close> by auto
+ then show ?thesis
+ unfolding isCont_iff by simp
+ qed
+ ultimately show "\<forall>\<^sub>F w in nhds z. zor_poly f z w
+ = zor_poly ff 0 (w - z)"
+ by (elim at_within_isCont_imp_nhds;auto)
+qed
+
lemma
fixes f g::"complex \<Rightarrow> complex" and z::complex
assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z"
@@ -979,7 +1283,7 @@
have fz_lim: "f\<midarrow> z \<rightarrow> f z"
by (metis assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on)
have gz_lim: "g \<midarrow>z\<rightarrow>g z"
- by (metis r open_ball at_within_open ball_subset_cball centre_in_ball
+ by (metis r open_ball at_within_open ball_subset_cball centre_in_ball
continuous_on_def continuous_on_subset holomorphic_on_imp_continuous_on)
have if_0:"if f z=0 then n > 0 else n=0"
proof -
@@ -1185,7 +1489,7 @@
unfolding z'_def using \<open>d>0\<close> \<open>r>0\<close> by (auto simp add:dist_norm)
moreover have "f z' \<noteq> 0"
proof (subst fg_eq[OF _ \<open>z'\<noteq>z\<close>])
- have "z' \<in> cball z r"
+ have "z' \<in> cball z r"
unfolding z'_def using \<open>r>0\<close> \<open>d>0\<close> by (auto simp add:dist_norm)
then show " z' \<in> s" using r(2) by blast
show "g z' * (z' - z) powr of_int n \<noteq> 0"
@@ -1493,4 +1797,476 @@
from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
qed
-end
\ No newline at end of file
+lemma
+ assumes "is_pole f (x :: complex)" "open A" "x \<in> A"
+ assumes "\<And>y. y \<in> A - {x} \<Longrightarrow> (f has_field_derivative f' y) (at y)"
+ shows is_pole_deriv': "is_pole f' x"
+ and zorder_deriv': "zorder f' x = zorder f x - 1"
+proof -
+ have holo: "f holomorphic_on A - {x}"
+ using assms by (subst holomorphic_on_open) auto
+ obtain r where r: "r > 0" "ball x r \<subseteq> A"
+ using assms(2,3) openE by blast
+ moreover have "open (ball x r - {x})"
+ by auto
+ ultimately have "isolated_singularity_at f x"
+ by (auto simp: isolated_singularity_at_def analytic_on_open
+ intro!: exI[of _ r] holomorphic_on_subset[OF holo])
+ hence ev: "\<forall>\<^sub>F w in at x. zor_poly f x w = f w * (w - x) ^ nat (- zorder f x)"
+ using \<open>is_pole f x\<close> zor_poly_pole_eq by blast
+
+ define P where "P = zor_poly f x"
+ define n where "n = nat (-zorder f x)"
+
+ obtain r where r: "r > 0" "cball x r \<subseteq> A" "P holomorphic_on cball x r" "zorder f x < 0" "P x \<noteq> 0"
+ "\<forall>w\<in>cball x r - {x}. f w = P w / (w - x) ^ n \<and> P w \<noteq> 0"
+ unfolding P_def n_def using zorder_exist_pole[OF holo assms(2,3,1)] by blast
+ have n: "n > 0"
+ using r(4) by (auto simp: n_def)
+
+ have [derivative_intros]: "(P has_field_derivative deriv P w) (at w)"
+ if "w \<in> ball x r" for w
+ using that by (intro holomorphic_derivI[OF holomorphic_on_subset[OF r(3), of "ball x r"]]) auto
+
+ define D where "D = (\<lambda>w. (deriv P w * (w - x) - of_nat n * P w) / (w - x) ^ (n + 1))"
+ define n' where "n' = n - 1"
+ have n': "n = Suc n'"
+ using n by (simp add: n'_def)
+
+ have "eventually (\<lambda>w. w \<in> ball x r) (nhds x)"
+ using \<open>r > 0\<close> by (intro eventually_nhds_in_open) auto
+ hence ev'': "eventually (\<lambda>w. w \<in> ball x r - {x}) (at x)"
+ by (auto simp: eventually_at_filter elim: eventually_mono)
+
+ {
+ fix w assume w: "w \<in> ball x r - {x}"
+ have ev': "eventually (\<lambda>w. w \<in> ball x r - {x}) (nhds w)"
+ using w by (intro eventually_nhds_in_open) auto
+
+ have "((\<lambda>w. P w / (w - x) ^ n) has_field_derivative D w) (at w)"
+ apply (rule derivative_eq_intros refl | use w in force)+
+ using w
+ apply (simp add: divide_simps D_def)
+ apply (simp add: n' algebra_simps)
+ done
+ also have "?this \<longleftrightarrow> (f has_field_derivative D w) (at w)"
+ using r by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev']) auto
+ finally have "(f has_field_derivative D w) (at w)" .
+ moreover have "(f has_field_derivative f' w) (at w)"
+ using w r by (intro assms) auto
+ ultimately have "D w = f' w"
+ using DERIV_unique by blast
+ } note D_eq = this
+
+ have "is_pole D x"
+ unfolding D_def using n \<open>r > 0\<close> \<open>P x \<noteq> 0\<close>
+ by (intro is_pole_basic[where A = "ball x r"] holomorphic_intros holomorphic_on_subset[OF r(3)]) auto
+ also have "?this \<longleftrightarrow> is_pole f' x"
+ by (intro is_pole_cong eventually_mono[OF ev''] D_eq) auto
+ finally show "is_pole f' x" .
+
+ have "zorder f' x = -int (Suc n)"
+ proof (rule zorder_eqI)
+ show "open (ball x r)" "x \<in> ball x r"
+ using \<open>r > 0\<close> by auto
+ show "f' w = (deriv P w * (w - x) - of_nat n * P w) * (w - x) powr of_int (- int (Suc n))"
+ if "w \<in> ball x r" "w \<noteq> x" for w
+ using that D_eq[of w] n by (auto simp: D_def powr_diff powr_minus powr_nat' divide_simps)
+ qed (use r n in \<open>auto intro!: holomorphic_intros\<close>)
+ thus "zorder f' x = zorder f x - 1"
+ using n by (simp add: n_def)
+qed
+
+lemma
+ assumes "is_pole f (x :: complex)" "isolated_singularity_at f x"
+ shows is_pole_deriv: "is_pole (deriv f) x"
+ and zorder_deriv: "zorder (deriv f) x = zorder f x - 1"
+proof -
+ from assms(2) obtain r where r: "r > 0" "f analytic_on ball x r - {x}"
+ by (auto simp: isolated_singularity_at_def)
+ hence holo: "f holomorphic_on ball x r - {x}"
+ by (subst (asm) analytic_on_open) auto
+ have *: "x \<in> ball x r" "open (ball x r)" "open (ball x r - {x})"
+ using \<open>r > 0\<close> by auto
+ show "is_pole (deriv f) x" "zorder (deriv f) x = zorder f x - 1"
+ by (rule is_pole_deriv' zorder_deriv', (rule assms * holomorphic_derivI holo | assumption)+)+
+qed
+
+lemma removable_singularity_deriv':
+ assumes "f \<midarrow>x\<rightarrow> c" "x \<in> A" "open (A :: complex set)"
+ assumes "\<And>y. y \<in> A - {x} \<Longrightarrow> (f has_field_derivative f' y) (at y)"
+ shows "\<exists>c. f' \<midarrow>x\<rightarrow> c"
+proof -
+ have holo: "f holomorphic_on A - {x}"
+ using assms by (subst holomorphic_on_open) auto
+
+ define g where "g = (\<lambda>y. if y = x then c else f y)"
+ have deriv_g_eq: "deriv g y = f' y" if "y \<in> A - {x}" for y
+ proof -
+ have ev: "eventually (\<lambda>y. y \<in> A - {x}) (nhds y)"
+ using that assms by (intro eventually_nhds_in_open) auto
+ have "(f has_field_derivative f' y) (at y)"
+ using assms that by auto
+ also have "?this \<longleftrightarrow> (g has_field_derivative f' y) (at y)"
+ by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev]) (auto simp: g_def)
+ finally show ?thesis
+ by (intro DERIV_imp_deriv assms)
+ qed
+
+ have "g holomorphic_on A"
+ unfolding g_def using assms assms(1) holo by (intro removable_singularity) auto
+ hence "deriv g holomorphic_on A"
+ by (intro holomorphic_deriv assms)
+ hence "continuous_on A (deriv g)"
+ by (meson holomorphic_on_imp_continuous_on)
+ hence "(deriv g \<longlongrightarrow> deriv g x) (at x within A)"
+ using assms by (auto simp: continuous_on_def)
+ also have "?this \<longleftrightarrow> (f' \<longlongrightarrow> deriv g x) (at x within A)"
+ by (intro filterlim_cong refl) (auto simp: eventually_at_filter deriv_g_eq)
+ finally have "f' \<midarrow>x\<rightarrow> deriv g x"
+ using \<open>open A\<close> \<open>x \<in> A\<close> by (meson tendsto_within_open)
+ thus ?thesis
+ by blast
+qed
+
+lemma removable_singularity_deriv:
+ assumes "f \<midarrow>x\<rightarrow> c" "isolated_singularity_at f x"
+ shows "\<exists>c. deriv f \<midarrow>x\<rightarrow> c"
+proof -
+ from assms(2) obtain r where r: "r > 0" "f analytic_on ball x r - {x}"
+ by (auto simp: isolated_singularity_at_def)
+ hence holo: "f holomorphic_on ball x r - {x}"
+ using analytic_imp_holomorphic by blast
+ show ?thesis
+ using assms(1)
+ proof (rule removable_singularity_deriv')
+ show "x \<in> ball x r" "open (ball x r)"
+ using \<open>r > 0\<close> by auto
+ qed (auto intro!: holomorphic_derivI[OF holo])
+qed
+
+lemma not_essential_deriv':
+ assumes "not_essential f x" "x \<in> A" "open A"
+ assumes "\<And>y. y \<in> A - {x} \<Longrightarrow> (f has_field_derivative f' y) (at y)"
+ shows "not_essential f' x"
+proof -
+ have holo: "f holomorphic_on A - {x}"
+ using assms by (subst holomorphic_on_open) auto
+ from assms consider "is_pole f x" | c where "f \<midarrow>x\<rightarrow> c"
+ by (auto simp: not_essential_def)
+ thus ?thesis
+ proof cases
+ case 1
+ hence "is_pole f' x"
+ using is_pole_deriv' assms by blast
+ thus ?thesis by (auto simp: not_essential_def)
+ next
+ case (2 c)
+ from 2 have "\<exists>c. f' \<midarrow>x\<rightarrow> c"
+ by (rule removable_singularity_deriv'[OF _ assms(2-4)])
+ thus ?thesis
+ by (auto simp: not_essential_def)
+ qed
+qed
+
+lemma not_essential_deriv[singularity_intros]:
+ assumes "not_essential f x" "isolated_singularity_at f x"
+ shows "not_essential (deriv f) x"
+proof -
+ from assms(2) obtain r where r: "r > 0" "f analytic_on ball x r - {x}"
+ by (auto simp: isolated_singularity_at_def)
+ hence holo: "f holomorphic_on ball x r - {x}"
+ by (subst (asm) analytic_on_open) auto
+ show ?thesis
+ using assms(1)
+ proof (rule not_essential_deriv')
+ show "x \<in> ball x r" "open (ball x r)"
+ using \<open>r > 0\<close> by auto
+ qed (auto intro!: holomorphic_derivI[OF holo])
+qed
+
+lemma not_essential_frequently_0_imp_tendsto_0:
+ fixes f :: "complex \<Rightarrow> complex"
+ assumes sing: "isolated_singularity_at f z" "not_essential f z"
+ assumes freq: "frequently (\<lambda>z. f z = 0) (at z)"
+ shows "f \<midarrow>z\<rightarrow> 0"
+proof -
+ from freq obtain g :: "nat \<Rightarrow> complex" where g: "filterlim g (at z) at_top" "\<And>n. f (g n) = 0"
+ using frequently_atE by blast
+ have "eventually (\<lambda>x. f (g x) = 0) sequentially"
+ using g by auto
+ hence fg: "(\<lambda>x. f (g x)) \<longlonglongrightarrow> 0"
+ by (simp add: tendsto_eventually)
+
+ from assms(2) consider c where "f \<midarrow>z\<rightarrow> c" | "is_pole f z"
+ unfolding not_essential_def by blast
+ thus ?thesis
+ proof cases
+ case (1 c)
+ have "(\<lambda>x. f (g x)) \<longlonglongrightarrow> c"
+ by (rule filterlim_compose[OF 1 g(1)])
+ with fg have "c = 0"
+ using LIMSEQ_unique by blast
+ with 1 show ?thesis by simp
+ next
+ case 2
+ have "filterlim (\<lambda>x. f (g x)) at_infinity sequentially"
+ by (rule filterlim_compose[OF _ g(1)]) (use 2 in \<open>auto simp: is_pole_def\<close>)
+ with fg have False
+ by (meson not_tendsto_and_filterlim_at_infinity sequentially_bot)
+ thus ?thesis ..
+ qed
+qed
+
+lemma not_essential_frequently_0_imp_eventually_0:
+ fixes f :: "complex \<Rightarrow> complex"
+ assumes sing: "isolated_singularity_at f z" "not_essential f z"
+ assumes freq: "frequently (\<lambda>z. f z = 0) (at z)"
+ shows "eventually (\<lambda>z. f z = 0) (at z)"
+proof -
+ from sing obtain r where r: "r > 0" and "f analytic_on ball z r - {z}"
+ by (auto simp: isolated_singularity_at_def)
+ hence holo: "f holomorphic_on ball z r - {z}"
+ by (subst (asm) analytic_on_open) auto
+ have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+ using r by (intro eventually_at_in_open) auto
+ from freq and this have "frequently (\<lambda>w. f w = 0 \<and> w \<in> ball z r - {z}) (at z)"
+ using frequently_eventually_frequently by blast
+ hence "frequently (\<lambda>w. w \<in> {w\<in>ball z r - {z}. f w = 0}) (at z)"
+ by (simp add: conj_commute)
+ hence limpt: "z islimpt {w\<in>ball z r - {z}. f w = 0}"
+ using islimpt_conv_frequently_at by blast
+
+ define g where "g = (\<lambda>w. if w = z then 0 else f w)"
+ have "f \<midarrow>z\<rightarrow> 0"
+ by (intro not_essential_frequently_0_imp_tendsto_0 assms)
+ hence g_holo: "g holomorphic_on ball z r"
+ unfolding g_def by (intro removable_singularity holo) auto
+
+ have g_eq_0: "g w = 0" if "w \<in> ball z r" for w
+ proof (rule analytic_continuation[where f = g])
+ show "open (ball z r)" "connected (ball z r)"
+ using r by auto
+ show "z islimpt {w\<in>ball z r - {z}. f w = 0}"
+ by fact
+ show "g w = 0" if "w \<in> {w \<in> ball z r - {z}. f w = 0}" for w
+ using that by (auto simp: g_def)
+ qed (use r that g_holo in auto)
+
+ have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+ using r by (intro eventually_at_in_open) auto
+ thus "eventually (\<lambda>w. f w = 0) (at z)"
+ proof eventually_elim
+ case (elim w)
+ thus ?case using g_eq_0[of w]
+ by (auto simp: g_def)
+ qed
+qed
+
+lemma pole_imp_not_constant:
+ fixes f :: "'a :: {perfect_space} \<Rightarrow> _"
+ assumes "is_pole f x" "open A" "x \<in> A" "A \<subseteq> insert x B"
+ shows "\<not>f constant_on B"
+proof
+ assume *: "f constant_on B"
+ then obtain c where c: "\<forall>x\<in>B. f x = c"
+ by (auto simp: constant_on_def)
+ have "eventually (\<lambda>y. y \<in> A - {x}) (at x)"
+ using assms by (intro eventually_at_in_open) auto
+ hence "eventually (\<lambda>y. f y = c) (at x)"
+ by eventually_elim (use c assms in auto)
+ hence **: "f \<midarrow>x\<rightarrow> c"
+ by (simp add: tendsto_eventually)
+ show False
+ using not_tendsto_and_filterlim_at_infinity[OF _ ** assms(1)[unfolded is_pole_def]] by simp
+qed
+
+
+lemma neg_zorder_imp_is_pole:
+ assumes iso:"isolated_singularity_at f z" and f_ness:"not_essential f z"
+ and "zorder f z < 0" and fre_nz:"\<exists>\<^sub>F w in at z. f w \<noteq> 0 "
+ shows "is_pole f z"
+proof -
+ define P where "P = zor_poly f z"
+ define n where "n = zorder f z"
+ have "n<0" unfolding n_def by (simp add: assms(3))
+ define nn where "nn = nat (-n)"
+
+ obtain r where "P z \<noteq> 0" "r>0" and r_holo:"P holomorphic_on cball z r" and
+ w_Pn:"(\<forall>w\<in>cball z r - {z}. f w = P w * (w - z) powr of_int n \<and> P w \<noteq> 0)"
+ using zorder_exist[OF iso f_ness fre_nz,folded P_def n_def] by auto
+
+ have "is_pole (\<lambda>w. P w * (w - z) powr of_int n) z"
+ unfolding is_pole_def
+ proof (rule tendsto_mult_filterlim_at_infinity)
+ show "P \<midarrow>z\<rightarrow> P z"
+ by (meson open_ball \<open>0 < r\<close> ball_subset_cball centre_in_ball
+ continuous_on_eq_continuous_at continuous_on_subset
+ holomorphic_on_imp_continuous_on isContD r_holo)
+ show "P z\<noteq>0" by (simp add: \<open>P z \<noteq> 0\<close>)
+
+ have "LIM x at z. inverse ((x - z) ^ nat (-n)) :> at_infinity"
+ apply (subst filterlim_inverse_at_iff[symmetric])
+ using \<open>n<0\<close>
+ by (auto intro!:tendsto_eq_intros filterlim_atI
+ simp add:eventually_at_filter)
+ then show "LIM x at z. (x - z) powr of_int n :> at_infinity"
+ proof (elim filterlim_mono_eventually)
+ have "inverse ((x - z) ^ nat (-n)) = (x - z) powr of_int n"
+ if "x\<noteq>z" for x
+ apply (subst powr_of_int)
+ using \<open>n<0\<close> using that by auto
+ then show "\<forall>\<^sub>F x in at z. inverse ((x - z) ^ nat (-n))
+ = (x - z) powr of_int n"
+ by (simp add: eventually_at_filter)
+ qed auto
+ qed
+ moreover have "\<forall>\<^sub>F w in at z. f w = P w * (w - z) powr of_int n"
+ unfolding eventually_at_le
+ apply (rule exI[where x=r])
+ using w_Pn \<open>r>0\<close> by (simp add: dist_commute)
+ ultimately show ?thesis using is_pole_cong by fast
+qed
+
+lemma is_pole_divide_zorder:
+ fixes f g::"complex \<Rightarrow> complex" and z::complex
+ assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z"
+ and f_ness:"not_essential f z" and g_ness:"not_essential g z"
+ and fg_nconst: "\<exists>\<^sub>Fw in (at z). f w * g w\<noteq> 0"
+ and z_less:"zorder f z < zorder g z"
+ shows "is_pole (\<lambda>z. f z / g z) z"
+proof -
+ define fn gn fg where "fn=zorder f z" and "gn=zorder g z"
+ and "fg=(\<lambda>w. f w / g w)"
+
+ have "isolated_singularity_at fg z"
+ unfolding fg_def using f_iso g_iso g_ness
+ by (auto intro:singularity_intros)
+ moreover have "not_essential fg z"
+ unfolding fg_def using f_iso g_iso g_ness f_ness
+ by (auto intro:singularity_intros)
+ moreover have "zorder fg z < 0"
+ proof -
+ have "zorder fg z = fn - gn"
+ using zorder_divide[OF f_iso g_iso f_ness g_ness
+ fg_nconst,folded fn_def gn_def fg_def] .
+ then show ?thesis
+ using z_less by (simp add: fn_def gn_def)
+ qed
+ moreover have "\<exists>\<^sub>F w in at z. fg w \<noteq> 0"
+ using fg_nconst unfolding fg_def by force
+ ultimately show "is_pole fg z"
+ using neg_zorder_imp_is_pole by auto
+qed
+
+lemma isolated_pole_imp_nzero_times:
+ assumes f_iso:"isolated_singularity_at f z"
+ and "is_pole f z"
+ shows "\<exists>\<^sub>Fw in (at z). deriv f w * f w \<noteq> 0"
+proof (rule ccontr)
+ assume "\<not> (\<exists>\<^sub>F w in at z. deriv f w * f w \<noteq> 0)"
+ then have "\<forall>\<^sub>F x in at z. deriv f x * f x = 0"
+ unfolding not_frequently by simp
+ moreover have "\<forall>\<^sub>F w in at z. f w \<noteq> 0"
+ using non_zero_neighbour_pole[OF \<open>is_pole f z\<close>] .
+ moreover have "\<forall>\<^sub>F w in at z. deriv f w \<noteq> 0"
+ using is_pole_deriv[OF \<open>is_pole f z\<close> f_iso,THEN non_zero_neighbour_pole]
+ .
+ ultimately have "\<forall>\<^sub>F w in at z. False"
+ apply eventually_elim
+ by auto
+ then show False by auto
+qed
+
+lemma isolated_pole_imp_neg_zorder:
+ assumes f_iso:"isolated_singularity_at f z"
+ and "is_pole f z"
+ shows "zorder f z<0"
+proof -
+ obtain e where [simp]:"e>0" and f_holo:"f holomorphic_on ball z e - {z}"
+ using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by blast
+ show ?thesis
+ using zorder_exist_pole[OF f_holo,simplified,OF \<open>is_pole f z\<close>]
+ by auto
+qed
+
+lemma isolated_singularity_at_deriv[singularity_intros]:
+ assumes "isolated_singularity_at f x"
+ shows "isolated_singularity_at (deriv f) x"
+proof -
+ obtain r where "r>0" "f analytic_on ball x r - {x}"
+ using assms unfolding isolated_singularity_at_def by auto
+ from analytic_deriv[OF this(2)]
+ have "deriv f analytic_on ball x r - {x}" .
+ with \<open>r>0\<close> show ?thesis
+ unfolding isolated_singularity_at_def by auto
+qed
+
+lemma zorder_deriv_minus_1:
+ fixes f g::"complex \<Rightarrow> complex" and z::complex
+ assumes f_iso:"isolated_singularity_at f z"
+ and f_ness:"not_essential f z"
+ and f_nconst:"\<exists>\<^sub>F w in at z. f w \<noteq> 0"
+ and f_ord:"zorder f z \<noteq>0"
+ shows "zorder (deriv f) z = zorder f z - 1"
+proof -
+ define P where "P = zor_poly f z"
+ define n where "n = zorder f z"
+ have "n\<noteq>0" unfolding n_def using f_ord by auto
+
+ obtain r where "P z \<noteq> 0" "r>0" and P_holo:"P holomorphic_on cball z r"
+ and "(\<forall>w\<in>cball z r - {z}. f w
+ = P w * (w - z) powr of_int n \<and> P w \<noteq> 0)"
+ using zorder_exist[OF f_iso f_ness f_nconst,folded P_def n_def] by auto
+ from this(4)
+ have f_eq:"(\<forall>w\<in>cball z r - {z}. f w
+ = P w * (w - z) powi n \<and> P w \<noteq> 0)"
+ using complex_powr_of_int f_ord n_def by presburger
+
+ define D where "D = (\<lambda>w. (deriv P w * (w - z) + of_int n * P w)
+ * (w - z) powi (n - 1))"
+
+ have deriv_f_eq:"deriv f w = D w" if "w \<in> ball z r - {z}" for w
+ proof -
+ have ev': "eventually (\<lambda>w. w \<in> ball z r - {z}) (nhds w)"
+ using that by (intro eventually_nhds_in_open) auto
+
+ define wz where "wz = w - z"
+
+ have "wz \<noteq>0" unfolding wz_def using that by auto
+ moreover have "(P has_field_derivative deriv P w) (at w)"
+ by (meson DiffD1 Elementary_Metric_Spaces.open_ball P_holo
+ ball_subset_cball holomorphic_derivI holomorphic_on_subset that)
+ ultimately have "((\<lambda>w. P w * (w - z) powi n) has_field_derivative D w) (at w)"
+ unfolding D_def using that
+ apply (auto intro!: derivative_eq_intros)
+ apply (fold wz_def)
+ by (auto simp:algebra_simps simp flip:power_int_add_1')
+ also have "?this \<longleftrightarrow> (f has_field_derivative D w) (at w)"
+ using f_eq
+ by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev']) auto
+ ultimately have "(f has_field_derivative D w) (at w)" by simp
+ moreover have "(f has_field_derivative deriv f w) (at w)"
+ by (metis DERIV_imp_deriv calculation)
+ ultimately show ?thesis using DERIV_imp_deriv by blast
+ qed
+
+ show "zorder (deriv f) z = n - 1"
+ proof (rule zorder_eqI)
+ show "open (ball z r)" "z \<in> ball z r"
+ using \<open>r > 0\<close> by auto
+ define g where "g=(\<lambda>w. (deriv P w * (w - z) + of_int n * P w))"
+ show "g holomorphic_on ball z r"
+ unfolding g_def using P_holo
+ by (auto intro!:holomorphic_intros)
+ show "g z \<noteq> 0"
+ unfolding g_def using \<open>P z \<noteq> 0\<close> \<open>n\<noteq>0\<close> by auto
+ show "deriv f w =
+ (deriv P w * (w - z) + of_int n * P w) * (w - z) powr of_int (n - 1)"
+ if "w \<in> ball z r" "w \<noteq> z" for w
+ apply (subst complex_powr_of_int)
+ using deriv_f_eq that unfolding D_def by auto
+ qed
+qed
+
+end
--- a/src/HOL/Complex_Analysis/Contour_Integration.thy Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy Wed Feb 08 15:05:24 2023 +0000
@@ -94,8 +94,6 @@
subsection\<^marker>\<open>tag unimportant\<close> \<open>Reversing a path\<close>
-
-
lemma has_contour_integral_reversepath:
assumes "valid_path g" and f: "(f has_contour_integral i) g"
shows "(f has_contour_integral (-i)) (reversepath g)"
@@ -807,9 +805,8 @@
lemma contour_integral_const_linepath [simp]: "contour_integral (linepath a b) (\<lambda>x. c) = c*(b - a)"
by (rule contour_integral_unique [OF has_contour_integral_const_linepath])
-lemma contour_integral_neg:
- "f contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. -(f x)) = -(contour_integral g f)"
- by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_neg)
+lemma contour_integral_neg: "contour_integral g (\<lambda>z. -f z) = -contour_integral g f"
+ by (simp add: contour_integral_integral)
lemma contour_integral_add:
"f1 contour_integrable_on g \<Longrightarrow> f2 contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. f1 x + f2 x) =
@@ -903,6 +900,19 @@
unfolding contour_integrable_on_def
by (metis has_contour_integral_sum)
+lemma contour_integrable_lmul_iff:
+ "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c * f x) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
+ using contour_integrable_lmul[of f g c] contour_integrable_lmul[of "\<lambda>x. c * f x" g "inverse c"]
+ by (auto simp: field_simps)
+
+lemma contour_integrable_rmul_iff:
+ "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x * c) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
+ using contour_integrable_rmul[of f g c] contour_integrable_rmul[of "\<lambda>x. c * f x" g "inverse c"]
+ by (auto simp: field_simps)
+
+lemma contour_integrable_div_iff:
+ "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / c) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
+ using contour_integrable_rmul_iff[of "inverse c"] by (simp add: field_simps)
subsection\<^marker>\<open>tag unimportant\<close> \<open>Reversing a path integral\<close>
@@ -912,9 +922,9 @@
using has_contour_integral_reversepath valid_path_linepath by fastforce
lemma contour_integral_reverse_linepath:
- "continuous_on (closed_segment a b) f
- \<Longrightarrow> contour_integral (linepath a b) f = - (contour_integral(linepath b a) f)"
- by (metis contour_integrable_continuous_linepath contour_integral_unique has_contour_integral_integral has_contour_integral_reverse_linepath)
+ "continuous_on (closed_segment a b) f \<Longrightarrow> contour_integral (linepath a b) f = - (contour_integral(linepath b a) f)"
+ using contour_integral_reversepath by fastforce
+
text \<open>Splitting a path integral in a flat way.*)\<close>
--- a/src/HOL/Complex_Analysis/Residue_Theorem.thy Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Complex_Analysis/Residue_Theorem.thy Wed Feb 08 15:05:24 2023 +0000
@@ -454,9 +454,8 @@
theorem argument_principle:
fixes f::"complex \<Rightarrow> complex" and poles s:: "complex set"
- defines "pz \<equiv> {w. f w = 0 \<or> w \<in> poles}" \<comment> \<open>\<^term>\<open>pz\<close> is the set of poles and zeros\<close>
- assumes "open s" and
- "connected s" and
+ defines "pz \<equiv> {w\<in>s. f w = 0 \<or> w \<in> poles}" \<comment> \<open>\<^term>\<open>pz\<close> is the set of poles and zeros\<close>
+ assumes "open s" "connected s" and
f_holo:"f holomorphic_on s-poles" and
h_holo:"h holomorphic_on s" and
"valid_path g" and
@@ -464,7 +463,7 @@
path_img:"path_image g \<subseteq> s - pz" and
homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0" and
finite:"finite pz" and
- poles:"\<forall>p\<in>poles. is_pole f p"
+ poles:"\<forall>p\<in>s\<inter>poles. is_pole f p"
shows "contour_integral g (\<lambda>x. deriv f x * h x / f x) = 2 * pi * \<i> *
(\<Sum>p\<in>pz. winding_number g p * h p * zorder f p)"
(is "?L=?R")
@@ -505,10 +504,12 @@
case False
then have "p\<in>s-poles" using \<open>p\<in>s\<close> poles unfolding pz_def by auto
moreover have "open (s-poles)"
- using \<open>open s\<close>
- apply (elim open_Diff)
- apply (rule finite_imp_closed)
- using finite unfolding pz_def by simp
+ proof -
+ have "closed (s \<inter> poles)"
+ using finite by (simp add: pz_def finite_imp_closed rev_finite_subset subset_eq)
+ then show ?thesis
+ by (metis Diff_Compl Diff_Diff_Int Diff_eq \<open>open s\<close> open_Diff)
+ qed
ultimately have "isCont f p"
using holomorphic_on_imp_continuous_on[OF f_holo] continuous_on_eq_continuous_at
by auto
@@ -518,13 +519,21 @@
proof (rule ccontr)
assume "\<not> (\<exists>\<^sub>F w in at p. f w \<noteq> 0)"
then have "\<forall>\<^sub>F w in at p. f w= 0" unfolding frequently_def by auto
- then obtain rr where "rr>0" "\<forall>w\<in>ball p rr - {p}. f w =0"
+ then obtain r1 where "r1>0" and r1:"\<forall>w\<in>ball p r1 - {p}. f w =0"
unfolding eventually_at by (auto simp add:dist_commute)
- then have "ball p rr - {p} \<subseteq> {w\<in>ball p rr-{p}. f w=0}" by blast
- moreover have "infinite (ball p rr - {p})" using \<open>rr>0\<close> using finite_imp_not_open by fastforce
- ultimately have "infinite {w\<in>ball p rr-{p}. f w=0}" using infinite_super by blast
+ obtain r2 where "r2>0" and r2: "ball p r2 \<subseteq> s"
+ using \<open>p\<in>s\<close> \<open>open s\<close> openE by blast
+ define rr where "rr=min r1 r2"
+
+ from r1 r2
+ have "ball p rr - {p} \<subseteq> {w\<in> s \<inter> ball p rr-{p}. f w=0}"
+ unfolding rr_def by auto
+ moreover have "infinite (ball p rr - {p})"
+ using \<open>r1>0\<close> \<open>r2>0\<close> finite_imp_not_open
+ unfolding rr_def by fastforce
+ ultimately have "infinite {w\<in>s \<inter> ball p rr-{p}. f w=0}" using infinite_super by blast
then have "infinite pz"
- unfolding pz_def infinite_super by auto
+ unfolding pz_def by (smt (verit) infinite_super Collect_mono_iff DiffE Int_iff)
then show False using \<open>finite pz\<close> by auto
qed
ultimately obtain r where "pp p \<noteq> 0" and r:"r>0" "pp holomorphic_on cball p r"
@@ -795,7 +804,7 @@
theorem Rouche_theorem:
fixes f g::"complex \<Rightarrow> complex" and s:: "complex set"
defines "fg\<equiv>(\<lambda>p. f p + g p)"
- defines "zeros_fg\<equiv>{p. fg p = 0}" and "zeros_f\<equiv>{p. f p = 0}"
+ defines "zeros_fg\<equiv>{p\<in>s. fg p = 0}" and "zeros_f\<equiv>{p\<in>s. f p = 0}"
assumes
"open s" and "connected s" and
"finite zeros_fg" and
@@ -844,9 +853,8 @@
proof -
have "h p \<in> ball 1 1" when "p\<in>path_image \<gamma>" for p
proof -
- have "cmod (g p/f p) <1" using path_less[rule_format,OF that]
- apply (cases "cmod (f p) = 0")
- by (auto simp add: norm_divide)
+ have "cmod (g p/f p) <1"
+ by (smt (verit) divide_less_eq_1_pos norm_divide norm_ge_zero path_less that)
then show ?thesis unfolding h_def by (auto simp add:dist_complex_def)
qed
then have "path_image (h o \<gamma>) \<subseteq> ball 1 1"
@@ -935,9 +943,8 @@
assume "\<not> h p \<noteq> 0"
then have "g p / f p= -1" unfolding h_def by (simp add: add_eq_0_iff2)
then have "cmod (g p/f p) = 1" by auto
- moreover have "cmod (g p/f p) <1" using path_less[rule_format,OF that]
- apply (cases "cmod (f p) = 0")
- by (auto simp add: norm_divide)
+ moreover have "cmod (g p/f p) <1"
+ by (simp add: \<open>f p \<noteq> 0\<close> norm_divide path_less that)
ultimately show False by auto
qed
have der_fg:"deriv fg p = deriv f p + deriv g p" unfolding fg_def
@@ -963,20 +970,24 @@
ultimately show ?thesis by auto
qed
moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = c * (\<Sum>p\<in>zeros_fg. w p * zorder fg p)"
- unfolding c_def zeros_fg_def w_def
- proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo
- , of _ "{}" "\<lambda>_. 1",simplified])
- show "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto
- show "path_image \<gamma> \<subseteq> s - {p. fg p = 0}" using path_fg unfolding zeros_fg_def .
- show " finite {p. fg p = 0}" using \<open>finite zeros_fg\<close> unfolding zeros_fg_def .
+ proof -
+ have "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto
+ moreover
+ have "path_image \<gamma> \<subseteq> s - {p\<in>s. fg p = 0}" using path_fg unfolding zeros_fg_def .
+ moreover
+ have " finite {p\<in>s. fg p = 0}" using \<open>finite zeros_fg\<close> unfolding zeros_fg_def .
+ ultimately show ?thesis
+ unfolding c_def zeros_fg_def w_def
+ using argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo, of _ "{}" "\<lambda>_. 1"]
+ by simp
qed
moreover have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x) = c * (\<Sum>p\<in>zeros_f. w p * zorder f p)"
unfolding c_def zeros_f_def w_def
proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo
, of _ "{}" "\<lambda>_. 1",simplified])
show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto
- show "path_image \<gamma> \<subseteq> s - {p. f p = 0}" using path_f unfolding zeros_f_def .
- show " finite {p. f p = 0}" using \<open>finite zeros_f\<close> unfolding zeros_f_def .
+ show "path_image \<gamma> \<subseteq> s - {p\<in>s. f p = 0}" using path_f unfolding zeros_f_def .
+ show " finite {p\<in>s. f p = 0}" using \<open>finite zeros_f\<close> unfolding zeros_f_def .
qed
ultimately have " c* (\<Sum>p\<in>zeros_fg. w p * (zorder fg p)) = c* (\<Sum>p\<in>zeros_f. w p * (zorder f p))"
by auto
--- a/src/HOL/Filter.thy Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Filter.thy Wed Feb 08 15:05:24 2023 +0000
@@ -223,6 +223,16 @@
shows "\<exists>\<^sub>Fx in F. Q x \<and> P x"
using assms eventually_elim2 by (force simp add: frequently_def)
+lemma frequently_cong:
+ assumes ev: "eventually P F" and QR: "\<And>x. P x \<Longrightarrow> Q x \<longleftrightarrow> R x"
+ shows "frequently Q F \<longleftrightarrow> frequently R F"
+ unfolding frequently_def
+ using QR by (auto intro!: eventually_cong [OF ev])
+
+lemma frequently_eventually_frequently:
+ "frequently P F \<Longrightarrow> eventually Q F \<Longrightarrow> frequently (\<lambda>x. P x \<and> Q x) F"
+ using frequently_cong [of Q F P "\<lambda>x. P x \<and> Q x"] by meson
+
lemma eventually_frequently_const_simps:
"(\<exists>\<^sub>Fx in F. P x \<and> C) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<and> C"
"(\<exists>\<^sub>Fx in F. C \<and> P x) \<longleftrightarrow> C \<and> (\<exists>\<^sub>Fx in F. P x)"
@@ -606,12 +616,6 @@
lemma filtermap_INF: "filtermap f (\<Sqinter>b\<in>B. F b) \<le> (\<Sqinter>b\<in>B. filtermap f (F b))"
by (rule INF_greatest, rule filtermap_mono, erule INF_lower)
-lemma frequently_cong:
- assumes ev: "eventually P F" and QR: "\<And>x. P x \<Longrightarrow> Q x \<longleftrightarrow> R x"
- shows "frequently Q F \<longleftrightarrow> frequently R F"
- unfolding frequently_def
- using QR by (auto intro!: eventually_cong [OF ev])
-
lemma frequently_filtermap:
"frequently P (filtermap f F) = frequently (\<lambda>x. P (f x)) F"
by (simp add: frequently_def eventually_filtermap)
--- a/src/HOL/Topological_Spaces.thy Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Topological_Spaces.thy Wed Feb 08 15:05:24 2023 +0000
@@ -1078,6 +1078,37 @@
lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
+lemma Lim_cong:
+ assumes "eventually (\<lambda>x. f x = g x) F" "F = G"
+ shows "Lim F f = Lim G g"
+proof (cases "(\<exists>c. (f \<longlongrightarrow> c) F) \<and> F \<noteq> bot")
+ case True
+ then obtain c where c: "(f \<longlongrightarrow> c) F"
+ by blast
+ hence "Lim F f = c"
+ using True by (intro tendsto_Lim) auto
+ moreover have "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) G"
+ using assms by (intro filterlim_cong) auto
+ with True c assms have "Lim G g = c"
+ by (intro tendsto_Lim) auto
+ ultimately show ?thesis
+ by simp
+next
+ case False
+ show ?thesis
+ proof (cases "F = bot")
+ case True
+ thus ?thesis using assms
+ by (auto simp: Topological_Spaces.Lim_def)
+ next
+ case False
+ have "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) G" for c
+ using assms by (intro filterlim_cong) auto
+ thus ?thesis
+ by (auto simp: Topological_Spaces.Lim_def)
+ qed
+qed
+
lemma eventually_Lim_ident_at:
"(\<forall>\<^sub>F y in at x within X. P (Lim (at x within X) (\<lambda>x. x)) y) \<longleftrightarrow>
(\<forall>\<^sub>F y in at x within X. P x y)" for x::"'a::t2_space"
@@ -2217,6 +2248,18 @@
"continuous_on A (f :: 'a :: discrete_topology \<Rightarrow> _)"
by (auto simp: continuous_on_def at_discrete)
+lemma continuous_on_of_nat [continuous_intros]:
+ assumes "continuous_on A f"
+ shows "continuous_on A (\<lambda>n. of_nat (f n))"
+ using continuous_on_compose[OF assms continuous_on_discrete[of _ of_nat]]
+ by (simp add: o_def)
+
+lemma continuous_on_of_int [continuous_intros]:
+ assumes "continuous_on A f"
+ shows "continuous_on A (\<lambda>n. of_int (f n))"
+ using continuous_on_compose[OF assms continuous_on_discrete[of _ of_int]]
+ by (simp add: o_def)
+
subsubsection \<open>Continuity at a point\<close>
definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
@@ -2330,6 +2373,21 @@
"isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
using continuous_at_imp_continuous_at_within continuous_within_compose2 by blast
+lemma at_within_isCont_imp_nhds:
+ fixes f:: "'a:: {t2_space,perfect_space} \<Rightarrow> 'b:: t2_space"
+ assumes "\<forall>\<^sub>F w in at z. f w = g w" "isCont f z" "isCont g z"
+ shows "\<forall>\<^sub>F w in nhds z. f w = g w"
+proof -
+ have "g \<midarrow>z\<rightarrow> f z"
+ using assms isContD tendsto_cong by blast
+ moreover have "g \<midarrow>z\<rightarrow> g z" using \<open>isCont g z\<close> using isCont_def by blast
+ ultimately have "f z=g z" using LIM_unique by auto
+ moreover have "\<forall>\<^sub>F x in nhds z. x \<noteq> z \<longrightarrow> f x = g x"
+ using assms unfolding eventually_at_filter by auto
+ ultimately show ?thesis
+ by (auto elim:eventually_mono)
+qed
+
lemma filtermap_nhds_open_map':
assumes cont: "isCont f a"
and "open A" "a \<in> A"
@@ -2933,6 +2991,30 @@
by auto
qed
+lemma connected_Un_UN:
+ assumes "connected A" "\<And>X. X \<in> B \<Longrightarrow> connected X" "\<And>X. X \<in> B \<Longrightarrow> A \<inter> X \<noteq> {}"
+ shows "connected (A \<union> \<Union>B)"
+proof (rule connectedI_const)
+ fix f :: "'a \<Rightarrow> bool"
+ assume f: "continuous_on (A \<union> \<Union>B) f"
+ have "connected A" "continuous_on A f"
+ by (auto intro: assms continuous_on_subset[OF f(1)])
+ from connectedD_const[OF this] obtain c where c: "\<And>x. x \<in> A \<Longrightarrow> f x = c"
+ by metis
+ have "f x = c" if "x \<in> X" "X \<in> B" for x X
+ proof -
+ have "connected X" "continuous_on X f"
+ using that by (auto intro: assms continuous_on_subset[OF f])
+ from connectedD_const[OF this] obtain c' where c': "\<And>x. x \<in> X \<Longrightarrow> f x = c'"
+ by metis
+ from assms(3) and that obtain y where "y \<in> A \<inter> X"
+ by auto
+ with c[of y] c'[of y] c'[of x] that show ?thesis
+ by auto
+ qed
+ with c show "\<exists>c. \<forall>x\<in>A \<union> \<Union> B. f x = c"
+ by (intro exI[of _ c]) auto
+qed
section \<open>Linear Continuum Topologies\<close>
@@ -3885,5 +3967,4 @@
then show ?thesis using open_subdiagonal closed_Diff by auto
qed
-
end