Sparse VJP Contexts

Shape-indexed context builders used by the NF reverse-mode proofs. These helpers write only the positions touched by a local VJP rule and leave every other component at zero, which lets the sparse cases avoid unnecessary rounded additions.

Sparse Contexts For Local VJPs

def Proofs.RuntimeApprox.SparseContext.setIdx {α : Type} [TorchLean.Storage α] [Zero α] {Γ : List Spec.Shape} {s : Spec.Shape} : Idx Γ s → TorchLean.Tensor α s → TorchLean.TensorPack α Γ

Set a single Idx position in a TorchLean.TensorPack, filling all other entries with zeros.

def Proofs.RuntimeApprox.SparseContext.set2Idx {α : Type} [TorchLean.Storage α] [Zero α] [Add α] {Γ : List Spec.Shape} {s₁ s₂ : Spec.Shape} : Idx Γ s₁ → TorchLean.Tensor α s₁ → Idx Γ s₂ → TorchLean.Tensor α s₂ → TorchLean.TensorPack α Γ

Set two indices; if they coincide, add the contributions at that position.

def Proofs.RuntimeApprox.EList.zeros {ss : List Spec.Shape} : EList ss

An EList filled with zeros, used for sparse error-bound contexts.

def Proofs.RuntimeApprox.EList.setIdx {Γ : List Spec.Shape} {s : Spec.Shape} : Idx Γ s → ℝ → EList Γ

Set a single Idx position in an EList, filling all other entries with zeros.

def Proofs.RuntimeApprox.EList.set2Idx {Γ : List Spec.Shape} {s₁ s₂ : Spec.Shape} : Idx Γ s₁ → ℝ → Idx Γ s₂ → ℝ → ℝ → EList Γ

Set two indices in an EList; if they coincide, use the supplied combined value eBoth.