noncomputable def DifferentialOperators.dbarPoly : MvPolynomial (Fin 2) ℂ

The Cauchy-Riemann polynomial X₀ + i·X₁, whose associated constant-coefficient differential operator is the Cauchy-Riemann (∂̄) operator on ℝ² ≅ ℂ.

noncomputable def DifferentialOperators.dbarOp : TemperedDistribution (EuclideanSpace ℝ (Fin 2)) ℂ →L[ℂ] TemperedDistribution (EuclideanSpace ℝ (Fin 2)) ℂ

The Cauchy-Riemann (∂̄) operator on tempered distributions on ℝ², defined as the constant-coefficient differential operator with symbol dbarPoly.

noncomputable def DifferentialOperators.cauchyRiemannKernel : EuclideanSpace ℝ (Fin 2) → ℂ

The Cauchy-Riemann kernel (2π)⁻¹·(x + iy)⁻¹ on ℝ²: this is the (distributional) fundamental solution of the Cauchy-Riemann operator ∂̄.

noncomputable def DifferentialOperators.euclidProdMeasurableEquiv : EuclideanSpace ℝ (Fin 2) ≃ᵐ ℝ × ℝ

The measurable equivalence between EuclideanSpace ℝ (Fin 2) (with the L² product structure) and ℝ × ℝ.

theorem DifferentialOperators.cauchyRiemannKernel_locallyIntegrable : MeasureTheory.LocallyIntegrable cauchyRiemannKernel MeasureTheory.volume

The Cauchy-Riemann kernel is locally integrable with respect to Lebesgue measure on ℝ².

theorem DifferentialOperators.complex_norm_eq_euclidean_norm (v : EuclideanSpace ℝ (Fin 2)) : ‖↑(v.ofLp 0) + Complex.I * ↑(v.ofLp 1)‖ = ‖v‖

The norm of the complex number x + iy agrees with the Euclidean norm of the vector (x, y) in EuclideanSpace ℝ (Fin 2).

theorem DifferentialOperators.cauchyRiemannKernel_norm_le (v : EuclideanSpace ℝ (Fin 2)) (hv : 1 ≤ ‖v‖) : ‖cauchyRiemannKernel v‖ ≤ (2 * Real.pi)⁻¹

For ‖v‖ ≥ 1, the Cauchy-Riemann kernel is bounded in norm by (2π)⁻¹.

theorem DifferentialOperators.cauchyRiemannKernel_schwartz_integrable (φ : SchwartzMap (EuclideanSpace ℝ (Fin 2)) ℂ) : MeasureTheory.Integrable (fun (v : EuclideanSpace ℝ (Fin 2)) => φ v • cauchyRiemannKernel v) MeasureTheory.volume

The product of a Schwartz function with the Cauchy-Riemann kernel is Lebesgue integrable on ℝ².

theorem DifferentialOperators.cauchyRiemannKernel_integral_bound : ∃ (s : Finset (ℕ × ℕ)) (C : ℝ), 0 ≤ C ∧ ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin 2)) ℂ), ‖∫ (v : EuclideanSpace ℝ (Fin 2)), φ v • cauchyRiemannKernel v‖ ≤ C * (s.sup (schwartzSeminormFamily ℂ (EuclideanSpace ℝ (Fin 2)) ℂ)) φ

Continuity estimate for the Cauchy-Riemann functional: there exist a finite set s of Schwartz seminorm indices and a nonnegative constant C such that for every Schwartz function φ the integral ∫ φ v • cauchyRiemannKernel v is bounded by C · sup of seminorms in s`. This provides the continuity needed to define the Cauchy-Riemann tempered distribution.

noncomputable def DifferentialOperators.cauchyRiemannDistribution : TemperedDistribution (EuclideanSpace ℝ (Fin 2)) ℂ

The Cauchy-Riemann tempered distribution: the action φ ↦ ∫ φ v • cauchyRiemannKernel v, packaged as a tempered distribution on ℝ².

theorem DifferentialOperators.cauchyRiemannDistribution_apply (φ : SchwartzMap (EuclideanSpace ℝ (Fin 2)) ℂ) : cauchyRiemannDistribution φ = ∫ (v : EuclideanSpace ℝ (Fin 2)), φ v • cauchyRiemannKernel v

Defining identity for the Cauchy-Riemann distribution applied to a Schwartz test function.

theorem DifferentialOperators.cauchyPompeiu_excised_ball_integral_vanishes (ψ : SchwartzMap (EuclideanSpace ℝ (Fin 2)) ℂ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (v : EuclideanSpace ℝ (Fin 2)) in Metric.closedBall 0 ε, ψ v • cauchyRiemannKernel v) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

A Cauchy-Pompeiu auxiliary statement: the integral of ψ v • cauchyRiemannKernel v over a closed ball of radius ε around the origin tends to 0 as ε → 0⁺.

theorem DifferentialOperators.two_eps_mul_integral_inv_eps_sq_add_sq (ε : ℝ) (hε : 0 < ε) : 2 * ε * ∫ (y : ℝ) in -ε..ε, (ε ^ 2 + y ^ 2)⁻¹ = Real.pi

The integral identity 2ε · ∫_{-ε}^{ε} (ε² + y²)⁻¹ dy = π, used in the Cauchy-Pompeiu computation for the Cauchy-Riemann fundamental solution.

theorem DifferentialOperators.four_eps_mul_integral_inv_eps_sq_add_sq (ε : ℝ) (hε : 0 < ε) : 4 * ε * ∫ (y : ℝ) in -ε..ε, (ε ^ 2 + y ^ 2)⁻¹ = 2 * Real.pi

The integral identity 4ε · ∫_{-ε}^{ε} (ε² + y²)⁻¹ dy = 2π.

theorem DifferentialOperators.cauchyRiemannKernel_dbar_integral (φ : SchwartzMap (EuclideanSpace ℝ (Fin 2)) ℂ) : ∫ (v : EuclideanSpace ℝ (Fin 2)), ((LineDeriv.lineDerivOp (EuclideanSpace.single 0 1) φ) v + Complex.I • (LineDeriv.lineDerivOp (EuclideanSpace.single 1 1) φ) v) • cauchyRiemannKernel v = -φ 0

Key Cauchy-Pompeiu identity: for any Schwartz function φ, ∫ (∂_x φ + i·∂_y φ)(v) • cauchyRiemannKernel(v) dv = -φ(0). This is the integral form of Lemma 11.5 expressing the Cauchy-Riemann kernel as a fundamental solution of ∂̄.

theorem DifferentialOperators.fourier_polySymbol_eq_neg_dbar (φ : SchwartzMap (EuclideanSpace ℝ (Fin 2)) ℂ) : FourierTransform.fourier ((SchwartzMap.smulLeftCLM ℂ (polySymbol 2 dbarPoly)) (FourierTransformInv.fourierInv φ)) = -(LineDeriv.lineDerivOp (EuclideanSpace.single 0 1) φ + Complex.I • LineDeriv.lineDerivOp (EuclideanSpace.single 1 1) φ)

The Fourier-side identity expressing the Cauchy-Riemann symbol as a (negated) sum of partial derivatives: the Fourier multiplier by polySymbol 2 dbarPoly applied to the inverse Fourier transform of φ equals minus the Cauchy-Riemann differential operator applied to φ.

theorem DifferentialOperators.cauchyRiemannKernel_fourier_multiplier_integral (φ : SchwartzMap (EuclideanSpace ℝ (Fin 2)) ℂ) : ∫ (v : EuclideanSpace ℝ (Fin 2)), (FourierTransform.fourier ((SchwartzMap.smulLeftCLM ℂ (polySymbol 2 dbarPoly)) (FourierTransformInv.fourierInv φ))) v • cauchyRiemannKernel v = φ 0

The Fourier-side integral identity for the Cauchy-Riemann kernel: integrating the Fourier multiplier by polySymbol 2 dbarPoly of 𝓕⁻¹ φ against the Cauchy-Riemann kernel recovers φ(0).

theorem DifferentialOperators.dbar_fundamentalSolution : IsTemperedFundamentalSolution 2 dbarPoly cauchyRiemannDistribution

Lemma 11.5 (Cauchy-Riemann fundamental solution): the tempered distribution cauchyRiemannDistribution is a fundamental solution of the Cauchy-Riemann operator ∂̄, i.e. ∂̄ (cauchyRiemannDistribution) = δ₀.