feat(Mathematics/Calculus): coordinate Wirtinger calculus on ℂⁿ

[pariandrea]

Contents

Coordinate.lean specialises the directional Wirtinger calculus of Basic.lean
to the coordinate space ℂⁿ (spelled ι → ℂ for a Fintype ι), fixing the
direction to the I-th basis vector Pi.single I 1. It defines the coordinate
operators ∂_I f, ∂̄_I f as the partial Wirtinger derivatives in coordinate I,
and derives the computational rules that make the basis usable: the four Kronecker
coordinate values ∂_I z^J = δ_IJ, ∂̄_I z̄^J = δ_IJ, ∂̄_I z^J = ∂_I z̄^J = 0
(so z and z̄ behave as independent variables), real-linearity, the Leibniz and
finite-sum rules, inner-field conjugation, the two-term chain rule for an outer
g : ℂ → ℂ, the holomorphic/anti-holomorphic collapse, and the coordinate
specialisation of Schwarz's theorem, ∂_I ∂̄_J f = ∂̄_J ∂_I f on a C² field.

A real/complex restrictScalars bridge on the ι → ℂ domain
(differentiableAt_real_of_complex, fderivReal_apply_eq_complex) lets the
fderiv ℝ-based operators read off a holomorphic field's complex derivative,
the input to the collapse, with no restrictScalars appearing in any statement.

Motivation

Indexing the directional Wirtinger calculus by a coordinate I casts it in the
language of several complex variables: first derivatives ∂_I f assemble into a
gradient, mixed second derivatives ∂_I ∂̄_J f into a complex Hessian. By Schwarz
that Hessian is Hermitian, which is exactly Kähler-metric hermiticity for a real
potential K: g_{IJ̄} = ∂_I ∂̄_J K = star (g_{JĪ}). This is the calculus the N=1
SUSY formalisation runs on, with ι the chiral index.

Scope

This is the second instalment of a layered development (after #1163). The module
overview forward-references the downstream UpperHalfPlane application and the N=1
SUSY layer; both follow in subsequent PRs. The forward references are intentional.

AI disclosure

AI (Claude Code) was used extensively to draft lemma statements, proofs, and
documentation under my direction. I reviewed every declaration and take full
responsibility for the content.

Author responsibility

I am a PhD student in theoretical physics and am not an expert in complex calculus;
this development is needed for my current SUSY formalisation work. As with #1163, the
PR proves no novel mathematics: every result is the d = Pi.single I 1 specialisation
of a foundation lemma already merged in #1163, or a direct fderiv ℝ computation of a
coordinate projection. Correctness therefore rests on the machine-checked foundation
and Mathlib's Fréchet-derivative API, and the whole development compiles under the
kernel with no sorry and no new axioms.

References

Coordinate.lean adds no new external references; the notation and conventions are
inherited from Basic.lean (verified in #1163).

Lemmas and definitions added

No declarations are removed. All additions live in the new file, plus a one-line
import in Physlib.lean (the library aggregator).

Coordinate maps as continuous linear maps

• coordProjCLM, coordProjCLM_apply — the I-th coordinate z^I = u I as an
  ℝ-linear CLM.
• conjCoordCLM, conjCoordCLM_apply — the conjugated coordinate z̄^I = star (u I).
• conjConfig, conjConfig_apply — pointwise conjugation of a point of ι → ℂ.
• conjCLM, conjCLM_apply — pointwise conjugation bundled as an ℝ-linear CLM.
• conjCLM_smul_I — conjCLM is conjugate-ℂ-linear, conj (i·d) = −(i · conj d).

§A — the coordinate operators

• dWirtingerCoord, dWirtingerAntiCoord (def) — the coordinate Wirtinger operators
  ∂_I f, ∂̄_I f, definitionally the directional operators along Pi.single I 1.
• dWirtingerCoord_eq_dWirtingerDir, dWirtingerAntiCoord_eq_dWirtingerAntiDir —
  the definitional identification with the foundation operators.
• dWirtingerCoord_apply, dWirtingerAntiCoord_apply — the real-Fréchet form
  ∂_I f = ½(∂_x ∓ i·∂_y) f, unconditional.

§B — the Pi-domain restrictScalars bridge

• differentiableAt_real_of_complex — a ℂ-differentiable field on ι → ℂ is
  ℝ-differentiable.
• fderivReal_apply_eq_complex — its real and complex Fréchet derivatives agree
  pointwise, fderiv ℝ f u d = fderiv ℂ f u d; no restrictScalars in the type.

§C — properties of dWirtingerCoord

• dWirtingerCoord_congr_of_eventuallyEq_apply — locality at the base point.
• dWirtingerCoord_const, dWirtingerCoord_zero — vanish on constants (@[simp]).
• dWirtingerCoord_neg_apply — negation.
• dWirtingerCoord_coordProj — ∂_I z^J = δ_IJ (@[simp]).
• dWirtingerCoord_add_apply, dWirtingerCoord_smul_apply,
  dWirtingerCoord_mul_apply, dWirtingerCoord_fun_sum_apply — additivity,
  ℂ-linearity, Leibniz, the finite-sum rule.
• dWirtingerCoord_eq_complex_fderiv_apply — holomorphic collapse,
  ∂_I f = fderiv ℂ f u (Pi.single I 1).
• dWirtingerCoord_eq_zero_of_antiHolomorphic_apply — ∂_I annihilates an
  antiholomorphic field g ∘ conjConfig.

§D — properties of dWirtingerAntiCoord, and the coordinate values

• dWirtingerAntiCoord_congr_of_eventuallyEq_apply, dWirtingerAntiCoord_const,
  dWirtingerAntiCoord_zero, dWirtingerAntiCoord_neg_apply,
  dWirtingerAntiCoord_add_apply, dWirtingerAntiCoord_smul_apply,
  dWirtingerAntiCoord_mul_apply, dWirtingerAntiCoord_fun_sum_apply — the §C
  mirror.
• dWirtingerAntiCoord_coordProj — ∂̄_I z^J = 0 (@[simp]).
• dWirtingerCoord_conjCoord — ∂_I z̄^J = 0.
• dWirtingerAntiCoord_conjCoord — ∂̄_I z̄^J = δ_IJ.
• dWirtingerAntiCoord_eq_complex_fderiv_apply — anti-holomorphic collapse for an
  antiholomorphic field.
• dWirtingerAntiCoord_eq_zero_of_holomorphic_apply — ∂̄_I f = 0 for holomorphic f.
• differentiable_coordDiff, dWirtingerCoord_coordDiff,
  dWirtingerAntiCoord_coordDiff — Wirtinger derivatives of the coordinate
  difference z^J − z̄^J, ∂_I = δ_IJ and ∂̄_I = −δ_IJ.

§E — Wirtinger chain rules for an outer function

• dWirtingerCoord_comp_apply, dWirtingerAntiCoord_comp_apply — the two-term chain
  rule for an outer g : ℂ → ℂ, ∂_I(g∘f) = (∂g/∂f)·∂_I f + (∂g/∂f̄)·∂_I f̄.
• dWirtingerCoord_comp_holomorphic_apply, dWirtingerAntiCoord_comp_holomorphic_apply
  — the single-term collapse deriv g (f u) · ∂_I f for holomorphic g.
• dWirtingerCoord_star_comp_apply, dWirtingerAntiCoord_star_comp_apply —
  conjugating the inner field swaps the operators, ∂_I f̄ = conj (∂̄_I f) and dual.

§F — Schwarz's theorem for the coordinate operators

• differentiableAt_dWirtingerCoord, differentiableAt_dWirtingerAntiCoord — on a
  C² field a first coordinate derivative is itself real-differentiable.
• dWirtingerCoord_dWirtingerAntiCoord_comm — Schwarz's theorem in coordinate form,
  ∂_I ∂̄_J f = ∂̄_J ∂_I f, the Pi.single specialisation of the foundation
  dWirtingerDir_dWirtingerAntiDir_comm.

Private helpers (not exported)

smul_single_one, clinear_of_holomorphic, fderiv_coordProj,
conjConfig_single_one, coordDiff_eq_add_neg, outerHolo_fderiv_restrictScalars,
outerHolo_clinear, dWirtingerDir_one_eq_deriv, dWirtingerAntiDir_one_eq_zero.

Reviewer map

Suggested reading order:

1. Module overview (§i–§iii) — notation, the coordinate values, and the table
   of contents.
2. §A — the two operator definitions and their real-Fréchet form.
3. §B — the restrictScalars bridge feeding the holomorphic collapse.
4. §C–§D — the dWirtingerCoord rules, then the dWirtingerAntiCoord mirror and
   the four Kronecker coordinate values.
5. §E — the two-term chain rule and its holomorphic single-term collapse.
6. §F — differentiability of a first derivative, then the capstone Schwarz
   theorem dWirtingerCoord_dWirtingerAntiCoord_comm.

Each holomorphic lemma is immediately followed by its anti-holomorphic dual, so the
two can be reviewed as a pair. Every rule is the d = Pi.single I 1 specialisation of
its Basic.lean analogue from #1163.

[github-actions]

Thank you for this PR, which will now be reviewed. Please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

[jstoobysmith]

There is a lot of lemmas and definitions here that I don't think actually need making (i.e. they are simple rewrites of things already in Mathlib).

[jstoobysmith]

I don't think this should be needed here (can't we just use ContinuousLinearMap.proj )

[jstoobysmith]

Likewise with the other results before section A. below.

[jstoobysmith]

Is this needed?

[jstoobysmith]

One line

[jstoobysmith]

Is this needed as a new lemma?

[jstoobysmith]

likewise

[pariandrea]

There is a lot of lemmas and definitions here that I don't think actually need making (i.e. they are simple rewrites of things already in Mathlib).

Thanks you for the feedback. I agree on the bloat. I've cut the the code to the minimal set of lemmas needed to do computations.

• Coordinate CLM wrappers (coordProjCLM, conjCoordCLM, and the conjConfig family before §A) removed; the projections now use ContinuousLinearMap.proj (and its star) directly.
• Trivial restatements / Mathlib duplicates — smul_single_one inline; the _eq_dWirtingerDir inlined; differentiableAt_real_of_complex → DifferentiableAt.restrictScalars; fderivReal_apply_eq_complex → fderiv_restrictScalars + coe_restrictScalars' inline; the _zero and dWirtingerDir_one_eq_* lemmas folded into the proofs that used them; differentiable_coordDiff → by fun_prop; and the two outerHolo_* helpers merged into a single clinear_of_holomorphic.

Two things I kept, since they aren't Mathlib rewrites:

1. conjCLM (with conjCLM_apply and conjCLM_smul_I). The foundation conjugate-linear chain rules dWirtingerDir_comp_conjLinear / dWirtingerAntiDir_comp_conjLinear require the inner conjugation supplied as a bundled →L[ℝ]. I have however made it private.

2. The coordinate-difference derivatives (dWirtingerCoord_coordDiff, dWirtingerAntiCoord_coordDiff, and the private coordDiff_eq_add_neg). These give ∂_I (z^J − z̄^J) = δ_IJ and ∂̄_I (z^J − z̄^J) = −δ_IJ. Since z^J − z̄^J = 2i·Im(u^J), this is the combination any function of the coordinates' imaginary parts differentiates against ( useful for log Kähler potentials).

[jstoobysmith]

This now looks good to me - approved.