Differentiate three scalar functions

Run lake exe torchlean transcendentals to compare autograd with hand-computed derivatives:

• exp x has derivative exp x;
• 3 * x + 1 has derivative 3;
• exp (-2 * x) has derivative -2 * exp (-2 * x) by the chain rule.

All three are evaluated at x = 0.5 using Float and absolute tolerance 1e-6. Each check also rejects a named wrong answer. In particular, the last one distinguishes a missing minus sign from rounding error. Every check should print PASS or PASS-NEG; a mismatch exits with an error. No dataset or GPU is needed.

expProofSurface and expBackward_eq_adjoint_fderiv give the separate real-arithmetic theorem. The executable comparisons test the Float tape on these inputs; they do not prove its native implementation or establish a derivative at every input. Read expNegativeTwoFn, then gradAt, then checkAll for the application flow.

Proof objects and runtime checks

noncomputable def NN.Examples.Functional.Transcendentals.expProofSurface : Proofs.Autograd.OpSpecFDerivCorrect 1 1

The theorem-backed real-valued exp op used by the proof layer.

This is the actual proof layer object: it packages the forward op, its JVP, a Fréchet-derivative candidate, and the theorem that the JVP is the true derivative. The runtime checks below exercise the executable Float tape; this declaration points to the corresponding real-valued theorem.

theorem NN.Examples.Functional.Transcendentals.expBackward_eq_adjoint_fderiv (x δ : TorchLean.Tensor ℝ [1]) : Proofs.Autograd.getScalarE (expProofSurface.correct.op.backward x δ) = (Proofs.Autograd.vjp expProofSurface.forwardVec (Proofs.Autograd.getScalarE x)) (Proofs.Autograd.getScalarE δ)

For scalar exp over ℝ, the proved backward rule is the adjoint of the Fréchet derivative.

This is the theorem-level statement that the executable regression check is meant to complement.

Functions under test (written once; gradients come from autograd)

def NN.Examples.Functional.Transcendentals.expFn : TorchLean.autograd.Function [] []

$f(x)=e^x$.

def NN.Examples.Functional.Transcendentals.expNegativeTwoFn : TorchLean.autograd.Function [] []

$f(x)=e^{-2x}$; its derivative needs both the factor two and the minus sign.

def NN.Examples.Functional.Transcendentals.affineFn : TorchLean.autograd.Function [] []

$f(x)=3x+1$ via the scalar-affine op.

Float checks

def NN.Examples.Functional.Transcendentals.approx (a b : Float) (tol : Float := 1e-6) : Bool

Absolute-tolerance float compare.

def NN.Examples.Functional.Transcendentals.expectGrad (name : String) (got expected : Float) (tol : Float := 1e-6) : IO Unit

Positive control: name's autograd gradient is approximately equal to the expected value; throws on mismatch.

def NN.Examples.Functional.Transcendentals.expectNot (name : String) (got wrong : Float) (tol : Float := 1e-6) : IO Unit

Negative control: the gradient must not equal wrong; throws if it does.

def NN.Examples.Functional.Transcendentals.gradAt (f : TorchLean.autograd.Function [] []) (x0 : Float) : IO Float

Differentiate a scalar→scalar Fn at a Float point, returning the gradient.

def NN.Examples.Functional.Transcendentals.checkAll : IO Unit

Compare each derivative with its analytic value and reject a plausible wrong value.

The positive checks establish agreement at the sampled point; the negative controls show that those points and tolerances distinguish the particular mistakes named below.

def NN.Examples.Functional.Transcendentals.usage : String

Command-line help for the transcendental autograd checks.

def NN.Examples.Functional.Transcendentals.main (args : List String) : IO Unit

Entry point.