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. The power rule uses $d(x^y)=x^y(y'\log x+yx'/x)$ and requires the logarithm and quotient to be defined. Mathematical derivative theorems state their domain assumptions in the separate fderiv proof layer.

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.

@[instance_reducible]

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

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

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.

def Runtime.Autograd.Model.Dual.mk' {α : Type} (x dx : α) : Dual α

Convenience constructor using the (primal, tangent) order.

@[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. Each tangent is scaled before the sum: adding two large finite tangents first can overflow even when their average is representable.

@[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.

We use the standard identity $d(x^y)=x^y(y'\log x+yx'/x)$, which is mathematically justified only on domains where the right-hand side is defined.

@[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.

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.ofPrimalPack {α : Type} [TorchLean.Storage α] [TorchLean.Storage (Dual α)] [Zero α] {ss : List Spec.Shape} : TorchLean.TensorPack α ss → TorchLean.TensorPack (Dual α) ss

Lift a tensor pack to dual numbers with zero tangents.

def Runtime.Autograd.Model.DualTensor.withTangents {α : Type} [TorchLean.Storage α] [TorchLean.Storage (Dual α)] [Context α] {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.withTangentsPack {α : Type} [TorchLean.Storage α] [TorchLean.Storage (Dual α)] [Context α] {ss : List Spec.Shape} : TorchLean.TensorPack α ss → TorchLean.TensorPack α ss → TorchLean.TensorPack (Dual α) ss

Apply withTangents pointwise to a tensor pack.

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.

def Runtime.Autograd.Model.DualTensor.tangentPack {α : Type} [TorchLean.Storage α] [TorchLean.Storage (Dual α)] {ss : List Spec.Shape} : TorchLean.TensorPack (Dual α) ss → TorchLean.TensorPack α ss

Extract every tangent in a tensor pack.