Captured arithmetic derivatives

These theorems certify the actual forward and backward functions of the arithmetic OpSpecs. The right-hand tensor is fixed, so every derivative is diagonal. This is the input-gradient contract of these specifications; differentiating a second variable requires the corresponding two-input rule.

Over the reals, division by a fixed denominator is a linear map even when that denominator is zero: the totalized quotient is then constantly zero. The same fact applies to the fixed shifted denominator in safeDivOp. It does not remove the pole of safeInvOp, whose denominator varies with the differentiated input, or change the nonzero-denominator contract of floating-point division.

theorem Proofs.Autograd.PrimitiveSpecs.addOp_hasFDerivAt {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) : HasFDerivAt (fun (y : Vec s.size) => tensorToVec ((Spec.addOp rhs).forward (vecToTensor y))) (coordinateDeriv fun (x : Fin s.size) => 1) x

Adding a captured tensor has the identity coordinate derivative on every shape.

theorem Proofs.Autograd.PrimitiveSpecs.addOp_backward_eq_adjoint {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) (δ : TorchLean.Tensor ℝ s) : tensorToVec ((Spec.addOp rhs).backward (vecToTensor x) δ) = (ContinuousLinearMap.adjoint (fderiv ℝ (fun (y : Vec s.size) => tensorToVec ((Spec.addOp rhs).forward (vecToTensor y))) x)) (tensorToVec δ)

The captured addition backward is the adjoint of its forward derivative.

theorem Proofs.Autograd.PrimitiveSpecs.subOp_hasFDerivAt {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) : HasFDerivAt (fun (y : Vec s.size) => tensorToVec ((Spec.subOp rhs).forward (vecToTensor y))) (coordinateDeriv fun (x : Fin s.size) => 1) x

Subtracting a fixed tensor leaves the input derivative equal to the identity.

theorem Proofs.Autograd.PrimitiveSpecs.subOp_backward_eq_adjoint {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) (δ : TorchLean.Tensor ℝ s) : tensorToVec ((Spec.subOp rhs).backward (vecToTensor x) δ) = (ContinuousLinearMap.adjoint (fderiv ℝ (fun (y : Vec s.size) => tensorToVec ((Spec.subOp rhs).forward (vecToTensor y))) x)) (tensorToVec δ)

The captured subtraction backward has the positive input-gradient sign.

theorem Proofs.Autograd.PrimitiveSpecs.mulOp_hasFDerivAt {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) : HasFDerivAt (fun (y : Vec s.size) => tensorToVec ((Spec.mulOp rhs).forward (vecToTensor y))) (coordinateDeriv fun (i : Fin s.size) => (tensorToVec rhs).ofLp i) x

Multiplication by a fixed tensor scales each tangent by the matching captured entry.

theorem Proofs.Autograd.PrimitiveSpecs.mulOp_backward_eq_adjoint {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) (δ : TorchLean.Tensor ℝ s) : tensorToVec ((Spec.mulOp rhs).backward (vecToTensor x) δ) = (ContinuousLinearMap.adjoint (fderiv ℝ (fun (y : Vec s.size) => tensorToVec ((Spec.mulOp rhs).forward (vecToTensor y))) x)) (tensorToVec δ)

The stored multiplication backward is the adjoint of the diagonal forward derivative.

theorem Proofs.Autograd.PrimitiveSpecs.divOp_hasFDerivAt {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) : HasFDerivAt (fun (y : Vec s.size) => tensorToVec ((Spec.divOp rhs).forward (vecToTensor y))) (coordinateDeriv fun (i : Fin s.size) => 1 / (tensorToVec rhs).ofLp i) x

A fixed real denominator gives a linear quotient, including the totalized zero case.

theorem Proofs.Autograd.PrimitiveSpecs.divOp_backward_eq_adjoint {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) (δ : TorchLean.Tensor ℝ s) : tensorToVec ((Spec.divOp rhs).backward (vecToTensor x) δ) = (ContinuousLinearMap.adjoint (fderiv ℝ (fun (y : Vec s.size) => tensorToVec ((Spec.divOp rhs).forward (vecToTensor y))) x)) (tensorToVec δ)

The captured quotient backward agrees with the adjoint for every real fixed denominator.

theorem Proofs.Autograd.PrimitiveSpecs.safeDivOp_hasFDerivAt {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) : HasFDerivAt (fun (y : Vec s.size) => tensorToVec ((Spec.safeDivOp rhs).forward (vecToTensor y))) (coordinateDeriv fun (i : Fin s.size) => 1 / ((tensorToVec rhs).ofLp i + Context.defaultEpsilon)) x

The epsilon shift belongs to the fixed denominator, so it does not contribute a derivative.

theorem Proofs.Autograd.PrimitiveSpecs.safeDivOp_backward_eq_adjoint {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) (δ : TorchLean.Tensor ℝ s) : tensorToVec ((Spec.safeDivOp rhs).backward (vecToTensor x) δ) = (ContinuousLinearMap.adjoint (fderiv ℝ (fun (y : Vec s.size) => tensorToVec ((Spec.safeDivOp rhs).forward (vecToTensor y))) x)) (tensorToVec δ)

The actual shifted-division backward uses the same fixed denominator as its forward map.