Notation for analytic (Fréchet) derivatives in TorchLean autograd proofs

Mathlib already provides two very useful scoped notations in this area:

• open scoped InnerProduct enables postfix † for adjoints of bounded operators (ContinuousLinearMap.adjoint).
• open scoped Gradient enables ∇ f x for the gradient of a scalar function (in Hilbert spaces).

TorchLean’s autograd proofs are primarily VJP-first: the central analytic object is the adjoint of the Fréchet derivative (fderiv ℝ f x)†, which is exactly the vector-Jacobian product (Jacobian-transpose product) that PyTorch-style reverse-mode computes.

This file defines a small scoped notation VJP[f, x] for that operator.

@[reducible, inline]

noncomputable abbrev Proofs.Autograd.jacobian {E F : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : E → F) (x : E) : E →L[ℝ] F

The Jacobian (Fréchet derivative) of f at x, packaged as a bounded linear map.

def Autograd.«termJ[_,_]» : Lean.ParserDescr

The Jacobian (Fréchet derivative) of f at x, packaged as a bounded linear map.

@[reducible, inline]

noncomputable abbrev Proofs.Autograd.vjp {E F : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (f : E → F) (x : E) : F →L[ℝ] E

The vector-Jacobian product operator (VJP) of f at x.

VJP[f, x] : F →L[ℝ] E is the adjoint of the Fréchet derivative (fderiv ℝ f x) : E →L[ℝ] F.

When f is a scalar loss (F = ℝ), the gradient is VJP[f, x] 1 (equivalently ∇ f x).

def Autograd.«termVJP[_,_]» : Lean.ParserDescr

The vector-Jacobian product operator (VJP) of f at x.

VJP[f, x] : F →L[ℝ] E is the adjoint of the Fréchet derivative (fderiv ℝ f x) : E →L[ℝ] F.

When f is a scalar loss (F = ℝ), the gradient is VJP[f, x] 1 (equivalently ∇ f x).