Tensor coordinates for primitive derivatives

Flattening preserves the coordinate formulas of pointwise tensor operations. These lemmas connect the actual tensor functions to the diagonal calculus in PrimitiveSpecs, without restricting the tensor to one axis. A binary operation with a captured right argument then needs only the scalar derivative with respect to its left argument.

@[simp]

theorem Proofs.Autograd.PrimitiveSpecs.coordinatewise_apply {n : ℕ} (f : Fin n → ℝ → ℝ) (x : Vec n) (i : Fin n) : (coordinatewise f x).ofLp i = f i (x.ofLp i)

Coordinate evaluation removes the Euclidean wrapper around a pointwise function.

@[simp]

theorem Proofs.Autograd.PrimitiveSpecs.tensorToVec_mapSpec_apply {s : Spec.Shape} (f : ℝ → ℝ) (x : TorchLean.Tensor ℝ s) (i : Fin s.size) : (tensorToVec (TorchLean.Tensor.mapSpec f x)).ofLp i = f ((tensorToVec x).ofLp i)

Row-major flattening commutes with a unary pointwise map.

@[simp]

theorem Proofs.Autograd.PrimitiveSpecs.tensorToVec_map2Spec_apply {s : Spec.Shape} (f : ℝ → ℝ → ℝ) (x y : TorchLean.Tensor ℝ s) (i : Fin s.size) : (tensorToVec (TorchLean.Tensor.map2Spec f x y)).ofLp i = f ((tensorToVec x).ofLp i) ((tensorToVec y).ofLp i)

Both operands of a binary pointwise map use the same flattened coordinate.

@[simp]

theorem Proofs.Autograd.PrimitiveSpecs.tensorToVec_full_apply (s : Spec.Shape) (value : ℝ) (i : Fin s.size) : (tensorToVec (TorchLean.Tensor.full s value)).ofLp i = value

Every coordinate of a filled tensor is its fill value.

@[simp]

theorem Proofs.Autograd.PrimitiveSpecs.tensorToVec_mulSpec_apply {s : Spec.Shape} (x y : TorchLean.Tensor ℝ s) (i : Fin s.size) : (tensorToVec (x.mulSpec y)).ofLp i = (tensorToVec x).ofLp i * (tensorToVec y).ofLp i

Elementwise multiplication becomes multiplication of the corresponding real coordinates.

theorem Proofs.Autograd.PrimitiveSpecs.binaryElemOp_hasFDerivAt {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (f df : ℝ → ℝ → ℝ) (x : Vec s.size) (hf : ∀ (i : Fin s.size), HasDerivAt (fun (z : ℝ) => f z ((tensorToVec rhs).ofLp i)) (df (x.ofLp i) ((tensorToVec rhs).ofLp i)) (x.ofLp i)) : HasFDerivAt (fun (y : Vec s.size) => tensorToVec ((Spec.binaryElemOp rhs f df).forward (vecToTensor y))) (coordinateDeriv fun (i : Fin s.size) => df (x.ofLp i) ((tensorToVec rhs).ofLp i)) x

The captured-right constructor differentiates its actual tensor forward function.

theorem Proofs.Autograd.PrimitiveSpecs.binaryElemOp_backward_eq_adjoint {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (f df : ℝ → ℝ → ℝ) (x : Vec s.size) (hf : ∀ (i : Fin s.size), HasDerivAt (fun (z : ℝ) => f z ((tensorToVec rhs).ofLp i)) (df (x.ofLp i) ((tensorToVec rhs).ofLp i)) (x.ofLp i)) (δ : TorchLean.Tensor ℝ s) : tensorToVec ((Spec.binaryElemOp rhs f df).backward (vecToTensor x) δ) = (ContinuousLinearMap.adjoint (fderiv ℝ (fun (y : Vec s.size) => tensorToVec ((Spec.binaryElemOp rhs f df).forward (vecToTensor y))) x)) (tensorToVec δ)

Scalar derivative evidence certifies the stored captured-right backward formula.