Linear Algebra NF Reverse Nodes #
Reverse-mode approximation nodes for matrix-vector and matrix-matrix multiplication.
def
Proofs.RuntimeApprox.NFBackend.Impl.unsqueezeAfterLeading
{α : Type}
[TorchLean.Storage α]
{n : ℕ}
{s : Spec.Shape}
(tensor : TorchLean.Tensor α (Spec.Shape.dim n s))
:
TorchLean.Tensor α (Spec.Shape.dim n (Spec.Shape.dim 1 s))
Internal spelling of axis-one insertion used repeatedly in outer-product formulas.
Instances For
theorem
Proofs.RuntimeApprox.NFBackend.approxTensor_unsqueezeAfterLeading
{β : FloatLib.Numerics.Radix}
{fexp : ℤ → ℤ}
{rnd : ℝ → ℤ}
{n : ℕ}
{s : Spec.Shape}
{xS : Spec.SpecTensor (Spec.Shape.dim n s)}
{xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) (Spec.Shape.dim n s)}
{eps : ℝ}
(hx : approxTensor toSpec xS xR eps)
:
The internal axis-one spelling is an exact shape operation.
noncomputable def
Proofs.RuntimeApprox.NFBackend.matVecMulRevNode
{β : FloatLib.Numerics.Radix}
{fexp : ℤ → ℤ}
[FloatLib.Floats.Formats.Flocq.ValidExp fexp]
{rnd : ℝ → ℤ}
[FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd]
{Γ : List Spec.Shape}
{m n : ℕ}
(A : Idx Γ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))
(v : Idx Γ (Spec.Shape.dim n Spec.Shape.scalar))
:
Reverse node for matrix-vector multiplication (matVecMulSpec).
VJP uses the standard adjoint identities: δW = δ ⊗ x and δx = Wᵀ δ (expressed in tensor form),
with NF error bounds layered over the primitive ops.
Instances For
noncomputable def
Proofs.RuntimeApprox.NFBackend.matMulRevNode
{β : FloatLib.Numerics.Radix}
{fexp : ℤ → ℤ}
[FloatLib.Floats.Formats.Flocq.ValidExp fexp]
{rnd : ℝ → ℤ}
[FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd]
{Γ : List Spec.Shape}
{m n p : ℕ}
(A : Idx Γ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))
(B : Idx Γ (Spec.Shape.dim n (Spec.Shape.dim p Spec.Shape.scalar)))
:
Reverse node for matrix multiplication (matMulSpec).
VJP uses the standard identities δA = δC * Bᵀ and δB = Aᵀ * δC (in appropriate shapes),
with NF error bounds layered over the primitive ops.