Proofs for the Taylor cut lemma #
- Jets (
fst_aeval_dualNumber,snd_aeval_dualNumber,aeval_jet): over the dual numbersR[ε], a polynomial takes the valueP(x) + ε ∑ⱼ ∂ⱼP(x) dⱼatx + ε d. Applied twice, overL[s][t] = L[s, t]/(s², t²)it takes ata + s v + t uthe value with coefficientsP(a),∇P(a) · v,∇P(a) · uandvᵀ H u, whereHis the Hessian ofPata. - Formal evaluation (
trace_eq_aeval_wirePolynomial): over every commutative algebra, the value of a wire is its wire polynomial evaluated at the input. - The cut kernel (
cutKernel): the directionsδalong which no crossing wire moves to first order. It has codimension at most the number of crossing signals. - Mixing jets: two jets whose crossing wires agree have equal boundary keys, so cut and paste
(
SingleCut.trace_mix) and the vanishing mixed second difference (trace_add_trace_eq_trace_mix_add_trace_mix) apply overL[s, t]. Reading off coefficients shows that the cut kernel splits into its parts on the two sides of the cut, that a direction on one side does not move the wires of the other side, and that the Hessian of every wire pairs the two sides to zero. - Linear algebra (
finrank_add_finrank_add_rank_le): subspacesVandWorthogonal through a matrixBhavedim V + dim W + rank B ≤the sum of the dimensions, by Sylvester's rank inequality applied to basis matrices.
Jets #
The real part of a polynomial at a dual number is its value at the real parts.
First-order Taylor expansion. The dual part of P(x + ε d) is ∑ⱼ ∂ⱼP(x) dⱼ.
First-order Taylor expansion at a point of L.
The point a + s v + t u over L[s][t] = L[s, t]/(s², t²).
Equations
- Algebraic.Cutwidth.MultiOutput.Taylor.Internal.jet a v u j = TrivSqZeroExt.inl (TrivSqZeroExt.inl (a j) + TrivSqZeroExt.inr (v j)) + TrivSqZeroExt.inr (TrivSqZeroExt.inl (u j))
Instances For
Second-order Taylor expansion. At a + s v + t u, a polynomial takes the value
P(a) + s ∇P(a)·v + t ∇P(a)·u + s t vᵀ H u, with H its Hessian at a.
The second derivatives of a product of two variables. ∂ₖ ∂ₗ (Xₚ X_q) is the number of
ways to match (l, k) with (p, q) or (q, p).
Formal evaluation #
Evaluating a program with polynomial gates commutes with algebra homomorphisms.
Over every commutative algebra, a wire carries its wire polynomial evaluated at the input.
The cut kernel #
The value of every wire at a jet.
Two inputs with the same values on every crossing wire have the same boundary key.
The cut kernel: the directions along which no crossing wire moves to first order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cut kernel has codimension at most the number of crossing signals.
A direction in the cut kernel and the zero direction give jets with equal boundary keys.
The left part of a kernel direction. Moving only the inputs in S along a kernel
direction moves the wires in S as the full direction does and fixes the other wires.
The right part of a kernel direction.
The Hessian pairs the two sides to zero. For kernel directions v on the inputs in S
and u on the other inputs, the second-order cross term of every wire vanishes.
The linear map keeping the coordinates of the inputs in S and zeroing the others.
Equations
- Algebraic.Cutwidth.MultiOutput.Taylor.Internal.mixLeft S = { toFun := fun (δ : Fin n → L) => Algebraic.Cutwidth.SingleCut.mix S δ 0, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The linear map keeping the coordinates of the inputs outside S and zeroing the others.
Equations
- Algebraic.Cutwidth.MultiOutput.Taylor.Internal.mixRight S = { toFun := fun (δ : Fin n → L) => Algebraic.Cutwidth.SingleCut.mix S 0 δ, map_add' := ⋯, map_smul' := ⋯ }
Instances For
One-sided forward determination. A direction supported on inputsIn S that fixes the
forward signals to first order fixes every wire outside S to first order.
One-sided backward determination. Symmetrically, a direction supported outside
inputsIn S that fixes the backward signals to first order fixes every wire in S to first
order.
The subspace of directions on X annihilated by the rows C of M, extended by zero
outside X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Vectors of matSubKer M X C vanish outside X.
Vectors of matSubKer M X C are annihilated by the rows C of M.
The directed Taylor cut lemma. There are subspaces V of directions on the inputs in S
and W of directions on the other inputs, with |X_S| ≤ dim V + |forward S| and
|X_T| ≤ dim W + |backward S| separately, such that V fixes every wire outside S and W
every wire in S to first order, and the Hessian of every wire pairs V with W to zero.
The Taylor cut lemma. There are subspaces V of directions on the inputs in S and W
of directions on the other inputs, of total dimension at least n minus the number of crossing
signals, such that V fixes every wire outside S and W every wire in S to first order,
and the Hessian of every wire pairs V with W to zero.
Linear algebra #
Orthogonal subspaces. If vᵀ B u = 0 for all v ∈ V and u ∈ W, then
dim V + dim W + rank B is at most the sum of the dimensions of the two spaces.
Orthogonal subspaces with side conditions. If J₁ annihilates V, J₂ annihilates W,
and V and W are orthogonal through B, then
dim V + dim W + rank (fromBlocks B J₁ᵀ J₂ 0) ≤ |ι| + |κ|.
Rank consequences #
Kernel dimension. A subspace of vectors vanishing outside X that the rows Y of M
annihilate has dimension at most |X| - rank M[Y, X].
The forward Jacobian consequence. At every point, the block of the Jacobian of the outputs
from the inputs in S to the outputs outside S has rank at most |forward p S|.
The backward Jacobian consequence. Symmetrically, the block of the Jacobian of the outputs
from the inputs outside S to the outputs in S has rank at most |backward p S|.
The Jacobian consequence. At every point, the blocks of the Jacobian of the outputs
from the inputs in S to the outputs outside S, and from the other inputs to the outputs in
S, have ranks summing to at most the number of crossing signals.
The Hessian-type cut bound for any orthogonal form. If a matrix H pairs to zero every
v and u that every wire Hessian at a pairs to zero, then its block H[X_S, X_T] has rank at
most the number of crossing signals.
The Hessian consequence. At every point and for every combination ∑ₒ cₒ fₒ of the
outputs, the block of its Hessian between the inputs in S and the other inputs has rank at
most the number of crossing signals.
The unified first-and-second-order jet cut bound. At every point a and for every
combination H = ∑ₒ cₒ ∇² fₒ(a) of the output Hessians, the combined block matrix formed by
H[X_S, X_T], J[O_T, X_S]ᵀ, and J[O_S, X_T] has rank at most |forward p S| + |backward p S|.