The Cauchy integrand of a continuous compactly supported function is integrable

Proved

JHolomorphic.integrable_inv_sub_smul_of_continuous

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

complex-analysismeasure-theory

Let $E$ be a complex normed space and $g:\mathbb C\to E$ continuous with compact support. For every $z\in\mathbb C$ the function $\zeta\mapsto (z-\zeta)^{-1}g(\zeta)$ is Lebesgue integrable on $\mathbb C$ , so the Cauchy transform of $g$ is defined by a genuinely convergent integral at every point.

Formalization Note Integrable (fun ζ => (z - ζ)⁻¹ • g ζ) with respect to volume on ℂ.

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

/-- For a continuous compactly supported `g : ℂ → E` and any `z`, the map `ζ ↦ (z - ζ)⁻¹ • g ζ` is integrable. -/
theorem integrable_inv_sub_smul_of_continuous {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] {g : ℂ → E} (hg : Continuous g) (hgc : HasCompactSupport g) (z : ℂ) :
    Integrable (fun ζ => (z - ζ)⁻¹ • g ζ) := by
  sorry

end JHolomorphic

Source

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

View graph