noncomputable def HIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (x₁ x₂ y : ℝ) : E

Equations

• HIntegral f x₁ x₂ y = ∫ (x : ℝ) in x₁..x₂, f (↑x + ↑y * Complex.I)

noncomputable def VIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (x y₁ y₂ : ℝ) : E

Equations

• VIntegral f x y₁ y₂ = Complex.I • ∫ (y : ℝ) in y₁..y₂, f (↑x + ↑y * Complex.I)

noncomputable def HIntegral' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (x₁ x₂ y : ℝ) : E

Equations

• HIntegral' f x₁ x₂ y = (1 / (2 * ↑Real.pi * Complex.I)) • HIntegral f x₁ x₂ y

noncomputable def VIntegral' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (x y₁ y₂ : ℝ) : E

Equations

• VIntegral' f x y₁ y₂ = (1 / (2 * ↑Real.pi * Complex.I)) • VIntegral f x y₁ y₂

theorem HIntegral_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x₁ x₂ y : ℝ} : HIntegral f x₁ x₂ y = -HIntegral f x₂ x₁ y

theorem VIntegral_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x y₁ y₂ : ℝ} : VIntegral f x y₁ y₂ = -VIntegral f x y₂ y₁

noncomputable def RectangleIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) : E

A RectangleIntegral of a function f is one over a rectangle determined by z and w in ℂ.

Equations

• RectangleIntegral f z w = HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im - VIntegral f z.re z.im w.im

@[reducible, inline]

noncomputable abbrev RectangleIntegral' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) : E

A RectangleIntegral' of a function f is one over a rectangle determined by z and w in ℂ, divided by 2 * π * I.

Equations

• RectangleIntegral' f z w = (1 / (2 * ↑Real.pi * Complex.I)) • RectangleIntegral f z w

noncomputable def UpperUIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (σ σ' T : ℝ) : E

Equations

• UpperUIntegral f σ σ' T = (HIntegral f σ σ' T + Complex.I • ∫ (y : ℝ) in Set.Ici T, f (↑σ' + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in Set.Ici T, f (↑σ + ↑y * Complex.I)

noncomputable def LowerUIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (σ σ' T : ℝ) : E

Equations

• LowerUIntegral f σ σ' T = (HIntegral f σ σ' (-T) - Complex.I • ∫ (y : ℝ) in Set.Iic (-T), f (↑σ' + ↑y * Complex.I)) + Complex.I • ∫ (y : ℝ) in Set.Iic (-T), f (↑σ + ↑y * Complex.I)

noncomputable def VerticalIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (σ : ℝ) : E

Equations

• VerticalIntegral f σ = Complex.I • ∫ (t : ℝ), f (↑σ + ↑t * Complex.I)

@[reducible, inline]

noncomputable abbrev VerticalIntegral' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (σ : ℝ) : E

Equations

• VerticalIntegral' f σ = (1 / (2 * ↑Real.pi * Complex.I)) • VerticalIntegral f σ

theorem verticalIntegral_split_three {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {σ : ℝ} (a b : ℝ) (hf : MeasureTheory.Integrable (fun (t : ℝ) => f (↑σ + ↑t * Complex.I)) MeasureTheory.volume) : VerticalIntegral f σ = (Complex.I • ∫ (t : ℝ) in Set.Iic a, f (↑σ + ↑t * Complex.I)) + VIntegral f σ a b + Complex.I • ∫ (t : ℝ) in Set.Ici b, f (↑σ + ↑t * Complex.I)

theorem DiffVertRect_eq_UpperLowerUs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {σ σ' T : ℝ} (f_int_σ : MeasureTheory.Integrable (fun (t : ℝ) => f (↑σ + ↑t * Complex.I)) MeasureTheory.volume) (f_int_σ' : MeasureTheory.Integrable (fun (t : ℝ) => f (↑σ' + ↑t * Complex.I)) MeasureTheory.volume) : VerticalIntegral f σ' - VerticalIntegral f σ - RectangleIntegral f (↑σ - Complex.I * ↑T) (↑σ' + Complex.I * ↑T) = UpperUIntegral f σ σ' T - LowerUIntegral f σ σ' T

@[reducible, inline]

abbrev HolomorphicOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (s : Set ℂ) : Prop

A function is HolomorphicOn a set if it is complex differentiable on that set.

Equations

• HolomorphicOn f s = DifferentiableOn ℂ f s

theorem existsDifferentiableOn_of_bddAbove {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {s : Set ℂ} {c : ℂ} (hc : s ∈ nhds c) (hd : HolomorphicOn f (s \ {c})) (hb : BddAbove (norm ∘ f '' (s \ {c}))) : ∃ (g : ℂ → E), HolomorphicOn g s ∧ Set.EqOn f g (s \ {c})

theorem HolomorphicOn.vanishesOnRectangle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z w : ℂ} [CompleteSpace E] {U : Set ℂ} (f_holo : HolomorphicOn f U) (hU : z.Rectangle w ⊆ U) : RectangleIntegral f z w = 0

theorem RectangleIntegral_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {z w : ℂ} (h : Set.EqOn f g (RectangleBorder z w)) : RectangleIntegral f z w = RectangleIntegral g z w

theorem RectangleIntegral'_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {z w : ℂ} (h : Set.EqOn f g (RectangleBorder z w)) : RectangleIntegral' f z w = RectangleIntegral' g z w

theorem rectangleIntegral_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) : RectangleIntegral f z w = RectangleIntegral f w z

theorem rectangleIntegral_symm_re {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) : RectangleIntegral f (↑w.re + ↑z.im * Complex.I) (↑z.re + ↑w.im * Complex.I) = -RectangleIntegral f z w

def RectangleBorderIntegrable {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (z w : ℂ) : Prop

Equations

• RectangleBorderIntegrable f z w = (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)

theorem RectangleBorderIntegrable.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {z w : ℂ} {f g : ℂ → E} (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) : RectangleIntegral (f + g) z w = RectangleIntegral f z w + RectangleIntegral g z w

theorem ContinuousOn.rectangleBorder_integrable {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {z w : ℂ} (hf : ContinuousOn f (RectangleBorder z w)) : RectangleBorderIntegrable f z w

theorem ContinuousOn.rectangleBorderIntegrable {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {z w : ℂ} (hf : ContinuousOn f (z.Rectangle w)) : RectangleBorderIntegrable f z w

theorem ContinuousOn.rectangleBorderNoPIntegrable {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {z w p : ℂ} (hf : ContinuousOn f (z.Rectangle w \ {p})) (pNotOnBorder : p ∉ RectangleBorder z w) : RectangleBorderIntegrable f z w

theorem HolomorphicOn.rectangleBorderIntegrable' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z w p : ℂ} (hf : HolomorphicOn f (z.Rectangle w \ {p})) (hp : z.Rectangle w ∈ nhds p) : RectangleBorderIntegrable f z w

theorem HolomorphicOn.rectangleBorderIntegrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z w : ℂ} (hf : HolomorphicOn f (z.Rectangle w)) : RectangleBorderIntegrable f z w

theorem RectangleIntegralHSplit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a x₀ x₁ y₀ y₁ : ℝ} (f_int_x₀_a_bot : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑y₀ * Complex.I)) MeasureTheory.volume x₀ a) (f_int_a_x₁_bot : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑y₀ * Complex.I)) MeasureTheory.volume a x₁) (f_int_x₀_a_top : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑y₁ * Complex.I)) MeasureTheory.volume x₀ a) (f_int_a_x₁_top : IntervalIntegrable (fun (x : ℝ) => f (↑x + ↑y₁ * Complex.I)) MeasureTheory.volume a x₁) : RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I) = RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑a + ↑y₁ * Complex.I) + RectangleIntegral f (↑a + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I)

Given x₀ a x₁ : ℝ, and y₀ y₁ : ℝ and a function f : ℂ → ℂ so that both (t : ℝ) ↦ f(t + y₀ * I) and (t : ℝ) ↦ f(t + y₁ * I) are integrable over both t ∈ Icc x₀ a and t ∈ Icc a x₁, we have that RectangleIntegral f (x₀ + y₀ * I) (x₁ + y₁ * I) is the sum of RectangleIntegral f (x₀ + y₀ * I) (a + y₁ * I) and RectangleIntegral f (a + y₀ * I) (x₁ + y₁ * I).

theorem RectangleIntegralHSplit' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a x₀ x₁ y₀ y₁ : ℝ} (ha : a ∈ Set.uIcc x₀ x₁) (hf : RectangleBorderIntegrable f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I)) : RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I) = RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑a + ↑y₁ * Complex.I) + RectangleIntegral f (↑a + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I)

theorem RectangleIntegralVSplit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {b x₀ x₁ y₀ y₁ : ℝ} (f_int_y₀_b_left : IntervalIntegrable (fun (y : ℝ) => f (↑x₀ + ↑y * Complex.I)) MeasureTheory.volume y₀ b) (f_int_b_y₁_left : IntervalIntegrable (fun (y : ℝ) => f (↑x₀ + ↑y * Complex.I)) MeasureTheory.volume b y₁) (f_int_y₀_b_right : IntervalIntegrable (fun (y : ℝ) => f (↑x₁ + ↑y * Complex.I)) MeasureTheory.volume y₀ b) (f_int_b_y₁_right : IntervalIntegrable (fun (y : ℝ) => f (↑x₁ + ↑y * Complex.I)) MeasureTheory.volume b y₁) : RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I) = RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑b * Complex.I) + RectangleIntegral f (↑x₀ + ↑b * Complex.I) (↑x₁ + ↑y₁ * Complex.I)

theorem RectangleIntegralVSplit' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {b x₀ x₁ y₀ y₁ : ℝ} (hb : b ∈ Set.uIcc y₀ y₁) (hf : RectangleBorderIntegrable f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I)) : RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑y₁ * Complex.I) = RectangleIntegral f (↑x₀ + ↑y₀ * Complex.I) (↑x₁ + ↑b * Complex.I) + RectangleIntegral f (↑x₀ + ↑b * Complex.I) (↑x₁ + ↑y₁ * Complex.I)

theorem RectanglePullToNhdOfPole' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {z₀ z₁ z₂ z₃ p : ℂ} (h_orientation : z₀.re ≤ z₃.re ∧ z₀.im ≤ z₃.im ∧ z₁.re ≤ z₂.re ∧ z₁.im ≤ z₂.im) (hp : z₁.Rectangle z₂ ∈ nhds p) (hz : z₁.Rectangle z₂ ⊆ z₀.Rectangle z₃) (fHolo : HolomorphicOn f (z₀.Rectangle z₃ \ {p})) : RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂

theorem RectanglePullToNhdOfPole {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {z w p : ℂ} (zRe_lt_wRe : z.re ≤ w.re) (zIm_lt_wIm : z.im ≤ w.im) (hp : z.Rectangle w ∈ nhds p) (fHolo : HolomorphicOn f (z.Rectangle w \ {p})) : ∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), RectangleIntegral f z w = RectangleIntegral f (-↑c - Complex.I * ↑c + p) (↑c + Complex.I * ↑c + p)

Given f holomorphic on a rectangle z and w except at a point p, the integral of f over the rectangle with corners z and w is the same as the integral of f over a small square centered at p.

theorem RectanglePullToNhdOfPole'' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {z w p : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : z.Rectangle w ∈ nhds p) (fHolo : HolomorphicOn f (z.Rectangle w \ {p})) : ∀ᶠ (c : ℝ) in nhdsWithin 0 (Set.Ioi 0), RectangleIntegral' f z w = RectangleIntegral' f (-↑c - Complex.I * ↑c + p) (↑c + Complex.I * ↑c + p)

theorem ResidueTheoremAtOrigin_aux1c (a b : ℝ) : have f := fun (y : ℝ) => (↑y + Complex.I)⁻¹; IntervalIntegrable f MeasureTheory.volume a b

theorem ResidueTheoremAtOrigin_aux1c' (a b : ℝ) : have f := fun (y : ℝ) => (↑y - Complex.I)⁻¹; IntervalIntegrable f MeasureTheory.volume a b

theorem ResidueTheoremAtOrigin_aux2c (a b : ℝ) : have f := fun (y : ℝ) => (1 + ↑y * Complex.I)⁻¹; IntervalIntegrable f MeasureTheory.volume a b

theorem ResidueTheoremAtOrigin_aux2c' (a b : ℝ) : have f := fun (y : ℝ) => (-1 + ↑y * Complex.I)⁻¹; IntervalIntegrable f MeasureTheory.volume a b

theorem RectangleIntegral.const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w c : ℂ) : RectangleIntegral (fun (s : ℂ) => c • f s) z w = c • RectangleIntegral f z w

theorem RectangleIntegral.const_mul' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w c : ℂ) : RectangleIntegral' (fun (s : ℂ) => c • f s) z w = c • RectangleIntegral' f z w

theorem RectangleIntegral.translate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w p : ℂ) : RectangleIntegral (fun (s : ℂ) => f (s - p)) z w = RectangleIntegral f (z - p) (w - p)

theorem RectangleIntegral.translate' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w p : ℂ) : RectangleIntegral' (fun (s : ℂ) => f (s - p)) z w = RectangleIntegral' f (z - p) (w - p)

theorem Complex.inv_re_add_im {x y : ℝ} : (↑x + ↑y * I)⁻¹ = (↑x - I * ↑y) / (↑x ^ 2 + ↑y ^ 2)

theorem sq_add_sq_ne_zero {x y : ℝ} (hy : y ≠ 0) : x ^ 2 + y ^ 2 ≠ 0

theorem continuous_self_div_sq_add_sq {y : ℝ} (hy : y ≠ 0) : Continuous fun (x : ℝ) => x / (x ^ 2 + y ^ 2)

theorem integral_self_div_sq_add_sq {x₁ x₂ y : ℝ} (hy : y ≠ 0) : ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = Real.log (x₂ ^ 2 + y ^ 2) / 2 - Real.log (x₁ ^ 2 + y ^ 2) / 2

theorem integral_const_div_sq_add_sq {x₁ x₂ y : ℝ} (hy : y ≠ 0) : ∫ (x : ℝ) in x₁..x₂, y / (x ^ 2 + y ^ 2) = Real.arctan (x₂ / y) - Real.arctan (x₁ / y)

theorem integral_const_div_self_add_im {A : ℂ} {x₁ x₂ y : ℝ} (hy : y ≠ 0) : ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * Complex.I) = A * (↑(Real.log (x₂ ^ 2 + y ^ 2)) / 2 - ↑(Real.log (x₁ ^ 2 + y ^ 2)) / 2) - A * Complex.I * (↑(Real.arctan (x₂ / y)) - ↑(Real.arctan (x₁ / y)))

theorem integral_const_div_re_add_self {A : ℂ} {x y₁ y₂ : ℝ} (hx : x ≠ 0) : ∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * Complex.I) = A / Complex.I * (↑(Real.log (y₂ ^ 2 + (-x) ^ 2)) / 2 - ↑(Real.log (y₁ ^ 2 + (-x) ^ 2)) / 2) - A / Complex.I * Complex.I * (↑(Real.arctan (y₂ / -x)) - ↑(Real.arctan (y₁ / -x)))

theorem ResidueTheoremAtOrigin' {z w c : ℂ} (h1 : z.re < 0) (h2 : z.im < 0) (h3 : 0 < w.re) (h4 : 0 < w.im) : RectangleIntegral (fun (s : ℂ) => c / s) z w = 2 * Complex.I * ↑Real.pi * c

theorem ResidueTheoremInRectangle {z w p c : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : z.Rectangle w ∈ nhds p) : RectangleIntegral' (fun (s : ℂ) => c / (s - p)) z w = c

theorem ResidueTheoremAtOrigin : RectangleIntegral' (fun (s : ℂ) => 1 / s) (-1 - Complex.I) (1 + Complex.I) = 1

theorem ResidueTheoremOnRectangleWithSimplePole {f g : ℂ → ℂ} {z w p A : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : z.Rectangle w ∈ nhds p) (gHolo : HolomorphicOn g (z.Rectangle w)) (principalPart : Set.EqOn (f - fun (s : ℂ) => A / (s - p)) g (z.Rectangle w \ {p})) : RectangleIntegral' f z w = A

theorem IsBigO_to_BddAbove {f : ℂ → ℂ} {p : ℂ} (f_near_p : f =O[nhdsWithin p {p}ᶜ] 1) : ∃ U ∈ nhds p, BddAbove (norm ∘ f '' (U \ {p}))

theorem BddAbove_on_rectangle_of_bdd_near {z w p : ℂ} {f : ℂ → ℂ} (f_cont : ContinuousOn f (z.Rectangle w \ {p})) (f_near_p : f =O[nhdsWithin p {p}ᶜ] 1) : BddAbove (norm ∘ f '' (z.Rectangle w \ {p}))

theorem ResidueTheoremOnRectangleWithSimplePole' {f : ℂ → ℂ} {z w p A : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (pInRectInterior : z.Rectangle w ∈ nhds p) (fHolo : HolomorphicOn f (z.Rectangle w \ {p})) (near_p : (f - fun (s : ℂ) => A / (s - p)) =O[nhdsWithin p {p}ᶜ] 1) : RectangleIntegral' f z w = A

Residue calculus: residues, simple poles, and the rectangle residue theorem

The simple-pole residue, sumResiduesIn, the HasSimplePolesOn scaffold, and the rectangle residue theorem RectangleIntegral'_eq_sumResiduesIn. Extracted from CH2.lean as general, reusable contour-integration lemmas (see issue #1537).

def HasSimplePolesOn (f : ℂ → ℂ) (s : Set ℂ) : Prop

Every pole of f in s is at most simple: the meromorphic order is ≥ -1 everywhere on s (no poles of order ≤ -2).

Temporary scaffold. The placeholder residue below (and Mathlib's current residue-theorem API) is only correct for simple poles, so this hypothesis is added to Lemma 5.1 / Proposition 5.2 and their sub-lemmas to make them provable with the present API. It holds in the intended applications (e.g. ζ'/ζ, whose poles are all simple) and is to be removed once Mathlib gains general higher-order residue support.

Equations

• HasSimplePolesOn f s = ∀ z ∈ s, ↑(-1) ≤ meromorphicOrderAt f z

theorem HasSimplePolesOn.mono {f : ℂ → ℂ} {s t : Set ℂ} (h : HasSimplePolesOn f t) (hst : s ⊆ t) : HasSimplePolesOn f s

noncomputable def residue (f : ℂ → ℂ) (z₀ : ℂ) : ℂ

Placeholder definition — valid only for simple poles. The residue of f at z₀, defined as the simple-pole limit lim_{z → z₀} (z - z₀) · f z (matching the convention of Phi_circ.residue / Phi_star.residue). At a point of analyticity this is 0 and at a simple pole it is the usual residue, but at a higher-order or essential singularity the limit diverges and this returns a junk value.

A general complex residue (and the residue theorem) is planned for Mathlib but not yet available, so results stated in terms of this residue are likely not provable in full generality with the current API. This is a deliberate stopgap, to be replaced with the robust notion once the Mathlib residue-theorem API lands.

Equations

• residue f z₀ = (nhdsWithin z₀ {z₀}ᶜ).limUnder fun (z : ℂ) => (z - z₀) * f z

noncomputable def sumResiduesIn (f : ℂ → ℂ) (S : Set ℂ) : ℂ

The sum of residues of f over a region S, as a tsum over S. Points of analyticity contribute 0, so this is effectively the sum over the poles of f in S; when finitely many poles lie in S the tsum equals the finite sum of their residues, regardless of |S|. (With infinitely many poles, summability must be assumed for the value to be meaningful.)

Equations

• sumResiduesIn f S = ∑' (z : ↑S), residue f ↑z

theorem residue_eq_of_tendsto {f : ℂ → ℂ} {p c : ℂ} (h : Filter.Tendsto (fun (z : ℂ) => (z - p) * f z) (nhdsWithin p {p}ᶜ) (nhds c)) : residue f p = c

theorem residue_analyticAt_eq_zero {f : ℂ → ℂ} {p : ℂ} (hf : AnalyticAt ℂ f p) : residue f p = 0

theorem simplePole_sub_residue_isBigO_one {f : ℂ → ℂ} {p : ℂ} (hf : MeromorphicAt f p) (hord : meromorphicOrderAt f p = ↑(-1)) : (f - fun (z : ℂ) => residue f p / (z - p)) =O[nhdsWithin p {p}ᶜ] 1

theorem verticalPath_not_eventuallyConst (r x : ℝ) : ¬Filter.EventuallyConst (fun (y : ℝ) => ↑r + ↑y * Complex.I) (nhds x)

theorem RectangleIntegral'_eq_sumResiduesIn {f : ℂ → ℂ} {z w : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im) (f_mero : MeromorphicOn f (z.Rectangle w)) (f_no_poles_boundary : Disjoint (RectangleBorder z w) {z : ℂ | meromorphicOrderAt f z < 0}) (f_poles_finite : (z.Rectangle w ∩ {z : ℂ | meromorphicOrderAt f z < 0}).Finite) (f_simple_poles : HasSimplePolesOn f (z.Rectangle w)) : RectangleIntegral' f z w = sumResiduesIn f (z.Rectangle w ∩ {z : ℂ | meromorphicOrderAt f z < 0})

The Residue Theorem on a rectangle for functions with simple poles.

theorem residue_eq_zero_of_not_pole_of_meromorphicAt {F : ℂ → ℂ} {s : ℂ} (hs_mero : MeromorphicAt F s) (hs_not_pole : 0 ≤ meromorphicOrderAt F s) : residue F s = 0

theorem sumResiduesIn_inter_eq_of_set_eq {F : ℂ → ℂ} {Rn S2 P : Set ℂ} (h_set_eq : Rn ∩ P = S2 ∩ P) (h_residue_zero : ∀ s ∈ S2, s ∉ P → residue F s = 0) : sumResiduesIn F (Rn ∩ P) = sumResiduesIn F S2