Parameterized contour integrals (L4.2a)

Contour integrals along a parameterized closed curve γ : ℝ → ℂ, defined as the interval integral ∫ t in 0..2π, deriv γ t • f (γ t). This is exactly the shape of Mathlib's circleIntegral (the special case γ = circleMap c R), so the circle results of CircleCauchy.lean transfer by rfl, while general smooth boundaries of convex domains — the contours of the Crouzeix–Palencia argument — become available.

Main declarations

• ContourIntegrable f γ — integrability of t ↦ deriv γ t • f (γ t) on [0, 2π].
• contourIntegral f γ — the contour integral ∫ t in 0..2π, deriv γ t • f (γ t).
• contourIntegral_circleMap, contourIntegrable_circleMap_iff — agreement with Mathlib's circleIntegral / CircleIntegrable for γ = circleMap c R.
• ContourIntegrable.of_continuousOn — continuity of the curve derivative and of f on the trace gives integrability.
• contourIntegral_add, contourIntegral_sub, contourIntegral_neg, contourIntegral_smul — linearity in the integrand.
• ContinuousLinearMap.contourIntegral_comp_comm, contourIntegral_const_mul, contourIntegral_mul_const — continuous linear maps and constant algebra factors commute with the integral.
• norm_contourIntegral_le_of_norm_le_const — the length-type bound ‖∫‖ ≤ 2π C.
• contourIntegral_eq_sub_of_hasDerivAt, contourIntegral_eq_zero_of_hasDerivAt_of_closed — the fundamental theorem of calculus along γ: an integrand with a global primitive integrates to the boundary difference, hence to 0 along a closed curve (Cauchy's theorem for integrands with a primitive).

def ContourIntegrable {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : ℂ → F) (γ : ℝ → ℂ) : Prop

f is integrable along the parameterized curve γ over [0, 2π]: the integrand t ↦ deriv γ t • f (γ t) is interval integrable.

Equations

• ContourIntegrable f γ = IntervalIntegrable (fun (t : ℝ) => deriv γ t • f (γ t)) MeasureTheory.volume 0 (2 * Real.pi)

noncomputable def contourIntegral {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : ℂ → F) (γ : ℝ → ℂ) : F

The contour integral ∫ t in 0..2π, γ'(t) • f (γ t) of f along the parameterized curve γ.

Equations

• contourIntegral f γ = ∫ (t : ℝ) in 0..2 * Real.pi, deriv γ t • f (γ t)

theorem contourIntegral_circleMap {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : ℂ → F) (c : ℂ) (R : ℝ) : contourIntegral f (circleMap c R) = circleIntegral f c R

Along the circle parameterization circleMap c R the contour integral is Mathlib's circleIntegral.

theorem contourIntegrable_circleMap_iff {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} {c : ℂ} (R : ℝ) : ContourIntegrable f (circleMap c R) ↔ CircleIntegrable f c R

Along the circle parameterization circleMap c R contour integrability is Mathlib's CircleIntegrable.

theorem ContourIntegrable.of_continuousOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} {γ : ℝ → ℂ} (hγ : ContinuousOn γ (Set.Icc 0 (2 * Real.pi))) (hγ' : ContinuousOn (deriv γ) (Set.Icc 0 (2 * Real.pi))) (hf : ContinuousOn f (γ '' Set.Icc 0 (2 * Real.pi))) : ContourIntegrable f γ

A function continuous on the trace of a curve with continuous derivative is contour integrable.

theorem contourIntegral_add {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f g : ℂ → F} {γ : ℝ → ℂ} (hf : ContourIntegrable f γ) (hg : ContourIntegrable g γ) : contourIntegral (fun (z : ℂ) => f z + g z) γ = contourIntegral f γ + contourIntegral g γ

theorem contourIntegral_neg {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : ℂ → F) (γ : ℝ → ℂ) : contourIntegral (fun (z : ℂ) => -f z) γ = -contourIntegral f γ

theorem contourIntegral_sub {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f g : ℂ → F} {γ : ℝ → ℂ} (hf : ContourIntegrable f γ) (hg : ContourIntegrable g γ) : contourIntegral (fun (z : ℂ) => f z - g z) γ = contourIntegral f γ - contourIntegral g γ

theorem contourIntegral_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (a : ℂ) (f : ℂ → F) (γ : ℝ → ℂ) : contourIntegral (fun (z : ℂ) => a • f z) γ = a • contourIntegral f γ

theorem ContinuousLinearMap.contourIntegral_comp_comm {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace F] [CompleteSpace G] (L : F →L[ℂ] G) {f : ℂ → F} {γ : ℝ → ℂ} (hf : ContourIntegrable f γ) : contourIntegral (fun (z : ℂ) => L (f z)) γ = L (contourIntegral f γ)

Continuous complex-linear maps commute with contour integrals.

theorem contourIntegral_const_mul {B : Type u_3} [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] {f : ℂ → B} {γ : ℝ → ℂ} (b : B) (hf : ContourIntegrable f γ) : contourIntegral (fun (z : ℂ) => b * f z) γ = b * contourIntegral f γ

A constant left factor moves through a contour integral in a complex Banach algebra.

theorem contourIntegral_mul_const {B : Type u_3} [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] {f : ℂ → B} {γ : ℝ → ℂ} (b : B) (hf : ContourIntegrable f γ) : contourIntegral (fun (z : ℂ) => f z * b) γ = contourIntegral f γ * b

A constant right factor moves through a contour integral in a complex Banach algebra.

theorem norm_contourIntegral_le_of_norm_le_const {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} {γ : ℝ → ℂ} {C : ℝ} (h : ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖deriv γ t • f (γ t)‖ ≤ C) : ‖contourIntegral f γ‖ ≤ 2 * Real.pi * C

The length-type bound: if the integrand γ'(t) • f (γ t) is bounded by C on [0, 2π], the contour integral is bounded by 2π C.

theorem contourIntegral_eq_sub_of_hasDerivAt {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {f Fp : ℂ → F} {γ : ℝ → ℂ} (hγ : ∀ t ∈ Set.Icc 0 (2 * Real.pi), DifferentiableAt ℝ γ t) (hF : ∀ t ∈ Set.Icc 0 (2 * Real.pi), HasDerivAt Fp (f (γ t)) (γ t)) (hint : ContourIntegrable f γ) : contourIntegral f γ = Fp (γ (2 * Real.pi)) - Fp (γ 0)

Fundamental theorem of calculus along a curve: if Fp is a primitive of f along the trace of the differentiable curve γ, the contour integral is the boundary difference.

theorem contourIntegral_eq_zero_of_hasDerivAt_of_closed {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f Fp : ℂ → F} {γ : ℝ → ℂ} (hγ : ∀ t ∈ Set.Icc 0 (2 * Real.pi), DifferentiableAt ℝ γ t) (hF : ∀ t ∈ Set.Icc 0 (2 * Real.pi), HasDerivAt Fp (f (γ t)) (γ t)) (hint : ContourIntegrable f γ) (hclosed : γ (2 * Real.pi) = γ 0) : contourIntegral f γ = 0

Cauchy's theorem for integrands with a global primitive: along a closed differentiable curve the contour integral of f = Fp' vanishes.