A machine-checked solution to the Jacobians challenge

16.7. Dbar.DbarDisk🔗

Jacobians.Dbar.DbarDisk — source

dbar

The Wirtinger anti-holomorphic derivative ∂̄f = ½(∂ₓf + i ∂_y f), written via the real Fréchet derivative fderiv ℝ f evaluated at the basis directions 1 and I. f is holomorphic at z iff dbar f z = 0 (see dbar_eq_zero_of_differentiableAt).

noncomputable def dbar (f : ℂ → ℂ) (z : ℂ) : ℂ

dbar_const

@[simp] theorem dbar_const (c : ℂ) (z : ℂ) : dbar (fun _ => c) z = 0

cauchyKernel

The Cauchy-transform kernel K ζ = 1/(π·ζ), so that the convolution u(z) = (g ⋆ K)(z) = (1/π)∬ g(ζ)/(z-ζ) dA(ζ) satisfies ∂̄u = g (Cauchy–Pompeiu, with this sign convention; see cauchyPompeiu / dbar_cauchyTransform).

noncomputable def cauchyKernel (ζ : ℂ) : ℂ

integrableOn_inv_closedBall

The inverse function ζ ↦ ζ⁻¹ is integrable on every closed ball of ℂ: in polar coordinates the area element r dr dθ exactly cancels the 1/r singularity.

theorem integrableOn_inv_closedBall (R : ℝ) :
    IntegrableOn (fun ζ : ℂ => ζ⁻¹) (Metric.closedBall 0 R) volume

locallyIntegrable_cauchyKernel

D0. The Cauchy kernel K ζ = -(1/(π·ζ)) is locally integrable on ℂ.

theorem locallyIntegrable_cauchyKernel : LocallyIntegrable cauchyKernel volume

cauchyTransform

The Cauchy transform of g: u = g ⋆ K with K the Cauchy kernel, computed against complex multiplication. Pointwise u(x) = ∫ g(t)·K(x−t) dt = -(1/π)∬ g(ζ)/(x−ζ) dA(ζ).

noncomputable def cauchyTransform (g : ℂ → ℂ) : ℂ → ℂ

contDiff_cauchyTransform

D1 (regularity). For g ∈ C^∞_c, the Cauchy transform u = g ⋆ K is C^∞.

theorem contDiff_cauchyTransform {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g)
    (hgsupp : HasCompactSupport g) : ContDiff ℝ (⊤ : ℕ∞) (cauchyTransform g)

cauchyTransform_smul

ℝ-homogeneity of the Cauchy transform (free — smul commutes with the convolution integral; no integrability needed).

theorem cauchyTransform_smul (c : ℝ) (g : ℂ → ℂ) :
    cauchyTransform (c • g) = c • cauchyTransform g

cauchyTransform_add

Additivity of the Cauchy transform on compactly-supported continuous functions: both convolution integrands are integrable (HasCompactSupport.convolutionExists_left against the locally integrable kernel), so the integral of the sum splits (ConvolutionExists.add_distrib).

theorem cauchyTransform_add {f g : ℂ → ℂ} (hf : Continuous f) (hfs : HasCompactSupport f)
    (hg : Continuous g) (hgs : HasCompactSupport g) :
    cauchyTransform (f + g) = cauchyTransform f + cauchyTransform g

hasFDerivAt_cauchyTransform

D1 (derivative). For g ∈ C^∞_c, the Fréchet derivative of u = g ⋆ K is (fderiv ℝ g) ⋆ K (with the precomposed bilinear map), evaluated at each point.

theorem hasFDerivAt_cauchyTransform {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g)
    (hgsupp : HasCompactSupport g) (x : ℂ) :
    HasFDerivAt (cauchyTransform g)
      (((fderiv ℝ g) ⋆[(ContinuousLinearMap.mul ℝ ℂ).precompL ℂ, volume] cauchyKernel) x) x

dbar_cauchyTransform

D3 bridge. ∂̄ commutes through the Cauchy transform onto the *smooth* factor: ∂̄(g ⋆ K) = (∂̄g) ⋆ K. Combined with D1's derivative formula and the fact that the evaluation maps T ↦ T 1, T ↦ T I (and hence dbar) commute with the Bochner integral.

theorem dbar_cauchyTransform {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g)
    (hgsupp : HasCompactSupport g) (z : ℂ) :
    dbar (cauchyTransform g) z
      = (dbar g ⋆[ContinuousLinearMap.mul ℝ ℂ, volume] cauchyKernel) z

dbar_eq_zero_of_differentiableAt

A function that is ℂ-differentiable (holomorphic) at z satisfies the homogeneous Cauchy–Riemann equation ∂̄ f = 0 there. This is the Wirtinger characterization and validates the definition of dbar.

theorem dbar_eq_zero_of_differentiableAt {f : ℂ → ℂ} {z : ℂ}
    (hf : DifferentiableAt ℂ f z) : dbar f z = 0

continuous_dbar

dbar g is continuous when g is C^∞ (it is a fixed continuous-linear combination of the first Fréchet derivative, which is itself continuous).

theorem continuous_dbar {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) : Continuous (dbar g)

hasCompactSupport_dbar

dbar g has compact support when g does (dbar is built from fderiv g, whose support is contained in tsupport g).

theorem hasCompactSupport_dbar {g : ℂ → ℂ}
    (hgsupp : HasCompactSupport g) : HasCompactSupport (dbar g)

integrable_dbar_mul_cauchyKernel

Integrability of the area integrand ζ ↦ (∂̄g)(ζ)·K(z−ζ): ∂̄g is continuous with compact support and K(z−·) is locally integrable (a reflection/translation of the kernel K).

theorem integrable_dbar_mul_cauchyKernel {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g)
    (hgsupp : HasCompactSupport g) (z : ℂ) :
    Integrable (fun ζ => dbar g ζ * cauchyKernel (z - ζ)) volume

fderiv_apply_basis

Evaluate the ℝ-linear map fderiv ℝ g w at a complex direction a + b·I in the {1, I} basis: (fderiv ℝ g w)(a + b·I) = a·(fderiv … 1) + b·(fderiv … I) for real a, b.

theorem fderiv_apply_basis (g : ℂ → ℂ) (w : ℂ) (a b : ℝ) :
    (fderiv ℝ g w) (a + b * I) = (a : ℂ) * (fderiv ℝ g w) 1 + (b : ℂ) * (fderiv ℝ g w) I

dbar_polar_identity

Polar–Wirtinger identity (purely algebraic, from ℝ-linearity of fderiv ℝ g). With c = cos θ + sin θ·I = e^{iθ}, the anti-radial Wirtinger derivative decomposes into the radial (fderiv … c) and angular (fderiv … (I·c)) directional derivatives: e^{−iθ}·(2·∂̄g w) = (fderiv ℝ g w) c + I·(fderiv ℝ g w) (I·c).

theorem dbar_polar_identity (g : ℂ → ℂ) (w : ℂ) (θ : ℝ) :
    (Real.cos θ - Real.sin θ * I) * ((2 : ℂ) * dbar g w)
      = (fderiv ℝ g w) (Real.cos θ + Real.sin θ * I)
        + I * (fderiv ℝ g w) (I * (Real.cos θ + Real.sin θ * I))

contDiff_radialMap

theorem contDiff_radialMap (z c : ℂ) : ContDiff ℝ (⊤ : ℕ∞) (radialMap z c)

contDiff_radial

The radial slice r ↦ g(z + r•c) is C^∞.

theorem contDiff_radial {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (z c : ℂ) :
    ContDiff ℝ (⊤ : ℕ∞) (fun r : ℝ => g (radialMap z c r))

hasCompactSupport_radial

theorem hasCompactSupport_radial {g : ℂ → ℂ} (hgsupp : HasCompactSupport g) {c : ℂ}
    (hc : c ≠ 0) (z : ℂ) : HasCompactSupport (fun r : ℝ => g (radialMap z c r))

deriv_radial

The radial derivative deriv (fun r => g(z + r•c)) r = (fderiv ℝ g (z + r•c)) c.

theorem deriv_radial {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (z c : ℂ) (r : ℝ) :
    deriv (fun r : ℝ => g (radialMap z c r)) r = (fderiv ℝ g (radialMap z c r)) c

radial_integral

The radial integral produces the answer: ∫_{r>0} (fderiv ℝ g (z+r•c)) c dr = −g(z) for c ≠ 0 (1D fundamental theorem of calculus, compact support kills the r→∞ endpoint).

theorem radial_integral {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hgsupp : HasCompactSupport g)
    {c : ℂ} (hc : c ≠ 0) (z : ℂ) :
    ∫ r in Set.Ioi (0 : ℝ), (fderiv ℝ g (radialMap z c r)) c = -g z

contDiff_angularMap

theorem contDiff_angularMap (z : ℂ) (r : ℝ) : ContDiff ℝ (⊤ : ℕ∞) (angularMap z r)

deriv_angular

The angular derivative deriv (fun θ => g(z + r·c(θ))) θ = (fderiv ℝ g w)(r·I·c(θ)), where w = z + r·c(θ) and c(θ) = cos θ + sin θ·I, since d/dθ c(θ) = I·c(θ).

theorem deriv_angular {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (z : ℂ) (r : ℝ) (θ : ℝ) :
    deriv (fun θ : ℝ => g (angularMap z r θ)) θ
      = (fderiv ℝ g (angularMap z r θ))
          ((r : ℂ) * (I * (Real.cos θ + Real.sin θ * I)))

angular_integral

The angular integral vanishes: ∫_{θ∈(−π,π)} (fderiv ℝ g w)(I·c(θ)) dθ = 0, where w = z + r·c(θ), c(θ) = cos θ + sin θ·I. By the angular FTC, the integral of the directional derivative collapses to the endpoints θ=±π, and c(π)=c(−π)=−1, so they cancel.

theorem angular_integral {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (z : ℂ) {r : ℝ} (hr : r ≠ 0) :
    ∫ θ in (-π)..π, (fderiv ℝ g (angularMap z r θ)) (I * (Real.cos θ + Real.sin θ * I)) = 0

exists_radius_fderiv_eq_zero

A bound M beyond which the radial slice leaves tsupport (fderiv ℝ g): there is M with ∀ r > M, ∀ θ, fderiv ℝ g (z + r·c(θ)) = 0 (where ‖c(θ)‖ = 1).

theorem exists_radius_fderiv_eq_zero {g : ℂ → ℂ} (hgsupp : HasCompactSupport g) (z : ℂ) :
    ∃ M : ℝ, ∀ r : ℝ, M < r → ∀ θ : ℝ,
      fderiv ℝ g (z + (r : ℂ) * (Real.cos θ + Real.sin θ * I)) = 0

integrableOn_target_of_continuous_of_vanishing

Integrability on the polar target Ioi 0 ×ˢ Ioo (−π) π for a continuous integrand that vanishes for r = p.1 > M: it then lives on the compact Icc 0 M ×ˢ Icc (−π) π.

theorem integrableOn_target_of_continuous_of_vanishing {f : ℝ × ℝ → ℂ} (hf : Continuous f)
    {M : ℝ} (hvanish : ∀ p : ℝ × ℝ, M < p.1 → f p = 0) :
    IntegrableOn f (Set.Ioi 0 ×ˢ Set.Ioo (-π) π) volume

cauchyPompeiu_area

D2 core — the Cauchy–Pompeiu area-integral identity. For g ∈ C^∞_c, ∬_ℂ (∂̄g)(ζ)/(ζ−z) dA(ζ) = −π·g(z).

This is THE genuine mathematical content of the ∂̄-disk atom and the single remaining gap.

PLANNED PROOF — polar coordinates (NOT Green's theorem; this route avoids the unscaffolded annulus-divergence theorem entirely):

  1. Translate ζ ↦ z + w (integral_add_left_eq_self): ∫ (∂̄g)(ζ)/(ζ−z) = ∫ (∂̄g)(z+w)/w.

  2. Polar change of variables (Complex.integral_comp_polarCoord_symm): the Jacobian factor r cancels 1/w (r/(r e^{iθ}) = e^{−iθ}), giving ∫_{(r,θ)∈(0,∞)×(−π,π)} e^{−iθ}·(∂̄g)(z + r e^{iθ}) dr dθ.

  3. The polar-Wirtinger identity dbar_polar_identity: rewrites the integrand as a ½-combination of the radial directional derivative (fderiv g w) c and the angular one (fderiv g w)(I·c), where c = e^{iθ}, w = z + r·c.

  4. The radial part integrates over r∈(0,∞) to −g(z) (radial_integral), then over θ to −2π·g(z). The angular part integrates over θ∈(−π,π) to 0 (angular_integral, with c(π)=c(−π)=−1). Net ½·(−2π·g(z)) = −π·g(z).

BOTH genuine analytic pieces — the radial FTC (radial_integral) and the angular vanishing (angular_integral). Steps 1–4 below handle translation, polar CoV, the e^{−iθ} simplification, and the dbar_polar_identity rewrite), reducing the goal to ∫_{target} ½·(R(p) + I·A(p)) = −π·g(z) with R = (fderiv g w) c (radial), A = (fderiv g w)(I·c) (angular), w = radialMap z (c θ) r. REMAINING GAP: only the final split + Fubini interchange: ½[∫_target R + I·∫_target A], with ∫_target R = ∫_θ (∫_r R) = ∫_θ (−g z) = −2π·g(z) (Fubini, radial_integral) and ∫_target A = ∫_r (∫_θ A) = ∫_r 0 = 0 (Fubini-swapped, angular_integral). The blocker is the Fubini integrability side-conditions on target = Ioi 0 ×ˢ Ioo(−π) π (no packaged polar-integrability transport in Mathlib). ~50–100 LoC. See the probe report.

theorem cauchyPompeiu_area {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hgsupp : HasCompactSupport g)
    (z : ℂ) : ∫ ζ, dbar g ζ / (ζ - z) = -π * g z

cauchyPompeiu

D2 (Cauchy–Pompeiu). For g ∈ C^∞_c, (∂̄g) ⋆ K = g. Reduces by elementary algebra to the area-integral identity cauchyPompeiu_area.

theorem cauchyPompeiu {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hgsupp : HasCompactSupport g)
    (z : ℂ) : (dbar g ⋆[ContinuousLinearMap.mul ℝ ℂ, volume] cauchyKernel) z = g z

dbar_solvable_of_compactSupport

Main theorem (∂̄-on-a-disk solvability atom). For g ∈ C^∞_c(ℂ), the Cauchy transform u = g ⋆ K is a C^∞ solution of the inhomogeneous Cauchy–Riemann equation ∂̄u = g everywhere. Combines D1 (regularity), the D3 bridge ∂̄(g⋆K) = (∂̄g)⋆K, and D2 (Cauchy–Pompeiu (∂̄g)⋆K = g).

theorem dbar_solvable_of_compactSupport {g : ℂ → ℂ}
    (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hgsupp : HasCompactSupport g) :
    ∃ u : ℂ → ℂ, ContDiff ℝ (⊤ : ℕ∞) u ∧ ∀ z, dbar u z = g z