Cotangent #
This file contains lemmas about the cotangent function, including useful series expansions.
In particular, we prove that
π * cot (π * z) = π * I - 2 * π * I * ∑' n : ℕ, Complex.exp (2 * π * I * z) ^ n
as well as the infinite sum representation of cotangent (also known as the Mittag-Leffler
expansion): π * cot (π * z) = 1 / z + ∑' n : ℕ+, (1 / (z - n) + 1 / (z + n))
.
theorem
tendsto_euler_sin_prod'
{x : ℂ}
(h0 : x ≠ 0)
:
Filter.Tendsto (fun (n : ℕ) => ∏ i ∈ Finset.range n, (1 + sineTerm x i)) Filter.atTop
(nhds (Complex.sin (↑Real.pi * x) / (↑Real.pi * x)))
theorem
HasProdLocallyUniformlyOn_euler_sin_prod :
HasProdLocallyUniformlyOn (fun (n : ℕ) (z : ℂ) => 1 + sineTerm z n)
(fun (x : ℂ) => Complex.sin (↑Real.pi * x) / (↑Real.pi * x)) Complex.integerComplement
sin π z
is non vanishing on the complement of the integers in ℂ
.
theorem
cot_pi_mul_contDiffWithinAt
{x : ℂ}
(k : ℕ∞)
(hx : x ∈ Complex.integerComplement)
:
ContDiffWithinAt ℂ (↑k) (fun (x : ℂ) => (↑Real.pi * x).cot) UpperHalfPlane.upperHalfPlaneSet x
theorem
tendsto_logDeriv_euler_sin_div
{x : ℂ}
(hx : x ∈ Complex.integerComplement)
:
Filter.Tendsto (fun (n : ℕ) => logDeriv (fun (z : ℂ) => ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) Filter.atTop
(nhds (logDeriv (fun (t : ℂ) => Complex.sin (↑Real.pi * t) / (↑Real.pi * t)) x))
theorem
logDeriv_prod_sineTerm_eq_sum_cotTerm
{x : ℂ}
(hx : x ∈ Complex.integerComplement)
(n : ℕ)
:
logDeriv (fun (z : ℂ) => ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x = ∑ j ∈ Finset.range n, cotTerm x j
theorem
tendsto_logDeriv_euler_cot_sub
{x : ℂ}
(hx : x ∈ Complex.integerComplement)
:
Filter.Tendsto (fun (n : ℕ) => ∑ j ∈ Finset.range n, cotTerm x j) Filter.atTop
(nhds (↑Real.pi * (↑Real.pi * x).cot - 1 / x))
theorem
summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm
{k : ℕ}
(hk : 1 ≤ k)
:
SummableLocallyUniformlyOn
(fun (n : ℕ) => iteratedDerivWithin k (fun (z : ℂ) => cotTerm z n) UpperHalfPlane.upperHalfPlaneSet)
UpperHalfPlane.upperHalfPlaneSet
theorem
differentiableOn_iteratedDerivWithin_cotTerm
(n l : ℕ)
:
DifferentiableOn ℂ (iteratedDerivWithin l (fun (z : ℂ) => cotTerm z n) UpperHalfPlane.upperHalfPlaneSet)
UpperHalfPlane.upperHalfPlaneSet
theorem
iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum
{z : ℂ}
{k : ℕ}
(hk : 1 ≤ k)
(hz : z ∈ UpperHalfPlane.upperHalfPlaneSet)
:
theorem
iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow
{k : ℕ}
(hk : 1 ≤ k)
{z : ℂ}
(hz : z ∈ UpperHalfPlane.upperHalfPlaneSet)
:
The series expansion of the iterated derivative of π cot (π z)
.