Rectangle identity behind the shift rule of the proof notes, §0/§5.1: for F holomorphic on the strip 0 < Re t < 2, ∮_{∂([1/2,3/2]×[-T,T])} F(t) π²/sin²(πt) dt = 2πi F'(1). Proof: π²/sin²(πt) = -(π cot πt)', so by the fundamental theorem of calculus on the four edges the boundary integral equals that of F'(t) π cot(πt), which has the single simple pole t = 1 in the rectangle with residue F'(1).

noncomputable def Zeta32.Analytic.Contour.Kc (t : ℂ) : ℂ

K(t) = π²/sin²(πt).

Equations

• Zeta32.Analytic.Contour.Kc t = ↑Real.pi ^ 2 / Complex.sin (↑Real.pi * t) ^ 2

noncomputable def Zeta32.Analytic.Contour.cotK (t : ℂ) : ℂ

π cot(πt).

Equations

• Zeta32.Analytic.Contour.cotK t = ↑Real.pi * Complex.cos (↑Real.pi * t) / Complex.sin (↑Real.pi * t)

def Zeta32.Analytic.Contour.strip : Set ℂ

The open strip 0 < Re t < 2.

Equations

• Zeta32.Analytic.Contour.strip = {t : ℂ | 0 < t.re ∧ t.re < 2}

theorem Zeta32.Analytic.Contour.isOpen_strip : IsOpen strip

theorem Zeta32.Analytic.Contour.one_mem_strip : 1 ∈ strip

theorem Zeta32.Analytic.Contour.sin_pi_ne_zero_of_mem_strip {t : ℂ} (ht : t ∈ strip) (h1 : t ≠ 1) : Complex.sin (↑Real.pi * t) ≠ 0

theorem Zeta32.Analytic.Contour.hasDerivAt_sin_pi (t : ℂ) : HasDerivAt (fun (u : ℂ) => Complex.sin (↑Real.pi * u)) (Complex.cos (↑Real.pi * t) * ↑Real.pi) t

theorem Zeta32.Analytic.Contour.hasDerivAt_cos_pi (t : ℂ) : HasDerivAt (fun (u : ℂ) => Complex.cos (↑Real.pi * u)) (-Complex.sin (↑Real.pi * t) * ↑Real.pi) t

theorem Zeta32.Analytic.Contour.hasDerivAt_cotK {t : ℂ} (hs : Complex.sin (↑Real.pi * t) ≠ 0) : HasDerivAt cotK (-Kc t) t

theorem Zeta32.Analytic.Contour.continuousAt_Kc {t : ℂ} (hs : Complex.sin (↑Real.pi * t) ≠ 0) : ContinuousAt Kc t

theorem Zeta32.Analytic.Contour.continuousAt_cotK {t : ℂ} (hs : Complex.sin (↑Real.pi * t) ≠ 0) : ContinuousAt cotK t

Edges of a rectangle avoiding an interior point

def Zeta32.Analytic.Contour.rectMinus (z w p : ℂ) : Set ℂ

The closed rectangle [z, w] with the point p removed.

Equations

• Zeta32.Analytic.Contour.rectMinus z w p = Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im \ {p}

theorem Zeta32.Analytic.Contour.mem_rectMinus_bottom {z w p : ℂ} (hp : p.im ∈ Set.Ioo z.im w.im) {x : ℝ} (hx : x ∈ Set.uIcc z.re w.re) : ↑x + ↑z.im * Complex.I ∈ rectMinus z w p

theorem Zeta32.Analytic.Contour.mem_rectMinus_top {z w p : ℂ} (hp : p.im ∈ Set.Ioo z.im w.im) {x : ℝ} (hx : x ∈ Set.uIcc z.re w.re) : ↑x + ↑w.im * Complex.I ∈ rectMinus z w p

theorem Zeta32.Analytic.Contour.mem_rectMinus_right {z w p : ℂ} (hp : p.re ∈ Set.Ioo z.re w.re) {y : ℝ} (hy : y ∈ Set.uIcc z.im w.im) : ↑w.re + ↑y * Complex.I ∈ rectMinus z w p

theorem Zeta32.Analytic.Contour.mem_rectMinus_left {z w p : ℂ} (hp : p.re ∈ Set.Ioo z.re w.re) {y : ℝ} (hy : y ∈ Set.uIcc z.im w.im) : ↑z.re + ↑y * Complex.I ∈ rectMinus z w p

theorem Zeta32.Analytic.Contour.edges_intervalIntegrable {z w p : ℂ} {f : ℂ → ℂ} (hre : p.re ∈ Set.Ioo z.re w.re) (him : p.im ∈ Set.Ioo z.im w.im) (hf : ContinuousOn f (rectMinus z w p)) : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑z.im * Complex.I)) MeasureTheory.volume z.re w.re ∧ IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑w.im * Complex.I)) MeasureTheory.volume z.re w.re ∧ IntervalIntegrable (fun (y : ℝ) => f (↑w.re + ↑y * Complex.I)) MeasureTheory.volume z.im w.im ∧ IntervalIntegrable (fun (y : ℝ) => f (↑z.re + ↑y * Complex.I)) MeasureTheory.volume z.im w.im

The four edge integrals of a function continuous on the rectangle minus an interior point.

theorem Zeta32.Analytic.Contour.boundaryIntegral_add_of_continuousOn {z w p : ℂ} {f g : ℂ → ℂ} (hre : p.re ∈ Set.Ioo z.re w.re) (him : p.im ∈ Set.Ioo z.im w.im) (hf : ContinuousOn f (rectMinus z w p)) (hg : ContinuousOn g (rectMinus z w p)) : boundaryIntegral (fun (s : ℂ) => f s + g s) z w = boundaryIntegral f z w + boundaryIntegral g z w

theorem Zeta32.Analytic.Contour.boundaryIntegral_eq_zero_of_hasDerivAt {z w p : ℂ} {G f : ℂ → ℂ} (hre : p.re ∈ Set.Ioo z.re w.re) (him : p.im ∈ Set.Ioo z.im w.im) (hG : ∀ t ∈ rectMinus z w p, HasDerivAt G (f t) t) (hf : ContinuousOn f (rectMinus z w p)) : boundaryIntegral f z w = 0

Fundamental theorem of calculus on a rectangle: the boundary integral of a derivative vanishes.

The rectangle [1/2, 3/2] × [-T, T]

noncomputable def Zeta32.Analytic.Contour.zT (T : ℝ) : ℂ

Lower-left corner.

Equations

• Zeta32.Analytic.Contour.zT T = { re := 1 / 2, im := -T }

noncomputable def Zeta32.Analytic.Contour.wT (T : ℝ) : ℂ

Upper-right corner.

Equations

• Zeta32.Analytic.Contour.wT T = { re := 3 / 2, im := T }

theorem Zeta32.Analytic.Contour.one_re_mem (T : ℝ) : Complex.re 1 ∈ Set.Ioo (zT T).re (wT T).re

theorem Zeta32.Analytic.Contour.one_im_mem {T : ℝ} (hT : 0 < T) : Complex.im 1 ∈ Set.Ioo (zT T).im (wT T).im

theorem Zeta32.Analytic.Contour.rect_subset_strip (T : ℝ) : Set.uIcc (zT T).re (wT T).re ×ℂ Set.uIcc (zT T).im (wT T).im ⊆ strip

theorem Zeta32.Analytic.Contour.rectMinus_subset (T : ℝ) : rectMinus (zT T) (wT T) 1 ⊆ strip \ {1}

theorem Zeta32.Analytic.Contour.sin_ne_zero_of_mem_rectMinus {T : ℝ} {t : ℂ} (ht : t ∈ rectMinus (zT T) (wT T) 1) : Complex.sin (↑Real.pi * t) ≠ 0

noncomputable def Zeta32.Analytic.Contour.sinSlope : ℂ → ℂ

S₁(t) = sin(πt)/(t-1), extended holomorphically by S₁(1) = -π.

Equations

• Zeta32.Analytic.Contour.sinSlope = dslope (fun (u : ℂ) => Complex.sin (↑Real.pi * u)) 1

theorem Zeta32.Analytic.Contour.sin_eq_mul_sinSlope (t : ℂ) : Complex.sin (↑Real.pi * t) = (t - 1) * sinSlope t

theorem Zeta32.Analytic.Contour.sinSlope_one : sinSlope 1 = -↑Real.pi

theorem Zeta32.Analytic.Contour.differentiable_sinSlope : Differentiable ℂ sinSlope

theorem Zeta32.Analytic.Contour.sinSlope_ne_zero {t : ℂ} (ht : t ∈ strip) : sinSlope t ≠ 0

theorem Zeta32.Analytic.Contour.boundaryIntegral_mul_Kc {F : ℂ → ℂ} (hF : DifferentiableOn ℂ F strip) {T : ℝ} (hT : 0 < T) : boundaryIntegral (fun (t : ℂ) => F t * Kc t) (zT T) (wT T) = 2 * ↑Real.pi * Complex.I * deriv F 1

Rectangle identity.