--- a/src/HOL/Analysis/Complex_Transcendental.thy Mon Apr 07 12:36:56 2025 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Apr 08 19:06:00 2025 +0100
@@ -2919,6 +2919,16 @@
qed (use z in auto)
qed
+lemma has_field_derivative_csqrt' [derivative_intros]:
+ assumes "(f has_field_derivative f') (at x within A)" "f x \<notin> \<real>\<^sub>\<le>\<^sub>0"
+ shows "((\<lambda>x. csqrt (f x)) has_field_derivative (f' / (2 * csqrt (f x)))) (at x within A)"
+proof -
+ have "((csqrt \<circ> f) has_field_derivative (inverse (2 * csqrt (f x)) * f')) (at x within A)"
+ using has_field_derivative_csqrt assms(1) by (rule DERIV_chain) fact
+ thus ?thesis
+ by (simp add: o_def field_simps)
+qed
+
lemma field_differentiable_at_csqrt:
"z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt field_differentiable at z"
using field_differentiable_def has_field_derivative_csqrt by blast
--- a/src/HOL/Analysis/Gamma_Function.thy Mon Apr 07 12:36:56 2025 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Tue Apr 08 19:06:00 2025 +0100
@@ -35,66 +35,6 @@
finally show ?thesis .
qed
-lemma plus_one_in_nonpos_Ints_imp: "z + 1 \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> z \<in> \<int>\<^sub>\<le>\<^sub>0"
- using nonpos_Ints_diff_Nats[of "z+1" "1"] by simp_all
-
-lemma of_int_in_nonpos_Ints_iff:
- "(of_int n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n \<le> 0"
- by (auto simp: nonpos_Ints_def)
-
-lemma one_plus_of_int_in_nonpos_Ints_iff:
- "(1 + of_int n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n \<le> -1"
-proof -
- have "1 + of_int n = (of_int (n + 1) :: 'a)" by simp
- also have "\<dots> \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n + 1 \<le> 0" by (subst of_int_in_nonpos_Ints_iff) simp_all
- also have "\<dots> \<longleftrightarrow> n \<le> -1" by presburger
- finally show ?thesis .
-qed
-
-lemma one_minus_of_nat_in_nonpos_Ints_iff:
- "(1 - of_nat n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n > 0"
-proof -
- have "(1 - of_nat n :: 'a) = of_int (1 - int n)" by simp
- also have "\<dots> \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n > 0" by (subst of_int_in_nonpos_Ints_iff) presburger
- finally show ?thesis .
-qed
-
-lemma fraction_not_in_ints:
- assumes "\<not>(n dvd m)" "n \<noteq> 0"
- shows "of_int m / of_int n \<notin> (\<int> :: 'a :: {division_ring,ring_char_0} set)"
-proof
- assume "of_int m / (of_int n :: 'a) \<in> \<int>"
- then obtain k where "of_int m / of_int n = (of_int k :: 'a)" by (elim Ints_cases)
- with assms have "of_int m = (of_int (k * n) :: 'a)" by (auto simp add: field_split_simps)
- hence "m = k * n" by (subst (asm) of_int_eq_iff)
- hence "n dvd m" by simp
- with assms(1) show False by contradiction
-qed
-
-lemma fraction_not_in_nats:
- assumes "\<not>n dvd m" "n \<noteq> 0"
- shows "of_int m / of_int n \<notin> (\<nat> :: 'a :: {division_ring,ring_char_0} set)"
-proof
- assume "of_int m / of_int n \<in> (\<nat> :: 'a set)"
- also note Nats_subset_Ints
- finally have "of_int m / of_int n \<in> (\<int> :: 'a set)" .
- moreover have "of_int m / of_int n \<notin> (\<int> :: 'a set)"
- using assms by (intro fraction_not_in_ints)
- ultimately show False by contradiction
-qed
-
-lemma not_in_Ints_imp_not_in_nonpos_Ints: "z \<notin> \<int> \<Longrightarrow> z \<notin> \<int>\<^sub>\<le>\<^sub>0"
- by (auto simp: Ints_def nonpos_Ints_def)
-
-lemma double_in_nonpos_Ints_imp:
- assumes "2 * (z :: 'a :: field_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0"
- shows "z \<in> \<int>\<^sub>\<le>\<^sub>0 \<or> z + 1/2 \<in> \<int>\<^sub>\<le>\<^sub>0"
-proof-
- from assms obtain k where k: "2 * z = - of_nat k" by (elim nonpos_Ints_cases')
- thus ?thesis by (cases "even k") (auto elim!: evenE oddE simp: field_simps)
-qed
-
-
lemma sin_series: "(\<lambda>n. ((-1)^n / fact (2*n+1)) *\<^sub>R z^(2*n+1)) sums sin z"
proof -
from sin_converges[of z] have "(\<lambda>n. sin_coeff n *\<^sub>R z^n) sums sin z" .
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Mon Apr 07 12:36:56 2025 +0200
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Tue Apr 08 19:06:00 2025 +0100
@@ -412,12 +412,88 @@
finally show ?case by simp
qed simp_all
+lemma higher_deriv_cmult':
+ assumes "f analytic_on {x}"
+ shows "(deriv ^^ j) (\<lambda>x. c * f x) x = c * (deriv ^^ j) f x"
+ using assms higher_deriv_cmult[of f _ x j c] assms
+ using analytic_at_two by blast
+
+lemma deriv_cmult':
+ assumes "f analytic_on {x}"
+ shows "deriv (\<lambda>x. c * f x) x = c * deriv f x"
+ using higher_deriv_cmult'[OF assms, of 1 c] by simp
+
+lemma analytic_derivI:
+ assumes "f analytic_on {z}"
+ shows "(f has_field_derivative (deriv f z)) (at z within A)"
+ using assms holomorphic_derivI[of f _ z] analytic_at by blast
+
+lemma deriv_compose_analytic:
+ fixes f g :: "complex \<Rightarrow> complex"
+ assumes "f analytic_on {g z}" "g analytic_on {z}"
+ shows "deriv (\<lambda>x. f (g x)) z = deriv f (g z) * deriv g z"
+proof -
+ have "((f \<circ> g) has_field_derivative (deriv f (g z) * deriv g z)) (at z)"
+ by (intro DERIV_chain analytic_derivI assms)
+ thus ?thesis
+ by (auto intro!: DERIV_imp_deriv simp add: o_def)
+qed
+
lemma valid_path_compose_holomorphic:
assumes "valid_path g" "f holomorphic_on S" and "open S" "path_image g \<subseteq> S"
shows "valid_path (f \<circ> g)"
by (meson assms holomorphic_deriv holomorphic_on_imp_continuous_on holomorphic_on_imp_differentiable_at
holomorphic_on_subset subsetD valid_path_compose)
+lemma valid_path_compose_analytic:
+ assumes "valid_path g" and holo:"f analytic_on S" and "path_image g \<subseteq> S"
+ shows "valid_path (f \<circ> g)"
+proof (rule valid_path_compose[OF \<open>valid_path g\<close>])
+ fix x assume "x \<in> path_image g"
+ then show "f field_differentiable at x"
+ using analytic_on_imp_differentiable_at analytic_on_open assms holo by blast
+next
+ show "continuous_on (path_image g) (deriv f)"
+ by (intro holomorphic_on_imp_continuous_on analytic_imp_holomorphic analytic_intros
+ analytic_on_subset[OF holo] assms)
+qed
+
+lemma analytic_on_deriv [analytic_intros]:
+ assumes "f analytic_on g ` A"
+ assumes "g analytic_on A"
+ shows "(\<lambda>x. deriv f (g x)) analytic_on A"
+proof -
+ have "(deriv f \<circ> g) analytic_on A"
+ by (rule analytic_on_compose_gen[OF assms(2) analytic_deriv[OF assms(1)]]) auto
+ thus ?thesis
+ by (simp add: o_def)
+qed
+
+lemma contour_integral_comp_analyticW:
+ assumes "f analytic_on s" "valid_path \<gamma>" "path_image \<gamma> \<subseteq> s"
+ shows "contour_integral (f \<circ> \<gamma>) g = contour_integral \<gamma> (\<lambda>w. deriv f w * g (f w))"
+proof -
+ obtain spikes where "finite spikes" and \<gamma>_diff: "\<gamma> C1_differentiable_on {0..1} - spikes"
+ using \<open>valid_path \<gamma>\<close> unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
+ show "contour_integral (f \<circ> \<gamma>) g
+ = contour_integral \<gamma> (\<lambda>w. deriv f w * g (f w))"
+ unfolding contour_integral_integral
+ proof (rule integral_spike[rule_format,OF negligible_finite[OF \<open>finite spikes\<close>]])
+ fix t::real assume t:"t \<in> {0..1} - spikes"
+ then have "\<gamma> differentiable at t"
+ using \<gamma>_diff unfolding C1_differentiable_on_eq by auto
+ moreover have "f field_differentiable at (\<gamma> t)"
+ proof -
+ have "\<gamma> t \<in> s" using t assms unfolding path_image_def by auto
+ thus ?thesis
+ using \<open>f analytic_on s\<close> analytic_on_imp_differentiable_at by blast
+ qed
+ ultimately show "deriv f (\<gamma> t) * g (f (\<gamma> t)) * vector_derivative \<gamma> (at t) =
+ g ((f \<circ> \<gamma>) t) * vector_derivative (f \<circ> \<gamma>) (at t)"
+ by (subst vector_derivative_chain_at_general) (simp_all add:field_simps)
+ qed
+qed
+
subsection\<open>Morera's theorem\<close>
lemma Morera_local_triangle_ball:
--- a/src/HOL/Complex_Analysis/Meromorphic.thy Mon Apr 07 12:36:56 2025 +0200
+++ b/src/HOL/Complex_Analysis/Meromorphic.thy Tue Apr 08 19:06:00 2025 +0100
@@ -618,6 +618,11 @@
by (auto simp: isCont_def)
qed
+lemma analytic_on_imp_nicely_meromorphic_on:
+ "f analytic_on A \<Longrightarrow> f nicely_meromorphic_on A"
+ by (meson analytic_at_imp_isCont analytic_on_analytic_at
+ analytic_on_imp_meromorphic_on isContD nicely_meromorphic_on_def)
+
lemma remove_sings_meromorphic [meromorphic_intros]:
assumes "f meromorphic_on A"
shows "remove_sings f meromorphic_on A"
--- a/src/HOL/Library/Nonpos_Ints.thy Mon Apr 07 12:36:56 2025 +0200
+++ b/src/HOL/Library/Nonpos_Ints.thy Tue Apr 08 19:06:00 2025 +0100
@@ -305,4 +305,101 @@
lemma ii_not_nonpos_Reals [iff]: "\<i> \<notin> \<real>\<^sub>\<le>\<^sub>0"
by (simp add: complex_nonpos_Reals_iff)
+lemma plus_one_in_nonpos_Ints_imp: "z + 1 \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> z \<in> \<int>\<^sub>\<le>\<^sub>0"
+ using nonpos_Ints_diff_Nats[of "z+1" "1"] by simp_all
+
+lemma of_int_in_nonpos_Ints_iff:
+ "(of_int n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n \<le> 0"
+ by (auto simp: nonpos_Ints_def)
+
+lemma one_plus_of_int_in_nonpos_Ints_iff:
+ "(1 + of_int n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n \<le> -1"
+proof -
+ have "1 + of_int n = (of_int (n + 1) :: 'a)" by simp
+ also have "\<dots> \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n + 1 \<le> 0" by (subst of_int_in_nonpos_Ints_iff) simp_all
+ also have "\<dots> \<longleftrightarrow> n \<le> -1" by presburger
+ finally show ?thesis .
+qed
+
+lemma one_minus_of_nat_in_nonpos_Ints_iff:
+ "(1 - of_nat n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n > 0"
+proof -
+ have "(1 - of_nat n :: 'a) = of_int (1 - int n)" by simp
+ also have "\<dots> \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n > 0" by (subst of_int_in_nonpos_Ints_iff) presburger
+ finally show ?thesis .
+qed
+
+lemma fraction_not_in_ints:
+ assumes "\<not>(n dvd m)" "n \<noteq> 0"
+ shows "of_int m / of_int n \<notin> (\<int> :: 'a :: {division_ring,ring_char_0} set)"
+proof
+ assume "of_int m / (of_int n :: 'a) \<in> \<int>"
+ then obtain k where "of_int m / of_int n = (of_int k :: 'a)" by (elim Ints_cases)
+ with assms have "of_int m = (of_int (k * n) :: 'a)" by (auto simp add: field_split_simps)
+ hence "m = k * n" by (subst (asm) of_int_eq_iff)
+ hence "n dvd m" by simp
+ with assms(1) show False by contradiction
+qed
+
+lemma fraction_not_in_nats:
+ assumes "\<not>n dvd m" "n \<noteq> 0"
+ shows "of_int m / of_int n \<notin> (\<nat> :: 'a :: {division_ring,ring_char_0} set)"
+proof
+ assume "of_int m / of_int n \<in> (\<nat> :: 'a set)"
+ also note Nats_subset_Ints
+ finally have "of_int m / of_int n \<in> (\<int> :: 'a set)" .
+ moreover have "of_int m / of_int n \<notin> (\<int> :: 'a set)"
+ using assms by (intro fraction_not_in_ints)
+ ultimately show False by contradiction
+qed
+
+lemma not_in_Ints_imp_not_in_nonpos_Ints: "z \<notin> \<int> \<Longrightarrow> z \<notin> \<int>\<^sub>\<le>\<^sub>0"
+ by (auto simp: Ints_def nonpos_Ints_def)
+
+lemma double_in_nonpos_Ints_imp:
+ assumes "2 * (z :: 'a :: field_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0"
+ shows "z \<in> \<int>\<^sub>\<le>\<^sub>0 \<or> z + 1/2 \<in> \<int>\<^sub>\<le>\<^sub>0"
+proof-
+ from assms obtain k where k: "2 * z = - of_nat k" by (elim nonpos_Ints_cases')
+ thus ?thesis by (cases "even k") (auto elim!: evenE oddE simp: field_simps)
+qed
+
+lemma fraction_numeral_Ints_iff [simp]:
+ "numeral a / numeral b \<in> (\<int> :: 'a :: {division_ring, ring_char_0} set)
+ \<longleftrightarrow> (numeral b :: int) dvd numeral a" (is "?L=?R")
+proof
+ show "?L \<Longrightarrow> ?R"
+ by (metis fraction_not_in_ints of_int_numeral zero_neq_numeral)
+ assume ?R
+ then obtain k::int where "numeral a = numeral b * (of_int k :: 'a)"
+ unfolding dvd_def by (metis of_int_mult of_int_numeral)
+ then show ?L
+ by (metis Ints_of_int divide_eq_eq mult.commute of_int_mult of_int_numeral)
+qed
+
+lemma fraction_numeral_Ints_iff1 [simp]:
+ "1 / numeral b \<in> (\<int> :: 'a :: {division_ring, ring_char_0} set)
+ \<longleftrightarrow> b = Num.One" (is "?L=?R")
+ using fraction_numeral_Ints_iff [of Num.One, where 'a='a] by simp
+
+lemma fraction_numeral_Nats_iff [simp]:
+ "numeral a / numeral b \<in> (\<nat> :: 'a :: {division_ring, ring_char_0} set)
+ \<longleftrightarrow> (numeral b :: int) dvd numeral a" (is "?L=?R")
+proof
+ show "?L \<Longrightarrow> ?R"
+ using Nats_subset_Ints fraction_numeral_Ints_iff by blast
+ assume ?R
+ then obtain k::nat where "numeral a = numeral b * (of_nat k :: 'a)"
+ unfolding dvd_def
+ by (metis dvd_def int_dvd_int_iff of_nat_mult of_nat_numeral)
+ then show ?L
+ by (metis mult_of_nat_commute nonzero_divide_eq_eq of_nat_in_Nats
+ zero_neq_numeral)
+qed
+
+lemma fraction_numeral_Nats_iff1 [simp]:
+ "1 / numeral b \<in> (\<nat> :: 'a :: {division_ring, ring_char_0} set)
+ \<longleftrightarrow> b = Num.One" (is "?L=?R")
+ using fraction_numeral_Nats_iff [of Num.One, where 'a='a] by simp
+
end