Prove2Me

Pompeiu's formula for compactly supported C1C^1 maps into a complex Banach space

Proved
JHolomorphic.integral_inv_sub_smul_dbar_eq

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

complex-analysispseudoholomorphic-curves

Let EE be a complex Banach space and h:C→Eh:\mathbb C\to E a C1C^1 map with compact support. Write ∂sh\partial_s h, ∂th\partial_t h for its partial derivatives in the real and imaginary directions. For every z∈Cz\in\mathbb C,

∫C∂sh(ζ)+i ∂th(ζ)z−ζ dζ=2π h(z),\int_{\mathbb C}\frac{\partial_s h(\zeta)+i\,\partial_t h(\zeta)}{z-\zeta}\,d\zeta=2\pi\,h(z),

i.e. the Cauchy transform inverts ∂s+i∂t\partial_s+i\partial_t up to the factor 2π2\pi on compactly supported C1C^1 maps.

Formalization Note ∂sh(ζ)\partial_s h(\zeta) and ∂th(ζ)\partial_t h(\zeta) are fderiv ℝ h ζ 1 and fderiv ℝ h ζ Complex.I. The integrability of the integrand at zz is taken as a hypothesis hint; it always holds, the hypothesis only fixes that the Bochner integral is the genuine one.

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

/-- Vector-valued Pompeiu formula: for `h : ℂ → E` of class `C¹` with compact support, `∫ (z - ζ)⁻¹ • (∂ₛh + i ∂ₜh)(ζ) dζ = 2π h(z)`. -/
theorem integral_inv_sub_smul_dbar_eq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
    [CompleteSpace E] (h : ℂ → E) (hh : ContDiff ℝ 1 h) (hc : HasCompactSupport h) (z : ℂ)
    (hint : Integrable (fun ζ => (z - ζ)⁻¹ • (fderiv ℝ h ζ 1 + Complex.I • fderiv ℝ h ζ Complex.I))) :
    ∫ ζ, (z - ζ)⁻¹ • (fderiv ℝ h ζ 1 + Complex.I • fderiv ℝ h ζ Complex.I) =
      (2 * Real.pi : ℂ) • h z := by
  sorry

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

View graph