dd^c calculus: pluriharmonicity, naturality, linearity

TERM-SCOPE(Kahler) — this module uses the restricted sense of "Kahler"; the source repository's terms register records what is backed and what is not.

Category: 1-Mathlib (CSD-free; flat differential forms on a complex inner product space, in the d^c vocabulary of KahlerPotential.lean).

The three facts about dd^c K = d(d^c K) that a chart-invariance argument for the Fubini–Study form needs, none of which existed:

• ★ dcForm_re_eq_neg_dForm_im — Cauchy–Riemann in this vocabulary: for holomorphic f, d^c(Re f) = -d(Im f); hence ★ ddcForm_re_eq_zero — the real part of a holomorphic function is pluriharmonic, dd^c (Re f) = 0 — by d² = 0 (extDeriv_extDeriv_apply);
• ★ ddcForm_log_norm_eq_zero — log ‖L ·‖ is pluriharmonic away from the kernel of a complex-linear functional L. Proved from the previous item with a local holomorphic logarithm: Complex.log off the slit plane, Complex.log ∘ (-·) on it (Complex.mem_slitPlane_or_neg_mem_slitPlane), so no branch is ever chosen globally;
• ★ ddcForm_comp — naturality: for holomorphic τ, dd^c (K ∘ τ) is the pullback of dd^c K along fderiv ℝ τ. Its d^c half (dcForm_comp) is the chain rule plus the fact that the real derivative of a holomorphic map commutes with J (DifferentiableAt.fderiv_restrictScalars); its d half is upstream's extDeriv_pullback;
• ddcForm_sub', ddcForm_const_smul', contDiffAt_dcForm — linearity in the potential, in the local (ContDiffAt) form that a potential singular off an open set needs.

Honest scope

Everything here is on a flat complex inner product space, in the E → E [⋀^Fin k]→L[ℝ] ℝ representation. The manifold-level d does not exist (step (2b)); these are the flat lemmas a chart-by-chart argument composes.

Provenance and references. KahlerPotential.lean (dcForm, ddcForm, fsChartForm); Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean (extDeriv_pullback, extDeriv_extDeriv_apply); Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean (contDiffAt_log).

theorem Kahler.dcForm_re_eq_neg_dForm_im {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {f : E → ℂ} {x : E} (hf : DifferentiableAt ℂ f x) : dcForm (fun (w : E) => (f w).re) x = -dForm (fun (w : E) => (f w).im) x

theorem Kahler.ddcForm_re_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {f : E → ℂ} {x : E} (hf : ContDiffAt ℂ ⊤ f x) : ddcForm (fun (w : E) => (f w).re) x = 0

B2b: the real part of a holomorphic function is pluriharmonic: dd^c (Re f) = 0.

theorem Kahler.ddcForm_log_norm_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (L : E →L[ℂ] ℂ) {x : E} (hx : L x ≠ 0) : ddcForm (fun (w : E) => Real.log ‖L w‖) x = 0

B2c: log ‖L ·‖ is pluriharmonic away from the kernel, for L complex-linear.

Naturality and linearity

theorem Kahler.ddcForm_sub {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {K₁ K₂ : E → ℝ} (h₁ : ContDiff ℝ (↑⊤) K₁) (h₂ : ContDiff ℝ (↑⊤) K₂) (x : E) : ddcForm (K₁ - K₂) x = ddcForm K₁ x - ddcForm K₂ x

B2e: dd^c is additive in the potential (globally smooth potentials).

theorem Kahler.dcForm_comp {E : Type u_2} {E' : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] {K : E' → ℝ} {τ : E → E'} {y : E} (hK : DifferentiableAt ℝ K (τ y)) (hτ : DifferentiableAt ℂ τ y) : dcForm (K ∘ τ) y = (dcForm K (τ y)).compContinuousLinearMap (fderiv ℝ τ y)

B2d, step 1: d^c is natural under holomorphic maps.

theorem Kahler.ddcForm_comp {E : Type u_2} {E' : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] {K : E' → ℝ} {τ : E → E'} {x : E} (hK : ContDiff ℝ (↑⊤) K) (hτ : ContDiffAt ℂ ⊤ τ x) : ddcForm (K ∘ τ) x = (ddcForm K (τ x)).compContinuousLinearMap (fderiv ℝ τ x)

B2d: dd^c is natural under holomorphic maps (the pullback of dd^c K is dd^c (K ∘ τ)).

theorem Kahler.contDiffAt_dcForm {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {m : WithTop ℕ∞} {K : E → ℝ} {x : E} (hK : ContDiffAt ℝ (m + 1) K x) : ContDiffAt ℝ m (dcForm K) x

Local smoothness of d^c K from local smoothness of K.

theorem Kahler.ddcForm_sub' {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {K₁ K₂ : E → ℝ} {x : E} (h₁ : ContDiffAt ℝ 2 K₁ x) (h₂ : ContDiffAt ℝ 2 K₂ x) : ddcForm (K₁ - K₂) x = ddcForm K₁ x - ddcForm K₂ x

Local additivity of dd^c in the potential.

theorem Kahler.ddcForm_const_smul' {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {K : E → ℝ} {x : E} (c : ℝ) (hK : ContDiffAt ℝ 2 K x) : ddcForm (c • K) x = c • ddcForm K x

Local homogeneity of dd^c in the potential.