Prove2Me

The L² solutions of ∂̄f + z f̄ = 0 on the plane are real multiples of a Gaussian

Proved
CauchyRiemannIndex.plane_holomorphic_solutions

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+z\,\bar f=0

is of the form f(z)=c e−∣z∣2/2f(z)=c\,e^{-|z|^2/2} for a real constant cc.

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.21 (p. 96): with `∂̄ = ∂ₛ + i ∂ₜ`, every smooth solution `f ∈ L²(ℂ, ℂ)`
of `∂̄f + z f̄ = 0` is a constant real multiple of `e^{-|z|²/2}`. -/
theorem plane_holomorphic_solutions (f : ℂ → ℂ) (hf : ContDiff ℝ ∞ f)
    (h2 : MemLp f 2 volume)
    (heq : ∀ z, fderiv ℝ f z 1 + Complex.I * fderiv ℝ f z Complex.I +
      z * (starRingEnd ℂ) (f z) = 0) :
    ∃ c : ℝ, ∀ z, f z = c * Complex.exp (-(‖z‖ ^ 2 / 2 : ℝ)) := 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.21, p. 96
Read-back

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

Read-back: CauchyRiemannIndex.plane_holomorphic_solutions

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

Hypotheses. f∈C∞f\in C^\infty (real); f∈L2(C)f\in L^2(\mathbb C); for all zz:

∂sf(z)+i ∂tf(z)+z f(z)‾=0(∂ˉf+zfˉ=0, ∂ˉ=∂s+i∂t).\partial_sf(z)+i\,\partial_tf(z)+z\,\overline{f(z)}=0\qquad(\bar\partial f+z\bar f=0,\ \bar\partial=\partial_s+i\partial_t).

Definitions used. None from the setting file; fderiv ℝ f z 1=∂sf=\partial_sf, fderiv ℝ f z Complex.I=∂tf=\partial_tf.

Conclusion. ∃c∈R ∀z: f(z)=c e−∣z∣2/2\exists c\in\mathbb R\ \forall z:\ f(z)=c\,e^{-|z|^2/2} (exponent -(‖z‖ ^ 2 / 2 : ℝ) cast to C\mathbb C; ∥z∥=∣z∣\|z\|=|z|).

Degenerate cases. f=0f=0: c=0c=0.

Remarks. The reality of cc is essential and correct: for f=ce−∣z∣2/2f=ce^{-|z|^2/2}, ∂sf=−sf\partial_sf=-sf, ∂tf=−tf\partial_tf=-tf, so ∂ˉf=−(s+it)f=−zf\bar\partial f=-(s+it)f=-zf, and zfˉ=zcˉe−∣z∣2/2z\bar f=z\bar c e^{-|z|^2/2}; the sum vanishes iff cˉ=c\bar c=c. The Gaussian is in L2L^2 and smooth, so the solution set is exactly the real line R⋅e−∣z∣2/2\mathbb R\cdot e^{-|z|^2/2} (the statement only claims "⊆\subseteq", which is the nontrivial direction).

Soundness checks.

  1. Coercions: (c : ℂ) real cast, real exponent cast to C\mathbb C inside Complex.exp; precedence -(‖z‖^2/2) correct. Quantifier: cc chosen before zz (global constant), correct.
  2. Truth: applying ∂=∂s−i∂t\partial=\partial_s-i\partial_t: ∂(zfˉ)=2fˉ+z ∂ˉf‾=2fˉ−∣z∣2f\partial(z\bar f)=2\bar f+z\,\overline{\bar\partial f}=2\bar f-|z|^2f, so Δf=∣z∣2f−2fˉ\Delta f=|z|^2f-2\bar f. With f=a+ibf=a+ib: (−Δ+∣z∣2−2)a=0(-\Delta+|z|^2-2)a=0, (−Δ+∣z∣2+2)b=0(-\Delta+|z|^2+2)b=0. Harmonic-oscillator spectrum {2,4,… }\{2,4,\dots\} with simple ground state e−∣z∣2/2e^{-|z|^2/2} gives b=0b=0, a=ce−∣z∣2/2a=ce^{-|z|^2/2}. True, not vacuous.

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