Theory Cotangent_PFD_Formula
section ‹The Partial-Fraction Formula for the Cotangent Function›
theory Cotangent_PFD_Formula
imports "HOL-Complex_Analysis.Complex_Analysis" "HOL-Real_Asymp.Real_Asymp"
begin
subsection ‹Auxiliary lemmas›
lemma uniformly_on_image:
"uniformly_on (f ` A) g = filtercomap (λh. h ∘ f) (uniformly_on A (g ∘ f))"
unfolding uniformly_on_def by (simp add: filtercomap_INF)
lemma uniform_limit_image:
"uniform_limit (f ` A) g h F ⟷ uniform_limit A (λx y. g x (f y)) (λx. h (f x)) F"
by (simp add: uniformly_on_image filterlim_filtercomap_iff o_def)
lemma Ints_add_iff1 [simp]: "x ∈ ℤ ⟹ x + y ∈ ℤ ⟷ y ∈ ℤ"
by (metis Ints_add Ints_diff add.commute add_diff_cancel_right')
lemma Ints_add_iff2 [simp]: "y ∈ ℤ ⟹ x + y ∈ ℤ ⟷ x ∈ ℤ"
by (metis Ints_add Ints_diff add_diff_cancel_right')
text ‹
If a set is discrete (i.e. the difference between any two points is bounded from below),
it has no limit points:
›
lemma discrete_imp_not_islimpt:
assumes e: "0 < e"
and d: "∀x ∈ S. ∀y ∈ S. dist y x < e ⟶ y = x"
shows "¬x islimpt S"
proof
assume "x islimpt S"
hence "x islimpt S - {x}"
by (meson islimpt_punctured)
moreover from assms have "closed (S - {x})"
by (intro discrete_imp_closed) auto
ultimately show False
unfolding closed_limpt by blast
qed
text ‹
In particular, the integers have no limit point:
›
lemma Ints_not_limpt: "¬((x :: 'a :: real_normed_algebra_1) islimpt ℤ)"
by (rule discrete_imp_not_islimpt[of 1]) (auto elim!: Ints_cases simp: dist_of_int)
text ‹
The following lemma allows evaluating telescoping sums of the form
\[\sum\limits_{n=0}^\infty \left(f(n) - f(n + k)\right)\]
where $f(n) \longrightarrow 0$, i.e.\ where all terms except for the first ‹k› are
cancelled by later summands.
›
lemma sums_long_telescope:
fixes f :: "nat ⇒ 'a :: {topological_group_add, topological_comm_monoid_add, ab_group_add}"
assumes lim: "f ⇢ 0"
shows "(λn. f n - f (n + c)) sums (∑k<c. f k)" (is "_ sums ?S")
proof -
thm tendsto_diff
have "(λN. ?S - (∑n<c. f (N + n))) ⇢ ?S - 0"
by (intro tendsto_intros tendsto_null_sum filterlim_compose[OF assms]; real_asymp)
hence "(λN. ?S - (∑n<c. f (N + n))) ⇢ ?S"
by simp
moreover have "eventually (λN. ?S - (∑n<c. f (N + n)) = (∑n<N. f n - f (n + c))) sequentially"
using eventually_ge_at_top[of c]
proof eventually_elim
case (elim N)
have "(∑n<N. f n - f (n + c)) = (∑n<N. f n) - (∑n<N. f (n + c))"
by (simp only: sum_subtractf)
also have "(∑n<N. f n) = (∑n∈{..<c} ∪ {c..<N}. f n)"
using elim by (intro sum.cong) auto
also have "… = (∑n<c. f n) + (∑n∈{c..<N}. f n)"
by (subst sum.union_disjoint) auto
also have "(∑n<N. f (n + c)) = (∑n∈{c..<N+c}. f n)"
using elim by (intro sum.reindex_bij_witness[of _ "λn. n - c" "λn. n + c"]) auto
also have "… = (∑n∈{c..<N}∪{N..<N+c}. f n)"
using elim by (intro sum.cong) auto
also have "… = (∑n∈{c..<N}. f n) + (∑n∈{N..<N+c}. f n)"
by (subst sum.union_disjoint) auto
also have "(∑n∈{N..<N+c}. f n) = (∑n<c. f (N + n))"
by (intro sum.reindex_bij_witness[of _ "λn. n + N" "λn. n - N"]) auto
finally show ?case
by simp
qed
ultimately show ?thesis
unfolding sums_def by (rule Lim_transform_eventually)
qed
subsection ‹Definition of auxiliary function›
text ‹
The following function is the infinite sum appearing on the right-hand side of the
cotangent formula. It can be written either as
\[\sum_{n=1}^\infty\left(\frac{1}{x + n} + \frac{1}{x - n}\right)\]
or as
\[2x \sum_{n=1}^\infty \frac{1}{x^2 - n^2}\ .\]
›
definition cot_pfd :: "'a :: {real_normed_field, banach} ⇒ 'a" where
"cot_pfd x = (∑n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))"
text ‹
The sum in the definition of \<^const>‹cot_pfd› converges uniformly on compact sets.
This implies, in particular, that \<^const>‹cot_pfd› is holomorphic (and thus also continuous).
›
lemma uniform_limit_cot_pfd_complex:
assumes "R ≥ 0"
shows "uniform_limit (cball 0 R :: complex set)
(λN x. ∑n<N. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) cot_pfd sequentially"
unfolding cot_pfd_def
proof (rule Weierstrass_m_test_ev)
have "eventually (λN. of_nat (N + 1) > R) at_top"
by real_asymp
thus "∀⇩F N in sequentially. ∀(x::complex)∈cball 0 R. norm (2 * x / (x ^ 2 - of_nat (Suc N) ^ 2)) ≤
2 * R / (real (N + 1) ^ 2 - R ^ 2)"
proof eventually_elim
case (elim N)
show ?case
proof safe
fix x :: complex assume x: "x ∈ cball 0 R"
have "(1 + real N)⇧2 - R⇧2 ≤ norm ((1 + of_nat N :: complex) ^ 2) - norm (x ^ 2)"
using x by (auto intro: power_mono simp: norm_power simp flip: of_nat_Suc)
also have "… ≤ norm (x⇧2 - (1 + of_nat N :: complex)⇧2)"
by (metis norm_minus_commute norm_triangle_ineq2)
finally show "norm (2 * x / (x⇧2 - (of_nat (Suc N))⇧2)) ≤ 2 * R / (real (N + 1) ^ 2 - R ^ 2)"
unfolding norm_mult norm_divide using ‹R ≥ 0› x elim
by (intro mult_mono frac_le) (auto intro: power_strict_mono)
qed
qed
next
show "summable (λN. 2 * R / (real (N + 1) ^ 2 - R ^ 2))"
proof (rule summable_comparison_test_bigo)
show "(λN. 2 * R / (real (N + 1) ^ 2 - R ^ 2)) ∈ O(λN. 1 / real N ^ 2)"
by real_asymp
next
show "summable (λn. norm (1 / real n ^ 2))"
using inverse_power_summable[of 2] by (simp add: field_simps)
qed
qed
lemma sums_cot_pfd_complex:
fixes x :: complex
shows "(λn. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) sums cot_pfd x"
using tendsto_uniform_limitI[OF uniform_limit_cot_pfd_complex[of "norm x"], of x]
by (simp add: sums_def)
lemma sums_cot_pfd_complex'_aux:
fixes x :: "'a :: {banach, real_normed_field, field_char_0}"
assumes "x ∉ ℤ - {0}"
shows "2 * x / (x ^ 2 - of_nat (Suc n) ^ 2) =
1 / (x + of_nat (Suc n)) + 1 / (x - of_nat (Suc n))"
proof -
have neq1: "x + of_nat (Suc n) ≠ 0"
using assms by (subst add_eq_0_iff2) (auto simp del: of_nat_Suc)
have neq2: "x - of_nat (Suc n) ≠ 0"
using assms by (auto simp del: of_nat_Suc)
have neq3: "x ^ 2 - of_nat (Suc n) ^ 2 ≠ 0"
using assms by (auto simp del: of_nat_Suc simp: power2_eq_iff)
show ?thesis using neq1 neq2 neq3
by (simp add: divide_simps del: of_nat_Suc) (auto simp: power2_eq_square algebra_simps)
qed
lemma sums_cot_pfd_complex':
fixes x :: complex
assumes "x ∉ ℤ - {0}"
shows "(λn. 1 / (x + of_nat (Suc n)) + 1 / (x - of_nat (Suc n))) sums cot_pfd x"
using sums_cot_pfd_complex[of x] sums_cot_pfd_complex'_aux[OF assms] by simp
lemma summable_cot_pfd_complex:
fixes x :: complex
shows "summable (λn. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))"
using sums_cot_pfd_complex[of x] by (simp add: sums_iff)
lemma summable_cot_pfd_real:
fixes x :: real
shows "summable (λn. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))"
proof -
have "summable (λn. complex_of_real (2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)))"
using summable_cot_pfd_complex[of "of_real x"] by simp
also have "?this ⟷ ?thesis"
by (rule summable_of_real_iff)
finally show ?thesis .
qed
lemma sums_cot_pfd_real:
fixes x :: real
shows "(λn. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) sums cot_pfd x"
using summable_cot_pfd_real[of x] by (simp add: cot_pfd_def sums_iff)
lemma cot_pfd_complex_of_real [simp]: "cot_pfd (complex_of_real x) = of_real (cot_pfd x)"
using sums_of_real[OF sums_cot_pfd_real[of x], where ?'a = complex]
sums_cot_pfd_complex[of "of_real x"] sums_unique2 by auto
lemma uniform_limit_cot_pfd_real:
assumes "R ≥ 0"
shows "uniform_limit (cball 0 R :: real set)
(λN x. ∑n<N. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) cot_pfd sequentially"
proof -
have "uniform_limit (cball 0 R)
(λN x. Re (∑n<N. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))) (λx. Re (cot_pfd x)) sequentially"
by (intro uniform_limit_intros uniform_limit_cot_pfd_complex assms)
hence "uniform_limit (of_real ` cball 0 R)
(λN x. Re (∑n<N. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))) (λx. Re (cot_pfd x)) sequentially"
by (rule uniform_limit_on_subset) auto
thus ?thesis
by (simp add: uniform_limit_image)
qed
subsection ‹Holomorphicity and continuity›
lemma has_field_derivative_cot_pfd_complex:
fixes z :: complex
assumes z: "z ∈ -(ℤ-{0})"
shows "(cot_pfd has_field_derivative (-Polygamma 1 (1 + z) - Polygamma 1 (1 - z))) (at z)"
proof -
define f :: "nat ⇒ complex ⇒ complex"
where "f = (λN x. ∑n<N. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))"
define f' :: "nat ⇒ complex ⇒ complex"
where "f' = (λN x. ∑n<N. -1/(x + of_nat (Suc n)) ^ 2 - 1/(x - of_nat (Suc n)) ^ 2)"
have "∃g'. ∀x∈- (ℤ - {0}). (cot_pfd has_field_derivative g' x) (at x) ∧ (λn. f' n x) ⇢ g' x"
proof (rule has_complex_derivative_uniform_sequence)
show "open (-(ℤ - {0}) :: complex set)"
by (intro open_Compl closed_subset_Ints) auto
next
fix n :: nat and x :: complex
assume x: "x ∈ -(ℤ - {0})"
have nz: "x⇧2 - (of_nat (Suc n))⇧2 ≠ 0" for n
proof
assume "x⇧2 - (of_nat (Suc n))⇧2 = 0"
hence "(of_nat (Suc n))⇧2 = x⇧2"
by algebra
hence "x = of_nat (Suc n) ∨ x = -of_nat (Suc n)"
by (subst (asm) eq_commute, subst (asm) power2_eq_iff) auto
moreover have "(of_nat (Suc n) :: complex) ∈ ℤ" "(-of_nat (Suc n) :: complex) ∈ ℤ"
by (intro Ints_minus Ints_of_nat)+
ultimately show False using x
by (auto simp del: of_nat_Suc)
qed
have nz1: "x + of_nat (Suc k) ≠ 0" for k
using x by (subst add_eq_0_iff2) (auto simp del: of_nat_Suc)
have nz2: "x - of_nat (Suc k) ≠ 0" for k
using x by (auto simp del: of_nat_Suc)
have "((λx. 2 * x / (x⇧2 - (of_nat (Suc k))⇧2)) has_field_derivative
- 1 / (x + of_nat (Suc k))⇧2 - 1 / (x - of_nat (Suc k))⇧2) (at x)" for k :: nat
proof -
have "((λx. inverse (x + of_nat (Suc k)) + inverse (x - of_nat (Suc k))) has_field_derivative
- inverse ((x + of_nat (Suc k)) ^ 2)- inverse ((x - of_nat (Suc k))) ^ 2) (at x)"
by (rule derivative_eq_intros refl nz1 nz2)+ (simp add: power2_eq_square)
also have "?this ⟷ ?thesis"
proof (intro DERIV_cong_ev)
have "eventually (λt. t ∈ -(ℤ-{0})) (nhds x)" using x
by (intro eventually_nhds_in_open open_Compl closed_subset_Ints) auto
thus "eventually (λt. inverse (t + of_nat (Suc k)) + inverse (t - of_nat (Suc k)) =
2 * t / (t⇧2 - (of_nat (Suc k))⇧2)) (nhds x)"
proof eventually_elim
case (elim t)
thus ?case
using sums_cot_pfd_complex'_aux[of t k] by (auto simp add: field_simps)
qed
qed (auto simp: field_simps)
finally show ?thesis .
qed
thus "(f n has_field_derivative f' n x) (at x)"
unfolding f_def f'_def by (intro DERIV_sum)
next
fix x :: complex assume x: "x ∈ -(ℤ-{0})"
have "open (-(ℤ-{0}) :: complex set)"
by (intro open_Compl closed_subset_Ints) auto
then obtain r where r: "r > 0" "cball x r ⊆ -(ℤ-{0})"
using x open_contains_cball by blast
have "uniform_limit (cball x r) f cot_pfd sequentially"
using uniform_limit_cot_pfd_complex[of "norm x + r"] unfolding f_def
proof (rule uniform_limit_on_subset)
show "cball x r ⊆ cball 0 (cmod x + r)"
by (subst cball_subset_cball_iff) auto
qed (use ‹r > 0› in auto)
thus "∃d>0. cball x d ⊆ - (ℤ - {0}) ∧ uniform_limit (cball x d) f cot_pfd sequentially"
using r by (intro exI[of _ r]) auto
qed
then obtain g' where g': "⋀x. x∈-(ℤ - {0}) ⟹ (cot_pfd has_field_derivative g' x) (at x)"
"⋀x. x∈-(ℤ - {0}) ⟹ (λn. f' n x) ⇢ g' x" by blast
have "(λn. f' n z) ⇢ -Polygamma 1 (1 + z) - Polygamma 1 (1 - z)"
proof -
have "(λn. -inverse (((1 + z) + of_nat n) ^ Suc 1) -
inverse (((1 - z) + of_nat n) ^ Suc 1)) sums
(-((-1) ^ Suc 1 * Polygamma 1 (1 + z) / fact 1) -
(-1) ^ Suc 1 * Polygamma 1 (1 - z) / fact 1)"
using z by (intro sums_diff sums_minus Polygamma_LIMSEQ) (auto simp: add_eq_0_iff)
also have "… = -Polygamma 1 (1 + z) - Polygamma 1 (1 - z)"
by simp
also have "(λn. -inverse (((1 + z) + of_nat n) ^ Suc 1) - inverse (((1 - z) + of_nat n) ^ Suc 1)) =
(λn. -1/(z + of_nat (Suc n)) ^ 2 - 1/(z - of_nat (Suc n)) ^ 2)"
by (simp add: f'_def field_simps power2_eq_square)
finally show ?thesis
unfolding sums_def f'_def .
qed
with g'(2)[OF z] have "g' z = -Polygamma 1 (1 + z) - Polygamma 1 (1 - z)"
using LIMSEQ_unique by blast
with g'(1)[OF z] show ?thesis
by simp
qed
lemma has_field_derivative_cot_pfd_complex' [derivative_intros]:
assumes "(g has_field_derivative g') (at x within A)" and "g x ∉ ℤ - {0}"
shows "((λx. cot_pfd (g x :: complex)) has_field_derivative
(-Polygamma 1 (1 + g x) - Polygamma 1 (1 - g x)) * g') (at x within A)"
using DERIV_chain2[OF has_field_derivative_cot_pfd_complex assms(1)] assms(2) by auto
lemma Polygamma_real_conv_complex: "x ≠ 0 ⟹ Polygamma n x = Re (Polygamma n (of_real x))"
by (simp add: Polygamma_of_real)
lemma has_field_derivative_cot_pfd_real [derivative_intros]:
assumes "(g has_field_derivative g') (at x within A)" and "g x ∉ ℤ - {0}"
shows "((λx. cot_pfd (g x :: real)) has_field_derivative
(-Polygamma 1 (1 + g x) - Polygamma 1 (1 - g x)) * g') (at x within A)"
proof -
have *: "complex_of_real (g x) ∉ ℤ - {0}"
using assms(2) by auto
have **: "(1 + g x) ≠ 0" "(1 - g x) ≠ 0"
using assms(2) by (auto simp: add_eq_0_iff)
have "((λx. Re ((cot_pfd ∘ (λx. of_real (g x))) x)) has_field_derivative
(-Polygamma 1 (1 + g x) - Polygamma 1 (1 - g x)) * g') (at x within A)"
by (rule derivative_eq_intros has_vector_derivative_real_field
field_vector_diff_chain_within assms refl *)+
(use ** in ‹auto simp: Polygamma_real_conv_complex›)
thus ?thesis
by simp
qed
lemma holomorphic_on_cot_pfd [holomorphic_intros]:
assumes "A ⊆ -(ℤ-{0})"
shows "cot_pfd holomorphic_on A"
proof -
have "cot_pfd holomorphic_on (-(ℤ-{0}))"
unfolding holomorphic_on_def
using has_field_derivative_cot_pfd_complex field_differentiable_at_within
field_differentiable_def by fast
thus ?thesis
by (rule holomorphic_on_subset) (use assms in auto)
qed
lemma holomorphic_on_cot_pfd' [holomorphic_intros]:
assumes "f holomorphic_on A" "⋀x. x ∈ A ⟹ f x ∉ ℤ - {0}"
shows "(λx. cot_pfd (f x)) holomorphic_on A"
using holomorphic_on_compose[OF assms(1) holomorphic_on_cot_pfd] assms(2)
by (auto simp: o_def)
lemma continuous_on_cot_pfd_complex [continuous_intros]:
assumes "continuous_on A f" "⋀z. z ∈ A ⟹ f z ∉ ℤ - {0}"
shows "continuous_on A (λx. cot_pfd (f x :: complex))"
by (rule continuous_on_compose2[OF holomorphic_on_imp_continuous_on[OF
holomorphic_on_cot_pfd[OF order.refl]] assms(1)]) (use assms(2) in auto)
lemma continuous_on_cot_pfd_real [continuous_intros]:
assumes "continuous_on A f" "⋀z. z ∈ A ⟹ f z ∉ ℤ - {0}"
shows "continuous_on A (λx. cot_pfd (f x :: real))"
proof -
have "continuous_on A (λx. Re (cot_pfd (of_real (f x))))"
by (rule continuous_intros assms)+ (use assms in auto)
thus ?thesis
by simp
qed
subsection ‹Functional equations›
text ‹
In this section, we will show three few functional equations for the function \<^const>‹cot_pfd›.
The first one is trivial; the other two are a bit tedious and not very insightful, so I
will not comment on them.
›
text ‹\<^const>‹cot_pfd› is an odd function:›
lemma cot_pfd_complex_minus [simp]: "cot_pfd (-x :: complex) = -cot_pfd x"
proof -
have "(λn. 2 * (-x) / ((-x) ^ 2 - of_nat (Suc n) ^ 2)) =
(λn. - (2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)))"
by simp
also have "… sums -cot_pfd x"
by (intro sums_minus sums_cot_pfd_complex)
finally show ?thesis
using sums_cot_pfd_complex[of "-x"] sums_unique2 by blast
qed
lemma cot_pfd_real_minus [simp]: "cot_pfd (-x :: real) = -cot_pfd x"
using cot_pfd_complex_minus[of "of_real x"]
unfolding of_real_minus [symmetric] cot_pfd_complex_of_real of_real_eq_iff .
text ‹\<^term>‹1 / x + cot_pfd x› is periodic with period 1:›
lemma cot_pfd_plus_1_complex:
assumes "x ∉ ℤ"
shows "cot_pfd (x + 1 :: complex) = cot_pfd x - 1 / (x + 1) + 1 / x"
proof -
have *: "x ^ 2 ≠ of_nat n ^ 2" if "x ∉ ℤ" for x :: complex and n
using that by (metis Ints_of_nat minus_in_Ints_iff power2_eq_iff)
have **: "x + of_nat n ≠ 0" if "x ∉ ℤ" for x :: complex and n
using that by (metis Ints_0 Ints_add_iff2 Ints_of_nat)
have [simp]: "x ≠ 0"
using assms by auto
have [simp]: "x + 1 ≠ 0"
using assms by (metis "**" of_nat_1)
have [simp]: "x + 2 ≠ 0"
using **[of x 2] assms by simp
have lim: "(λn. 1 / (x + of_nat (Suc n))) ⇢ 0"
by (intro tendsto_divide_0[OF tendsto_const] tendsto_add_filterlim_at_infinity[OF tendsto_const]
filterlim_compose[OF tendsto_of_nat] filterlim_Suc)
have sum1: "(λn. 1 / (x + of_nat (Suc n)) - 1 / (x + of_nat (Suc n + 2))) sums
(∑n<2. 1 / (x + of_nat (Suc n)))"
using sums_long_telescope[OF lim, of 2] by (simp add: algebra_simps)
have "(λn. 2 * x / (x⇧2 - (of_nat (Suc n))⇧2) - 2 * (x + 1) / ((x + 1)^2 - (of_nat (Suc (Suc n)))⇧2))
sums (cot_pfd x - (cot_pfd (x + 1) - 2 * (x + 1) / ((x + 1)^2 - (of_nat (Suc 0) ^ 2))))"
using sums_cot_pfd_complex[of "x + 1"]
by (intro sums_diff sums_cot_pfd_complex, subst sums_Suc_iff) auto
also have "2 * (x + 1) / ((x + 1)^2 - (of_nat (Suc 0) ^ 2)) = 2 * (x + 1) / (x * (x + 2))"
by (simp add: algebra_simps power2_eq_square)
also have "(λn. 2 * x / (x⇧2 - (of_nat (Suc n))⇧2) -
2 * (x + 1) / ((x + 1)⇧2 - (of_nat (Suc (Suc n)))⇧2)) =
(λn. 1 / (x + of_nat (Suc n)) - 1 / (x + of_nat (Suc n + 2)))"
using *[of x] *[of "x + 1"] **[of x] **[of "x + 1"] assms
apply (intro ext)
apply (simp add: divide_simps del: of_nat_add of_nat_Suc)
apply (simp add: algebra_simps power2_eq_square)
done
finally have sum2: "(λn. 1 / (x + of_nat (Suc n)) - 1 / (x + of_nat (Suc n + 2))) sums
(cot_pfd x - cot_pfd (x + 1) + 2 * (x + 1) / (x * (x + 2)))"
by (simp add: algebra_simps)
have "cot_pfd x - cot_pfd (x + 1) + 2 * (x + 1) / (x * (x + 2)) =
(∑n<2. 1 / (x + of_nat (Suc n)))"
using sum1 sum2 sums_unique2 by blast
hence "cot_pfd x - cot_pfd (x + 1) = -2 * (x + 1) / (x * (x + 2)) + 1 / (x + 1) + 1 / (x + 2)"
by (simp add: eval_nat_numeral divide_simps) algebra?
also have "… = 1 / (x + 1) - 1 / x"
by (simp add: divide_simps) algebra?
finally show ?thesis
by algebra
qed
lemma cot_pfd_plus_1_real:
assumes "x ∉ ℤ"
shows "cot_pfd (x + 1 :: real) = cot_pfd x - 1 / (x + 1) + 1 / x"
proof -
have "cot_pfd (complex_of_real (x + 1)) = cot_pfd (of_real x) - 1 / (of_real x + 1) + 1 / of_real x"
using cot_pfd_plus_1_complex[of x] assms by simp
also have "… = complex_of_real (cot_pfd x - 1 / (x + 1) + 1 / x)"
by simp
finally show ?thesis
unfolding cot_pfd_complex_of_real of_real_eq_iff .
qed
text ‹
\<^const>‹cot_pfd› satisfies the following functional equation:
\[2 f(x) = f\left(\frac{x}{2}\right) + f\left(\frac{x+1}{2}\right) + \frac{2}{x+1}\]
›
lemma cot_pfd_funeq_complex:
fixes x :: complex
assumes "x ∉ ℤ"
shows "2 * cot_pfd x = cot_pfd (x / 2) + cot_pfd ((x + 1) / 2) + 2 / (x + 1)"
proof -
define f :: "complex ⇒ nat ⇒ complex" where "f = (λx n. 1 / (x + of_nat (Suc n)))"
define g :: "complex ⇒ nat ⇒ complex" where "g = (λx n. 1 / (x - of_nat (Suc n)))"
define h :: "complex ⇒ nat ⇒ complex" where "h = (λx n. 2 * (f x (n + 1) + g x n))"
have sums: "(λn. f x n + g x n) sums cot_pfd x" if "x ∉ ℤ" for x
unfolding f_def g_def using that by (intro sums_cot_pfd_complex') auto
have "x / 2 ∉ ℤ"
proof
assume "x / 2 ∈ ℤ"
hence "2 * (x / 2) ∈ ℤ"
by (intro Ints_mult) auto
thus False using assms by simp
qed
moreover have "(x + 1) / 2 ∉ ℤ"
proof
assume "(x + 1) / 2 ∈ ℤ"
hence "2 * ((x + 1) / 2) - 1 ∈ ℤ"
by (intro Ints_mult Ints_diff) auto
thus False using assms by (simp add: field_simps)
qed
ultimately have "(λn. (f (x / 2) n + g (x / 2) n) + (f ((x+1) / 2) n + g ((x+1) / 2) n)) sums
(cot_pfd (x / 2) + cot_pfd ((x + 1) / 2))"
by (intro sums_add sums)
also have "(λn. (f (x / 2) n + g (x / 2) n) + (f ((x+1) / 2) n + g ((x+1) / 2) n)) =
(λn. h x (2 * n) + h x (2 * n + 1))"
proof
fix n :: nat
have "(f (x / 2) n + g (x / 2) n) + (f ((x+1) / 2) n + g ((x+1) / 2) n) =
(f (x / 2) n + f ((x+1) / 2) n) + (g (x / 2) n + g ((x+1) / 2) n)"
by algebra
also have "f (x / 2) n + f ((x+1) / 2) n = 2 * (f x (2 * n + 1) + f x (2 * n + 2))"
by (simp add: f_def field_simps)
also have "g (x / 2) n + g ((x+1) / 2) n = 2 * (g x (2 * n) + g x (2 * n + 1))"
by (simp add: g_def field_simps)
also have "2 * (f x (2 * n + 1) + f x (2 * n + 2)) + … =
h x (2 * n) + h x (2 * n + 1)"
unfolding h_def by (simp add: algebra_simps)
finally show "(f (x / 2) n + g (x / 2) n) + (f ((x+1) / 2) n + g ((x+1) / 2) n) =
h x (2 * n) + h x (2 * n + 1)" .
qed
finally have sum1:
"(λn. h x (2 * n) + h x (2 * n + 1)) sums (cot_pfd (x / 2) + cot_pfd ((x + 1) / 2))" .
have "f x ⇢ 0" unfolding f_def
by (intro tendsto_divide_0[OF tendsto_const]
tendsto_add_filterlim_at_infinity[OF tendsto_const]
filterlim_compose[OF tendsto_of_nat] filterlim_Suc)
hence "(λn. 2 * (f x n + g x n) + 2 * (f x (Suc n) - f x n)) sums (2 * cot_pfd x + 2 * (0 - f x 0))"
by (intro sums_add sums sums_mult telescope_sums assms)
also have "(λn. 2 * (f x n + g x n) + 2 * (f x (Suc n) - f x n)) = h x"
by (simp add: h_def algebra_simps fun_eq_iff)
finally have *: "h x sums (2 * cot_pfd x - 2 * f x 0)"
by simp
have "(λn. sum (h x) {n * 2..<n * 2 + 2}) sums (2 * cot_pfd x - 2 * f x 0)"
using sums_group[OF *, of 2] by simp
also have "(λn. sum (h x) {n*2..<n*2+2}) = (λn. h x (2 * n) + h x (2 * n + 1))"
by (simp add: mult_ac)
finally have sum2: "(λn. h x (2 * n) + h x (2 * n + 1)) sums (2 * cot_pfd x - 2 * f x 0)" .
have "cot_pfd (x / 2) + cot_pfd ((x + 1) / 2) = 2 * cot_pfd x - 2 * f x 0"
using sum1 sum2 sums_unique2 by blast
also have "2 * f x 0 = 2 / (x + 1)"
by (simp add: f_def)
finally show ?thesis by algebra
qed
lemma cot_pfd_funeq_real:
fixes x :: real
assumes "x ∉ ℤ"
shows "2 * cot_pfd x = cot_pfd (x / 2) + cot_pfd ((x + 1) / 2) + 2 / (x + 1)"
proof -
have "complex_of_real (2 * cot_pfd x) = 2 * cot_pfd (complex_of_real x)"
by simp
also have "… = complex_of_real (cot_pfd (x / 2) + cot_pfd ((x + 1) / 2) + 2 / (x + 1))"
using assms by (subst cot_pfd_funeq_complex) (auto simp flip: cot_pfd_complex_of_real)
finally show ?thesis
by (simp only: of_real_eq_iff)
qed
subsection ‹The limit at 0›
lemma cot_pfd_real_tendsto_0: "cot_pfd ─0→ (0 :: real)"
proof -
have "filterlim cot_pfd (nhds 0) (at (0 :: real) within ball 0 1)"
proof (rule swap_uniform_limit)
show "uniform_limit (ball 0 1)
(λN x. ∑n<N. 2 * x / (x⇧2 - (real (Suc n))⇧2)) cot_pfd sequentially"
using uniform_limit_cot_pfd_real[OF zero_le_one] by (rule uniform_limit_on_subset) auto
have "((λx. 2 * x / (x⇧2 - (real (Suc n))⇧2)) ⤏ 0) (at 0 within ball 0 1)" for n
proof (rule filterlim_mono)
show "((λx. 2 * x / (x⇧2 - (real (Suc n))⇧2)) ⤏ 0) (at 0)"
by real_asymp
qed (auto simp: at_within_le_at)
thus "∀⇩F N in sequentially.
((λx. ∑n<N. 2 * x / (x⇧2 - (real (Suc n))⇧2)) ⤏ 0) (at 0 within ball 0 1)"
by (intro always_eventually allI tendsto_null_sum)
qed auto
thus ?thesis
by (simp add: at_within_open_NO_MATCH)
qed
subsection ‹Final result›
text ‹
To show the final result, we first prove the real case using Herglotz's trick, following
the presentation in `Proofs from {THE BOOK}'.~\<^cite>‹‹Chapter~23› in "thebook"›.
›
lemma cot_pfd_formula_real:
assumes "x ∉ ℤ"
shows "pi * cot (pi * x) = 1 / x + cot_pfd x"
proof -
have ev_not_int: "eventually (λx. r x ∉ ℤ) (at x)"
if "filterlim r (at (r x)) (at x)" for r :: "real ⇒ real" and x :: real
proof (rule eventually_compose_filterlim[OF _ that])
show "eventually (λx. x ∉ ℤ) (at (r x))"
using Ints_not_limpt[of "r x"] islimpt_iff_eventually by blast
qed
text ‹
We define the function $h(z)$ as the difference of the left-hand side and right-hand side.
The left-hand side and right-hand side have singularities at the integers, but we will
later see that these can be removed as ‹h› tends to ‹0› there.
›
define f :: "real ⇒ real" where "f = (λx. pi * cot (pi * x))"
define g :: "real ⇒ real" where "g = (λx. 1 / x + cot_pfd x)"
define h where "h = (λx. if x ∈ ℤ then 0 else f x - g x)"
have [simp]: "h x = 0" if "x ∈ ℤ" for x
using that by (simp add: h_def)
text ‹
It is easy to see that the left-hand side and the right-hand side, and as a consequence
also our function ‹h›, are odd and periodic with period 1.
›
have odd_h: "h (-x) = -h x" for x
by (simp add: h_def minus_in_Ints_iff f_def g_def)
have per_f: "f (x + 1) = f x" for x
by (simp add: f_def algebra_simps cot_def)
have per_g: "g (x + 1) = g x" if "x ∉ ℤ" for x
using that by (simp add: g_def cot_pfd_plus_1_real)
interpret h: periodic_fun_simple' h
by standard (auto simp: h_def per_f per_g)
text ‹
‹h› tends to 0 at 0 (and thus at all the integers).
›
have h_lim: "h ─0→ 0"
proof (rule Lim_transform_eventually)
have "eventually (λx. x ∉ ℤ) (at (0 :: real))"
by (rule ev_not_int) real_asymp
thus "eventually (λx::real. pi * cot (pi * x) - 1 / x - cot_pfd x = h x) (at 0)"
by eventually_elim (simp add: h_def f_def g_def)
next
have "(λx::real. pi * cot (pi * x) - 1 / x) ─0→ 0"
unfolding cot_def by real_asymp
hence "(λx::real. pi * cot (pi * x) - 1 / x - cot_pfd x) ─0→ 0 - 0"
by (intro tendsto_intros cot_pfd_real_tendsto_0)
thus "(λx. pi * cot (pi * x) - 1 / x - cot_pfd x) ─0→ 0"
by simp
qed
text ‹
This means that our ‹h› is in fact continuous everywhere:
›
have cont_h: "continuous_on A h" for A
proof -
have "isCont h x" for x
proof (cases "x ∈ ℤ")
case True
then obtain n where [simp]: "x = of_int n"
by (auto elim: Ints_cases)
show ?thesis unfolding isCont_def
by (subst at_to_0) (use h_lim in ‹simp add: filterlim_filtermap h.plus_of_int›)
next
case False
have "continuous_on (-ℤ) (λx. f x - g x)"
by (auto simp: f_def g_def sin_times_pi_eq_0 mult.commute[of pi] intro!: continuous_intros)
hence "isCont (λx. f x - g x) x"
by (rule continuous_on_interior)
(use False in ‹auto simp: interior_open open_Compl[OF closed_Ints]›)
also have "eventually (λy. y ∈ -ℤ) (nhds x)"
using False by (intro eventually_nhds_in_open) auto
hence "eventually (λx. f x - g x = h x) (nhds x)"
by eventually_elim (auto simp: h_def)
hence "isCont (λx. f x - g x) x ⟷ isCont h x"
by (rule isCont_cong)
finally show ?thesis .
qed
thus ?thesis
by (simp add: continuous_at_imp_continuous_on)
qed
note [continuous_intros] = continuous_on_compose2[OF cont_h]
text ‹
Through the functional equations of the sine and cosine function, we can derive
the following functional equation for ‹f› that holds for all non-integer reals:
›
have eq_f: "f x = (f (x / 2) + f ((x + 1) / 2)) / 2" if "x ∉ ℤ" for x
proof -
have "x / 2 ∉ ℤ"
using that by (metis Ints_add field_sum_of_halves)
hence nz1: "sin (x/2 * pi) ≠ 0"
by (subst sin_times_pi_eq_0) auto
have "(x + 1) / 2 ∉ ℤ"
proof
assume "(x + 1) / 2 ∈ ℤ"
hence "2 * ((x + 1) / 2) - 1 ∈ ℤ"
by (intro Ints_mult Ints_diff) auto
thus False using that by (simp add: field_simps)
qed
hence nz2: "sin ((x+1)/2 * pi) ≠ 0"
by (subst sin_times_pi_eq_0) auto
have nz3: "sin (x * pi) ≠ 0"
using that by (subst sin_times_pi_eq_0) auto
have eq: "sin (pi * x) = 2 * sin (pi * x / 2) * cos (pi * x / 2)"
"cos (pi * x) = (cos (pi * x / 2))⇧2 - (sin (pi * x / 2))⇧2"
using sin_double[of "pi * x / 2"] cos_double[of "pi * x / 2"] by simp_all
show ?thesis using nz1 nz2 nz3
apply (simp add: f_def cot_def field_simps )
apply (simp add: add_divide_distrib sin_add cos_add power2_eq_square eq algebra_simps)
done
qed
text ‹
The corresponding functional equation for \<^const>‹cot_pfd› that we have already shown
leads to the same functional equation for ‹g› as we just showed for ‹f›:
›
have eq_g: "g x = (g (x / 2) + g ((x + 1) / 2)) / 2" if "x ∉ ℤ" for x
using cot_pfd_funeq_real[OF that] by (simp add: g_def)
text ‹
This then leads to the same functional equation for ‹h›, and because ‹h› is continuous
everywhere, we can extend the validity of the equation to the full domain.
›
have eq_h: "h x = (h (x / 2) + h ((x + 1) / 2)) / 2" for x
proof -
have "eventually (λx. x ∉ ℤ) (at x)" "eventually (λx. x / 2 ∉ ℤ) (at x)"
"eventually (λx. (x + 1) / 2 ∉ ℤ) (at x)"
by (rule ev_not_int; real_asymp)+
hence "eventually (λx. h x - (h (x / 2) + h ((x + 1) / 2)) / 2 = 0) (at x)"
proof eventually_elim
case (elim x)
thus ?case using eq_f[of x] eq_g[of x]
by (simp add: h_def field_simps)
qed
hence "(λx. h x - (h (x / 2) + h ((x + 1) / 2)) / 2) ─x→ 0"
by (simp add: tendsto_eventually)
moreover have "continuous_on UNIV (λx. h x - (h (x / 2) + h ((x + 1) / 2)) / 2)"
by (auto intro!: continuous_intros)
ultimately have "h x - (h (x / 2) + h ((x + 1) / 2)) / 2 = 0"
by (meson LIM_unique UNIV_I continuous_on_def)
thus ?thesis
by simp
qed
text ‹
Since ‹h› is periodic with period 1 and continuous, it must attain a global maximum ‹h›
somewhere in the interval $[0, 1]$. Let's call this maximum $m$ and let $x_0$ be some point
in the interval $[0, 1]$ such that $h(x_0) = m$.
›
define m where "m = Sup (h ` {0..1})"
have "m ∈ h ` {0..1}"
unfolding m_def
proof (rule closed_contains_Sup)
have "compact (h ` {0..1})"
by (intro compact_continuous_image cont_h) auto
thus "bdd_above (h ` {0..1})" "closed (h ` {0..1})"
by (auto intro: compact_imp_closed compact_imp_bounded bounded_imp_bdd_above)
qed auto
then obtain x0 where x0: "x0 ∈ {0..1}" "h x0 = m"
by blast
have h_le_m: "h x ≤ m" for x
proof -
have "h x = h (frac x)"
unfolding frac_def by (rule h.minus_of_int [symmetric])
also have "… ≤ m" unfolding m_def
proof (rule cSup_upper)
have "frac x ∈ {0..1}"
using frac_lt_1[of x] by auto
thus "h (frac x) ∈ h ` {0..1}"
by blast
next
have "compact (h ` {0..1})"
by (intro compact_continuous_image cont_h) auto
thus "bdd_above (h ` {0..1})"
by (auto intro: compact_imp_bounded bounded_imp_bdd_above)
qed
finally show ?thesis .
qed
text ‹
Through the functional equation for ‹h›, we can show that if ‹h› attains its maximum at
some point ‹x›, it also attains it at $\frac{1}{2} x$. By iterating this, it attains the
maximum at all points of the form $2^{-n} x_0$.
›
have h_eq_m_iter_aux: "h (x / 2) = m" if "h x = m" for x
using eq_h[of x] that h_le_m[of "x / 2"] h_le_m[of "(x + 1) / 2"] by simp
have h_eq_m_iter: "h (x0 / 2 ^ n) = m" for n
proof (induction n)
case (Suc n)
have "h (x0 / 2 ^ Suc n) = h (x0 / 2 ^ n / 2)"
by (simp add: field_simps)
also have "… = m"
by (rule h_eq_m_iter_aux) (use Suc.IH in auto)
finally show ?case .
qed (use x0 in auto)
text ‹
Since the sequence $n \mapsto 2^{-n} x_0$ tends to 0 and ‹h› is continuous, we derive ‹m = 0›.
›
have "(λn. h (x0 / 2 ^ n)) ⇢ h 0"
by (rule continuous_on_tendsto_compose[OF cont_h[of UNIV]]) (force | real_asymp)+
moreover from h_eq_m_iter have "(λn. h (x0 / 2 ^ n)) ⇢ m"
by simp
ultimately have "m = h 0"
using tendsto_unique by force
hence "m = 0"
by simp
text ‹
Since ‹h› is odd, this means that ‹h› is identically zero everywhere, and our result follows.
›
have "h x = 0"
using h_le_m[of x] h_le_m[of "-x"] ‹m = 0› odd_h[of x] by linarith
thus ?thesis
using assms by (simp add: h_def f_def g_def)
qed
text ‹
We now lift the result from the domain ‹ℝ∖ℤ› to ‹ℂ∖ℤ›. We do this by noting that ‹ℂ∖ℤ› is
connected and the point $\frac{1}{2}$ is both in ‹ℂ∖ℤ› and a limit point of ‹ℝ∖ℤ›.
›
lemma one_half_limit_point_Reals_minus_Ints: "(1 / 2 :: complex) islimpt ℝ - ℤ"
proof (rule islimptI)
fix T :: "complex set"
assume "1 / 2 ∈ T" "open T"
then obtain r where r: "r > 0" "ball (1 / 2) r ⊆ T"
using open_contains_ball by blast
define y where "y = 1 / 2 + min r (1 / 2) / 2"
have "y ∈ {0<..<1}"
using r by (auto simp: y_def)
hence "complex_of_real y ∈ ℝ - ℤ"
by (auto elim!: Ints_cases)
moreover have "complex_of_real y ≠ 1 / 2"
proof
assume "complex_of_real y = 1 / 2"
also have "1 / 2 = complex_of_real (1 / 2)"
by simp
finally have "y = 1 / 2"
unfolding of_real_eq_iff .
with r show False
by (auto simp: y_def)
qed
moreover have "complex_of_real y ∈ ball (1 / 2) r"
using ‹r > 0› by (auto simp: y_def dist_norm)
with r have "complex_of_real y ∈ T"
by blast
ultimately show "∃y∈ℝ - ℤ. y ∈ T ∧ y ≠ 1 / 2"
by blast
qed
theorem cot_pfd_formula_complex:
fixes z :: complex
assumes "z ∉ ℤ"
shows "pi * cot (pi * z) = 1 / z + cot_pfd z"
proof -
let ?f = "λz::complex. pi * cot (pi * z) - 1 / z - cot_pfd z"
have "pi * cot (pi * z) - 1 / z - cot_pfd z = 0"
proof (rule analytic_continuation[where f = ?f])
show "?f holomorphic_on -ℤ"
unfolding cot_def by (intro holomorphic_intros) (auto simp: sin_eq_0)
next
show "open (-ℤ :: complex set)" "connected (-ℤ :: complex set)"
by (auto intro!: path_connected_imp_connected path_connected_complement_countable countable_int)
next
show "ℝ - ℤ ⊆ (-ℤ :: complex set)"
by auto
next
show "(1 / 2 :: complex) islimpt ℝ - ℤ"
by (rule one_half_limit_point_Reals_minus_Ints)
next
show "1 / (2 :: complex) ∈ -ℤ"
using fraction_not_in_ints[of 2 1, where ?'a = complex] by auto
next
show "z ∈ -ℤ"
using assms by simp
next
show "?f z = 0" if "z ∈ ℝ - ℤ" for z
proof -
have "complex_of_real pi * cot (complex_of_real pi * z) - 1 / z - cot_pfd z =
complex_of_real (pi * cot (pi * Re z) - 1 / Re z - cot_pfd (Re z))"
using that by (auto elim!: Reals_cases simp: cot_of_real)
also have "… = 0"
by (subst cot_pfd_formula_real) (use that in ‹auto elim!: Reals_cases›)
finally show ?thesis .
qed
qed
thus ?thesis
by algebra
qed
end