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

Identification of the Euclidean norm on ℝ² with the complex modulus on ℂ under the canonical map (x, y) ↦ x + iy.

theorem DifferentialOperators.norm_cauchyRiemannKernel_eq (v : EuclideanSpace ℝ (Fin 2)) : ‖cauchyRiemannKernel v‖ = (2 * Real.pi)⁻¹ * ‖v‖⁻¹

Pointwise norm of the Cauchy–Riemann kernel 1 / (2π · z): ‖K(v)‖ = (2π)⁻¹ · ‖v‖⁻¹ for v ≠ 0.

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

Uniform bound on the Cauchy–Riemann kernel away from the origin: for ‖v‖ ≥ 1, ‖K(v)‖ ≤ (2π)⁻¹.

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

Integrability of φ · K where φ is Schwartz and K is the Cauchy–Riemann kernel: the product is integrable on ℝ², by splitting into the unit ball (where K is locally integrable and φ is bounded) and its complement (where K is bounded and φ is integrable).

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

Schwartz-seminorm bound on the integral ∫ φ · K: there exists a finite set of indices and a constant such that ‖∫ φ · K‖ is controlled by the corresponding Schwartz seminorm of φ, expressing the continuity of the linear functional φ ↦ ∫ φ · K on Schwartz space.

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

The tempered distribution E defined by integration against the Cauchy–Riemann kernel K(z) = 1 / (2π z). This is the candidate fundamental solution of ∂̄ on ℝ².

@[simp]

theorem DifferentialOperators.dbarFundSolDist_apply (φ : SchwartzMap (EuclideanSpace ℝ (Fin 2)) ℂ) : dbarFundSolDist φ = ∫ (v : EuclideanSpace ℝ (Fin 2)), φ v * cauchyRiemannKernel v

Evaluation formula for the candidate fundamental solution distribution E: pairing with a Schwartz function φ is ∫ φ(v) · K(v) dv.

theorem DifferentialOperators.dbarFundSolDist_eq_cauchyRiemannDistribution : dbarFundSolDist = cauchyRiemannDistribution

The mkCLM-packaged distribution dbarFundSolDist agrees with the underlying cauchyRiemannDistribution already defined elsewhere.

theorem DifferentialOperators.dbar_dbarFundSol_eq_delta : dbarOp dbarFundSolDist = TemperedDistribution.delta 0

Lemma 11.5 of Melrose (the ∂̄ part): the Cauchy–Riemann kernel distribution is a fundamental solution for ∂̄, i.e. ∂̄ E = δ₀ on ℝ².

theorem DifferentialOperators.dbarFundSolDist_isFundSol : IsTemperedFundamentalSolution 2 dbarPoly dbarFundSolDist

The Cauchy–Riemann kernel distribution E is a tempered fundamental solution of ∂̄, realising Lemma 11.5 of Melrose at the level of the IsTemperedFundamentalSolution predicate.