Higher-order semantics of runtime dual numbers #
A nested dual value stores mixed derivatives in independent infinitesimal directions. jet
gives those coefficients their mathematical meaning using mathlib's Fréchet derivative. The
operation theorems connect that meaning to the actual runtime arithmetic at every finite order.
The last direction occupies the outermost dual layer. Extracting every tangent gives
iteratedFDeriv applied to the complete direction tuple, with no factorial scaling. The
input space is any real normed space; directions need not be distinct or coordinate vectors.
These are exact-real scalar rules. Model lowering, effectful evaluation, and floating-point rounding require their own links to these semantics.
All mixed derivative coefficients of a function along the supplied directions.
Instances For
Embedding a constant is valid at every order, not just for one forward pass.
All coefficients of the zero function vanish.
A linear input coordinate has its value and supplied directions, and no higher coefficients.
Scalar input seeding agrees with the identity function's full derivative data.
The runtime negation rule preserves all derivative coefficients.
The derivative coefficients depend only on the function near the evaluation point.
Addition preserves mixed derivatives under pointwise smoothness assumptions.
Subtraction preserves mixed derivatives under pointwise smoothness assumptions.
The runtime product rule needs smoothness only near the evaluation point.
Runtime addition preserves every derivative coefficient through order n.
Runtime subtraction preserves mixed derivatives through the requested finite order.
The constant one has primal one and no derivative coefficients at any depth.
The runtime product rule remains correct under arbitrary nesting.
The runtime exponential rule preserves mixed derivatives through order n.
The sine and cosine runtime rules preserve one another's higher derivatives.
The cosine rule, including its alternating derivative signs, is valid at every order.
Runtime comparisons inspect the primal value, not its derivative coefficients.
The runtime quotient rule preserves every derivative coefficient away from a zero denominator. Both functions need be smooth only near the evaluation point.
Strict positivity of a jet depends only on its primal value.
The analytic sigmoid rule preserves every mixed derivative of a smooth real input function.
The scalar range repair is inactive over exact reals; the runtime's weighted pullback reduces to the derivative used by mathlib. No floating-point accuracy claim is made here.
The runtime tanh rule computes every mixed derivative of a smooth real input function.
Hyperbolic sine preserves higher derivatives through the runtime's mutual sinh/cosh rules.
Hyperbolic cosine preserves higher derivatives through the runtime's mutual sinh/cosh rules.
The runtime exponential rule preserves mixed derivatives through order n.
The sine and cosine runtime rules preserve one another's higher derivatives.
The cosine rule, including its alternating derivative signs, is valid at every order.
The runtime tanh rule computes every mixed derivative of a smooth real input function.
Hyperbolic sine preserves higher derivatives through the runtime's mutual sinh/cosh rules.
Hyperbolic cosine preserves higher derivatives through the runtime's mutual sinh/cosh rules.
Direct scalar exponential evaluation on seeded runtime inputs.
Direct scalar sine evaluation on seeded runtime inputs.
Direct scalar cosine evaluation on seeded runtime inputs.
Direct scalar tanh evaluation on seeded runtime inputs.
Direct scalar hyperbolic sine evaluation on seeded runtime inputs.
Direct scalar hyperbolic cosine evaluation on seeded runtime inputs.
Extracting every tangent gives the iterated derivative under local smoothness.
The extracted runtime coefficient is mathlib's iterated Fréchet derivative.
A smooth update with a local jet law preserves jets in the supplied traversal order.
Ordered sums preserve locally smooth derivative coefficients of entries and accumulator.
Ordered products preserve local jets without requiring nonzero factors.
Ordered summation propagates all derivatives of its entries and initial accumulator.
Ordered products propagate all derivatives without requiring nonzero factors.