Prove2Me

The L² norm of the Cauchy–Riemann operator equals the L² norm of the gradient for compactly supported maps

Disproved
DbarRegularity.dbar_l2_identity

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

calderon-zygmundcauchy-riemannelliptic-regularityharmonic-analysissingular-integrals

Write z=s+itz=s+it for z∈Cz\in\mathbb{C}, φs=∂φ/∂s\varphi_s=\partial\varphi/\partial s, φt=∂φ/∂t\varphi_t=\partial\varphi/\partial t and ∂ˉφ=φs+iφt\bar\partial\varphi=\varphi_s+i\varphi_t. Cn\mathbb{C}^n carries the Hermitian norm, and ∥⋅∥Lp\|\cdot\|_{L^p} is the LpL^p norm on C\mathbb{C} with respect to Lebesgue measure. For every smooth compactly supported map φ:C→Cn\varphi:\mathbb{C}\to\mathbb{C}^n,

∥∂ˉφ∥L2(C)2=∥φs∥L2(C)2+∥φt∥L2(C)2.\|\bar\partial\varphi\|_{L^2(\mathbb{C})}^2=\|\varphi_s\|_{L^2(\mathbb{C})}^2+\|\varphi_t\|_{L^2(\mathbb{C})}^2 .

Formalization Note ContDiff ℝ ∞ φ is C∞C^\infty smoothness over R\mathbb{R} (not analyticity). φs\varphi_s and φt\varphi_t are fderiv ℝ φ z 1 and fderiv ℝ φ z Complex.I, and ∂ˉφ\bar\partial\varphi is dbar φ. Cn\mathbb{C}^n is EuclideanSpace ℂ (Fin n). The squared norms are the Bochner integrals ∫ z, ‖·‖ ^ 2 of continuous compactly supported functions.

Retired (2026-10-12). As formalized, ∫ z, A + ∫ z, B parses as ∫ z, (A + ∫ w, B), so the statement is false (disproved). The corrected statement is DbarRegularity.integral_norm_dbar_sq.

Preamble
import Definitions.Def_DbarRegularity_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic
Formal statement
namespace DbarRegularity

open MeasureTheory Metric Filter Topology
open scoped ENNReal NNReal ContDiff

/-- Abbas–Hofer, *Holomorphic Curves and Global Questions in Contact Geometry*, § 4.2, formula (4.4)
(p. 100): for a smooth compactly supported `φ : ℂ → ℂⁿ`,
`‖∂̄φ‖²_{L²(ℂ)} = ‖φ_s‖²_{L²(ℂ)} + ‖φ_t‖²_{L²(ℂ)}`, where `z = s + i t`. -/
theorem dbar_l2_identity {n : ℕ} (φ : ℂ → EuclideanSpace ℂ (Fin n)) (hφ : ContDiff ℝ ∞ φ)
    (hc : HasCompactSupport φ) :
    ∫ z, ‖dbar φ z‖ ^ 2 = ∫ z, ‖fderiv ℝ φ z 1‖ ^ 2 + ∫ z, ‖fderiv ℝ φ z Complex.I‖ ^ 2 := by sorry

end DbarRegularity
Source
C. Abbas, H. Hofer, Holomorphic Curves and Global Questions in Contact Geometry, Birkhäuser Advanced Texts Basler Lehrbücher, Birkhäuser (2019), https://doi.org/10.1007/978-3-030-11803-7, § 4.2, formula (4.4), p. 100
Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: DbarRegularity.dbar_l2_identity

Setting. n∈Nn\in\mathbb N, φ:C→Cn\varphi:\mathbb C\to\mathbb C^n (EuclideanSpace ℂ (Fin n), Hermitian norm), z=s+itz=s+it, Lebesgue measure on C\mathbb C.

Hypotheses. φ\varphi is C∞C^\infty over R\mathbb R (ContDiff ℝ ∞), with compact support.

Definitions used. fderiv ℝ φ z 1 =φs(z)=\varphi_s(z), the derivative in direction 11. fderiv ℝ φ z Complex.I =φt(z)=\varphi_t(z), the derivative in direction ii. dbar φ z =φs(z)+i φt(z)=\varphi_s(z)+i\,\varphi_t(z).

Conclusion.

∫C∣φs+iφt∣2 dz=∫C∣φs∣2 dz+∫C∣φt∣2 dz.\int_{\mathbb C}|\varphi_s+i\varphi_t|^2\,dz=\int_{\mathbb C}|\varphi_s|^2\,dz+\int_{\mathbb C}|\varphi_t|^2\,dz .

Degenerate cases. n=0n=0: every term is 0. φ=0\varphi=0: 0=00=0.

Soundness checks.

  1. Lean defaults. Under open scoped ContDiff, ∞ is ((⊤ : ℕ∞) : WithTop ℕ∞), i.e. C∞C^\infty and not analytic. This was confirmed in Mathlib Analysis/Calculus/ContDiff/FTaylorSeries.lean:120; the analytic exponent is ω. Compactly supported smooth maps are therefore plentiful, and the statement is not vacuous. The ENNReal ∞ notation is also in scope, but only the ContDiff reading typechecks at type WithTop ℕ∞. All three integrands are continuous with compact support, hence integrable, so the Bochner integrals are the true values and not default zeros. The identities Dφ(z)1=∂sφD\varphi(z)1=\partial_s\varphi and Dφ(z)i=∂tφD\varphi(z)i=\partial_t\varphi are correct for z=s+itz=s+it. There are no rpow, toReal or ℕ-subtraction issues; ^ 2 is a natural-number power of a real.
  2. There are no constants and no quantifier order beyond ∀n ∀φ\forall n\,\forall\varphi. The statement is true: expanding gives a cross term 2 Re∫⟨φs,iφt⟩2\,\mathrm{Re}\int\langle\varphi_s,i\varphi_t\rangle, which vanishes after integration by parts for compactly supported smooth φ\varphi.

Remarks. None.

Verdict: no mis-formalization observed

View graph