Research proof index

The two-term Wirtinger chain rule for dWirtingerDir, outer g : ℂ → ℂ and inner f : V → ℂ: ∂_v(g∘f) = (∂g/∂f)·∂_v f + (∂g/∂f̄)·∂_v f̄. realLinear_apply_eq_wirtinger splits the chain rule's outer ℝ-linear factor into the ∂g/∂f, ∂g/∂f̄ coefficients, each multiplying its inner directional derivative ∂_v f, ∂_v f̄.

Schwarz's theorem for the directional Wirtinger operators: on a C² field f the holomorphic and anti-holomorphic directional derivatives commute in any two directions, ∂_v ∂̄_w f = ∂̄_w ∂_v f. The commutation adds no analytic input. By the §G bridge each order expands into a real-linear combination of the second real Fréchet derivative `fderiv ℝ...

Conjugating the function swaps the operators up to an outer conjugation: ∂_v f̄ = conj (∂̄_v f).

Prefix-event split for a bind. Prefix points satisfying p are charged in full; off-prefix continuations are charged by the uniform tail bound ε.

Convex prefix-event split for a bind. The off-prefix tail bound ε is charged only on the mass outside p, giving Pr[p] + (1 - Pr[p]) * ε.

First-moment / Markov bound (support-restricted cost). Variant of probEvent_le_tsum_probOutput_mul_cost whose c ≥ 1 hypothesis need only hold on the support of mx.