Prove2Me

The equation ∂̄f + z̄ f̄ = 0 has no nonzero L² solutions on the plane

Proved
CauchyRiemannIndex.plane_antiholomorphic_no_solution

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

cauchy-riemannconley-zehnder-indexfredholm-indexsobolev-spacessymplectic-geometry

Let ∂ˉ=∂s+i∂t\bar\partial=\partial_s+i\partial_t on C\mathbb{C}, z=s+itz=s+it. Every smooth f:C→Cf:\mathbb{C}\to\mathbb{C} with f∈L2(C)f\in L^2(\mathbb{C}) and

∂ˉf+zˉ fˉ=0\bar\partial f+\bar z\,\bar f=0

is identically zero.

Formalization Note ∂sf\partial_sf, ∂tf\partial_tf are fderiv ℝ f z 1 and fderiv ℝ f z Complex.I; smoothness is ContDiff ℝ ∞ f and square integrability is MemLp f 2 volume.

Preamble
import Definitions.Def_CauchyRiemannIndex_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic
Formal statement
namespace CauchyRiemannIndex

open MeasureTheory Matrix Filter Topology
open scoped ENNReal NNReal ContDiff RealInnerProductSpace

/-- Wendl, Proposition 5.20 (p. 96): with `∂̄ = ∂ₛ + i ∂ₜ`, the equation `∂̄f + z̄ f̄ = 0` has no
nontrivial smooth solution `f ∈ L²(ℂ, ℂ)`. -/
theorem plane_antiholomorphic_no_solution (f : ℂ → ℂ) (hf : ContDiff ℝ ∞ f)
    (h2 : MemLp f 2 volume)
    (heq : ∀ z, fderiv ℝ f z 1 + Complex.I * fderiv ℝ f z Complex.I +
      (starRingEnd ℂ) z * (starRingEnd ℂ) (f z) = 0) :
    f = 0 := by
  sorry

end CauchyRiemannIndex
Source
C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 5, Proposition 5.20, p. 96
Read-back

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

Read-back: CauchyRiemannIndex.plane_antiholomorphic_no_solution

Setting. f:C→Cf:\mathbb C\to\mathbb C, z=s+itz=s+it.

Hypotheses. f∈C∞f\in C^\infty (real sense, ContDiff ℝ ∞); f∈L2(C,Lebesgue)f\in L^2(\mathbb C,\text{Lebesgue}); for all zz:

∂sf(z)+i ∂tf(z)+zˉ f(z)‾=0,\partial_sf(z)+i\,\partial_tf(z)+\bar z\,\overline{f(z)}=0,

where ∂sf=Df(z) 1\partial_sf=Df(z)\,1, ∂tf=Df(z) i\partial_tf=Df(z)\,i (fderiv ℝ f z 1, fderiv ℝ f z Complex.I).

Definitions used. None from the setting file beyond notation; ∂ˉ=∂s+i∂t\bar\partial=\partial_s+i\partial_t (no factor 12\tfrac12).

Conclusion. f≡0f\equiv0.

Degenerate cases. f=0f=0 satisfies all hypotheses, conclusion holds. Gaussian test: f=ce−∣z∣2/2f=ce^{-|z|^2/2} gives ∂ˉf=−zf\bar\partial f=-zf, so the equation reads −zc+zˉcˉ=0-zc+\bar z\bar c=0 for all zz, forcing c=0c=0 ✓.

Remarks. volume on C\mathbb C is Lebesgue measure; starRingEnd ℂ is conjugation; ∞ is C∞C^\infty.

Soundness checks.

  1. Coercions: none; precedence of +/* is as written; universal quantifier over all z∈Cz\in\mathbb C.
  2. Truth: applying ∂=∂s−i∂t\partial=\partial_s-i\partial_t (note ∂zˉ=0\partial\bar z=0 and ∂fˉ=∂ˉf‾=−zˉfˉ‾=−zf\partial\bar f=\overline{\bar\partial f}=\overline{-\bar z\bar f}=-zf) gives Δf=∣z∣2f\Delta f=|z|^2f, i.e. (−Δ+∣z∣2)f=0(-\Delta+|z|^2)f=0 with f∈L2f\in L^2. The harmonic oscillator on R2\mathbb R^2 is essentially self-adjoint on Cc∞C_c^\infty with spectrum ≥2\ge2, so f=0f=0. True, not vacuous (hypotheses are not contradictory: f=0f=0).

Verdict: no mis-formalization observed

Human review

  • Endorsed by Shuze Chen · Oct 14, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Mazecto · Oct 14, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph