Dual

Dual numbers for forward-mode differentiation.

This runtime-oriented Dual α scalar can be used to compute:

• Jacobian-vector products by running a function once with dual inputs, and
• Hessian-vector products by running reverse-mode over dual scalars (forward-over-reverse).

The rules follow the primal branch. Absolute value and guarded square root select zero tangent at zero; minimum and maximum split ties equally. ReLU separately selects zero at its kink, and tensor clamp selects zero tangent at either endpoint. These choices agree with the recorded graph rules.

detach removes the tangent and recursively clears differentiation metadata from the primal, so nested dual computations respect the same boundary. A power with a constant exponent uses $yx^{y-1}x'$, without evaluating a logarithm. A varying exponent uses $x^y(y'\log x+yx'/x)$ on its domain. Mathematical derivative theorems state their domain assumptions in the separate fderiv proof layer.

Compensated log1p and expm1 use analytic chain rules rather than differentiating their rounding-dependent branches. This also preserves higher derivatives when dual numbers are nested.

structure Runtime.Autograd.Model.Dual (α : Type) : Type

A dual number $x+\varepsilon\,dx$ used for forward-mode automatic differentiation.

re is the primal value and du is the tangent (directional derivative). When you run a computation once on dual inputs, the resulting du component computes a Jacobian-vector product.

• re : α

  Primal part: the value the ordinary computation would have produced.

• du : α

  Tangent part, the coefficient of ε. Truncating at ε² = 0 is what makes the arithmetic rules below exactly the chain rule.

def Runtime.Autograd.Model.instReprDual.repr {α✝ : Type} [Repr α✝] : Dual α✝ → ℕ → Std.Format

@[instance_reducible]

instance Runtime.Autograd.Model.instReprDual {α✝ : Type} [Repr α✝] : Repr (Dual α✝)

def Runtime.Autograd.Model.Dual.primal {α : Type} (x : Dual α) : α

Project the primal component of a dual number.

def Runtime.Autograd.Model.Dual.tangent {α : Type} (x : Dual α) : α

Project the tangent component of a dual number.

def Runtime.Autograd.Model.Dual.ofPrimal {α : Type} [Zero α] (x : α) : Dual α

Embed a primal value as a dual number with zero tangent.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instInhabitedOfZero {α : Type} [Inhabited α] [Zero α] : Inhabited (Dual α)

Dual is inhabited by default primal value with zero tangent.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instZero {α : Type} [Zero α] : Zero (Dual α)

Zero dual number: $0+\varepsilon\cdot0$.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instOneOfZero {α : Type} [One α] [Zero α] : One (Dual α)

One dual number: $1+\varepsilon\cdot0$.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instNeg {α : Type} [Neg α] : Neg (Dual α)

Negation is componentwise: $-(x+\varepsilon\,dx)=-x+\varepsilon(-dx)$.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instAdd {α : Type} [Add α] : Add (Dual α)

Addition is componentwise, so tangents add linearly.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instSub {α : Type} [Sub α] : Sub (Dual α)

Subtraction is componentwise, so tangents subtract linearly.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instMulOfAdd {α : Type} [Mul α] [Add α] : Mul (Dual α)

Multiplication uses the product rule: $(xy)'=x'y+xy'$.

@[inline]

def Runtime.Autograd.Model.Dual.checkedDiv {α : Type} (ops : TorchLean.Numeric.QuotientArithmetic α) (x y : Dual α) : Dual α × UInt8

Evaluate a complete quotient layer while retaining all enclosed range flags.

@[instance_reducible, inline]

instance Runtime.Autograd.Model.Dual.instQuotientArithmetic {α : Type} [lower : TorchLean.Numeric.QuotientArithmetic α] : TorchLean.Numeric.QuotientArithmetic (Dual α)

Lift checked arithmetic through both coefficients without discarding inner range flags.

@[instance_reducible, inline]

instance Runtime.Autograd.Model.Dual.instDivOfMulOfSubOfAddOfBEqOfZeroOfQuotientArithmetic {α : Type} [Div α] [Mul α] [Sub α] [Add α] [BEq α] [Zero α] [TorchLean.Numeric.QuotientArithmetic α] : Div (Dual α)

Division uses the quotient rule $(x/y)'=(x'y-xy')/y^2$ at every nesting depth.

For native binary32/64 coefficient trees, ordinary operations retain this evaluation order. If any enclosed operation exposes a nonfinite or subnormal value, including a nonzero product or quotient rounded to zero, we replay the complete quotient over exact rational coefficients. Every final coefficient is then rounded independently to its native format. A representable mixed derivative can therefore survive an intermediate overflow or underflow at an inner depth. Replay requires all input coefficients finite and the denominator's scalar primal nonzero. Otherwise the native quotient-rule result is retained. An unrepresentable exact coefficient still rounds to infinity or zero; coefficients are never clamped or deleted.

The scope is one quotient of the given coefficient trees. Rounding before entry is irreversible; ordinary rounding and cancellation outside a detected range event retain their native semantics. Carriers without checked coefficient arithmetic retain the previous operational rearrangement.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instBEq {α : Type} [BEq α] : BEq (Dual α)

Boolean equality compares primals only (tangents are treated as metadata).

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instLT {α : Type} [LT α] : LT (Dual α)

Strict order compares primals only.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instLE {α : Type} [LE α] : LE (Dual α)

Non-strict order compares primals only.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instMaxOfStorageOfContext {α : Type} [TorchLean.Storage α] [Context α] : Max (Dual α)

Take the larger primal and its tangent. Equal primals split the tangent equally between the two arguments, matching the graph's elementwise maximum rule. The shared average scales before adding and replays finite coefficients if halving loses range. Neither an overflowing raw sum nor two rounded-zero halves should erase a representable average.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instMinOfStorageOfContext {α : Type} [TorchLean.Storage α] [Context α] : Min (Dual α)

Elementwise minimum uses the same equal split at a tie as the graph's minimum rule.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instNatCastOfStorageOfContext {α : Type} [TorchLean.Storage α] [Context α] : NatCast (Dual α)

Coerce naturals into dual numbers with zero tangent.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instMathFunctionsOfStorageOfContext {α : Type} [TorchLean.Storage α] [Context α] : MathFunctions (Dual α)

Forward-mode chain rule implementations for MathFunctions over dual numbers.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instPowOfStorageOfContext {α : Type} [TorchLean.Storage α] [Context α] : Pow (Dual α) (Dual α)

Power rule for x^y over dual numbers.

If the exponent tangent is identically zero, use $yx^{y-1}x'$ instead of evaluating an unused logarithm or dividing by the base. This includes polynomial derivatives at zero and negative inputs. The zero test inspects all nested coefficients, not just their primals. A varying exponent uses the logarithmic rule on the scalar backend's domain. When its arithmetic loses range, a bounded positive-base enclosure combines both directions before rounding.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instContextOfStorage {α : Type} [TorchLean.Storage α] [Context α] : Context (Dual α)

Lift a scalar Context to dual numbers by deciding comparisons on primals.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instAtan2OfStorageOfContext {α : Type} [TorchLean.Storage α] [Context α] [Atan2 α] : Atan2 (Dual α)

Differentiate the polar angle in real coordinates away from the origin and branch cut.

Scaling both coordinates avoids squaring a large magnitude. At the origin we select zero tangent, where the angle has no classical derivative. The primal retains the component backend's signed-zero and branch-cut convention. The shared tangent rule combines the original finite coefficients if scaled seeds lose range or their products cancel.

def Runtime.Autograd.Model.DualTensor.ofPrimal {α : Type} [TorchLean.Storage α] [TorchLean.Storage (Dual α)] [Zero α] {s : Spec.Shape} : TorchLean.Tensor α s → TorchLean.Tensor (Dual α) s

Map a tensor of primals to a tensor of duals with zero tangents.

def Runtime.Autograd.Model.DualTensor.withTangents {α : Type} [TorchLean.Storage α] [TorchLean.Storage (Dual α)] {s : Spec.Shape} (primal tangent : TorchLean.Tensor α s) : TorchLean.Tensor (Dual α) s

Combine a primal tensor and a tangent tensor into a dual tensor.

This is the tensor-level analogue of Dual.mk.

def Runtime.Autograd.Model.DualTensor.tangent {α : Type} [TorchLean.Storage α] [TorchLean.Storage (Dual α)] {s : Spec.Shape} (tensor : TorchLean.Tensor (Dual α) s) : TorchLean.Tensor α s

Project the tangent part of a dual tensor.