Wirtinger derivatives and the Cauchy–Riemann bridge

Unit: dbar-solvability (docs/design/dbar-solvability.md §4.1). Mathlib-only planar file: no project imports, no manifold variables, so downstream planar consumers (planar-stokes-atoms, residue-calculus, monodromy, ...) can import it without dragging in the manifold stack (D10).

• wirtingerD, wirtingerDbar : the Wick/Wirtinger derivatives of a function ℂ → ℂ, defined as plain (junk-tolerant) functions via fderiv ℝ.
• fderiv_apply_eq_wirtinger : the workhorse decomposition of the real differential on the basis {1, I}.
• The Cauchy–Riemann bridge: DifferentiableAt ℂ f z ↔ DifferentiableAt ℝ f z ∧ wirtingerDbar f z = 0 (hand-built; mathlib has no Analysis/Complex/CauchyRiemann.lean at the pin).
• The (0,1) chain rule wirtingerDbar_comp_differentiableAt (transition law for Form01).
• Regularity of the operator: contDiffOn_wirtingerDbar, continuous_wirtingerDbar, hasCompactSupport_wirtingerDbar.

noncomputable def RS.wirtingerD (f : ℂ → ℂ) (z : ℂ) : ℂ

The Wirtinger ∂ (holomorphic) derivative, (∂f/∂x - i ∂f/∂y)/2 in real coordinates. Junk 0 if f is not ℝ-differentiable at z.

Equations

• RS.wirtingerD f z = ((fderiv ℝ f z) 1 - Complex.I * (fderiv ℝ f z) Complex.I) / 2

noncomputable def RS.wirtingerDbar (f : ℂ → ℂ) (z : ℂ) : ℂ

The Wirtinger dbar (anti-holomorphic) derivative, (∂f/∂x + i ∂f/∂y)/2 in real coordinates. Junk 0 if f is not ℝ-differentiable at z.

Equations

• RS.wirtingerDbar f z = ((fderiv ℝ f z) 1 + Complex.I * (fderiv ℝ f z) Complex.I) / 2

The Wirtinger decomposition of an ℝ-linear map

theorem RS.clm_apply_eq_add_conj_smul (L : ℂ →L[ℝ] ℂ) (v : ℂ) : L v = (L 1 - Complex.I * L Complex.I) / 2 * v + (L 1 + Complex.I * L Complex.I) / 2 * (starRingEnd ℂ) v

ℝ-linear maps ℂ → ℂ decompose as v ↦ a v + b v-bar (values on the basis 1, I).

theorem RS.fderiv_apply_eq_wirtinger (f : ℂ → ℂ) (z : ℂ) (_hf : DifferentiableAt ℝ f z) (v : ℂ) : (fderiv ℝ f z) v = wirtingerD f z * v + wirtingerDbar f z * (starRingEnd ℂ) v

THE workhorse: the Wirtinger decomposition of the real differential.

Arithmetic

theorem RS.wirtingerDbar_add (f g : ℂ → ℂ) (z : ℂ) (hf : DifferentiableAt ℝ f z) (hg : DifferentiableAt ℝ g z) : wirtingerDbar (f + g) z = wirtingerDbar f z + wirtingerDbar g z

theorem RS.wirtingerDbar_sub (f g : ℂ → ℂ) (z : ℂ) (hf : DifferentiableAt ℝ f z) (hg : DifferentiableAt ℝ g z) : wirtingerDbar (f - g) z = wirtingerDbar f z - wirtingerDbar g z

theorem RS.wirtingerDbar_neg (f : ℂ → ℂ) (z : ℂ) : wirtingerDbar (-f) z = -wirtingerDbar f z

theorem RS.wirtingerDbar_const_mul (f : ℂ → ℂ) (z c : ℂ) (hf : DifferentiableAt ℝ f z) : wirtingerDbar (fun (w : ℂ) => c * f w) z = c * wirtingerDbar f z

theorem RS.wirtingerDbar_congr_nhds (f g : ℂ → ℂ) (z : ℂ) (h : f =ᶠ[nhds z] g) : wirtingerDbar f z = wirtingerDbar g z

theorem RS.wirtingerDbar_zero (z : ℂ) : wirtingerDbar 0 z = 0

theorem RS.wirtingerDbar_const (z c : ℂ) : wirtingerDbar (fun (x : ℂ) => c) z = 0

Holomorphy ↔ Cauchy–Riemann

theorem RS.wirtingerDbar_eq_zero_of_differentiableAt (f : ℂ → ℂ) (z : ℂ) (hf : DifferentiableAt ℂ f z) : wirtingerDbar f z = 0

theorem RS.wirtingerD_eq_deriv (f : ℂ → ℂ) (z : ℂ) (hf : DifferentiableAt ℂ f z) : wirtingerD f z = deriv f z

theorem RS.differentiableAt_of_wirtingerDbar_eq_zero (f : ℂ → ℂ) (z : ℂ) (hf : DifferentiableAt ℝ f z) (h : wirtingerDbar f z = 0) : DifferentiableAt ℂ f z

Cauchy–Riemann bridge (hand-built; no mathlib counterpart at the pin).

theorem RS.differentiableAt_iff_wirtingerDbar_eq_zero (f : ℂ → ℂ) (z : ℂ) : DifferentiableAt ℂ f z ↔ DifferentiableAt ℝ f z ∧ wirtingerDbar f z = 0

theorem RS.differentiableOn_of_wirtingerDbar_eq_zero (f : ℂ → ℂ) {s : Set ℂ} (_hs : IsOpen s) (hf : ∀ z ∈ s, DifferentiableAt ℝ f z) (h : ∀ z ∈ s, wirtingerDbar f z = 0) : DifferentiableOn ℂ f s

theorem RS.analyticOnNhd_of_wirtingerDbar_eq_zero (f : ℂ → ℂ) {s : Set ℂ} (hs : IsOpen s) (hf : ∀ z ∈ s, DifferentiableAt ℝ f z) (h : ∀ z ∈ s, wirtingerDbar f z = 0) : AnalyticOnNhd ℂ f s

The (0,1) chain rule

theorem RS.wirtingerDbar_comp_differentiableAt (f : ℂ → ℂ) (z : ℂ) {τ : ℂ → ℂ} (hF : DifferentiableAt ℝ f (τ z)) (hτ : DifferentiableAt ℂ τ z) : wirtingerDbar (f ∘ τ) z = (starRingEnd ℂ) (deriv τ z) * wirtingerDbar f (τ z)

(0,1) chain rule along a holomorphic map — the transition law of (0,1)-coefficients.

theorem RS.wirtingerD_comp_differentiableAt (f : ℂ → ℂ) (z : ℂ) {τ : ℂ → ℂ} (hF : DifferentiableAt ℝ f (τ z)) (hτ : DifferentiableAt ℂ τ z) : wirtingerD (f ∘ τ) z = deriv τ z * wirtingerD f (τ z)

Companion ∂-chain-rule (the (1,0) transition law).

Regularity of the operator

theorem RS.contDiffOn_wirtingerDbar (f : ℂ → ℂ) {s : Set ℂ} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑⊤) f s) : ContDiffOn ℝ (↑⊤) (wirtingerDbar f) s

theorem RS.continuous_wirtingerDbar (f : ℂ → ℂ) (hf : ContDiff ℝ (↑⊤) f) : Continuous (wirtingerDbar f)

theorem RS.hasCompactSupport_wirtingerDbar (f : ℂ → ℂ) (hf : HasCompactSupport f) : HasCompactSupport (wirtingerDbar f)