Physlib.Mathematics.Calculus.Wirtinger.Basic

Wirtinger calculus

Notation

* The differentiation direction is a *subscript*: `∂_v f` and `∂̄_v f` are the holomorphic and anti-holomorphic Wirtinger derivatives of `f` in direction `v`, splitting the total real derivative `d_v f` (straight `d` for the total, `∂`/`∂̄` for the parts). For iterated derivatives (§I) the operators compose, `∂_v ∂̄_w f`. * A `/∂` fraction differentiates with respect to a *variable*, not a direction: a real coordinate `∂f/∂x`, or the argument of a one-variable function in the chain rule, `∂g/∂f`, `∂g/∂f̄` (outer `g : ℂ → ℂ`, inner `f : V → ℂ`). * `f̄` is the pointwise conjugate `p ↦ conj (f p)`.

* `v`, `w` are directions in `V`. * `u : V` is the *fixed* base point a derivative is evaluated at — the implicit point in the subscript notation. * `p : V` is the *bound* base-point variable when a derivative is repackaged as a function of position: the inner field of an iterated operator (`fun p => dWirtingerAntiDir f w p`, §I), or the composite in the chain rule (`fun p => g (f p)`, §D).

Base points (`u`, `p`) and directions (`v`, `w`) all live in `V`: a vector space is its own tangent space, so a displacement from a point is again an element of `V` (`u + t·v`).

i. Overview

This module is the **foundation** of physlib's Wirtinger calculus. It defines the **directional Wirtinger derivatives** of `f : V → ℂ` on a complex vector space `V`, along a direction `v : V` (a complex number when `V = ℂ`, a vector in general):

`∂_v f = (1/2)(d_v f − i·d_{i·v} f)` (`dWirtingerDir`) `∂̄_v f = (1/2)(d_v f + i·d_{i·v} f)` (`dWirtingerAntiDir`)

Here `d_v f = fderiv ℝ f u v` is the real Fréchet derivative along `v`, the limit `lim_{t→0} (f(u + t·v) − f(u)) / t` over real `t`; so "real" names the scalar `t`, not the direction `v`, and over all `v` these limits form the `ℝ`-linear map `fderiv ℝ f u : V → ℂ`. The second direction `i·v` is `v` turned 90° by the complex structure on `V`, so `(v, i·v)` is an orthogonal frame in `v`'s own (arbitrary) direction, a rotated and rescaled copy of the axes `(1, i)`. For `V = ℂ` one may take `v = 1`, giving `d_v f = ∂f/∂x` and `d_{i·v} f = ∂f/∂y`; writing `z = x + i y` and `z̄ = x − i y`, the formulas recover the classical `∂f/∂z = (1/2)(∂_x − i ∂_y)f` and `∂f/∂z̄ = (1/2)(∂_x + i ∂_y)f`.

The two operators measure the failure of `ℂ`-linearity. The real derivative always commutes with real scaling and addition; `ℂ`-linearity asks in addition that it commute with `i`, that is `d_{i·v} f = i·d_v f`. The gap `d_{i·v} f − i·d_v f` to that condition is exactly `−2i·∂̄_v f`, so `∂̄_v f` is the obstruction to `ℂ`-linearity and vanishes precisely when `f` is holomorphic. Equivalently, the operators split the real derivative into its holomorphic and anti-holomorphic parts, the directional form of the Dolbeault decomposition `d = ∂ + ∂̄`, which sum back to

`d_v f = ∂_v f + ∂̄_v f`.

This is the coordinate-free form of treating `z` and `z̄` as independent (the `V = ℂ` case above). When `f` is holomorphic the anti-holomorphic half vanishes and `∂_v f` is the ordinary complex derivative (§F). Everything rests on `fderiv ℝ`, with no lower Wirtinger layer.

On these operators the module builds the **full directional calculus**:

* real-linearity, the Leibniz rule, and the finite-sum rule (§B); * the inner-field conjugation lemmas, swapping the two operators (§C); * the two-term Wirtinger chain rule for an outer `g : ℂ → ℂ` (§D); * domain conjugation: precomposing with a conjugate-linear map swaps the two operators (§E); * the holomorphic / anti-holomorphic collapse, keyed on `ℂ`-linearity or conjugate-linearity of the real derivative along `v` (§F); * differentiability and locality of the operators on a `C²` field (§H).

The capstone (§I) is **Schwarz's theorem** in Wirtinger form. On a `C²` field the holomorphic and anti-holomorphic derivatives in any two directions commute:

`∂_v ∂̄_w f = ∂̄_w ∂_v f` (`dWirtingerDir_dWirtingerAntiDir_comm`)

It is no new analytic fact: it reduces to the symmetry of the second real Fréchet derivative (`ContDiffAt.isSymmSndFDerivAt`), carried out via the `weightedDirDeriv` bridge of §G.

ii. Key results

- `Physlib.Wirtinger.dWirtingerDir` / `dWirtingerAntiDir` : directional Wirtinger derivatives of `f : V → ℂ` along `v`. - `Physlib.Wirtinger.dWirtingerDir_add` / `dWirtingerDir_smul` / `dWirtingerDir_mul` / `dWirtingerDir_fun_sum` : real-linearity, the Leibniz rule, and the finite-sum rule (each with an anti-holomorphic dual). - `Physlib.Wirtinger.dWirtingerDir_star_comp` / `dWirtingerAntiDir_star_comp` : conjugating the inner field swaps the holomorphic and anti-holomorphic operators. - `Physlib.Wirtinger.dWirtingerDir_comp` / `dWirtingerAntiDir_comp` : the two-term Wirtinger chain rule for an outer `g : ℂ → ℂ`. - `Physlib.Wirtinger.dWirtingerDir_comp_conjLinear` / `dWirtingerAntiDir_comp_conjLinear` : precomposing with a conjugate-`ℂ`-linear map swaps the two operators (with the base point and direction transported through the map). - `Physlib.Wirtinger.dWirtingerDir_eq_of_clinear` / `dWirtingerAntiDir_eq_zero_of_clinear` : the holomorphic collapse, keyed on `ℂ`-linearity of the real derivative along the direction (each with a conjugate-`ℂ`-linear dual). - `Physlib.Wirtinger.differentiableAt_dWirtingerDir` / `differentiableAt_dWirtingerAntiDir` : the directional derivative of a `C²` field is itself real-differentiable. - `Physlib.Wirtinger.dWirtingerDir_congr_of_eventuallyEq` / `dWirtingerAntiDir_congr_of_eventuallyEq` : the directional derivative depends only on the field near the point. - `Physlib.Wirtinger.dWirtingerDir_dWirtingerAntiDir_comm` : Schwarz's theorem, `∂_v ∂̄_w f = ∂̄_w ∂_v f` for a `C²` `f`. - `Physlib.Wirtinger.realLinear_apply_eq_wirtinger` : the real-linear Wirtinger split `L w = a·w + b·star w` of any `L : ℂ →L[ℝ] ℂ`, the algebraic input to the chain rule (§D). - `Physlib.Wirtinger.fderiv_star_eq` : the real derivative of a pointwise conjugate `p ↦ star (f p)` is `conjCLE` composed with `fderiv ℝ f`, the analytic input to the conjugation lemmas (§C).

iii. Table of contents

A. The directional Wirtinger operators
B. Real-linearity and the Leibniz rule
C. Conjugation
D. The Wirtinger chain rule
E. Domain conjugation
F. The holomorphic collapse
G. The second-derivative bridge
H. Differentiability and locality
I. Schwarz's theorem

iv. References

- Kreutz-Delgado, *The Complex Gradient Operator and the CR-Calculus*, arXiv:0906.4835 — directional/multivariable formulation and two-term chain rule (§D); second-order theory behind §G–I. - Mortini & Rupp, *The Clairaut–Schwarz Theorem for Mixed Wirtinger Derivatives*, Bull. Iranian Math. Soc. 48 (2022), 2643–2647 — the mixed holomorphic/anti-holomorphic symmetry of §I under the same `C²` hypothesis, with the same reduction to real Schwarz used here. - Koor, Qiu, Kwek & Rebentrost, *A short tutorial on Wirtinger Calculus with applications in quantum information*, arXiv:2312.04858 — companion exposition of the scalar single/multivariable calculus and sign conventions. - *Complex differential form*, Wikipedia (section "The Dolbeault operators") — the `d = ∂ + ∂̄` splitting and the `∂`/`∂̄` notation this module's operators are named after.

A. The directional Wirtinger operators

The two directional operators repackage the real Fréchet derivative of `f` along `v` and `i·v` into a holomorphic part `∂_v f` and an anti-holomorphic part `∂̄_v f`, the combinations `(1/2)(d_v f ∓ i·d_{i·v} f)`. Both share one shape, `weightedDirDeriv`, the base-point field `p ↦ (1/2)(d_{b₁} f + c·d_{b₂} f)`, and are its two specializations at `c = ∓i`, `(b₁, b₂) = (v, i·v)`. Defining the operators through it makes their second derivative — the engine of Schwarz's theorem (§G, §I) — a single bridge lemma. Both are `ℂ`-valued and depend on the base point `u`.

B. Real-linearity and the Leibniz rule

The directional operators are built from `fderiv ℝ`, so they inherit its vanishing on constants, additivity, negation, complex-scalar compatibility, the finite-sum rule, and — through the Fréchet product rule — a Wirtinger Leibniz rule.

C. Conjugation

Conjugating the inner field `f` swaps the two operators, up to an outer conjugation on the value (`fderiv_star_eq`):

`∂_v f̄ = conj (∂̄_v f)`, `∂̄_v f̄ = conj (∂_v f)`.

Each operator applied to the conjugate field `f̄` returns the *other* operator on `f`, conjugated — the bar exchanges holomorphic and anti-holomorphic dependence. Concretely, on `V = ℂ` take the holomorphic `f(z) = z`, with `∂_z z = 1`, `∂̄_z z = 0`:

* `∂_v f̄ = conj (∂̄_v f)` reads `∂_z z̄ = conj 0 = 0` — the conjugate `z̄` has no holomorphic part; * the dual `∂̄_v f̄ = conj (∂_v f)` reads `∂̄_z z̄ = conj 1 = 1` — all of `z̄`'s dependence sits in the anti-holomorphic operator.

The chain rule of §D builds on these to handle a conjugated inner argument.

D. The Wirtinger chain rule

Composing with an outer `g : ℂ → ℂ` gives a **two-term** chain rule:

`∂_v(g∘f) = (∂g/∂f)·∂_v f + (∂g/∂f̄)·∂_v f̄`.

A non-holomorphic `g` depends on both its argument and its conjugate, so both channels contribute: the holomorphic `∂g/∂f` and the anti-holomorphic `∂g/∂f̄`, each times the matching inner derivative — two terms where the complex-analytic rule has one. The two coefficients come from `realLinear_apply_eq_wirtinger`: every `ℝ`-linear `L : ℂ → ℂ` splits as `L w = a·w + b·conj w`, and on the outer real derivative `L = fderiv ℝ g (f u)` that gives `a = ∂g/∂f`, `b = ∂g/∂f̄`. The proof applies this split to the outer factor and reuses the §C conjugation lemmas for the `∂_v f̄` term.

E. Domain conjugation

The goal is to differentiate anti-holomorphic functions: a holomorphic `g` precomposed with conjugation of its input (the scalar case is `g(z̄)`, but the input is a general vector). So this section conjugates a function's *input*: precomposing `g` with a domain map `L : V → V'` (forming `g ∘ L`) swaps the two operators, whereas §C conjugated the output. The map `L` is **conjugate-`ℂ`-linear**: real-linear and continuous, but anti-commuting with `i`:

`L (i · x) = −(i · L x)`,

the abstract form of `conj (i·x) = −i · conj x`. That sign flip swaps the two operators: in the holomorphic combination `(1/2)(d_v f − i·d_{i·v} f)` the `d_{i·v} f` term picks up the minus from `L`, turning it anti-holomorphic. So precomposition `g ∘ L` swaps `∂ ↔ ∂̄`, with `g`'s derivative taken at the mapped point `L u` in the mapped direction `L v`:

`∂_v(g ∘ L)` at `u` = `∂̄_{L v} g` at `L u` `∂̄_v(g ∘ L)` at `u` = `∂_{L v} g` at `L u`

(`dWirtingerDir_comp_conjLinear` and its dual `dWirtingerAntiDir_comp_conjLinear`).

Concretely on `ℂ`, let `L : z ↦ z̄` and `g(z) = log(z)`, so `g ∘ L` is `z ↦ log(z̄)`. The theorem computes this composite's derivatives from the known derivative of `log`, swapping the operator. Its anti-holomorphic derivative is `log`'s ordinary derivative `1/z` at the mapped point `z̄`:

`∂̄_z log(z̄) = 1/z̄`,

while its holomorphic derivative vanishes, `∂_z log(z̄) = 0`, because `log` is holomorphic. So `log(z̄)` is purely anti-holomorphic, with its dependence carried by `∂̄`.

So precomposing with conjugation turns `∂` into `∂̄` and vice versa: a holomorphic `g(z̄)` has zero holomorphic derivative, and its anti-holomorphic derivative is just `g`'s ordinary complex derivative (§F, and the example above). The proof uses only `L`'s anti-commutation with `i`, so it holds over any complex `V`, `V'`.

F. The holomorphic collapse

The two-operator split collapses to one exactly when `f` is holomorphic along `v`, i.e. its real derivative is `ℂ`-linear there (`d_{i·v} f = i·d_v f`, the Cauchy–Riemann condition): then `∂_v f` is the full real derivative `d_v f` and `∂̄_v f` vanishes. Dually, a conjugate-`ℂ`-linear derivative makes `∂_v f` vanish and `∂̄_v f` the full derivative.

The lemmas take this `ℂ`-linearity condition directly as hypothesis, not holomorphy itself. The reason is a clean division of labor.

**The domain-general collapse.** Given the identity `d_{i·v} f = i·d_v f`, the collapse is pure algebra: unfold `∂_v f = (1/2)(d_v f − i·d_{i·v} f)`, substitute the identity, and `∂_v f` reduces to `d_v f` while `∂̄_v f` cancels to `0`. No property of the domain `V` enters, so a single proof covers every complex `V`.

**The domain-specific bridge.** Holomorphy is stated through the complex derivative `fderiv ℂ`, but the collapse is about the real derivative `fderiv ℝ`; the implication `f` holomorphic ⟹ `d_{i·v} f = i·d_v f` is the bridge between them. Relating the two derivatives is domain-specific, so each consumer establishes the bridge in its own setting, then applies the domain-general lemma above.

G. The second-derivative bridge

Schwarz's theorem (§I) commutes two Wirtinger operators, so it differentiates a directional Wirtinger derivative a *second* time. This section bridges that second derivative to the second real Fréchet derivative `fderiv ℝ (fderiv ℝ f) u`, where mixed partials are already symmetric.

Each directional operator is, definitionally, a combination `(1/2)(d_{b₁} f + c·d_{b₂} f)` of the real derivative along two directions (`c = −i` holomorphic with `b₂ = i·b₁`, `c = +i` anti-holomorphic). `weightedDirDeriv` records this as a function of the base point, with `b₁`, `b₂` left free: the directions stay fixed while the point `p` varies, turning the one-point derivative into a field `V → ℂ` that can itself be differentiated. Differentiating it once more sends each first derivative to `fderiv ℝ (fderiv ℝ f) u` on two slots.

The two inner directions `b₁`, `b₂` are intrinsic: they are the pair a Wirtinger derivative already combines (`v` and `i·v`). The second differentiation, by contrast, is an ordinary Fréchet derivative along one new direction `a`, so the bridge lands directly on the plain second derivative `fderiv ℝ (fderiv ℝ f) u` in the outer slot `a` and inner slot `b₁`/`b₂`, whose slot symmetry (`ContDiffAt.isSymmSndFDerivAt`) drives Schwarz. The *outer* Wirtinger combination is rebuilt afterward by instantiating `a` at `v` and `i·v`.

Because `weightedDirDeriv` and its bridge `fderiv_weightedDirDeriv` are generic in `c`, `b₁`, `b₂`, one lemma serves every second-order pairing. The four combinations (holomorphic or anti-holomorphic, twice) differ only in their coefficients and all reduce to `fderiv ℝ (fderiv ℝ f) u` on the directions `v`, `i·v`, `w`, `i·w`. §I discharges the mixed pairing that Kähler geometry needs; the others follow from the same bridge with a different `(c, b₁, b₂)`, then `ContDiffAt.isSymmSndFDerivAt` and `ring`.

The operators are already `weightedDirDeriv` by definition (§A); this section differentiates that shared field a second time.

**Structure.**

* `hasFDerivAt_fderiv_apply`, `hasFDerivAt_weightedDirDeriv` : the evaluation field `p ↦ d_b f`, and hence `weightedDirDeriv`, is differentiable wherever `fderiv ℝ f` is. * `fderiv_weightedDirDeriv` : the bridge, sending a derivative of `weightedDirDeriv` along a direction `a` to the second Fréchet derivative `fderiv ℝ (fderiv ℝ f) u` in the two slots. * `dWirtingerDir_eq_weightedDirDeriv`, `dWirtingerAntiDir_eq_weightedDirDeriv` : the operators `∂_v f`, `∂̄_v f` are `weightedDirDeriv` at `(c, b₁, b₂) = (−i, v, i·v)` and `(i, w, i·w)`. * `fderiv_dWirtingerDir`, `fderiv_dWirtingerAntiDir` : specialize the bridge, so a second derivative of `∂_v f`, `∂̄_v f` lands on `fderiv ℝ (fderiv ℝ f) u` in the two slots.

H. Differentiability and locality

Schwarz (§I) and the coordinate layer treat a directional derivative as a field in the base point `p`, and need two regularity facts about it. Both are public packagings of §G, consumed in `Coordinate.lean`.

**Differentiability.** On a `C²` field the directional derivative `p ↦ ∂_v f` is itself real-differentiable (`differentiableAt_dWirtingerDir`): by §G it is a `weightedDirDeriv`, and `fderiv ℝ f` is differentiable for a `C²` `f`. Without this a Wirtinger derivative could not be differentiated a second time, as Schwarz (§I) does.

**Locality.** The value `∂_v f` at `u` depends only on how `f` behaves near `u`, inherited from `fderiv ℝ f u`: the operator is built from it, and a Fréchet derivative is fixed by `f` on an arbitrarily small neighbourhood. So if `f₁` and `f₂` coincide on some neighbourhood of `u` (in Lean `f₁ =ᶠ[nhds u] f₂`, where `=ᶠ` is equality on a filter-large set and `[nhds u]` is the neighbourhood filter of `u`) they have the same directional derivative at `u` (`dWirtingerDir_congr_of_eventuallyEq`). This is what makes the operators usable on functions regular only on a restricted domain (the Kähler potentials, defined on a slit domain rather than all of `V`): the derivative at `u` needs only `f` near `u`, so a consumer may swap `f` for a locally-equal representative and rely on the local `C²`/holomorphy hypotheses (`ContDiffAt`, `DifferentiableAt`), which likewise depend only on `f` near `u`: their `...At` form asks for regularity only on a neighbourhood of `u`, which a restricted-domain function has at each point of its domain.

I. Schwarz's theorem

34 declarations

definition

Weighted directional derivative field $p \mapsto \frac{1}{2} (d_{b_1} f(p) + c \cdot d_{b_2} f(p))$

#weightedDirDeriv

Given a function $f: V \to \mathbb{C}$ defined on a complex vector space $V$ , a complex weight $c \in \mathbb{C}$ , and two directions $b_1, b_2 \in V$ , this definition is the function mapping a base point $p \in V$ to the weighted combination of real Fréchet derivatives: $p \mapsto \frac{1}{2} (d_{b_1} f(p) + c \cdot d_{b_2} f(p))$ where $d_v f(p)$ denotes the real Fréchet derivative of $f$ at the point $p$ in the direction $v$ .

definition

Holomorphic directional Wirtinger derivative $\partial_v f$

#dWirtingerDir

Given a function $f: V \to \mathbb{C}$ defined on a complex vector space $V$ , a direction vector $v \in V$ , and a base point $u \in V$ , the **holomorphic directional Wirtinger derivative** $\partial_v f(u)$ is defined as: $\partial_v f(u) = \frac{1}{2} \left( d_v f(u) - i \cdot d_{i \cdot v} f(u) \right)$ where $d_v f(u)$ denotes the real Fréchet derivative of $f$ at the point $u$ in the direction $v$ , and $i \cdot v$ is the direction $v$ transformed by the complex structure of $V$ . This corresponds to the weighted directional derivative field with weight $c = -i$ and directions $b_1 = v, b_2 = i \cdot v$ .

definition

Anti-holomorphic directional Wirtinger derivative $\bar{\partial}_v f$

#dWirtingerAntiDir

For a function $f: V \to \mathbb{C}$ defined on a complex vector space $V$ , the anti-holomorphic directional Wirtinger derivative at a base point $u \in V$ along a direction $v \in V$ is defined as: $\bar{\partial}_v f(u) = \frac{1}{2} (d_v f(u) + i d_{iv} f(u))$ where $d_v f(u)$ (also denoted as $fderiv \mathbb{R} f u v$ ) represents the real Fréchet derivative of $f$ at the point $u$ in the direction $v$ .

theorem

$\partial_v g = \frac{1}{2} (d_v g - i d_{iv} g)$

#dWirtingerDir_apply

For a function $g : V \to \mathbb{C}$ defined on a complex vector space $V$ , the holomorphic directional Wirtinger derivative $\partial_v g$ at a base point $u \in V$ along a direction $v \in V$ is given by: $\partial_v g(u) = \frac{1}{2} (d_v g(u) - i \cdot d_{iv} g(u))$ where $d_v g(u)$ denotes the real Fréchet derivative of $g$ at $u$ in the direction $v$ , and $i v$ is the direction $v$ transformed by the complex structure of $V$ .

theorem

$\bar{\partial}_v g = \frac{1}{2} (d_v g + i d_{iv} g)$

#dWirtingerAntiDir_apply

For a function $g: V \to \mathbb{C}$ defined on a complex vector space $V$ , the anti-holomorphic directional Wirtinger derivative $\bar{\partial}_v g$ at a base point $u \in V$ along a direction $v \in V$ is given by the formula: $\bar{\partial}_v g(u) = \frac{1}{2} \left( d_v g(u) + i d_{iv} g(u) \right)$ where $d_v g(u)$ (the real Fréchet derivative $fderiv \mathbb{R} g u v$ ) denotes the derivative of $g$ at the point $u$ in the direction $v$ , and $iv$ is the direction $v$ transformed by the complex structure of $V$ .

theorem

$\partial_v c = 0$

#dWirtingerDir_const

Let $V$ be a complex vector space. For any constant $c \in \mathbb{C}$ , the holomorphic directional Wirtinger derivative $\partial_v$ of the constant function $p \mapsto c$ at a point $u \in V$ along a direction $v \in V$ is zero: $\partial_v c = 0$ This property follows from the fact that the real Fréchet derivative of a constant function is zero in any direction.

theorem

$\bar{\partial}_v c = 0$

#dWirtingerAntiDir_const

For any constant $c \in \mathbb{C}$ and any vectors $v, u \in V$ in a complex vector space $V$ , the anti-holomorphic directional Wirtinger derivative of the constant function $f(p) = c$ at the base point $u$ along the direction $v$ is zero: $\bar{\partial}_v c = 0$

theorem

$\partial_v (-g) = -\partial_v g$

#dWirtingerDir_neg

Let $V$ be a complex vector space. For any function $g: V \to \mathbb{C}$ , any direction vector $v \in V$ , and any base point $u \in V$ , the holomorphic directional Wirtinger derivative $\partial_v$ of the negated function $-g$ is the negation of the derivative of $g$ : $\partial_v (-g)(u) = -\partial_v g(u)$ This property holds without requiring $g$ to be differentiable, as it inherits the linearity of the underlying real Fréchet derivative.

theorem

$\bar{\partial}_v (-g) = -\bar{\partial}_v g$

#dWirtingerAntiDir_neg

For any function $g: V \to \mathbb{C}$ and any vectors $v, u \in V$ , the anti-holomorphic directional Wirtinger derivative of the negated function $-g$ at the base point $u$ along the direction $v$ satisfies $\bar{\partial}_v (-g)(u) = -\bar{\partial}_v g(u)$

theorem

$\partial_v(g + h) = \partial_v g + \partial_v h$

#dWirtingerDir_add

Let $V$ be a complex vector space, $u, v \in V$ be a base point and a direction vector, and $g, h: V \to \mathbb{C}$ be functions. If $g$ and $h$ are real-differentiable at $u$ , then the holomorphic directional Wirtinger derivative of their sum satisfies: $\partial_v (g + h)(u) = \partial_v g(u) + \partial_v h(u)$

theorem

$\bar{\partial}_v (g + h) = \bar{\partial}_v g + \bar{\partial}_v h$

#dWirtingerAntiDir_add

Let $V$ be a complex vector space, and let $g, h: V \to \mathbb{C}$ be functions that are real-differentiable at a base point $u \in V$ . For any direction $v \in V$ , the anti-holomorphic directional Wirtinger derivative $\bar{\partial}_v$ is additive: $\bar{\partial}_v (g + h)(u) = \bar{\partial}_v g(u) + \bar{\partial}_v h(u)$ where $(g+h)$ denotes the pointwise sum of the functions.

theorem

$\partial_v (c \cdot g) = c \cdot \partial_v g$

#dWirtingerDir_smul

Let $V$ be a complex vector space, $u, v \in V$ be a base point and a direction vector, and $c \in \mathbb{C}$ be a complex scalar. If $g: V \to \mathbb{C}$ is a function that is real-differentiable at $u$ , then the holomorphic directional Wirtinger derivative of the scalar product $c \cdot g$ satisfies: $\partial_v (c \cdot g)(u) = c \cdot \partial_v g(u)$

theorem

$\bar{\partial}_v (c \cdot g) = c \bar{\partial}_v g$

#dWirtingerAntiDir_smul

Let $V$ be a complex vector space and $g: V \to \mathbb{C}$ be a function. If $g$ is real-differentiable at a point $u \in V$ , then for any complex scalar $c \in \mathbb{C}$ and any direction $v \in V$ , the anti-holomorphic directional Wirtinger derivative $\bar{\partial}_v$ satisfies: $\bar{\partial}_v (c \cdot g)(u) = c \cdot \bar{\partial}_v g(u)$ where $(c \cdot g)$ is the function defined by $(c \cdot g)(p) = c \cdot g(p)$ .

theorem

Leibniz Rule for the Holomorphic Directional Wirtinger Derivative $\partial_v(g \cdot h) = (\partial_v g) h + g (\partial_v h)$

#dWirtingerDir_mul

Let $V$ be a complex vector space and $u, v \in V$ be a base point and a direction vector, respectively. If the functions $g, h : V \to \mathbb{C}$ are real-differentiable at $u$ , then the holomorphic directional Wirtinger derivative of their product $g \cdot h$ satisfies the Leibniz rule: $\partial_v (g \cdot h)(u) = \partial_v g(u) \cdot h(u) + g(u) \cdot \partial_v h(u)$ where $\partial_v$ denotes the holomorphic directional Wirtinger derivative `dWirtingerDir`.

theorem

Wirtinger Leibniz rule: $\bar{\partial}_v(g \cdot h) = \bar{\partial}_v g \cdot h + g \cdot \bar{\partial}_v h$

#dWirtingerAntiDir_mul

Let $V$ be a complex vector space and $g, h: V \to \mathbb{C}$ be two functions that are real-differentiable at a point $u \in V$ . For any direction $v \in V$ , the anti-holomorphic directional Wirtinger derivative $\bar{\partial}_v$ of the product $g \cdot h$ at $u$ satisfies the Leibniz rule: $\bar{\partial}_v(g \cdot h)(u) = \bar{\partial}_v g(u) \cdot h(u) + g(u) \cdot \bar{\partial}_v h(u)$

theorem

Finite-sum rule for the holomorphic Wirtinger derivative: $\partial_v (\sum F_a) = \sum \partial_v F_a$

#dWirtingerDir_fun_sum

Let $V$ be a complex vector space and $s$ be a finite set of indices. Let $\{F_a\}_{a \in s}$ be a family of functions $F_a : V \to \mathbb{C}$ such that each $F_a$ is real-differentiable at a point $u \in V$ . Then for any direction $v \in V$ , the holomorphic directional Wirtinger derivative of the sum $\sum_{a \in s} F_a$ at $u$ is the sum of the holomorphic directional Wirtinger derivatives of the individual functions: $\partial_v \left( \sum_{a \in s} F_a \right)(u) = \sum_{a \in s} \partial_v F_a(u)$

theorem

Finite-sum rule for the anti-holomorphic Wirtinger derivative: $\bar{\partial}_v (\sum F_a) = \sum \bar{\partial}_v F_a$

#dWirtingerAntiDir_fun_sum

Let $V$ be a complex vector space and $s$ be a finite set of indices. Let $\{F_a\}_{a \in s}$ be a family of functions $F_a : V \to \mathbb{C}$ such that each $F_a$ is real-differentiable at a point $u \in V$ . Then for any direction $v \in V$ , the anti-holomorphic directional Wirtinger derivative of the sum $\sum_{a \in s} F_a$ at $u$ is the sum of the anti-holomorphic directional Wirtinger derivatives of the individual functions: $\bar{\partial}_v \left( \sum_{a \in s} F_a \right)(u) = \sum_{a \in s} \bar{\partial}_v F_a(u)$

theorem

The real Fréchet derivative commutes with complex conjugation ( $d\bar{f} = \overline{df}$ )

#fderiv_star_eq

Let $E$ be a real normed vector space and $f: E \to \mathbb{C}$ be a function that is real-differentiable at a point $u \in E$ . The real Fréchet derivative of the pointwise conjugate function $p \mapsto \overline{f(p)}$ at $u$ is equal to the complex conjugation map (denoted as `conjCLE`) composed with the real Fréchet derivative of $f$ at $u$ . In physicists' notation, this is expressed as $d\bar{f} = \text{conj}(df)$ .

theorem

$\partial_v \bar{f} = \overline{\bar{\partial}_v f}$

#dWirtingerDir_star_comp

Let $f: V \to \mathbb{C}$ be a function on a complex vector space $V$ that is real-differentiable at a point $u \in V$ . For any direction $v \in V$ , the holomorphic directional Wirtinger derivative of the pointwise conjugate function $\bar{f}$ (defined by $\bar{f}(p) = \overline{f(p)}$ ) at $u$ is equal to the complex conjugate of the anti-holomorphic directional Wirtinger derivative of $f$ at $u$ : $\partial_v \bar{f}(u) = \overline{\bar{\partial}_v f(u)}$ where $\partial_v$ and $\bar{\partial}_v$ denote the holomorphic and anti-holomorphic directional Wirtinger derivatives, respectively.

theorem

$\bar{\partial}_v \bar{f} = \overline{\partial_v f}$

#dWirtingerAntiDir_star_comp

Let $f: V \to \mathbb{C}$ be a function on a complex vector space $V$ that is real-differentiable at a point $u \in V$ . For any direction $v \in V$ , the anti-holomorphic directional Wirtinger derivative of the pointwise conjugate function $\bar{f}$ (defined by $\bar{f}(p) = \overline{f(p)}$ ) is equal to the complex conjugate of the holomorphic directional Wirtinger derivative of $f$ : $\bar{\partial}_v \bar{f}(u) = \overline{\partial_v f(u)}$ where $\bar{\partial}_v$ and $\partial_v$ denote the anti-holomorphic and holomorphic directional Wirtinger derivatives, respectively.

theorem

Wirtinger decomposition $L(w) = a w + b \bar{w}$ for real-linear $L: \mathbb{C} \to \mathbb{C}$

#realLinear_apply_eq_wirtinger

Let $L: \mathbb{C} \to \mathbb{C}$ be a continuous real-linear map. For any complex number $w \in \mathbb{C}$ , $L(w)$ can be split into a holomorphic and an anti-holomorphic part according to the formula: $L(w) = \frac{1}{2}(L(1) - i L(i)) w + \frac{1}{2}(L(1) + i L(i)) \bar{w}$ where $i$ is the imaginary unit and $\bar{w}$ denotes the complex conjugate of $w$ . The coefficients $a = \frac{1}{2}(L(1) - i L(i))$ and $b = \frac{1}{2}(L(1) + i L(i))$ are known as the Wirtinger weights of the map $L$ .

theorem

Wirtinger chain rule for $\partial_v (g \circ f)$

#dWirtingerDir_comp

Let $V$ be a complex vector space. For any direction $v \in V$ and base point $u \in V$ , let $f: V \to \mathbb{C}$ be a function real-differentiable at $u$ , and let $g: \mathbb{C} \to \mathbb{C}$ be a function real-differentiable at $f(u)$ . The holomorphic directional Wirtinger derivative of the composite function $g \circ f$ at $u$ is given by the two-term chain rule: $\partial_v (g \circ f)(u) = \partial_1 g(f(u)) \cdot \partial_v f(u) + \bar{\partial}_1 g(f(u)) \cdot \partial_v \bar{f}(u)$ where $\partial_1 g$ and $\bar{\partial}_1 g$ (also denoted as $\frac{\partial g}{\partial f}$ and $\frac{\partial g}{\partial \bar{f}}$ ) are the holomorphic and anti-holomorphic Wirtinger derivatives of $g$ evaluated at $f(u)$ in the unit direction $1 \in \mathbb{C}$ , and $\bar{f}$ denotes the pointwise complex conjugate function $p \mapsto \overline{f(p)}$ .

theorem

Anti-holomorphic Wirtinger Chain Rule: $\bar{\partial}_v(g \circ f) = \frac{\partial g}{\partial f} \bar{\partial}_v f + \frac{\partial g}{\partial \bar{f}} \bar{\partial}_v \bar{f}$

#dWirtingerAntiDir_comp

Let $V$ be a complex vector space. Suppose $f: V \to \mathbb{C}$ is a function real-differentiable at $u \in V$ , and $g: \mathbb{C} \to \mathbb{C}$ is a function real-differentiable at $f(u)$ . For any direction $v \in V$ , the anti-holomorphic directional Wirtinger derivative of the composition $g \circ f$ at $u$ is given by the two-term chain rule: $\bar{\partial}_v(g \circ f)(u) = \partial_1 g(f(u)) \cdot \bar{\partial}_v f(u) + \bar{\partial}_1 g(f(u)) \cdot \bar{\partial}_v \bar{f}(u)$ where $\partial_1 g$ and $\bar{\partial}_1 g$ are the holomorphic and anti-holomorphic Wirtinger derivatives of $g$ in the direction $1 \in \mathbb{C}$ , and $\bar{f}$ denotes the pointwise complex conjugate of $f$ .

theorem

$\partial_v (g \circ L) = \bar{\partial}_{L v} g$ for Conjugate-Linear $L$

#dWirtingerDir_comp_conjLinear

Let $V$ and $V'$ be complex vector spaces. Suppose $L: V \to V'$ is a continuous $\mathbb{R}$ -linear map that is conjugate-linear, satisfying $L(i \cdot x) = -i \cdot L(x)$ for all $x \in V$ . Let $g: V' \to \mathbb{C}$ be a function that is real-differentiable at $L(u)$ for some base point $u \in V$ . Then for any direction $v \in V$ , the holomorphic directional Wirtinger derivative of the composition $g \circ L$ at $u$ along $v$ is equal to the anti-holomorphic directional Wirtinger derivative of $g$ at $L(u)$ along the direction $L(v)$ : $\partial_v (g \circ L)(u) = \bar{\partial}_{L v} g(L u)$

theorem

$\bar{\partial}_v (g \circ L) = \partial_{L v} g$ for conjugate-linear $L$

#dWirtingerAntiDir_comp_conjLinear

Let $V$ and $V'$ be complex vector spaces. Let $g : V' \to \mathbb{C}$ be a function and $L : V \to V'$ be a continuous $\mathbb{R}$ -linear map. Suppose $L$ is conjugate- $\mathbb{C}$ -linear, meaning $L(i \cdot x) = -i \cdot L(x)$ for all $x \in V$ . If $g$ is real-differentiable at $L(u)$ for some base point $u \in V$ , then for any direction $v \in V$ , the anti-holomorphic directional Wirtinger derivative of the composition $g \circ L$ at $u$ along $v$ equals the holomorphic directional Wirtinger derivative of $g$ at $L(u)$ along $L(v)$ : $\bar{\partial}_v (g \circ L)(u) = \partial_{L v} g (L u)$

theorem

$\partial_v f = d_v f$ for $\mathbb{C}$ -Linear Directions

#dWirtingerDir_eq_of_clinear

For a function $f: V \to \mathbb{C}$ on a complex vector space $V$ , along a direction $v \in V$ where the real Fréchet derivative at a point $u \in V$ is $\mathbb{C}$ -linear (that is, $d_{i \cdot v} f(u) = i \cdot d_v f(u)$ ), a **holomorphic collapse** occurs where the holomorphic directional Wirtinger derivative $\partial_v f(u)$ is equal to the real Fréchet derivative $d_v f(u)$ .

theorem

$\bar{\partial}_v f = 0$ if the real derivative is $\mathbb{C}$ -linear along $v$

#dWirtingerAntiDir_eq_zero_of_clinear

Let $f: V \to \mathbb{C}$ be a function on a complex vector space $V$ . If the real Fréchet derivative of $f$ at a point $u \in V$ is $\mathbb{C}$ -linear in the direction $v \in V$ , satisfying $d_{iv} f(u) = i d_v f(u)$ , then the anti-holomorphic directional Wirtinger derivative of $f$ at $u$ along $v$ vanishes: $\bar{\partial}_v f(u) = 0$

theorem

$\partial_v f = 0$ if the real derivative is conjugate-linear along $v$

#dWirtingerDir_eq_zero_of_antilinear

Let $f: V \to \mathbb{C}$ be a function defined on a complex vector space $V$ . If the real Fréchet derivative of $f$ at a point $u \in V$ is conjugate-linear in the direction $v \in V$ , satisfying the condition $d_{i \cdot v} f(u) = -i \cdot d_v f(u)$ , then the holomorphic directional Wirtinger derivative of $f$ at $u$ along $v$ vanishes: $\partial_v f(u) = 0$

theorem

$\bar{\partial}_v f = d_v f$ for conjugate-linear derivatives

#dWirtingerAntiDir_eq_of_antilinear

Let $V$ be a complex vector space and $f: V \to \mathbb{C}$ a function. For any direction $v \in V$ , if the real Fréchet derivative of $f$ at a point $u$ is conjugate-linear along $v$ , meaning it satisfies the condition $d_{iv} f(u) = -i d_v f(u)$ , then the anti-holomorphic directional Wirtinger derivative $\bar{\partial}_v f(u)$ is equal to the real derivative $d_v f(u)$ .

theorem

$f \in C^2 \implies \partial_v f$ is real-differentiable

#differentiableAt_dWirtingerDir

Let $V$ be a complex vector space and $f: V \to \mathbb{C}$ be a function. If $f$ is twice continuously differentiable (in the real sense) at a point $u \in V$ (i.e., $f \in C^2$ at $u$ ), then for any direction $v \in V$ , the holomorphic directional Wirtinger derivative field $p \mapsto \partial_v f(p)$ is real-differentiable at $u$ .

theorem

$f \in C^2 \implies \bar{\partial}_w f$ is real-differentiable

#differentiableAt_dWirtingerAntiDir

Let $V$ be a complex vector space and $f: V \to \mathbb{C}$ be a function. If $f$ is twice continuously differentiable (in the real sense) at a point $u \in V$ (i.e., $f \in C^2$ at $u$ ), then for any direction $w \in V$ , the anti-holomorphic directional Wirtinger derivative field $p \mapsto \bar{\partial}_w f(p)$ is real-differentiable at $u$ .

theorem

Local Equality of Functions Implies Equality of $\partial_v f$

#dWirtingerDir_congr_of_eventuallyEq

Let $V$ be a complex vector space and $u \in V$ be a base point. If two functions $f_1, f_2: V \to \mathbb{C}$ are equal on some neighborhood of $u$ , then for any direction $v \in V$ , their holomorphic directional Wirtinger derivatives at $u$ are equal: $\partial_v f_1(u) = \partial_v f_2(u)$

theorem

Local Equality of Functions Implies Equality of $\bar{\partial}_v f$

#dWirtingerAntiDir_congr_of_eventuallyEq

Let $V$ be a complex vector space and $u \in V$ be a base point. If two functions $f_1, f_2: V \to \mathbb{C}$ are equal on some neighborhood of $u$ , then for any direction $v \in V$ , their anti-holomorphic directional Wirtinger derivatives at $u$ are equal: $\bar{\partial}_v f_1(u) = \bar{\partial}_v f_2(u)$

theorem

$\partial_v \bar{\partial}_w f = \bar{\partial}_w \partial_v f$ for $C^2$ functions (Schwarz's Theorem)

#dWirtingerDir_dWirtingerAntiDir_comm

Let $V$ be a complex vector space and $f: V \to \mathbb{C}$ be a function. If $f$ is twice continuously real-differentiable (of class $C^2$ ) at a base point $u \in V$ , then for any two direction vectors $v, w \in V$ , the holomorphic directional Wirtinger derivative along $v$ and the anti-holomorphic directional Wirtinger derivative along $w$ commute at $u$ : $\partial_v (\bar{\partial}_w f)(u) = \bar{\partial}_w (\partial_v f)(u)$ Here, $\partial_v$ denotes the holomorphic directional Wirtinger derivative defined by $\partial_v f = \frac{1}{2}(d_v f - i d_{iv} f)$ , and $\bar{\partial}_w$ denotes the anti-holomorphic directional Wirtinger derivative defined by $\bar{\partial}_w f = \frac{1}{2}(d_w f + i d_{iw} f)$ , where $d$ is the real Fréchet derivative.

Physlib.Mathematics.Calculus.Wirtinger.Basic

Wirtinger calculus

Notation

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. The directional Wirtinger operators

B. Real-linearity and the Leibniz rule

C. Conjugation

D. The Wirtinger chain rule

E. Domain conjugation

F. The holomorphic collapse

G. The second-derivative bridge

H. Differentiability and locality

I. Schwarz's theorem

Weighted directional derivative field p↦12(db1f(p)+c⋅db2f(p))p \mapsto \frac{1}{2} (d_{b_1} f(p) + c \cdot d_{b_2} f(p))p↦21​(db1​​f(p)+c⋅db2​​f(p))

Holomorphic directional Wirtinger derivative ∂vf\partial_v f∂v​f

Anti-holomorphic directional Wirtinger derivative ∂ˉvf\bar{\partial}_v f∂ˉv​f

∂vg=12(dvg−idivg)\partial_v g = \frac{1}{2} (d_v g - i d_{iv} g)∂v​g=21​(dv​g−idiv​g)

∂ˉvg=12(dvg+idivg)\bar{\partial}_v g = \frac{1}{2} (d_v g + i d_{iv} g)∂ˉv​g=21​(dv​g+idiv​g)

∂vc=0\partial_v c = 0∂v​c=0

∂ˉvc=0\bar{\partial}_v c = 0∂ˉv​c=0

∂v(−g)=−∂vg\partial_v (-g) = -\partial_v g∂v​(−g)=−∂v​g

∂ˉv(−g)=−∂ˉvg\bar{\partial}_v (-g) = -\bar{\partial}_v g∂ˉv​(−g)=−∂ˉv​g

∂v(g+h)=∂vg+∂vh\partial_v(g + h) = \partial_v g + \partial_v h∂v​(g+h)=∂v​g+∂v​h

∂ˉv(g+h)=∂ˉvg+∂ˉvh\bar{\partial}_v (g + h) = \bar{\partial}_v g + \bar{\partial}_v h∂ˉv​(g+h)=∂ˉv​g+∂ˉv​h

∂v(c⋅g)=c⋅∂vg\partial_v (c \cdot g) = c \cdot \partial_v g∂v​(c⋅g)=c⋅∂v​g

∂ˉv(c⋅g)=c∂ˉvg\bar{\partial}_v (c \cdot g) = c \bar{\partial}_v g∂ˉv​(c⋅g)=c∂ˉv​g

Leibniz Rule for the Holomorphic Directional Wirtinger Derivative ∂v(g⋅h)=(∂vg)h+g(∂vh)\partial_v(g \cdot h) = (\partial_v g) h + g (\partial_v h)∂v​(g⋅h)=(∂v​g)h+g(∂v​h)

Wirtinger Leibniz rule: ∂ˉv(g⋅h)=∂ˉvg⋅h+g⋅∂ˉvh\bar{\partial}_v(g \cdot h) = \bar{\partial}_v g \cdot h + g \cdot \bar{\partial}_v h∂ˉv​(g⋅h)=∂ˉv​g⋅h+g⋅∂ˉv​h

Finite-sum rule for the holomorphic Wirtinger derivative: ∂v(∑Fa)=∑∂vFa\partial_v (\sum F_a) = \sum \partial_v F_a∂v​(∑Fa​)=∑∂v​Fa​

Finite-sum rule for the anti-holomorphic Wirtinger derivative: ∂ˉv(∑Fa)=∑∂ˉvFa\bar{\partial}_v (\sum F_a) = \sum \bar{\partial}_v F_a∂ˉv​(∑Fa​)=∑∂ˉv​Fa​

The real Fréchet derivative commutes with complex conjugation (dfˉ=df‾d\bar{f} = \overline{df}dfˉ​=df​)

∂vfˉ=∂ˉvf‾\partial_v \bar{f} = \overline{\bar{\partial}_v f}∂v​fˉ​=∂ˉv​f​

∂ˉvfˉ=∂vf‾\bar{\partial}_v \bar{f} = \overline{\partial_v f}∂ˉv​fˉ​=∂v​f​

Wirtinger decomposition L(w)=aw+bwˉL(w) = a w + b \bar{w}L(w)=aw+bwˉ for real-linear L:C→CL: \mathbb{C} \to \mathbb{C}L:C→C

Wirtinger chain rule for ∂v(g∘f)\partial_v (g \circ f)∂v​(g∘f)

Anti-holomorphic Wirtinger Chain Rule: ∂ˉv(g∘f)=∂g∂f∂ˉvf+∂g∂fˉ∂ˉvfˉ\bar{\partial}_v(g \circ f) = \frac{\partial g}{\partial f} \bar{\partial}_v f + \frac{\partial g}{\partial \bar{f}} \bar{\partial}_v \bar{f}∂ˉv​(g∘f)=∂f∂g​∂ˉv​f+∂fˉ​∂g​∂ˉv​fˉ​

∂v(g∘L)=∂ˉLvg\partial_v (g \circ L) = \bar{\partial}_{L v} g∂v​(g∘L)=∂ˉLv​g for Conjugate-Linear LLL

∂ˉv(g∘L)=∂Lvg\bar{\partial}_v (g \circ L) = \partial_{L v} g∂ˉv​(g∘L)=∂Lv​g for conjugate-linear LLL

∂vf=dvf\partial_v f = d_v f∂v​f=dv​f for C\mathbb{C}C-Linear Directions

∂ˉvf=0\bar{\partial}_v f = 0∂ˉv​f=0 if the real derivative is C\mathbb{C}C-linear along vvv

∂vf=0\partial_v f = 0∂v​f=0 if the real derivative is conjugate-linear along vvv

∂ˉvf=dvf\bar{\partial}_v f = d_v f∂ˉv​f=dv​f for conjugate-linear derivatives

f∈C2 ⟹ ∂vff \in C^2 \implies \partial_v ff∈C2⟹∂v​f is real-differentiable

f∈C2 ⟹ ∂ˉwff \in C^2 \implies \bar{\partial}_w ff∈C2⟹∂ˉw​f is real-differentiable

Local Equality of Functions Implies Equality of ∂vf\partial_v f∂v​f

Local Equality of Functions Implies Equality of ∂ˉvf\bar{\partial}_v f∂ˉv​f

∂v∂ˉwf=∂ˉw∂vf\partial_v \bar{\partial}_w f = \bar{\partial}_w \partial_v f∂v​∂ˉw​f=∂ˉw​∂v​f for C2C^2C2 functions (Schwarz's Theorem)

Weighted directional derivative field $p \mapsto \frac{1}{2} (d_{b_1} f(p) + c \cdot d_{b_2} f(p))$

Holomorphic directional Wirtinger derivative $\partial_v f$

Anti-holomorphic directional Wirtinger derivative $\bar{\partial}_v f$

$\partial_v g = \frac{1}{2} (d_v g - i d_{iv} g)$

$\bar{\partial}_v g = \frac{1}{2} (d_v g + i d_{iv} g)$

$\partial_v c = 0$

$\bar{\partial}_v c = 0$

$\partial_v (-g) = -\partial_v g$

$\bar{\partial}_v (-g) = -\bar{\partial}_v g$

$\partial_v(g + h) = \partial_v g + \partial_v h$

$\bar{\partial}_v (g + h) = \bar{\partial}_v g + \bar{\partial}_v h$

$\partial_v (c \cdot g) = c \cdot \partial_v g$

$\bar{\partial}_v (c \cdot g) = c \bar{\partial}_v g$

Leibniz Rule for the Holomorphic Directional Wirtinger Derivative $\partial_v(g \cdot h) = (\partial_v g) h + g (\partial_v h)$

Wirtinger Leibniz rule: $\bar{\partial}_v(g \cdot h) = \bar{\partial}_v g \cdot h + g \cdot \bar{\partial}_v h$

Finite-sum rule for the holomorphic Wirtinger derivative: $\partial_v (\sum F_a) = \sum \partial_v F_a$

Finite-sum rule for the anti-holomorphic Wirtinger derivative: $\bar{\partial}_v (\sum F_a) = \sum \bar{\partial}_v F_a$

The real Fréchet derivative commutes with complex conjugation ( $d\bar{f} = \overline{df}$ )

$\partial_v \bar{f} = \overline{\bar{\partial}_v f}$

$\bar{\partial}_v \bar{f} = \overline{\partial_v f}$

Wirtinger decomposition $L(w) = a w + b \bar{w}$ for real-linear $L: \mathbb{C} \to \mathbb{C}$

Wirtinger chain rule for $\partial_v (g \circ f)$

Anti-holomorphic Wirtinger Chain Rule: $\bar{\partial}_v(g \circ f) = \frac{\partial g}{\partial f} \bar{\partial}_v f + \frac{\partial g}{\partial \bar{f}} \bar{\partial}_v \bar{f}$

$\partial_v (g \circ L) = \bar{\partial}_{L v} g$ for Conjugate-Linear $L$

$\bar{\partial}_v (g \circ L) = \partial_{L v} g$ for conjugate-linear $L$

$\partial_v f = d_v f$ for $\mathbb{C}$ -Linear Directions

$\bar{\partial}_v f = 0$ if the real derivative is $\mathbb{C}$ -linear along $v$

$\partial_v f = 0$ if the real derivative is conjugate-linear along $v$

$\bar{\partial}_v f = d_v f$ for conjugate-linear derivatives

$f \in C^2 \implies \partial_v f$ is real-differentiable

$f \in C^2 \implies \bar{\partial}_w f$ is real-differentiable

Local Equality of Functions Implies Equality of $\partial_v f$

Local Equality of Functions Implies Equality of $\bar{\partial}_v f$

$\partial_v \bar{\partial}_w f = \bar{\partial}_w \partial_v f$ for $C^2$ functions (Schwarz's Theorem)