Elementwise tape nodes

Reusable NodeFDerivCorrect wrappers for scalar functions lifted pointwise to tensors, including common activations such as ReLU, sigmoid, tanh, SiLU, GELU, ELU, and safe differentiable variants.

noncomputable def Proofs.Autograd.TapeNodes.getVec {Γ : List Spec.Shape} {n : ℕ} (idx : Idx Γ (Spec.Shape.dim n Spec.Shape.scalar)) (x : CtxVec Γ) : Vec n

CtxVec.get specialized to vector shapes.

noncomputable def Proofs.Autograd.TapeNodes.getVecCLM {Γ : List Spec.Shape} {n : ℕ} (idx : Idx Γ (Spec.Shape.dim n Spec.Shape.scalar)) : CtxVec Γ →L[ℝ] Vec n

CtxVec.getCLM specialized to vector shapes .dim n .scalar.

@[simp]

theorem Proofs.Autograd.TapeNodes.getVecCLM_apply {Γ : List Spec.Shape} {n : ℕ} (idx : Idx Γ (Spec.Shape.dim n Spec.Shape.scalar)) (x : CtxVec Γ) : (getVecCLM idx) x = getVec idx x

The vector-shaped context lookup agrees with getVec, size cast included.

@[simp]

theorem Proofs.Autograd.TapeNodes.getCLM_apply_ofLp {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (x : CtxVec Γ) (i : Fin s.size) : ((CtxVec.getCLM idx) x).ofLp i = (CtxVec.get idx x).ofLp i

Coordinate form of the general context lookup.

noncomputable def Proofs.Autograd.TapeNodes.singleVec {Γ : List Spec.Shape} {n : ℕ} (idx : Idx Γ (Spec.Shape.dim n Spec.Shape.scalar)) (v : Vec n) : CtxVec Γ

Inject a Vec n into a vectorized context at idx (fills other blocks with zeros).

@[simp]

theorem Proofs.Autograd.TapeNodes.inner_getVec_singleVec {Γ : List Spec.Shape} {n : ℕ} (idx : Idx Γ (Spec.Shape.dim n Spec.Shape.scalar)) (x : CtxVec Γ) (v : Vec n) : inner ℝ x (singleVec idx v) = inner ℝ (getVec idx x) v

Reading a context slot is adjoint to writing that slot: ⟪x, single idx v⟫ = ⟪get idx x, v⟫.

This is the adjointness fact behind every elementwise node's VJP. A node reads one slot and writes one slot, so its reverse pass is the transpose of its forward projection, and that is exactly what this equation says.

noncomputable def Proofs.Autograd.TapeNodes.elemwise {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (f f' : ℝ → ℝ) : Node Γ s

Elementwise node: apply a scalar function pointwise on a context entry.

noncomputable def Proofs.Autograd.TapeNodes.elemwiseFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (f f' : ℝ → ℝ) (hf : ∀ (z : ℝ), HasDerivAt f (f' z) z) : NodeFDerivCorrect (elemwise idx f f')

Analytic correctness for elemwise nodes from a scalar HasDerivAt hypothesis.

noncomputable def Proofs.Autograd.TapeNodes.elemwiseFderivAt {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (f f' : ℝ → ℝ) (xV : CtxVec Γ) (hf : ∀ (i : Fin s.size), HasDerivAt f (f' ((CtxVec.get idx xV).ofLp i)) ((CtxVec.get idx xV).ofLp i)) : NodeFDerivCorrectAt (elemwise idx f f') xV

Pointwise analytic correctness for elemwise nodes from a coordinatewise HasDerivAt hypothesis.

noncomputable def Proofs.Autograd.TapeNodes.relu {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime relu node (elementwise; nondifferentiable at zero).

noncomputable def Proofs.Autograd.TapeNodes.reluFderivAt {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (xV : CtxVec Γ) (hx : ∀ (i : Fin s.size), (CtxVec.get idx xV).ofLp i ≠ 0) : NodeFDerivCorrectAt (relu idx) xV

Pointwise NodeFDerivCorrectAt for relu under the assumption that inputs are nonzero.

noncomputable def Proofs.Autograd.TapeNodes.abs {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime abs node (elementwise; nondifferentiable at zero).

noncomputable def Proofs.Autograd.TapeNodes.absFderivAt {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (xV : CtxVec Γ) (hx : ∀ (i : Fin s.size), (CtxVec.get idx xV).ofLp i ≠ 0) : NodeFDerivCorrectAt (abs idx) xV

Pointwise NodeFDerivCorrectAt for abs under the assumption that inputs are nonzero.

noncomputable def Proofs.Autograd.TapeNodes.log {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime log node (elementwise; differentiable only away from zero).

noncomputable def Proofs.Autograd.TapeNodes.logFderivAt {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (xV : CtxVec Γ) (hx : ∀ (i : Fin s.size), (CtxVec.get idx xV).ofLp i ≠ 0) : NodeFDerivCorrectAt (log idx) xV

Pointwise NodeFDerivCorrectAt for log under the assumption that inputs are nonzero.

noncomputable def Proofs.Autograd.TapeNodes.inv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Elementwise inverse node (differentiable only away from zero).

noncomputable def Proofs.Autograd.TapeNodes.invFderivAt {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (xV : CtxVec Γ) (hx : ∀ (i : Fin s.size), (CtxVec.get idx xV).ofLp i ≠ 0) : NodeFDerivCorrectAt (inv idx) xV

Pointwise NodeFDerivCorrectAt for inv under the assumption that inputs are nonzero.

theorem Proofs.Autograd.TapeNodes.hasDerivAt_sqrt_clamp_of_pos {x : ℝ} (hx : 0 < x) : HasDerivAt (fun (y : ℝ) => √(max y 0)) (1 / (2 * √x)) x

Derivative of the scalar function y ↦ sqrt (max y 0) at positive points.

noncomputable def Proofs.Autograd.TapeNodes.sqrtClamp {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Elementwise "clamped sqrt": sqrt (max x 0) (differentiable on x > 0).

noncomputable def Proofs.Autograd.TapeNodes.sqrtClampFderivAt {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (xV : CtxVec Γ) (hx : ∀ (i : Fin s.size), 0 < (CtxVec.get idx xV).ofLp i) : NodeFDerivCorrectAt (sqrtClamp idx) xV

Pointwise NodeFDerivCorrectAt for sqrtClamp under the assumption that inputs are strictly positive.

noncomputable def Proofs.Autograd.TapeNodes.sqrt {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime sqrt node (elementwise; nondifferentiable at zero).

noncomputable def Proofs.Autograd.TapeNodes.sqrtFderivAt {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (xV : CtxVec Γ) (hx : ∀ (i : Fin s.size), (CtxVec.get idx xV).ofLp i ≠ 0) : NodeFDerivCorrectAt (sqrt idx) xV

Pointwise NodeFDerivCorrectAt for sqrt under the assumption that inputs are nonzero.

noncomputable def Proofs.Autograd.TapeNodes.logistic {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime scalar logistic node, applied elementwise.

Rank-one and matrix softmax use the dedicated last-axis softmax nodes below; this node is the one-dimensional logistic map used by scalar activations.

noncomputable def Proofs.Autograd.TapeNodes.logisticFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : NodeFDerivCorrect (logistic idx)

Global NodeFDerivCorrect for logistic (uses the scalar derivative lemma).

noncomputable def Proofs.Autograd.TapeNodes.sigmoid {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime sigmoid node (elementwise).

noncomputable def Proofs.Autograd.TapeNodes.sigmoidFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : NodeFDerivCorrect (sigmoid idx)

Global NodeFDerivCorrect for sigmoid.

noncomputable def Proofs.Autograd.TapeNodes.tanh {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime tanh node (elementwise).

noncomputable def Proofs.Autograd.TapeNodes.tanhFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : NodeFDerivCorrect (tanh idx)

Global NodeFDerivCorrect for tanh.

noncomputable def Proofs.Autograd.TapeNodes.softplus {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime softplus node (elementwise, smooth ReLU surrogate).

noncomputable def Proofs.Autograd.TapeNodes.softplusFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : NodeFDerivCorrect (softplus idx)

Global NodeFDerivCorrect for softplus.

noncomputable def Proofs.Autograd.TapeNodes.silu {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime silu node (elementwise).

noncomputable def Proofs.Autograd.TapeNodes.siluFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : NodeFDerivCorrect (silu idx)

Global NodeFDerivCorrect for SiLU.

noncomputable def Proofs.Autograd.TapeNodes.gelu {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime tanh-approximate gelu node (elementwise).

noncomputable def Proofs.Autograd.TapeNodes.geluFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : NodeFDerivCorrect (gelu idx)

Global NodeFDerivCorrect for tanh-approximate GELU.

noncomputable def Proofs.Autograd.TapeNodes.safeLog {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (ε : ℝ) : Node Γ s

Runtime safeLog node (elementwise, always-defined log surrogate).

noncomputable def Proofs.Autograd.TapeNodes.safeLogFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (ε : ℝ) (hε : 0 < ε) : NodeFDerivCorrect (safeLog idx ε)

Global NodeFDerivCorrect for safeLog (requires 0 < ε).

noncomputable def Proofs.Autograd.TapeNodes.smoothAbs {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (ε : ℝ) : Node Γ s

Runtime smoothAbs node (elementwise, smooth abs surrogate).

noncomputable def Proofs.Autograd.TapeNodes.smoothAbsFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (ε : ℝ) (hε : 0 < ε) : NodeFDerivCorrect (smoothAbs idx ε)

Global NodeFDerivCorrect for smoothAbs (requires 0 < ε).

noncomputable def Proofs.Autograd.TapeNodes.exp {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime exp node (elementwise).

noncomputable def Proofs.Autograd.TapeNodes.expFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : NodeFDerivCorrect (exp idx)

Global NodeFDerivCorrect instance for the elementwise exponential.

noncomputable def Proofs.Autograd.TapeNodes.sinh {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime sinh node (elementwise).

noncomputable def Proofs.Autograd.TapeNodes.sinhFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : NodeFDerivCorrect (sinh idx)

Global NodeFDerivCorrect for elementwise hyperbolic sine.

noncomputable def Proofs.Autograd.TapeNodes.cosh {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ s

Runtime cosh node (elementwise).

noncomputable def Proofs.Autograd.TapeNodes.coshFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : NodeFDerivCorrect (cosh idx)

Global NodeFDerivCorrect for elementwise hyperbolic cosine.

noncomputable def Proofs.Autograd.TapeNodes.elu {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (alpha : ℝ) : Node Γ s

Runtime elu node (elementwise; nondifferentiable at zero unless alpha = 1).

noncomputable def Proofs.Autograd.TapeNodes.eluFderivAt {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (alpha : ℝ) (xV : CtxVec Γ) (hx : ∀ (i : Fin s.size), (CtxVec.get idx xV).ofLp i ≠ 0) : NodeFDerivCorrectAt (elu idx alpha) xV

Pointwise NodeFDerivCorrectAt for ELU under the usual no-coordinate-at-the-kink assumption.

For arbitrary alpha, ELU has left derivative alpha and right derivative 1 at zero. Keeping the hypothesis here avoids baking PyTorch's subgradient convention into a mathematical derivative theorem.

noncomputable def Proofs.Autograd.TapeNodes.unaryOp {Γ : List Spec.Shape} {inDim outDim : ℕ} (idx : Idx Γ (Spec.Shape.dim inDim Spec.Shape.scalar)) (C : OpSpecFDerivCorrect inDim outDim) : Node Γ (Spec.Shape.dim outDim Spec.Shape.scalar)

Unary node applying an analytically-correct OpSpec at a context index.

noncomputable def Proofs.Autograd.TapeNodes.unaryOpFderiv {Γ : List Spec.Shape} {inDim outDim : ℕ} (idx : Idx Γ (Spec.Shape.dim inDim Spec.Shape.scalar)) (C : OpSpecFDerivCorrect inDim outDim) : NodeFDerivCorrect (unaryOp idx C)

NodeFDerivCorrect for unaryOp.

noncomputable def Proofs.Autograd.TapeNodes.linear {Γ : List Spec.Shape} {inDim outDim : ℕ} (x : Idx Γ (Spec.Shape.dim inDim Spec.Shape.scalar)) (m : Spec.LinearSpec ℝ inDim outDim) : Node Γ (Spec.Shape.dim outDim Spec.Shape.scalar)

Linear layer as a single tape node (fixed weights/bias in the Spec.LinearSpec).

noncomputable def Proofs.Autograd.TapeNodes.linearFderiv {Γ : List Spec.Shape} {inDim outDim : ℕ} (x : Idx Γ (Spec.Shape.dim inDim Spec.Shape.scalar)) (m : Spec.LinearSpec ℝ inDim outDim) : NodeFDerivCorrect (linear x m)

NodeFDerivCorrect for linear: the node derivative matches the spec's OpSpec derivative.