Contour integrals over rectangles

TheoremArctangent integral#✓fully proved

For real numbers \(a\), \(b\) and \(d\) with \(d \ne 0\), \(\int_a^b \frac{d}{x^2 + d^2}\,dx = \arctan\frac{b}{d} - \arctan\frac{a}{d}\).

theorem integral_div_add_sq {d a b : ℝ} (hc : d ≠ 0) :
    ∫ x : ℝ in a..b, d / (x ^ 2 + d ^ 2) = arctan (b / d) - arctan (a / d)
Used by 2
Used byDifference of horizontal integrals of the reciprocal · Integral of \(1/(c + iy)\) over a symmetric interval

TheoremIntegral of an odd function over a symmetric interval#✓fully proved

If \(f : \mathbb{R} \to \mathbb{R}\) satisfies \(f(-x) = -f(x)\) for every real \(x\), then \(\int_{-T}^{T} f(x)\,dx = 0\) for every real \(T\).

theorem odd_integral_eq_zero {f : ℝ → ℝ} (hodd : ∀ x, f (-x) = -f x) (T : ℝ) :
    ∫ x : ℝ in (-T)..T, f x = 0
Used by 1
Used byIntegral of \(1/(c + iy)\) over a symmetric interval

TheoremIntegral of \(1/(c + iy)\) over a symmetric interval#✓fully proved

For real numbers \(c \ne 0\) and \(T \ge 0\), \(\int_{-T}^{T} \frac{1}{c + iy}\,dy = 2\arctan(T/c)\), where the integrand is complex valued and the integral is taken over the real variable \(y\).

theorem vertical_side_one_div {c T : ℝ} (hc : c ≠ 0) (hT : 0 ≤ T) :
    ∫ y : ℝ in (-T)..T, (1 : ℂ) / (c + y * Complex.I) = 2 * arctan (T / c)
Uses 2 · Used by 2
Proof usesArctangent integral · Integral of an odd function over a symmetric interval
Used byRectangle integral of \(1/s\) around the origin · Rectangle integral of \(1/s\) with the pole outside

TheoremDifference of horizontal integrals of the reciprocal#✓fully proved

Let \(a \le b\) and \(T \ne 0\) be real numbers. Then \(\int_a^b \frac{dx}{x - iT} - \int_a^b \frac{dx}{x + iT} = 2i\left(\arctan\frac{b}{T} - \arctan\frac{a}{T}\right)\).

theorem horiz_diff_one_div {a b T : ℝ} (hT : T ≠ 0) (hab : a ≤ b) :
    (∫ x : ℝ in a..b, (1 : ℂ) / (x + -T * Complex.I))
      - (∫ x : ℝ in a..b, (1 : ℂ) / (x + T * Complex.I))
      = 2 * Complex.I * (arctan (b / T) - arctan (a / T))
Uses 1 · Used by 2
Proof usesArctangent integral
Used byRectangle integral of \(1/s\) around the origin · Rectangle integral of \(1/s\) with the pole outside

TheoremRectangle integral of \(1/s\) around the origin#✓fully proved

Let \(a, b, T\) be real numbers with \(a < 0 < b\) and \(T > 0\). Then

\[\int_a^b \frac{dx}{x - iT} - \int_a^b \frac{dx}{x + iT} + i \left( \int_{-T}^{T} \frac{dy}{b + iy} - \int_{-T}^{T} \frac{dy}{a + iy} \right) = 2\pi i,\]

that is, the integral of \(1/s\) over the positively oriented boundary of the rectangle with corners \(a - iT\) and \(b + iT\) equals \(2\pi i\).

theorem boundary_rect_one_div {a b T : ℝ} (ha : a < 0) (hb : 0 < b) (hT : 0 < T) :
    (∫ x : ℝ in a..b, (1 : ℂ) / (x + -T * Complex.I))
      - (∫ x : ℝ in a..b, (1 : ℂ) / (x + T * Complex.I))
      + Complex.I * ((∫ y : ℝ in (-T)..T, (1 : ℂ) / (b + y * Complex.I))
        - (∫ y : ℝ in (-T)..T, (1 : ℂ) / (a + y * Complex.I)))
      = 2 * Real.pi * Complex.I
Uses 2 · Used by 3
Proof usesDifference of horizontal integrals of the reciprocal · Integral of \(1/(c + iy)\) over a symmetric interval
Used byRectangle integral of \(1/z\) around the origin · Newman's Tauberian theorem · Rectangle integral of \(y^s/s\) around the origin

TheoremRectangle integral of \(1/s\) with the pole outside#✓fully proved

Let \(a, b, T\) be real numbers with \(0 < a \le b\) and \(T > 0\). Then

\[\int_a^b \frac{dx}{x - iT} - \int_a^b \frac{dx}{x + iT} + i \left( \int_{-T}^{T} \frac{dy}{b + iy} - \int_{-T}^{T} \frac{dy}{a + iy} \right) = 0,\]

that is, the integral of \(1/s\) over the positively oriented boundary of the rectangle with corners \(a - iT\) and \(b + iT\) vanishes.

theorem boundary_rect_one_div_outside {a b T : ℝ} (ha : 0 < a) (hab : a ≤ b)
    (hT : 0 < T) :
    (∫ x : ℝ in a..b, (1 : ℂ) / (x + -T * Complex.I))
      - (∫ x : ℝ in a..b, (1 : ℂ) / (x + T * Complex.I))
      + Complex.I * ((∫ y : ℝ in (-T)..T, (1 : ℂ) / (b + y * Complex.I))
        - (∫ y : ℝ in (-T)..T, (1 : ℂ) / (a + y * Complex.I)))
      = 0
Uses 2 · Used by 1
Proof usesDifference of horizontal integrals of the reciprocal · Integral of \(1/(c + iy)\) over a symmetric interval
Used byRectangle integral of \(y^s/s\) with the pole outside

StructureRectilinear rectangle#✓fully proved

A rectilinear rectangle is an axis-parallel rectangle in the complex plane, recorded by an ordered pair of complex numbers \(z\) and \(w\), its first and second corner, which are opposite corners of the rectangle.

Degenerate rectangles, in which \(z\) and \(w\) have the same real part or the same imaginary part, are allowed. The corners and their order determine the orientation of the boundary integral over the rectangle, and the boundary integral over a degenerate rectangle is zero.

structure RectilinearRectangle where
  first : ℂ
  second : ℂ
Used by 23
Used byBoundary integral over a rectangle · Cauchy–Goursat theorem for rectangles · Cauchy kernel with the pole outside a rectangle · Gluing rectangles along a horizontal side · Rectangle integral of \(1/z\) around the origin · Translating the Cauchy kernel to the origin · Rectangle integral of the Cauchy kernel at an interior point · Gluing rectangles along a vertical side · Carrier of an axis-parallel rectangle · Rectangle filling supported in a set · Rectilinear cycles homologous in a set · Winding index as an additive map · Rectangle index vanishes outside the rectangle · Contour integral over a rectilinear cycle · Additivity of the contour integral in the cycle · Contour integration as an additive map · Homologous rectilinear cycles have equal integrals · Cauchy–Goursat theorem for rectilinear cycles · Reversing a cycle negates its integral · Integral over a difference of cycles · Rectangle with given coordinate bounds · The cycle of a single rectangle · Rectilinear cycle

DefinitionRectangle with given coordinate bounds#✓fully proved

For real numbers \(x_0, x_1, y_0, y_1\), this is the rectilinear rectangle whose first corner is \(x_0 + i y_0\) and whose second corner is \(x_1 + i y_1\).

noncomputable def ofBounds (x₀ x₁ y₀ y₁ : ℝ) : RectilinearRectangle where
  first := (x₀ : ℂ) + (y₀ : ℂ) * Complex.I
  second := (x₁ : ℂ) + (y₁ : ℂ) * Complex.I
Uses 1 · Used by 5
Statement usesRectilinear rectangle
Used byGluing rectangles along a horizontal side · Rectangle integral of \(1/z\) around the origin · Translating the Cauchy kernel to the origin · Rectangle integral of the Cauchy kernel at an interior point · Gluing rectangles along a vertical side

DefinitionCarrier of an axis-parallel rectangle#✓fully proved

For an axis-parallel rectangle with opposite corners \(z\) and \(w\), its carrier is the closed rectangle of all \(u \in \mathbb{C}\) such that \(\operatorname{Re} u\) lies in the closed interval with endpoints \(\operatorname{Re} z\) and \(\operatorname{Re} w\), and \(\operatorname{Im} u\) lies in the closed interval with endpoints \(\operatorname{Im} z\) and \(\operatorname{Im} w\).

def carrier (r : RectilinearRectangle) : Set ℂ :=
  Complex.Rectangle r.first r.second
Uses 1 · Used by 6
Statement usesRectilinear rectangle
Used byCauchy–Goursat theorem for rectangles · Cauchy kernel with the pole outside a rectangle · Rectangle integral of the Cauchy kernel at an interior point · Rectangle filling supported in a set · Rectangle index vanishes outside the rectangle · Cauchy–Goursat theorem for rectilinear cycles

DefinitionBoundary integral over a rectangle#✓fully proved

Let \(E\) be a complex Banach space and let \(R\) be a rectilinear rectangle with first corner \(z\) and second corner \(w\). The boundary integral of a function \(f : \mathbb{C} \to E\) over \(R\) is

\[\int_{\operatorname{Re} z}^{\operatorname{Re} w} f(x + i \operatorname{Im} z)\,dx - \int_{\operatorname{Re} z}^{\operatorname{Re} w} f(x + i \operatorname{Im} w)\,dx + i \int_{\operatorname{Im} z}^{\operatorname{Im} w} f(\operatorname{Re} w + iy)\,dy - i \int_{\operatorname{Im} z}^{\operatorname{Im} w} f(\operatorname{Re} z + iy)\,dy,\]

where each integral is an oriented Bochner interval integral, so \(\int_a^b = -\int_b^a\).

The corner order determines the sign; when \(\operatorname{Re} z \le \operatorname{Re} w\) and \(\operatorname{Im} z \le \operatorname{Im} w\) this is the integral of \(f\) over the positively oriented boundary of the rectangle.

noncomputable def boundaryIntegral {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] [CompleteSpace E] (r : RectilinearRectangle) (f : ℂ → E) : E :=
  (∫ x : ℝ in r.first.re..r.second.re, f (x + r.first.im * Complex.I)) -
    (∫ x : ℝ in r.first.re..r.second.re, f (x + r.second.im * Complex.I)) +
      Complex.I • (∫ y : ℝ in r.first.im..r.second.im, f (r.second.re + y * Complex.I)) -
        Complex.I • (∫ y : ℝ in r.first.im..r.second.im, f (r.first.re + y * Complex.I))
Uses 1 · Used by 11
Statement usesRectilinear rectangle
Used byCauchy–Goursat theorem for rectangles · Cauchy kernel with the pole outside a rectangle · Gluing rectangles along a horizontal side · Rectangle integral of \(1/z\) around the origin · Translating the Cauchy kernel to the origin · Rectangle integral of the Cauchy kernel at an interior point · Gluing rectangles along a vertical side · Rectangle index vanishes outside the rectangle · Contour integral over a rectilinear cycle · Additivity of the contour integral in the cycle · Cauchy–Goursat theorem for rectilinear cycles

TheoremCauchy–Goursat theorem for rectangles#✓fully proved

Let \(E\) be a complex Banach space, let \(R\) be a rectilinear rectangle and let \(f : \mathbb{C} \to E\) be complex differentiable on the closed rectangle spanned by the corners of \(R\) (the carrier of \(R\)). Then the boundary integral of \(f\) over \(R\) is \(0\).

theorem boundaryIntegral_eq_zero {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] [CompleteSpace E] (r : RectilinearRectangle) {f : ℂ → E}
    (hf : DifferentiableOn ℂ f r.carrier) : r.boundaryIntegral f = 0
Uses 3 · Used by 3
Statement usesRectilinear rectangle · Boundary integral over a rectangle · Carrier of an axis-parallel rectangle
Used byCauchy kernel with the pole outside a rectangle · Rectangle index vanishes outside the rectangle · Cauchy–Goursat theorem for rectilinear cycles

TheoremGluing rectangles along a horizontal side#✓fully proved

Let \(E\) be a complex Banach space, let \(f : \mathbb{C} \to E\) and let \(x_0, x_1, y_0, y_1, y_2\) be real numbers such that the maps \(y \mapsto f(x_0 + iy)\) and \(y \mapsto f(x_1 + iy)\) are continuous on \(\mathbb{R}\). For real \(a, b, c, d\) write \(R(a, b, c, d)\) for the rectangle with corners \(a + ic\) and \(b + id\). Then the boundary integral of \(f\) over \(R(x_0, x_1, y_0, y_2)\) equals the sum of the boundary integrals of \(f\) over \(R(x_0, x_1, y_0, y_1)\) and over \(R(x_0, x_1, y_1, y_2)\).

No ordering of \(y_0, y_1, y_2\) is assumed: the common horizontal side cancels and the vertical integrals concatenate as oriented integrals.

theorem boundaryIntegral_ofBounds_horizontal_concat {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
    (f : ℂ → E) (x₀ x₁ y₀ y₁ y₂ : ℝ)
    (h₀ : Continuous fun y : ℝ ↦ f ((x₀ : ℂ) + (y : ℂ) * Complex.I))
    (h₁ : Continuous fun y : ℝ ↦ f ((x₁ : ℂ) + (y : ℂ) * Complex.I)) :
    (ofBounds x₀ x₁ y₀ y₂).boundaryIntegral f =
      (ofBounds x₀ x₁ y₀ y₁).boundaryIntegral f +
        (ofBounds x₀ x₁ y₁ y₂).boundaryIntegral f
Uses 3 · Used by 1
Statement usesBoundary integral over a rectangle · Rectangle with given coordinate bounds
Proof usesRectilinear rectangle
Used byRectangle integral of the Cauchy kernel at an interior point

TheoremGluing rectangles along a vertical side#✓fully proved

Let \(E\) be a complex Banach space, let \(f : \mathbb{C} \to E\) and let \(x_0, x_1, x_2, y_0, y_1\) be real numbers such that the maps \(x \mapsto f(x + iy_0)\) and \(x \mapsto f(x + iy_1)\) are continuous on \(\mathbb{R}\). For real \(a, b, c, d\) write \(R(a, b, c, d)\) for the rectangle with corners \(a + ic\) and \(b + id\). Then the boundary integral of \(f\) over \(R(x_0, x_2, y_0, y_1)\) equals the sum of the boundary integrals of \(f\) over \(R(x_0, x_1, y_0, y_1)\) and over \(R(x_1, x_2, y_0, y_1)\).

No ordering of \(x_0, x_1, x_2\) is assumed: the common vertical side cancels and the horizontal integrals concatenate as oriented integrals.

theorem boundaryIntegral_ofBounds_vertical_concat {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
    (f : ℂ → E) (x₀ x₁ x₂ y₀ y₁ : ℝ)
    (h₀ : Continuous fun x : ℝ ↦ f ((x : ℂ) + (y₀ : ℂ) * Complex.I))
    (h₁ : Continuous fun x : ℝ ↦ f ((x : ℂ) + (y₁ : ℂ) * Complex.I)) :
    (ofBounds x₀ x₂ y₀ y₁).boundaryIntegral f =
      (ofBounds x₀ x₁ y₀ y₁).boundaryIntegral f +
        (ofBounds x₁ x₂ y₀ y₁).boundaryIntegral f
Uses 3
Statement usesBoundary integral over a rectangle · Rectangle with given coordinate bounds
Proof usesRectilinear rectangle

TheoremCauchy kernel with the pole outside a rectangle#✓fully proved

Let \(R\) be a rectilinear rectangle and let \(w\) be a complex number that does not lie in the closed rectangle spanned by the corners of \(R\) (the carrier of \(R\)). Then the boundary integral of \(z \mapsto 1/(z - w)\) over \(R\) is \(0\).

theorem boundaryIntegral_inv_sub_eq_zero_of_not_mem_carrier
    (r : RectilinearRectangle) {w : ℂ} (hw : w ∉ r.carrier) :
    r.boundaryIntegral (fun z : ℂ ↦ (z - w)⁻¹) = 0
Uses 4 · Used by 1
Statement usesRectilinear rectangle · Boundary integral over a rectangle · Carrier of an axis-parallel rectangle
Proof usesCauchy–Goursat theorem for rectangles
Used byRectangle integral of the Cauchy kernel at an interior point

TheoremRectangle integral of \(1/z\) around the origin#✓fully proved

Let \(a, b, T\) be real numbers with \(a < 0 < b\) and \(T > 0\). Then the boundary integral of \(z \mapsto 1/z\) over the rectangle with corners \(a - iT\) and \(b + iT\) equals \(2\pi i\).

theorem boundaryIntegral_ofBounds_inv_eq_two_pi_mul_I {a b T : ℝ}
    (ha : a < 0) (hb : 0 < b) (hT : 0 < T) :
    (ofBounds a b (-T) T).boundaryIntegral (fun z : ℂ ↦ z⁻¹) =
      (2 * Real.pi : ℂ) * Complex.I
Uses 4 · Used by 1
Statement usesBoundary integral over a rectangle · Rectangle with given coordinate bounds
Proof usesRectangle integral of \(1/s\) around the origin · Rectilinear rectangle
Used byRectangle integral of the Cauchy kernel at an interior point

TheoremTranslating the Cauchy kernel to the origin#✓fully proved

For all real numbers \(x_0, x_1, y_0, y_1\) and every complex number \(w\), the boundary integral of \(z \mapsto 1/(z - w)\) over the rectangle with corners \(x_0 + iy_0\) and \(x_1 + iy_1\) equals the boundary integral of \(z \mapsto 1/z\) over the rectangle with corners \((x_0 - \operatorname{Re} w) + i(y_0 - \operatorname{Im} w)\) and \((x_1 - \operatorname{Re} w) + i(y_1 - \operatorname{Im} w)\).

theorem boundaryIntegral_ofBounds_inv_sub_eq_translate
    (x₀ x₁ y₀ y₁ : ℝ) (w : ℂ) :
    (ofBounds x₀ x₁ y₀ y₁).boundaryIntegral (fun z : ℂ ↦ (z - w)⁻¹) =
      (ofBounds (x₀ - w.re) (x₁ - w.re) (y₀ - w.im) (y₁ - w.im)).boundaryIntegral
        (fun z : ℂ ↦ z⁻¹)
Uses 3 · Used by 1
Statement usesBoundary integral over a rectangle · Rectangle with given coordinate bounds
Proof usesRectilinear rectangle
Used byRectangle integral of the Cauchy kernel at an interior point

TheoremRectangle integral of the Cauchy kernel at an interior point#✓fully proved

Let \(x_0, x_1, y_0, y_1\) be real numbers and let \(w\) be a complex number with \(x_0 < \operatorname{Re} w < x_1\) and \(y_0 < \operatorname{Im} w < y_1\). Then the boundary integral of \(z \mapsto 1/(z - w)\) over the rectangle with corners \(x_0 + iy_0\) and \(x_1 + iy_1\) equals \(2\pi i\).

theorem boundaryIntegral_ofBounds_inv_sub_eq_two_pi_mul_I
    {x₀ x₁ y₀ y₁ : ℝ} {w : ℂ}
    (hx₀ : x₀ < w.re) (hx₁ : w.re < x₁)
    (hy₀ : y₀ < w.im) (hy₁ : w.im < y₁) :
    (ofBounds x₀ x₁ y₀ y₁).boundaryIntegral (fun z : ℂ ↦ (z - w)⁻¹) =
      (2 * Real.pi : ℂ) * Complex.I
Uses 8
Statement usesBoundary integral over a rectangle · Rectangle with given coordinate bounds
Proof usesRectilinear rectangle · Cauchy kernel with the pole outside a rectangle · Gluing rectangles along a horizontal side · Rectangle integral of \(1/z\) around the origin · Translating the Cauchy kernel to the origin · Carrier of an axis-parallel rectangle

AbbreviationRectilinear cycle#✓fully proved

A rectilinear cycle is a finitely supported function from rectilinear rectangles to \(\mathbb{Z}\), that is, a finite formal sum \(\sum_r n_r\, r\) of rectilinear rectangles \(r\) with integer coefficients \(n_r\), read as the corresponding integer combination of oriented rectangle boundaries.

A negative coefficient reverses the orientation of the corresponding boundary.

abbrev RectilinearCycle := RectilinearRectangle →₀ ℤ
Uses 1 · Used by 12
Statement usesRectilinear rectangle
Used byRectangle filling supported in a set · Rectilinear cycles homologous in a set · Index of a rectilinear cycle · Winding index as an additive map · Contour integral over a rectilinear cycle · Additivity of the contour integral in the cycle · Contour integration as an additive map · Homologous rectilinear cycles have equal integrals · Cauchy–Goursat theorem for rectilinear cycles · Reversing a cycle negates its integral · Integral over a difference of cycles · The cycle of a single rectangle

DefinitionThe cycle of a single rectangle#✓fully proved

For a rectilinear rectangle \(r\), this is the rectilinear cycle in which \(r\) has coefficient \(1\) and every other rectangle has coefficient \(0\), that is, the boundary of \(r\) with the orientation given by its corner order.

noncomputable def ofRectangle (r : RectilinearRectangle) : RectilinearCycle :=
  Finsupp.single r 1
Uses 2 · Used by 1
Statement usesRectilinear cycle · Rectilinear rectangle
Used byRectangle index vanishes outside the rectangle

DefinitionContour integral over a rectilinear cycle#✓fully proved

Let \(E\) be a complex Banach space and \(f : \mathbb{C} \to E\). For a rectilinear cycle \(\Gamma\), a finite formal sum \(\sum_r n_r\, r\) of rectangles \(r\) with integer coefficients \(n_r\), the contour integral of \(f\) over \(\Gamma\) is \(\sum_r n_r \int_{\partial r} f\), where \(\int_{\partial r} f\) is the boundary integral of \(f\) over the oriented rectangle \(r\).

noncomputable def integral {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] [CompleteSpace E] (Γ : RectilinearCycle) (f : ℂ → E) : E :=
  Γ.sum fun r n ↦ n • r.boundaryIntegral f
Uses 3 · Used by 9
Statement usesRectilinear cycle · Rectilinear rectangle · Boundary integral over a rectangle
Used byIndex of a rectilinear cycle · Winding index as an additive map · Rectangle index vanishes outside the rectangle · Additivity of the contour integral in the cycle · Contour integration as an additive map · Homologous rectilinear cycles have equal integrals · Cauchy–Goursat theorem for rectilinear cycles · Reversing a cycle negates its integral · Integral over a difference of cycles

TheoremAdditivity of the contour integral in the cycle#✓fully proved

Let \(E\) be a complex Banach space and \(f : \mathbb{C} \to E\). For rectilinear cycles \(\Gamma\) and \(\Lambda\), the contour integral of \(f\) over \(\Gamma + \Lambda\) equals the integral of \(f\) over \(\Gamma\) plus the integral of \(f\) over \(\Lambda\).

theorem integral_add {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] [CompleteSpace E] (Γ Λ : RectilinearCycle) (f : ℂ → E) :
    integral (Γ + Λ) f = integral Γ f + integral Λ f
Uses 4 · Used by 4
Statement usesRectilinear cycle · Contour integral over a rectilinear cycle · Rectilinear rectangle
Proof usesBoundary integral over a rectangle
Used byWinding index as an additive map · Contour integration as an additive map · Reversing a cycle negates its integral · Integral over a difference of cycles

TheoremReversing a cycle negates its integral#✓fully proved

For every rectilinear cycle \(\Gamma\), every complex Banach space \(E\) and every function \(f : \mathbb{C} \to E\), the contour integral of \(f\) over \(-\Gamma\) is the negative of the contour integral of \(f\) over \(\Gamma\).

theorem integral_neg {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] [CompleteSpace E] (Γ : RectilinearCycle) (f : ℂ → E) :
    integral (-Γ) f = -integral Γ f
Uses 4 · Used by 1
Statement usesRectilinear cycle · Contour integral over a rectilinear cycle · Rectilinear rectangle
Proof usesAdditivity of the contour integral in the cycle
Used byIntegral over a difference of cycles

TheoremIntegral over a difference of cycles#✓fully proved

For rectilinear cycles \(\Gamma\) and \(\Lambda\), a complex Banach space \(E\) and a function \(f : \mathbb{C} \to E\), the contour integral of \(f\) over \(\Gamma - \Lambda\) equals the contour integral of \(f\) over \(\Gamma\) minus the contour integral of \(f\) over \(\Lambda\).

theorem integral_sub {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] [CompleteSpace E] (Γ Λ : RectilinearCycle) (f : ℂ → E) :
    integral (Γ - Λ) f = integral Γ f - integral Λ f
Uses 5 · Used by 1
Statement usesRectilinear cycle · Contour integral over a rectilinear cycle · Rectilinear rectangle
Proof usesAdditivity of the contour integral in the cycle · Reversing a cycle negates its integral
Used byHomologous rectilinear cycles have equal integrals

DefinitionContour integration as an additive map#✓fully proved

Let \(E\) be a complex Banach space and \(f : \mathbb{C} \to E\). The map sending a rectilinear cycle \(\Gamma\) to the contour integral of \(f\) over \(\Gamma\) is an additive group homomorphism from rectilinear cycles to \(E\).

noncomputable def integralAddHom {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] [CompleteSpace E] (f : ℂ → E) : RectilinearCycle →+ E where
  toFun Γ := Γ.integral f
  map_zero' := integral_zero f
  map_add' Γ Λ := integral_add Γ Λ f
Uses 4
Statement usesRectilinear cycle · Contour integral over a rectilinear cycle · Additivity of the contour integral in the cycle · Rectilinear rectangle

DefinitionRectangle filling supported in a set#✓fully proved

Let \(G \subseteq \mathbb{C}\). A rectilinear cycle \(\Gamma\), read as a filling by rectangles, is supported in \(G\) when, for every rectangle \(r\) whose coefficient in \(\Gamma\) is nonzero, the closed carrier of \(r\) is contained in \(G\).

def FillingSupportedIn (Γ : RectilinearCycle) (G : Set ℂ) : Prop :=
  ∀ r ∈ Γ.support, r.carrier ⊆ G
Uses 3 · Used by 2
Statement usesRectilinear cycle · Rectilinear rectangle · Carrier of an axis-parallel rectangle
Used byRectilinear cycles homologous in a set · Cauchy–Goursat theorem for rectilinear cycles

TheoremCauchy–Goursat theorem for rectilinear cycles#✓fully proved

Let \(E\) be a complex Banach space, let \(G \subseteq \mathbb{C}\), and let \(f : \mathbb{C} \to E\) be complex differentiable on \(G\). If \(\Gamma\) is a rectilinear cycle whose rectangle filling is supported in \(G\), that is, the closed rectangle of every rectangle occurring in \(\Gamma\) with nonzero coefficient is contained in \(G\), then the contour integral of \(f\) over \(\Gamma\) is \(0\).

theorem integral_eq_zero_of_fillingSupportedIn {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
    {Γ : RectilinearCycle} {G : Set ℂ} {f : ℂ → E}
    (hΓ : Γ.FillingSupportedIn G) (hf : DifferentiableOn ℂ f G) :
    Γ.integral f = 0
Uses 7 · Used by 1
Statement usesRectilinear cycle · Rectangle filling supported in a set · Contour integral over a rectilinear cycle
Proof usesRectilinear rectangle · Boundary integral over a rectangle · Cauchy–Goursat theorem for rectangles · Carrier of an axis-parallel rectangle
Used byHomologous rectilinear cycles have equal integrals

DefinitionRectilinear cycles homologous in a set#✓fully proved

Let \(G \subseteq \mathbb{C}\). Two rectilinear cycles \(\Gamma\) and \(\Lambda\) are homologous in \(G\) when the rectangle filling of \(\Gamma - \Lambda\) is supported in \(G\): every rectangle with nonzero coefficient in \(\Gamma - \Lambda\) has its closed carrier contained in \(G\).

def HomologousIn (Γ Λ : RectilinearCycle) (G : Set ℂ) : Prop :=
  (Γ - Λ).FillingSupportedIn G
Uses 3 · Used by 1
Statement usesRectilinear cycle · Rectangle filling supported in a set · Rectilinear rectangle
Used byHomologous rectilinear cycles have equal integrals

TheoremHomologous rectilinear cycles have equal integrals#✓fully proved

Let \(E\) be a complex Banach space, let \(G \subseteq \mathbb{C}\), and let \(f : \mathbb{C} \to E\) be complex differentiable on \(G\). If \(\Gamma\) and \(\Lambda\) are rectilinear cycles that are homologous in \(G\), that is, the closed rectangle of every rectangle occurring in \(\Gamma - \Lambda\) with nonzero coefficient is contained in \(G\), then the contour integral of \(f\) over \(\Gamma\) equals the contour integral of \(f\) over \(\Lambda\).

theorem integral_eq_of_homologousIn {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] [CompleteSpace E] {Γ Λ : RectilinearCycle}
    {G : Set ℂ} {f : ℂ → E} (hΓΛ : Γ.HomologousIn Λ G)
    (hf : DifferentiableOn ℂ f G) : Γ.integral f = Λ.integral f
Uses 6
Statement usesRectilinear cycle · Rectilinear cycles homologous in a set · Contour integral over a rectilinear cycle
Proof usesCauchy–Goursat theorem for rectilinear cycles · Integral over a difference of cycles · Rectilinear rectangle

DefinitionIndex of a rectilinear cycle#✓fully proved

For a rectilinear cycle \(\Gamma\) and a point \(w \in \mathbb{C}\), the index of \(\Gamma\) about \(w\) is \(\frac{1}{2\pi i}\int_\Gamma \frac{dz}{z - w}\), the contour integral over \(\Gamma\) of \(z \mapsto (z - w)^{-1}\), multiplied by \((2\pi i)^{-1}\).

With the conventions \(0^{-1} = 0\) and that a non-integrable integral is \(0\), the formula also has a value when \(w\) lies on the boundary of a rectangle occurring in \(\Gamma\); no geometric winding-number claim is made there.

noncomputable def index (Γ : RectilinearCycle) (w : ℂ) : ℂ :=
  ((2 * Real.pi : ℂ) * Complex.I)⁻¹ *
    Γ.integral (fun z : ℂ ↦ (z - w)⁻¹)
Uses 2 · Used by 2
Statement usesRectilinear cycle · Contour integral over a rectilinear cycle
Used byWinding index as an additive map · Rectangle index vanishes outside the rectangle

DefinitionWinding index as an additive map#✓fully proved

For a fixed point \(w \in \mathbb{C}\), the map sending a rectilinear cycle \(\Gamma\) to its index about \(w\) is an additive group homomorphism from rectilinear cycles to \(\mathbb{C}\).

noncomputable def indexAddHom (w : ℂ) : RectilinearCycle →+ ℂ where
  toFun Γ := Γ.index w
  map_zero' := by simp [index]
  map_add' Γ Λ := index_add Γ Λ w
Uses 5
Statement usesRectilinear cycle · Index of a rectilinear cycle · Contour integral over a rectilinear cycle · Additivity of the contour integral in the cycle · Rectilinear rectangle

TheoremRectangle index vanishes outside the rectangle#✓fully proved

For an axis-parallel rectangle \(r\) and a point \(w \in \mathbb{C}\) outside the closed carrier of \(r\), the index about \(w\) of the cycle consisting of the boundary of \(r\) is \(0\).

theorem index_ofRectangle_eq_zero_of_not_mem_carrier
    (r : RectilinearRectangle) {w : ℂ} (hw : w ∉ r.carrier) :
    index (ofRectangle r) w = 0
Uses 7
Statement usesIndex of a rectilinear cycle · The cycle of a single rectangle · Rectilinear rectangle · Carrier of an axis-parallel rectangle
Proof usesContour integral over a rectilinear cycle · Boundary integral over a rectangle · Cauchy–Goursat theorem for rectangles
31 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.