The Cauchy transform as a convolution

Proved

JHolomorphic.integral_inv_sub_smul_eq_lsmul_convolution

by Mazecto · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysismeasure-theory

Let $E$ be a complex normed space and $h:\mathbb C\to E$ . The Cauchy transform $z\mapsto\int_{\mathbb C}(z-\zeta)^{-1}h(\zeta)\,d\zeta$ coincides, as a function, with the convolution of the kernel $t\mapsto t^{-1}$ with $h$ , where the product is scalar multiplication. This identifies the transform with Mathlib's convolution so that the convolution API applies to it.

Formalization Note The right-hand side is (fun t : ℂ => t⁻¹) ⋆[ContinuousLinearMap.lsmul ℝ ℂ, volume] h, with E viewed as a real normed space. Both sides use the Bochner integral, so they agree also where the integrals diverge (both are $0$ there).

Preamble

import Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
import Mathlib.MeasureTheory.Measure.Lebesgue.Complex
import Mathlib.Analysis.SpecialFunctions.Integrability.Basic
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Convolution
import Mathlib.Analysis.Calculus.ContDiff.Basic

Formal statement

namespace JHolomorphic

open MeasureTheory Metric Filter Topology Set
open scoped ContDiff ENNReal Convolution

/-- The Cauchy transform `z ↦ ∫ (z - ζ)⁻¹ • h ζ dζ` is the Mathlib convolution of the kernel `t ↦ t⁻¹` with `h`, taken with the real bilinear map `lsmul ℝ ℂ`. -/
theorem integral_inv_sub_smul_eq_lsmul_convolution {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] (h : ℂ → E) :
    (fun z => ∫ ζ, (z - ζ)⁻¹ • h ζ) =
      (fun t : ℂ => t⁻¹) ⋆[(ContinuousLinearMap.lsmul ℝ ℂ : ℂ →L[ℝ] E →L[ℝ] E), volume] h := by
  sorry

end JHolomorphic

Source

Used for C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 2, Lemma 2.24

View graph