Theory Incomplete_Gamma_Lemma_Bucket
section ‹Auxiliary material›
theory Incomplete_Gamma_Lemma_Bucket
imports
"HOL-Complex_Analysis.Complex_Analysis"
Safe_Power
More_Dominated_Convergence
Derivative_Method
begin
lemma sgn_sqrt [simp]: "sgn (sqrt x) = sgn x"
by (auto simp: sgn_if)
lemma countably_generated_imp_convergent_sequence:
assumes "countably_generated_filter F" "F ≠ bot"
obtains X where "filterlim X F sequentially"
proof -
obtain B where B: "antimono_on UNIV B" "⋀P. eventually P F = (∃i::nat. ∀x∈B i. P x)"
using countably_generated_filter_iff_decseq[of F] assms by blast
have "B i ≠ {}" for i
using B(2)[of "λ_. False"] assms by (auto simp: trivial_limit_def)
hence "∀i. ∃x. x ∈ B i"
by blast
then obtain X where X: "X i ∈ B i" for i
by metis
have "filterlim X F sequentially"
unfolding filterlim_def le_filter_def eventually_filtermap
proof safe
fix P assume "eventually P F"
with B obtain i where i: "∀x∈B i. P x"
by blast
hence "P (X j)" if j: "j ≥ i" for j
using monotone_onD[OF B(1) _ _ j] X[of j] by auto
thus "eventually (λj. P (X j)) sequentially"
by (auto simp: eventually_at_top_linorder)
qed
thus ?thesis
by (rule that)
qed
lemma (in sequential_filter) dominated_convergence':
fixes f :: "'a ⇒ 'n::euclidean_space ⇒ 'm::euclidean_space"
assumes f: "eventually (λk. (f k) integrable_on S) F" and h: "h integrable_on S"
and le: "eventually (λk. ∀x∈S. norm (f k x) ≤ h x) F"
and conv: "⋀x. x ∈ S ⟹ ((λk. f k x) ⤏ g x) F"
shows "((λk. integral S (f k)) ⤏ integral S g) F"
proof (rule filterlim_sequentially_imp_filterlim)
fix X assume X: "filterlim X F sequentially"
have "eventually (λk. (∀x∈S. norm (f k x) ≤ h x) ∧ f k integrable_on S) F"
using f le by eventually_elim auto
hence "eventually (λk. (∀x∈S. norm (f (X k) x) ≤ h x) ∧ f (X k) integrable_on S) sequentially"
by (rule eventually_compose_filterlim) fact
then obtain N where N: "⋀k. k ≥ N ⟹ (∀x∈S. norm (f (X k) x) ≤ h x) ∧ f (X k) integrable_on S"
by (auto simp: eventually_at_top_linorder)
define X' where "X' = X ∘ ((+) N)"
have X': "∀x∈S. norm (f (X' k) x) ≤ h x" "f (X' k) integrable_on S" for k
using N[of "N + k"] by (simp_all add: X'_def)
have lim_X': "filterlim X' F sequentially" unfolding X'_def o_def
by (rule filterlim_compose[OF X])
(use filterlim_add_const_nat_at_top[of N] in ‹simp_all add: add_ac›)
have "(λn. integral S (f (X' n))) ⇢ integral S g"
proof (rule dominated_convergence)
show "h integrable_on S"
by fact
show "f (X' n) integrable_on S" for n
by (rule X')
show "norm (f (X' k) x) ≤ h x" if "x ∈ S" for x k
using X'[of k] that by auto
show "(λn. f (X' n) x) ⇢ g x" if "x ∈ S" for x
by (rule filterlim_compose[OF conv lim_X']) fact
qed
hence "(λn. integral S (f (X' (n - N)))) ⇢ integral S g"
by (rule filterlim_compose) (rule filterlim_minus_const_nat_at_top)
also have "?this ⟷ (λn. integral S (f (X n))) ⇢ integral S g"
proof (rule filterlim_cong)
show "eventually (λn. integral S (f (X' (n - N))) = integral S (f (X n))) at_top"
using eventually_ge_at_top[of N] by eventually_elim (auto simp: X'_def)
qed auto
finally show "(λn. integral S (f (X n))) ⇢ integral S g" .
qed
lemma dominated_convergence_countably_generated_filter:
fixes f :: "'a ⇒ 'n::euclidean_space ⇒ 'm::euclidean_space"
assumes cg: "countably_generated_filter F"
assumes f: "eventually (λk. (f k) integrable_on S) F" and h: "h integrable_on S"
and le: "eventually (λk. ∀x∈S. norm (f k x) ≤ h x) F"
and conv: "⋀x. x ∈ S ⟹ ((λk. f k x) ⤏ g x) F"
shows "F ≠ bot ⟹ g integrable_on S" "((λk. integral S (f k)) ⤏ integral S g) F"
proof -
interpret sequential_filter F
by (rule countably_generated_filter_imp_sequential_filter) fact
show "((λk. integral S (f k)) ⤏ integral S g) F"
using f h le conv by (rule dominated_convergence')
assume "F ≠ bot"
with cg obtain X where X: "filterlim X F sequentially"
using countably_generated_imp_convergent_sequence by blast
have "eventually (λk. (∀x∈S. norm (f k x) ≤ h x) ∧ f k integrable_on S) F"
using f le by eventually_elim auto
hence "eventually (λk. (∀x∈S. norm (f (X k) x) ≤ h x) ∧ f (X k) integrable_on S) sequentially"
by (rule eventually_compose_filterlim) fact
then obtain N where N: "⋀k. k ≥ N ⟹ (∀x∈S. norm (f (X k) x) ≤ h x) ∧ f (X k) integrable_on S"
by (auto simp: eventually_at_top_linorder)
define X' where "X' = X ∘ ((+) N)"
have X': "∀x∈S. norm (f (X' k) x) ≤ h x" "f (X' k) integrable_on S" for k
using N[of "N + k"] by (simp_all add: X'_def)
have lim_X': "filterlim X' F sequentially" unfolding X'_def o_def
by (rule filterlim_compose[OF X])
(use filterlim_add_const_nat_at_top[of N] in ‹simp_all add: add_ac›)
show "g integrable_on S"
proof (rule dominated_convergence)
show "h integrable_on S"
by fact
show "f (X' n) integrable_on S" for n
by (rule X')
show "norm (f (X' k) x) ≤ h x" if "x ∈ S" for x k
using X'[of k] that by auto
show "(λn. f (X' n) x) ⇢ g x" if "x ∈ S" for x
by (rule filterlim_compose[OF conv lim_X']) fact
qed
qed
lemma nonpos_Reals_real_eq: "ℝ⇩≤⇩0 = {..(0::real)}"
by (auto simp: nonpos_Reals_def)
lemma has_integral_complex_of_real_iff:
"((λx. of_real (f x) :: complex) has_integral (of_real I)) A ⟷ (f has_integral I) A"
proof
assume "((λx. of_real (f x) :: complex) has_integral (of_real I)) A"
thus "(f has_integral I) A"
by (subst (asm) has_integral_componentwise_iff) (auto simp: Basis_complex_def)
qed (auto intro: has_integral_of_real)
lemma integrable_on_complex_of_real_iff:
"(λx. of_real (f x) :: complex) integrable_on A ⟷ f integrable_on A"
using has_integral_complex_of_real_iff[of f _ A]
by (metis (lifting) ext Re_complex_of_real complex_inner_1_right integrable_component
integrable_on_def)
lemma integral_complex_of_real:
"integral A (λx. complex_of_real (f x)) = of_real (integral A f)"
proof (cases "f integrable_on A")
case True
thus ?thesis
using integral_linear[of f A complex_of_real]
by (auto simp: bounded_linear_of_real o_def)
next
case False
hence "¬(λx. complex_of_real (f x)) integrable_on A"
by (subst integrable_on_complex_of_real_iff)
with False show ?thesis
by (simp add: not_integrable_integral)
qed
lemma countable_nonpos_Ints [intro]: "countable ℤ⇩≤⇩0"
by (rule countable_subset[of _ "ℤ"]) (auto intro: countable_int)
lemma
fixes f :: "_ ⇒ _ ⇒ 'a :: {banach, second_countable_topology}"
assumes integrable: "⋀i. set_integrable M A (f i)"
and summable: "AE x∈A in M. summable (λi. norm (f i x))"
and sums: "summable (λi. (∫x∈A. norm (f i x) ∂M))"
shows set_integrable_suminf: "set_integrable M A (λx. (∑i. f i x))"
and sums_set_integral: "(λi. set_lebesgue_integral M A (f i)) sums (∫x∈A. (∑i. f i x) ∂M)"
and set_integral_suminf: "(∫x∈A. (∑i. f i x) ∂M) = (∑i. set_lebesgue_integral M A (f i))"
and summable_set_integral: "summable (λi. set_lebesgue_integral M A (f i))"
proof -
have 1: "integrable M (λx. indicat_real A x *⇩R f i x)" for i
using integrable[of i] unfolding set_integrable_def .
have 2: "AE x in M. summable (λi. norm (indicat_real A x *⇩R f i x))"
using summable by eventually_elim auto
have 3: "summable (λi. lebesgue_integral M (λx. norm (indicat_real A x *⇩R f i x)))"
using sums unfolding set_lebesgue_integral_def by simp
have "integrable M (λx. (∑i. indicator A x *⇩R f i x))"
using 1 2 3 by (rule integrable_suminf)
also have "(λx. (∑i. indicator A x *⇩R f i x)) = (λx. indicator A x *⇩R (∑i. f i x))"
by (auto simp: indicator_def)
finally show "set_integrable M A (λx. (∑i. f i x))"
unfolding set_integrable_def .
have "(λi. set_lebesgue_integral M A (f i)) sums (∫x. (∑i. indicator A x *⇩R f i x) ∂M)"
unfolding set_lebesgue_integral_def using 1 2 3 by (rule sums_integral)
also have "(∫x. (∑i. indicator A x *⇩R f i x) ∂M) = (∫x. indicator A x *⇩R (∑i. f i x) ∂M)"
by (rule Bochner_Integration.integral_cong) (simp_all add: indicator_def)
finally show "(λi. set_lebesgue_integral M A (f i)) sums (∫x∈A. (∑i. f i x) ∂M)"
unfolding set_lebesgue_integral_def .
have "(∫x∈A. ∑i. f i x∂M) = (∫x. (∑i. indicator A x *⇩R f i x) ∂M)"
unfolding set_lebesgue_integral_def
by (rule Bochner_Integration.integral_cong) (auto simp: indicator_def)
also have "… = (∑i. (∫x∈A. f i x ∂M))"
unfolding set_lebesgue_integral_def using 1 2 3 by (rule integral_suminf)
finally show "(∫x∈A. (∑i. f i x) ∂M) = (∑i. set_lebesgue_integral M A (f i))" .
show "summable (λi. set_lebesgue_integral M A (f i))"
unfolding set_lebesgue_integral_def using 1 2 3 by (rule summable_integral)
qed
lemma leibniz_rule_field_derivative_real:
fixes f::"'a::{real_normed_field, banach} ⇒ real ⇒ 'a"
assumes fx: "⋀x t. x ∈ U ⟹ t ∈ {a..b} ⟹ ((λx. f x t) has_field_derivative fx x t) (at x within U)"
assumes integrable_f2: "⋀x. x ∈ U ⟹ (f x) integrable_on {a..b}"
assumes cont_fx: "continuous_on (U × {a..b}) (λ(x, t). fx x t)"
assumes U: "x0 ∈ U" "convex U"
shows "((λx. integral {a..b} (f x)) has_field_derivative integral {a..b} (fx x0)) (at x0 within U)"
using leibniz_rule_field_derivative[of U a b f fx x0] assms by simp
lemma convex_minkowski_sum_ball:
fixes A :: "'a :: euclidean_space set"
assumes "convex A"
shows "convex (⋃x∈A. ball x r)"
proof -
have "convex (⋃x∈A. ⋃y∈ball 0 r. {x + y})"
by (rule convex_sums) (use assms in auto)
also have "(⋃x∈A. ⋃y∈ball 0 r. {x + y}) = (⋃x∈A. ball x r)"
proof (intro equalityI subsetI)
fix z assume "z ∈ (⋃x∈A. ⋃y∈ball 0 r. {x + y})"
thus "z ∈ (⋃x∈A. ball x r)"
by (force simp: dist_norm)
next
fix z assume "z ∈ (⋃x∈A. ball x r)"
then obtain x where "x ∈ A" "z ∈ ball x r"
by auto
hence "z = x + (z - x)" "z - x ∈ ball 0 r"
by (auto simp: dist_norm)
thus "z ∈ (⋃x∈A. ⋃y∈ball 0 r. {x + y})"
using ‹x ∈ A› by blast
qed
finally show ?thesis .
qed
lemma convex_minkowski_sum_cball:
fixes A :: "'a :: euclidean_space set"
assumes "convex A"
shows "convex (⋃x∈A. cball x r)"
proof -
have "convex (⋃x∈A. ⋃y∈cball 0 r. {x + y})"
by (rule convex_sums) (use assms in auto)
also have "(⋃x∈A. ⋃y∈cball 0 r. {x + y}) = (⋃x∈A. cball x r)"
proof (intro equalityI subsetI)
fix z assume "z ∈ (⋃x∈A. ⋃y∈cball 0 r. {x + y})"
thus "z ∈ (⋃x∈A. cball x r)"
by (force simp: dist_norm)
next
fix z assume "z ∈ (⋃x∈A. cball x r)"
then obtain x where "x ∈ A" "z ∈ cball x r"
by auto
hence "z = x + (z - x)" "z - x ∈ cball 0 r"
by (auto simp: dist_norm)
thus "z ∈ (⋃x∈A. ⋃y∈cball 0 r. {x + y})"
using ‹x ∈ A› by blast
qed
finally show ?thesis .
qed
lemma continuous_on_linepath [continuous_intros]:
assumes "continuous_on A f" "continuous_on A g" "continuous_on A h"
shows "continuous_on A (λx. linepath (f x) (g x) (h x))"
unfolding linepath_def by (intro continuous_intros assms)
lemma contour_integral_linepath_has_field_derivative:
assumes A: "open A" "a ∈ A" "z ∈ A" "closed_segment a z ⊆ A"
assumes holo: "f holomorphic_on A"
shows "((λz. contour_integral (linepath a z) f) has_field_derivative f z) (at z within B)"
proof -
define e where "e = (if A = UNIV then 1 else setdist (closed_segment a z) (-A))"
have "e > 0"
proof (cases "A = UNIV")
case False
hence "setdist (closed_segment a z) (-A) > 0"
using assms unfolding e_def
by (subst setdist_gt_0_compact_closed compact_path_image) auto
thus "e > 0"
using False by (auto simp: e_def)
qed (auto simp: e_def)
have dist_ge_e: "dist x y ≥ e" if "x ∈ closed_segment a z" "y ∈ -A" for x y
using setdist_le_dist[OF that] that by (auto simp: e_def)
define A' where "A' = (⋃x∈closed_segment a z. ball x e)"
have "A' ⊆ A"
proof
fix x assume "x ∈ A'"
then obtain y where "y ∈ closed_segment a z" "dist y x < e"
by (auto simp: A'_def)
thus "x ∈ A"
using dist_ge_e[of y x] by auto
qed
have "closed_segment a z ⊆ A'" "open A'"
using ‹e > 0› unfolding A'_def by fastforce+
have "convex A'"
unfolding A'_def by (intro convex_minkowski_sum_ball) auto
have "a ∈ A'" "z ∈ A'"
using ‹closed_segment a z ⊆ A'› by auto
note A' = ‹A' ⊆ A› ‹closed_segment a z ⊆ A'› ‹open A'› ‹convex A'› ‹a ∈ A'› ‹z ∈ A'›
note holo = holomorphic_on_subset[OF holo ‹A' ⊆ A›]
have "(f has_field_derivative deriv f z) (at z)" if "z ∈ A'" for z
using that A' A by (auto intro!: holomorphic_derivI holo)
note [derivative_intros] = DERIV_chain2[OF this]
note [continuous_intros] =
continuous_on_compose2[OF holomorphic_on_imp_continuous_on [OF holo]]
continuous_on_compose2[OF holomorphic_on_imp_continuous_on [OF holomorphic_deriv[OF holo]]]
have [derivative_intros]:
"((λx. linepath a x t) has_field_derivative of_real t) (at x within A')" for t x
by (auto simp: linepath_def scaleR_conv_of_real intro!: derivative_eq_intros)
have *: "linepath a b t ∈ A'" if "a ∈ A'" "b ∈ A'" "t ∈ {0..1}" for a b t
using that linepath_in_convex_hull[of a A' b t] A' by (simp add: hull_same)
have "((λz. integral {0..1} (λx. f (linepath a z x)) * (z - a)) has_field_derivative
integral {0..1} (λt. deriv f (linepath a z t) * of_real t) * (z - a) +
integral {0..1} (λx. f (linepath a z x))) (at z within A')"
(is "(_ has_field_derivative ?I) _")
by (rule derivative_eq_intros leibniz_rule_field_derivative_real * A')+
(insert assms A' *,
auto intro!: derivative_eq_intros leibniz_rule_field_derivative_real
integrable_continuous_real continuous_intros
simp: split_beta scaleR_conv_of_real)
also have "(λz. integral {0..1} (λx. f (linepath a z x)) * (z - a)) =
(λz. contour_integral (linepath a z) f)"
by (simp add: contour_integral_integral)
also have "?I = integral {0..1} (λx. deriv f (linepath a z x) * of_real x * (z - a) +
f (linepath a z x))" (is "_ = integral _ ?g")
by (subst integral_mult_left [symmetric], subst integral_add [symmetric])
(insert assms A', auto intro!: integrable_continuous_real continuous_intros simp: *)
also have "(?g has_integral of_real 1 * f (linepath a z 1) - of_real 0 * f (linepath a z 0)) {0..1}"
using * A A'
by (intro fundamental_theorem_of_calculus)
(auto intro!: derivative_eq_intros has_vector_derivative_real_field
simp: linepath_def scaleR_conv_of_real)
hence "integral {0..1} ?g = f (linepath a z 1)" by (simp add: has_integral_iff)
also have "linepath a z 1 = z" by (simp add: linepath_def)
also from ‹z ∈ A'› and ‹open A'› have "at z within A' = at z" by (rule at_within_open)
finally show ?thesis by (rule DERIV_subset) simp_all
qed
lemma set_integrable_bigo:
fixes f g :: "real ⇒ 'a :: {banach, real_normed_field, second_countable_topology}"
assumes "f ∈ O(λx. g x)" and "set_integrable lborel {a..} g"
assumes "⋀b. b ≥ a ⟹ set_integrable lborel {a..<b} f"
assumes [measurable]: "set_borel_measurable borel {a..} f"
shows "set_integrable lborel {a..} f"
proof -
from assms(1) obtain C x0 where C: "C > 0" "⋀x. x ≥ x0 ⟹ norm (f x) ≤ C * norm (g x)"
by (fastforce elim!: landau_o.bigE simp: eventually_at_top_linorder)
define x0' where "x0' = max a x0"
have "set_integrable lborel {a..<x0'} f"
by (intro assms) (auto simp: x0'_def)
moreover have "set_integrable lborel {x0'..} f" unfolding set_integrable_def
proof (rule Bochner_Integration.integrable_bound)
from assms(2) have "set_integrable lborel {x0'..} g"
by (rule set_integrable_subset) (auto simp: x0'_def)
thus "integrable lborel (λx. C *⇩R (indicator {x0'..} x *⇩R g x))" unfolding set_integrable_def
by (intro integrable_scaleR_right) (simp add: abs_mult norm_mult)
next
from assms(4) have "set_borel_measurable borel {x0'..} f"
by (rule set_borel_measurable_subset) (auto simp: x0'_def)
thus "(λx. indicator {x0'..} x *⇩R f x) ∈ borel_measurable lborel"
by (simp add: set_borel_measurable_def)
next
show "AE x in lborel. norm (indicator {x0'..} x *⇩R f x)
≤ norm (C *⇩R (indicator {x0'..} x *⇩R g x))"
using C by (intro AE_I2) (auto simp: abs_mult indicator_def x0'_def)
qed
ultimately have "set_integrable lborel ({a..<x0'} ∪ {x0'..}) f"
by (rule set_integrable_Un) auto
also have "{a..<x0'} ∪ {x0'..} = {a..}" by (auto simp: x0'_def)
finally show ?thesis .
qed
subsection ‹Miscellaneous preliminary material›
lemma uniform_limit_analytic_at:
assumes "uniform_limit A f g F"
assumes "eventually (λx. f x holomorphic_on A) F"
assumes "z ∈ A" "open A" "F ≠ bot"
shows "g analytic_on {z}"
proof -
obtain r where r: "r > 0" "cball z r ⊆ A"
using ‹z ∈ A› ‹open A› by (meson open_contains_cball)
show ?thesis
proof (rule holomorphic_uniform_limit[of z r f F g])
show "∀⇩F x in F. continuous_on (cball z r) (f x) ∧ f x holomorphic_on ball z r"
using assms(2)
proof eventually_elim
case (elim x)
have "ball z r ⊆ cball z r"
by auto
also have "… ⊆ A"
by fact
finally have "f x holomorphic_on ball z r"
using elim holomorphic_on_subset r by blast
moreover have "continuous_on (cball z r) (f x)"
using elim r by (auto intro: holomorphic_on_imp_continuous_on)
ultimately show ?case by blast
qed
next
assume "g holomorphic_on ball z r"
thus "g analytic_on {z}"
using ‹z ∈ A› ‹open A› analytic_at_ball r(1) by blast
next
show "uniform_limit (cball z r) f g F"
using assms(1) by (rule uniform_limit_on_subset) (use r in auto)
qed (use assms in auto)
qed
lemma uniform_limit_holomorphic:
assumes "uniform_limit A f g F"
assumes "eventually (λx. f x holomorphic_on A) F"
assumes "open A" "F ≠ bot"
shows "g holomorphic_on A"
proof -
have "g analytic_on A"
using uniform_limit_analytic_at[OF assms(1,2) _ assms(3,4)] analytic_on_analytic_at
by blast
thus ?thesis
using ‹open A› by (simp add: analytic_on_open)
qed
lemma Re_euler_mascheroni [simp]: "Re euler_mascheroni = euler_mascheroni"
and Im_euler_mascheroni [simp]: "Im euler_mascheroni = 0"
by (simp_all add: euler_mascheroni_def)
lemma has_real_derivative_imp_has_vector_derivative [derivative_intros]:
assumes "(f has_real_derivative f') (at x)"
shows "(f has_vector_derivative f') (at x)"
using assms by (simp add: has_real_derivative_iff_has_vector_derivative)
lemma DERIV_real_sqrt_generic':
assumes "x ≠ 0"
shows "(sqrt has_field_derivative (sgn x * inverse (sqrt x) / 2)) (at x within A)"
unfolding sqrt_def
by (rule has_field_derivative_at_within) (use assms in ‹auto intro!: DERIV_real_root_generic›)
lemma DERIV_real_root_generic':
assumes "x ≠ 0"
shows "(root n has_real_derivative (inverse (real n * (sgn x * root n x) ^ (n - Suc 0)))) (at x within A)"
proof (cases "n = 0")
case False
show ?thesis
by (rule has_field_derivative_at_within)
(use False assms in ‹auto intro!: DERIV_real_root_generic simp: field_simps sgn_if›)
next
case True
have "root 0 = (λx. 0)"
by (auto simp: root_def fun_eq_iff)
thus ?thesis
using True by auto
qed
declare
DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros del]
DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros del]
DERIV_real_sqrt_generic'[THEN DERIV_chain2, derivative_intros]
DERIV_real_root_generic'[THEN DERIV_chain2, derivative_intros]
lemmas [derivative_intros] = has_vector_derivative_real_field
lemma DERIV_complex_norm [derivative_intros]:
fixes f :: "real ⇒ complex"
assumes "f x ≠ 0" and [derivative_intros]: "(f has_vector_derivative D') (at x)"
shows "((λx. norm (f x)) has_field_derivative ((D' ∙ f x) / norm (f x))) (at x)"
proof -
have "norm (f x) > 0"
using assms by simp
hence *: "(Re (f x))⇧2 + (Im (f x))⇧2 > 0"
unfolding cmod_def by simp
hence **: "(Re (f x))⇧2 + (Im (f x))⇧2 ≠ 0"
by auto
from assms have ***: "Re (f x) ≠ 0 ∨ Im (f x) ≠ 0"
by (auto simp: complex_eq_iff)
show ?thesis unfolding cmod_def
using * by derivative (auto simp: divide_simps inner_complex_def)
qed
subsection ‹Preliminary facts about the Gamma and Digamma function›
lemma cnj_Digamma:
assumes [simp]: "s ≠ 0"
shows "cnj (Digamma s) = Digamma (cnj s)"
proof (rule tendsto_unique)
have "(λx. (complex_of_real (ln (real x)) - (∑n<x. inverse (cnj s + of_nat n)))) ⇢ Digamma (cnj s)"
(is "?f ⇢ _") by (rule tendsto_cnj Digamma_LIMSEQ)+ auto
also have "?f = (λx. cnj (complex_of_real (ln (real x)) - (∑n<x. inverse (s + of_nat n))))"
by simp
finally show "… ⇢ Digamma (cnj s)" .
show "(λx. cnj (complex_of_real (ln (real x)) - (∑n<x. inverse (s + of_nat n)))) ⇢ cnj (Digamma s)"
by (rule tendsto_cnj Digamma_LIMSEQ)+ auto
qed auto
lemma cnj_Polygamma:
assumes [simp]: "s ≠ 0"
shows "cnj (Polygamma n s) = Polygamma n (cnj s)"
proof (cases "n = 0")
case True
thus ?thesis using cnj_Digamma[of s] by simp
next
case False
have "(λk. inverse ((cnj s + of_nat k) ^ Suc n)) sums
((-1) ^ Suc n * Polygamma n (cnj s) / fact n)"
by (rule Polygamma_LIMSEQ) (use False in auto)
also have "(λk. inverse ((cnj s + of_nat k) ^ Suc n)) =
(λk. cnj (inverse ((s + of_nat k) ^ Suc n)))"
by simp
finally have "(λk. cnj (inverse ((s + of_nat k) ^ Suc n))) sums
((-1) ^ Suc n * Polygamma n (cnj s) / fact n)" .
moreover have "(λk. cnj (inverse ((s + of_nat k) ^ Suc n))) sums
(cnj ((-1) ^ Suc n * Polygamma n s / fact n))"
unfolding sums_cnj by (intro Polygamma_LIMSEQ) (use False in auto)
ultimately have "(-1) ^ Suc n * Polygamma n (cnj s) / fact n =
cnj ((-1) ^ Suc n * Polygamma n s / fact n)"
by (rule sums_unique2)
thus ?thesis by simp
qed
lemma norm_rGamma_Im_mono:
assumes "Re z1 = Re z2" "¦Im z1¦ ≤ ¦Im z2¦"
shows "norm (rGamma z1) ≤ norm (rGamma z2)"
proof -
define a b1 b2 where "a = Re z1" and "b1 = ¦Im z1¦" and "b2 = ¦Im z2¦"
from assms have b12: "0 ≤ b1" "b1 ≤ b2"
by (simp_all add: b1_def b2_def)
have *: "norm (rGamma_series_Weierstrass (Complex a b1) n) ≤ norm (rGamma_series_Weierstrass (Complex a b2) n)" for n
unfolding rGamma_series_Weierstrass_def norm_mult prod_norm [symmetric]
proof (intro mult_mono mult_nonneg_nonneg norm_ge_zero exp_ge_zero prod_nonneg ballI prod_mono conjI)
from b12 show "norm (Complex a b1) ≤ norm (Complex a b2)"
by (auto simp: cmod_def simp flip: abs_le_square_iff)
next
fix i assume i: "i ∈ {1..n}"
have *: "norm (1 + z / of_nat i) = norm (of_nat i + z) / real i" for z :: complex
proof -
have "norm (of_nat i + z) / real i = norm ((of_nat i + z) / of_nat i)"
by (subst norm_divide) auto
also have "(of_nat i + z) / of_nat i = 1 + z / of_nat i"
using i by (simp add: field_simps)
finally show ?thesis ..
qed
show "cmod (1 + Complex a b1 / of_nat i) ≤ cmod (1 + Complex a b2 / of_nat i)"
using i b12 unfolding *
by (intro divide_right_mono) (auto simp: cmod_def simp flip: abs_le_square_iff)
qed auto
have "norm (rGamma (Complex a b1)) ≤ norm (rGamma (Complex a b2))"
by (rule tendsto_le sequentially_bot tendsto_norm tendsto_norm rGamma_Weierstrass_complex)+
(rule always_eventually allI *)+
also have "Complex a b1 ∈ {z1, cnj z1}"
by (auto simp: a_def b1_def complex_eq_iff)
hence "norm (rGamma (Complex a b1)) = norm (rGamma z1)"
by (auto simp flip: cnj_rGamma)
also have "Complex a b2 ∈ {z2, cnj z2}"
by (auto simp: assms a_def b2_def complex_eq_iff)
hence "norm (rGamma (Complex a b2)) = norm (rGamma z2)"
by (auto simp flip: cnj_rGamma)
finally show ?thesis .
qed
lemma Re_Digamma_Im_mono:
assumes "Re z1 = Re z2" "Re z1 > 0" "¦Im z1¦ ≤ ¦Im z2¦"
shows "Re (Digamma z1) ≤ Re (Digamma z2)"
proof -
have [simp]: "z1 ≠ 0" "z2 ≠ 0"
using assms by (auto simp: complex_eq_iff)
define a b1 b2 where "a = Re z1" and "b1 = ¦Im z1¦" and "b2 = ¦Im z2¦"
have "Re (Digamma (Complex a b1)) ≤ Re (Digamma (Complex a b2))"
proof (rule tendsto_le[OF _ _ _ always_eventually[OF allI]])
fix k :: nat
have "(a + real n) / (b2⇧2 + (a + real n)⇧2) ≤ (a + real n) / (b1⇧2 + (a + real n)⇧2)" for n
using assms
by (intro divide_left_mono mult_pos_pos add_nonneg_pos)
(auto simp: a_def b1_def b2_def abs_le_square_iff)
hence "(∑x<k. Re (1 / (of_nat x + Complex a b2))) ≤ (∑x<k. Re (1 / (of_nat x + Complex a b1)))"
using assms by (intro sum_mono) (auto simp: Re_divide field_simps)
thus "Re (complex_of_real (ln (real k)) - (∑n<k. inverse (Complex a b1 + of_nat n))) ≤
Re (complex_of_real (ln (real k)) - (∑n<k. inverse (Complex a b2 + of_nat n)))"
by (simp add: field_simps)
next
show "sequentially ≠ bot" by simp
qed ((rule Digamma_LIMSEQ tendsto_Re)+; use assms in ‹simp add: a_def complex_eq_iff›)+
also have "Complex a b1 ∈ {z1, cnj z1}"
by (auto simp: complex_eq_iff a_def b1_def b2_def)
hence "Re (Digamma (Complex a b1)) = Re (Digamma z1)"
by (auto simp flip: cnj_Digamma)
also have "Complex a b2 ∈ {z2, cnj z2}"
by (auto simp: complex_eq_iff a_def b1_def b2_def assms)
hence "Re (Digamma (Complex a b2)) = Re (Digamma z2)"
by (auto simp flip: cnj_Digamma)
finally show ?thesis .
qed
lemma Digamma_Re_le_Re_Digamma:
assumes "Re z > 0"
shows "Digamma (Re z) ≤ Re (Digamma z)"
proof -
have "Digamma (Re z) = Re (Digamma (of_real (Re z)))"
using assms by (subst Polygamma_of_real) auto
also have "… ≤ Re (Digamma z)"
by (rule Re_Digamma_Im_mono) (use assms in auto)
finally show ?thesis .
qed
lemma Re_Digamma_nonneg:
assumes "Re z > 0" "Digamma (Re z) ≥ 0"
shows "Re (Digamma z) ≥ 0"
proof -
have "0 ≤ Digamma (Re z)"
using assms by simp
also have "… ≤ Re (Digamma z)"
by (rule Digamma_Re_le_Re_Digamma) (use assms in auto)
finally show ?thesis .
qed
lemma norm_Gamma_Re_mono:
assumes "Im z1 = Im z2" "Re z1 ≤ Re z2" "Re z1 > 0" "Digamma (Re z1) ≥ 0"
shows "norm (Gamma z1) ≤ norm (Gamma z2)"
proof -
define a1 a2 b where "a1 = Re z1" and "a2 = Re z2" and "b = Im z1"
have z1: "z1 = complex_of_real a1 + 𝗂 * complex_of_real b"
and z2: "z2 = complex_of_real a2 + 𝗂 * complex_of_real b"
by (simp_all add: a1_def a2_def b_def complex_eq_iff assms)
show "norm (Gamma z1) ≤ norm (Gamma z2)"
unfolding z1 z2
proof (rule deriv_nonneg_imp_mono[where g = "λa. norm (Gamma (complex_of_real a + 𝗂 * b))"])
fix x :: real
assume x: "x ∈ {a1..a2}"
with assms have "x > 0" by (auto simp: a1_def)
define z where "z = complex_of_real x + 𝗂 * complex_of_real b"
have *: "complex_of_real x + 𝗂 * complex_of_real b ∉ ℤ⇩≤⇩0"
using ‹x > 0› by (auto elim!: nonpos_Ints_cases simp: complex_eq_iff)
hence **: "Gamma (complex_of_real x + 𝗂 * complex_of_real b) ≠ 0"
by (subst Gamma_eq_zero_iff) auto
have "((λx. norm (Gamma (of_real x + 𝗂 * b))) has_field_derivative
(Gamma z * Digamma z) ∙ Gamma z / norm (Gamma z)) (at x)"
using * ** by derivative (auto simp: z_def)
also have "(Gamma z * Digamma z) ∙ Gamma z = Re (Digamma z) * norm (Gamma z) ^ 2"
by (simp add: inner_complex_def cmod_def power2_eq_square field_simps)
also have "… / norm (Gamma z) = Re (Digamma z) * norm (Gamma z)"
by (simp add: power2_eq_square)
finally show "((λx. norm (Gamma (of_real x + 𝗂 * b)))
has_field_derivative Re (Digamma z) * norm (Gamma z)) (at x)" .
from x have "Re z > 0"
using assms by (auto simp: z_def a1_def)
moreover {
have "0 ≤ Digamma a1" using assms by (simp add: a1_def)
also have "… ≤ Digamma (Re x)"
using assms x by (intro Digamma_real_mono) (auto simp: a1_def)
finally have "Digamma (Re x) ≥ 0" .
}
ultimately have "Re (Digamma z) ≥ 0"
by (intro Re_Digamma_nonneg) (auto simp: z_def)
thus "Re (Digamma z) * norm (Gamma z) ≥ 0"
using assms x by (intro mult_nonneg_nonneg) auto
qed (use assms in ‹auto simp: a1_def a2_def›)
qed
lemma norm_Gamma_Im_mono:
assumes "Re z1 = Re z2" "¦Im z1¦ ≤ ¦Im z2¦" "z1 ∈ ℤ⇩≤⇩0 ⟶ z2 ∈ ℤ⇩≤⇩0"
shows "norm (Gamma z1) ≥ norm (Gamma z2)"
proof (cases "z2 ∈ ℤ⇩≤⇩0")
case True
hence "Gamma z2 = 0" by (auto simp: Gamma_eq_zero_iff)
thus ?thesis by simp
next
case False
with assms have "z1 ∉ ℤ⇩≤⇩0"
by auto
with assms False norm_rGamma_Im_mono[of z1 z2] show ?thesis
by (auto simp: Gamma_def norm_divide field_simps rGamma_eq_zero_iff)
qed
lemma norm_Gamma_bound:
assumes "Re z ∉ ℤ⇩≤⇩0"
shows "norm (Gamma z) ≤ ¦Gamma (Re z)¦"
proof -
from assms have "z ∉ ℤ⇩≤⇩0"
by (auto simp: nonpos_Ints_def)
with norm_Gamma_Im_mono[of "of_real (Re z)" z] assms show ?thesis
by (auto simp: Gamma_complex_of_real of_real_in_nonpos_Ints_iff)
qed
lemma norm_Gamma_bound':
assumes "Re z > 0"
shows "norm (Gamma z) ≤ Gamma (Re z)"
proof -
from assms have "Re z ∉ ℤ⇩≤⇩0"
by (auto elim: nonpos_Ints_cases)
with assms show ?thesis
using norm_Gamma_bound[of z] by simp
qed
end