Instances For
Instances For
A RectangleIntegral of a function f is one over a rectangle
determined by z and w in ℂ.
Equations
Instances For
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
Instances For
Equations
Instances For
Equations
Instances For
Instances For
Equations
- VerticalIntegral' f σ = (1 / (2 * ↑Real.pi * Complex.I)) • VerticalIntegral f σ
Instances For
A function is HolomorphicOn a set if it is complex
differentiable on that set.
Equations
- HolomorphicOn f s = DifferentiableOn ℂ f s
Instances For
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)
Instances For
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).
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.
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).
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
Instances For
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.
Instances For
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
Instances For
The Residue Theorem on a rectangle for functions with simple poles.