--- a/src/HOL/Analysis/Derivative.thy Mon Jan 30 16:10:52 2017 +0100
+++ b/src/HOL/Analysis/Derivative.thy Tue Jan 31 15:52:47 2017 +0100
@@ -2412,6 +2412,15 @@
shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff)
+lemma deriv_cong_ev:
+ assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
+ shows "deriv f x = deriv g y"
+proof -
+ have "(\<lambda>D. (f has_field_derivative D) (at x)) = (\<lambda>D. (g has_field_derivative D) (at y))"
+ by (intro ext DERIV_cong_ev refl assms)
+ thus ?thesis by (simp add: deriv_def assms)
+qed
+
lemma real_derivative_chain:
fixes x :: real
shows "f differentiable at x \<Longrightarrow> g differentiable at (f x)
--- a/src/HOL/Analysis/Gamma_Function.thy Mon Jan 30 16:10:52 2017 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Tue Jan 31 15:52:47 2017 +0100
@@ -6,7 +6,7 @@
theory Gamma_Function
imports
- Complex_Transcendental
+ Cauchy_Integral_Theorem
Summation_Tests
Harmonic_Numbers
"~~/src/HOL/Library/Nonpos_Ints"
@@ -977,6 +977,40 @@
shows "A \<inter> \<real>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> continuous_on A ln_Gamma"
by (intro continuous_at_imp_continuous_on ballI isCont_ln_Gamma_complex[OF continuous_ident])
fastforce
+
+lemma deriv_Polygamma:
+ assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0"
+ shows "deriv (Polygamma m) z =
+ Polygamma (Suc m) (z :: 'a :: {real_normed_field,euclidean_space})"
+ by (intro DERIV_imp_deriv has_field_derivative_Polygamma assms)
+ thm has_field_derivative_Polygamma
+
+lemma higher_deriv_Polygamma:
+ assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0"
+ shows "(deriv ^^ n) (Polygamma m) z =
+ Polygamma (m + n) (z :: 'a :: {real_normed_field,euclidean_space})"
+proof -
+ have "eventually (\<lambda>u. (deriv ^^ n) (Polygamma m) u = Polygamma (m + n) u) (nhds z)"
+ proof (induction n)
+ case (Suc n)
+ from Suc.IH have "eventually (\<lambda>z. eventually (\<lambda>u. (deriv ^^ n) (Polygamma m) u = Polygamma (m + n) u) (nhds z)) (nhds z)"
+ by (simp add: eventually_eventually)
+ hence "eventually (\<lambda>z. deriv ((deriv ^^ n) (Polygamma m)) z =
+ deriv (Polygamma (m + n)) z) (nhds z)"
+ by eventually_elim (intro deriv_cong_ev refl)
+ moreover have "eventually (\<lambda>z. z \<in> UNIV - \<int>\<^sub>\<le>\<^sub>0) (nhds z)" using assms
+ by (intro eventually_nhds_in_open open_Diff open_UNIV) auto
+ ultimately show ?case by eventually_elim (simp_all add: deriv_Polygamma)
+ qed simp_all
+ thus ?thesis by (rule eventually_nhds_x_imp_x)
+qed
+
+lemma deriv_ln_Gamma_complex:
+ assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
+ shows "deriv ln_Gamma z = Digamma (z :: complex)"
+ by (intro DERIV_imp_deriv has_field_derivative_ln_Gamma_complex assms)
+
+
text \<open>
We define a type class that captures all the fundamental properties of the inverse of the Gamma function
@@ -1428,22 +1462,36 @@
lemma field_differentiable_rGamma: "rGamma field_differentiable (at z within A)"
using has_field_derivative_rGamma[of z] unfolding field_differentiable_def by blast
-lemma holomorphic_on_rGamma: "rGamma holomorphic_on A"
+lemma holomorphic_rGamma [holomorphic_intros]: "rGamma holomorphic_on A"
unfolding holomorphic_on_def by (auto intro!: field_differentiable_rGamma)
-lemma analytic_on_rGamma: "rGamma analytic_on A"
- unfolding analytic_on_def by (auto intro!: exI[of _ 1] holomorphic_on_rGamma)
+lemma analytic_rGamma: "rGamma analytic_on A"
+ unfolding analytic_on_def by (auto intro!: exI[of _ 1] holomorphic_rGamma)
lemma field_differentiable_Gamma: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma field_differentiable (at z within A)"
using has_field_derivative_Gamma[of z] unfolding field_differentiable_def by auto
-lemma holomorphic_on_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma holomorphic_on A"
+lemma holomorphic_Gamma [holomorphic_intros]: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma holomorphic_on A"
unfolding holomorphic_on_def by (auto intro!: field_differentiable_Gamma)
-lemma analytic_on_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma analytic_on A"
+lemma analytic_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma analytic_on A"
by (rule analytic_on_subset[of _ "UNIV - \<int>\<^sub>\<le>\<^sub>0"], subst analytic_on_open)
- (auto intro!: holomorphic_on_Gamma)
+ (auto intro!: holomorphic_Gamma)
+
+
+lemma field_differentiable_ln_Gamma_complex:
+ "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln_Gamma field_differentiable (at (z::complex) within A)"
+ by (rule field_differentiable_within_subset[of _ _ UNIV])
+ (force simp: field_differentiable_def intro!: derivative_intros)+
+
+lemma holomorphic_ln_Gamma [holomorphic_intros]: "A \<inter> \<real>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> ln_Gamma holomorphic_on A"
+ unfolding holomorphic_on_def by (auto intro!: field_differentiable_ln_Gamma_complex)
+
+lemma analytic_ln_Gamma: "A \<inter> \<real>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> ln_Gamma analytic_on A"
+ by (rule analytic_on_subset[of _ "UNIV - \<real>\<^sub>\<le>\<^sub>0"], subst analytic_on_open)
+ (auto intro!: holomorphic_ln_Gamma)
+
lemma has_field_derivative_rGamma_complex' [derivative_intros]:
"(rGamma has_field_derivative (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>-Re z\<rfloor>) * fact (nat \<lfloor>-Re z\<rfloor>) else
@@ -1454,12 +1502,12 @@
lemma field_differentiable_Polygamma:
- fixes z::complex
+ fixes z :: complex
shows
"z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Polygamma n field_differentiable (at z within A)"
using has_field_derivative_Polygamma[of z n] unfolding field_differentiable_def by auto
-lemma holomorphic_on_Polygamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Polygamma n holomorphic_on A"
+lemma holomorphic_on_Polygamma [holomorphic_intros]: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Polygamma n holomorphic_on A"
unfolding holomorphic_on_def by (auto intro!: field_differentiable_Polygamma)
lemma analytic_on_Polygamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Polygamma n analytic_on A"
@@ -1598,6 +1646,14 @@
lemma ln_Gamma_real_pos: "x > 0 \<Longrightarrow> ln_Gamma x = ln (Gamma x :: real)"
unfolding Gamma_real_pos_exp by simp
+lemma ln_Gamma_complex_conv_fact: "n > 0 \<Longrightarrow> ln_Gamma (of_nat n :: complex) = ln (fact (n - 1))"
+ using ln_Gamma_complex_of_real[of "real n"] Gamma_fact[of "n - 1", where 'a = real]
+ by (simp add: ln_Gamma_real_pos of_nat_diff Ln_of_real [symmetric])
+
+lemma ln_Gamma_real_conv_fact: "n > 0 \<Longrightarrow> ln_Gamma (real n) = ln (fact (n - 1))"
+ using Gamma_fact[of "n - 1", where 'a = real]
+ by (simp add: ln_Gamma_real_pos of_nat_diff Ln_of_real [symmetric])
+
lemma Gamma_real_pos: "x > (0::real) \<Longrightarrow> Gamma x > 0"
by (simp add: Gamma_real_pos_exp)
@@ -1612,8 +1668,18 @@
show "eventually (\<lambda>y. ln_Gamma y = (Re \<circ> ln_Gamma \<circ> of_real) y) (nhds x)"
by (auto elim!: eventually_mono simp: ln_Gamma_complex_of_real interior_open)
qed
+
+lemma field_differentiable_ln_Gamma_real:
+ "x > 0 \<Longrightarrow> ln_Gamma field_differentiable (at (x::real) within A)"
+ by (rule field_differentiable_within_subset[of _ _ UNIV])
+ (auto simp: field_differentiable_def intro!: derivative_intros)+
declare has_field_derivative_ln_Gamma_real[THEN DERIV_chain2, derivative_intros]
+
+lemma deriv_ln_Gamma_real:
+ assumes "z > 0"
+ shows "deriv ln_Gamma z = Digamma (z :: real)"
+ by (intro DERIV_imp_deriv has_field_derivative_ln_Gamma_real assms)
lemma has_field_derivative_rGamma_real' [derivative_intros]:
@@ -1985,203 +2051,6 @@
by (simp add: divide_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps)
qed
-(* TODO: perhaps this is unnecessary once we have the fact that a holomorphic function is
- infinitely differentiable *)
-private lemma Gamma_reflection_aux:
- defines "h \<equiv> \<lambda>z::complex. if z \<in> \<int> then 0 else
- (of_real pi * cot (of_real pi*z) + Digamma z - Digamma (1 - z))"
- defines "a \<equiv> complex_of_real pi"
- obtains h' where "continuous_on UNIV h'" "\<And>z. (h has_field_derivative (h' z)) (at z)"
-proof -
- define f where "f n = a * of_real (cos_coeff (n+1) - sin_coeff (n+2))" for n
- define F where "F z = (if z = 0 then 0 else (cos (a*z) - sin (a*z)/(a*z)) / z)" for z
- define g where "g n = complex_of_real (sin_coeff (n+1))" for n
- define G where "G z = (if z = 0 then 1 else sin (a*z)/(a*z))" for z
- have a_nz: "a \<noteq> 0" unfolding a_def by simp
-
- have "(\<lambda>n. f n * (a*z)^n) sums (F z) \<and> (\<lambda>n. g n * (a*z)^n) sums (G z)"
- if "abs (Re z) < 1" for z
- proof (cases "z = 0"; rule conjI)
- assume "z \<noteq> 0"
- note z = this that
-
- from z have sin_nz: "sin (a*z) \<noteq> 0" unfolding a_def by (auto simp: sin_eq_0)
- have "(\<lambda>n. of_real (sin_coeff n) * (a*z)^n) sums (sin (a*z))" using sin_converges[of "a*z"]
- by (simp add: scaleR_conv_of_real)
- from sums_split_initial_segment[OF this, of 1]
- have "(\<lambda>n. (a*z) * of_real (sin_coeff (n+1)) * (a*z)^n) sums (sin (a*z))" by (simp add: mult_ac)
- from sums_mult[OF this, of "inverse (a*z)"] z a_nz
- have A: "(\<lambda>n. g n * (a*z)^n) sums (sin (a*z)/(a*z))"
- by (simp add: field_simps g_def)
- with z show "(\<lambda>n. g n * (a*z)^n) sums (G z)" by (simp add: G_def)
- from A z a_nz sin_nz have g_nz: "(\<Sum>n. g n * (a*z)^n) \<noteq> 0" by (simp add: sums_iff g_def)
-
- have [simp]: "sin_coeff (Suc 0) = 1" by (simp add: sin_coeff_def)
- from sums_split_initial_segment[OF sums_diff[OF cos_converges[of "a*z"] A], of 1]
- have "(\<lambda>n. z * f n * (a*z)^n) sums (cos (a*z) - sin (a*z) / (a*z))"
- by (simp add: mult_ac scaleR_conv_of_real ring_distribs f_def g_def)
- from sums_mult[OF this, of "inverse z"] z assms
- show "(\<lambda>n. f n * (a*z)^n) sums (F z)" by (simp add: divide_simps mult_ac f_def F_def)
- next
- assume z: "z = 0"
- have "(\<lambda>n. f n * (a * z) ^ n) sums f 0" using powser_sums_zero[of f] z by simp
- with z show "(\<lambda>n. f n * (a * z) ^ n) sums (F z)"
- by (simp add: f_def F_def sin_coeff_def cos_coeff_def)
- have "(\<lambda>n. g n * (a * z) ^ n) sums g 0" using powser_sums_zero[of g] z by simp
- with z show "(\<lambda>n. g n * (a * z) ^ n) sums (G z)"
- by (simp add: g_def G_def sin_coeff_def cos_coeff_def)
- qed
- note sums = conjunct1[OF this] conjunct2[OF this]
-
- define h2 where [abs_def]:
- "h2 z = (\<Sum>n. f n * (a*z)^n) / (\<Sum>n. g n * (a*z)^n) + Digamma (1 + z) - Digamma (1 - z)" for z
- define POWSER where [abs_def]: "POWSER f z = (\<Sum>n. f n * (z^n :: complex))" for f z
- define POWSER' where [abs_def]: "POWSER' f z = (\<Sum>n. diffs f n * (z^n))" for f and z :: complex
- define h2' where [abs_def]:
- "h2' z = a * (POWSER g (a*z) * POWSER' f (a*z) - POWSER f (a*z) * POWSER' g (a*z)) /
- (POWSER g (a*z))^2 + Polygamma 1 (1 + z) + Polygamma 1 (1 - z)" for z
-
- have h_eq: "h t = h2 t" if "abs (Re t) < 1" for t
- proof -
- from that have t: "t \<in> \<int> \<longleftrightarrow> t = 0" by (auto elim!: Ints_cases simp: dist_0_norm)
- hence "h t = a*cot (a*t) - 1/t + Digamma (1 + t) - Digamma (1 - t)"
- unfolding h_def using Digamma_plus1[of t] by (force simp: field_simps a_def)
- also have "a*cot (a*t) - 1/t = (F t) / (G t)"
- using t by (auto simp add: divide_simps sin_eq_0 cot_def a_def F_def G_def)
- also have "\<dots> = (\<Sum>n. f n * (a*t)^n) / (\<Sum>n. g n * (a*t)^n)"
- using sums[of t] that by (simp add: sums_iff dist_0_norm)
- finally show "h t = h2 t" by (simp only: h2_def)
- qed
-
- let ?A = "{z. abs (Re z) < 1}"
- have "open ({z. Re z < 1} \<inter> {z. Re z > -1})"
- using open_halfspace_Re_gt open_halfspace_Re_lt by auto
- also have "({z. Re z < 1} \<inter> {z. Re z > -1}) = {z. abs (Re z) < 1}" by auto
- finally have open_A: "open ?A" .
- hence [simp]: "interior ?A = ?A" by (simp add: interior_open)
-
- have summable_f: "summable (\<lambda>n. f n * z^n)" for z
- by (rule powser_inside, rule sums_summable, rule sums[of "\<i> * of_real (norm z + 1) / a"])
- (simp_all add: norm_mult a_def del: of_real_add)
- have summable_g: "summable (\<lambda>n. g n * z^n)" for z
- by (rule powser_inside, rule sums_summable, rule sums[of "\<i> * of_real (norm z + 1) / a"])
- (simp_all add: norm_mult a_def del: of_real_add)
- have summable_fg': "summable (\<lambda>n. diffs f n * z^n)" "summable (\<lambda>n. diffs g n * z^n)" for z
- by (intro termdiff_converges_all summable_f summable_g)+
- have "(POWSER f has_field_derivative (POWSER' f z)) (at z)"
- "(POWSER g has_field_derivative (POWSER' g z)) (at z)" for z
- unfolding POWSER_def POWSER'_def
- by (intro termdiffs_strong_converges_everywhere summable_f summable_g)+
- note derivs = this[THEN DERIV_chain2[OF _ DERIV_cmult[OF DERIV_ident]], unfolded POWSER_def]
- have "isCont (POWSER f) z" "isCont (POWSER g) z" "isCont (POWSER' f) z" "isCont (POWSER' g) z"
- for z unfolding POWSER_def POWSER'_def
- by (intro isCont_powser_converges_everywhere summable_f summable_g summable_fg')+
- note cont = this[THEN isCont_o2[rotated], unfolded POWSER_def POWSER'_def]
-
- {
- fix z :: complex assume z: "abs (Re z) < 1"
- define d where "d = \<i> * of_real (norm z + 1)"
- have d: "abs (Re d) < 1" "norm z < norm d" by (simp_all add: d_def norm_mult del: of_real_add)
- have "eventually (\<lambda>z. h z = h2 z) (nhds z)"
- using eventually_nhds_in_nhd[of z ?A] using h_eq z
- by (auto elim!: eventually_mono simp: dist_0_norm)
-
- moreover from sums(2)[OF z] z have nz: "(\<Sum>n. g n * (a * z) ^ n) \<noteq> 0"
- unfolding G_def by (auto simp: sums_iff sin_eq_0 a_def)
- have A: "z \<in> \<int> \<longleftrightarrow> z = 0" using z by (auto elim!: Ints_cases)
- have no_int: "1 + z \<in> \<int> \<longleftrightarrow> z = 0" using z Ints_diff[of "1+z" 1] A
- by (auto elim!: nonpos_Ints_cases)
- have no_int': "1 - z \<in> \<int> \<longleftrightarrow> z = 0" using z Ints_diff[of 1 "1-z"] A
- by (auto elim!: nonpos_Ints_cases)
- from no_int no_int' have no_int: "1 - z \<notin> \<int>\<^sub>\<le>\<^sub>0" "1 + z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
- have "(h2 has_field_derivative h2' z) (at z)" unfolding h2_def
- by (rule DERIV_cong, (rule derivative_intros refl derivs[unfolded POWSER_def] nz no_int)+)
- (auto simp: h2'_def POWSER_def field_simps power2_eq_square)
- ultimately have deriv: "(h has_field_derivative h2' z) (at z)"
- by (subst DERIV_cong_ev[OF refl _ refl])
-
- from sums(2)[OF z] z have "(\<Sum>n. g n * (a * z) ^ n) \<noteq> 0"
- unfolding G_def by (auto simp: sums_iff a_def sin_eq_0)
- hence "isCont h2' z" using no_int unfolding h2'_def[abs_def] POWSER_def POWSER'_def
- by (intro continuous_intros cont
- continuous_on_compose2[OF _ continuous_on_Polygamma[of "{z. Re z > 0}"]]) auto
- note deriv and this
- } note A = this
-
- interpret h: periodic_fun_simple' h
- proof
- fix z :: complex
- show "h (z + 1) = h z"
- proof (cases "z \<in> \<int>")
- assume z: "z \<notin> \<int>"
- hence A: "z + 1 \<notin> \<int>" "z \<noteq> 0" using Ints_diff[of "z+1" 1] by auto
- hence "Digamma (z + 1) - Digamma (-z) = Digamma z - Digamma (-z + 1)"
- by (subst (1 2) Digamma_plus1) simp_all
- with A z show "h (z + 1) = h z"
- by (simp add: h_def sin_plus_pi cos_plus_pi ring_distribs cot_def)
- qed (simp add: h_def)
- qed
-
- have h2'_eq: "h2' (z - 1) = h2' z" if z: "Re z > 0" "Re z < 1" for z
- proof -
- have "((\<lambda>z. h (z - 1)) has_field_derivative h2' (z - 1)) (at z)"
- by (rule DERIV_cong, rule DERIV_chain'[OF _ A(1)])
- (insert z, auto intro!: derivative_eq_intros)
- hence "(h has_field_derivative h2' (z - 1)) (at z)" by (subst (asm) h.minus_1)
- moreover from z have "(h has_field_derivative h2' z) (at z)" by (intro A) simp_all
- ultimately show "h2' (z - 1) = h2' z" by (rule DERIV_unique)
- qed
-
- define h2'' where "h2'' z = h2' (z - of_int \<lfloor>Re z\<rfloor>)" for z
- have deriv: "(h has_field_derivative h2'' z) (at z)" for z
- proof -
- fix z :: complex
- have B: "\<bar>Re z - real_of_int \<lfloor>Re z\<rfloor>\<bar> < 1" by linarith
- have "((\<lambda>t. h (t - of_int \<lfloor>Re z\<rfloor>)) has_field_derivative h2'' z) (at z)"
- unfolding h2''_def by (rule DERIV_cong, rule DERIV_chain'[OF _ A(1)])
- (insert B, auto intro!: derivative_intros)
- thus "(h has_field_derivative h2'' z) (at z)" by (simp add: h.minus_of_int)
- qed
-
- have cont: "continuous_on UNIV h2''"
- proof (intro continuous_at_imp_continuous_on ballI)
- fix z :: complex
- define r where "r = \<lfloor>Re z\<rfloor>"
- define A where "A = {t. of_int r - 1 < Re t \<and> Re t < of_int r + 1}"
- have "continuous_on A (\<lambda>t. h2' (t - of_int r))" unfolding A_def
- by (intro continuous_at_imp_continuous_on isCont_o2[OF _ A(2)] ballI continuous_intros)
- (simp_all add: abs_real_def)
- moreover have "h2'' t = h2' (t - of_int r)" if t: "t \<in> A" for t
- proof (cases "Re t \<ge> of_int r")
- case True
- from t have "of_int r - 1 < Re t" "Re t < of_int r + 1" by (simp_all add: A_def)
- with True have "\<lfloor>Re t\<rfloor> = \<lfloor>Re z\<rfloor>" unfolding r_def by linarith
- thus ?thesis by (auto simp: r_def h2''_def)
- next
- case False
- from t have t: "of_int r - 1 < Re t" "Re t < of_int r + 1" by (simp_all add: A_def)
- with False have t': "\<lfloor>Re t\<rfloor> = \<lfloor>Re z\<rfloor> - 1" unfolding r_def by linarith
- moreover from t False have "h2' (t - of_int r + 1 - 1) = h2' (t - of_int r + 1)"
- by (intro h2'_eq) simp_all
- ultimately show ?thesis by (auto simp: r_def h2''_def algebra_simps t')
- qed
- ultimately have "continuous_on A h2''" by (subst continuous_on_cong[OF refl])
- moreover {
- have "open ({t. of_int r - 1 < Re t} \<inter> {t. of_int r + 1 > Re t})"
- by (intro open_Int open_halfspace_Re_gt open_halfspace_Re_lt)
- also have "{t. of_int r - 1 < Re t} \<inter> {t. of_int r + 1 > Re t} = A"
- unfolding A_def by blast
- finally have "open A" .
- }
- ultimately have C: "isCont h2'' t" if "t \<in> A" for t using that
- by (subst (asm) continuous_on_eq_continuous_at) auto
- have "of_int r - 1 < Re z" "Re z < of_int r + 1" unfolding r_def by linarith+
- thus "isCont h2'' z" by (intro C) (simp_all add: A_def)
- qed
-
- from that[OF cont deriv] show ?thesis .
-qed
-
lemma Gamma_reflection_complex:
fixes z :: complex
shows "Gamma z * Gamma (1 - z) = of_real pi / sin (of_real pi * z)"
@@ -2212,7 +2081,7 @@
qed
\<comment> \<open>@{term g} is entire.\<close>
- have g_g': "(g has_field_derivative (h z * g z)) (at z)" for z :: complex
+ have g_g' [derivative_intros]: "(g has_field_derivative (h z * g z)) (at z)" for z :: complex
proof (cases "z \<in> \<int>")
let ?h' = "\<lambda>z. Beta z (1 - z) * ((Digamma z - Digamma (1 - z)) * sin (z * of_real pi) +
of_real pi * cos (z * of_real pi))"
@@ -2260,6 +2129,10 @@
also have "g \<circ> (\<lambda>x. x - of_int n) = g" by (intro ext) (simp add: g.minus_of_int)
finally show "(g has_field_derivative (h z * g z)) (at z)" by (simp add: z h_def)
qed
+
+ have g_holo [holomorphic_intros]: "g holomorphic_on A" for A
+ by (rule holomorphic_on_subset[of _ UNIV])
+ (force simp: holomorphic_on_open intro!: derivative_intros)+
have g_eq: "g (z/2) * g ((z+1)/2) = Gamma (1/2)^2 * g z" if "Re z > -1" "Re z < 2" for z
proof (cases "z \<in> \<int>")
@@ -2320,7 +2193,10 @@
have g_nz [simp]: "g z \<noteq> 0" for z :: complex
unfolding g_def using Ints_diff[of 1 "1 - z"]
by (auto simp: Gamma_eq_zero_iff sin_eq_0 dest!: nonpos_Ints_Int)
-
+
+ have h_altdef: "h z = deriv g z / g z" for z :: complex
+ using DERIV_imp_deriv[OF g_g', of z] by simp
+
have h_eq: "h z = (h (z/2) + h ((z+1)/2)) / 2" for z
proof -
have "((\<lambda>t. g (t/2) * g ((t+1)/2)) has_field_derivative
@@ -2340,9 +2216,16 @@
thus "h z = (h (z/2) + h ((z+1)/2)) / 2" by simp
qed
- obtain h' where h'_cont: "continuous_on UNIV h'" and
- h_h': "\<And>z. (h has_field_derivative h' z) (at z)"
- unfolding h_def by (erule Gamma_reflection_aux)
+ have h_holo [holomorphic_intros]: "h holomorphic_on A" for A
+ unfolding h_altdef [abs_def]
+ by (rule holomorphic_on_subset[of _ UNIV]) (auto intro!: holomorphic_intros)
+ define h' where "h' = deriv h"
+ have h_h': "(h has_field_derivative h' z) (at z)" for z unfolding h'_def
+ by (auto intro!: holomorphic_derivI[of _ UNIV] holomorphic_intros)
+ have h'_holo [holomorphic_intros]: "h' holomorphic_on A" for A unfolding h'_def
+ by (rule holomorphic_on_subset[of _ UNIV]) (auto intro!: holomorphic_intros)
+ have h'_cont: "continuous_on UNIV h'"
+ by (intro holomorphic_on_imp_continuous_on holomorphic_intros)
have h'_eq: "h' z = (h' (z/2) + h' ((z+1)/2)) / 4" for z
proof -
@@ -2410,15 +2293,12 @@
unfolding g_def using that by (auto intro!: Reals_mult Gamma_complex_real)
have h_real: "h z \<in> \<real>" if "z \<in> \<real>" for z
unfolding h_def using that by (auto intro!: Reals_mult Reals_add Reals_diff Polygamma_Real)
- have g_nz: "g z \<noteq> 0" for z unfolding g_def using Ints_diff[of 1 "1-z"]
- by (auto simp: Gamma_eq_zero_iff sin_eq_0)
from h'_zero h_h'_2 have "\<exists>c. \<forall>z\<in>UNIV. h z = c"
by (intro has_field_derivative_zero_constant) (simp_all add: dist_0_norm)
then obtain c where c: "\<And>z. h z = c" by auto
have "\<exists>u. u \<in> closed_segment 0 1 \<and> Re (g 1) - Re (g 0) = Re (h u * g u * (1 - 0))"
by (intro complex_mvt_line g_g')
- find_theorems name:deriv Reals
then guess u by (elim exE conjE) note u = this
from u(1) have u': "u \<in> \<real>" unfolding closed_segment_def
by (auto simp: scaleR_conv_of_real)
--- a/src/HOL/Topological_Spaces.thy Mon Jan 30 16:10:52 2017 +0100
+++ b/src/HOL/Topological_Spaces.thy Tue Jan 31 15:52:47 2017 +0100
@@ -468,6 +468,10 @@
"eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)
+lemma eventually_eventually:
+ "eventually (\<lambda>y. eventually P (nhds y)) (nhds x) = eventually P (nhds x)"
+ by (auto simp: eventually_nhds)
+
lemma (in topological_space) eventually_nhds_in_open:
"open s \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
by (subst eventually_nhds) blast