Reduction and shape tape nodes

Scalar sums, broadcast-to, reduce-sum, reduce-mean, concatenation, and the linear shape adapters used by larger graph proofs.

noncomputable def Proofs.Autograd.TapeNodes.vecScalarCLM : ℝ →L[ℝ] Vec Spec.Shape.scalar.size

Continuous linear map embedding a scalar into the 1D scalar-vector representation.

@[simp]

theorem Proofs.Autograd.TapeNodes.vecScalarCLM_apply (a : ℝ) (i : Fin Spec.Shape.scalar.size) : (vecScalarCLM a).ofLp i = a

@[simp]

theorem Proofs.Autograd.TapeNodes.vecScalarCLM_ofLp (a : ℝ) (i : Fin Spec.Shape.scalar.size) : (vecScalarCLM a).ofLp i = a

def Proofs.Autograd.TapeNodes.sumCLM (n : ℕ) : Vec n →L[ℝ] ℝ

Continuous linear map summing the entries of a vector: x ↦ ∑ i, x i.

theorem Proofs.Autograd.TapeNodes.sumCLM_apply {n : ℕ} (x : Vec n) : (sumCLM n) x = ∑ i : Fin n, x.ofLp i

Evaluation lemma for sumCLM.

noncomputable def Proofs.Autograd.TapeNodes.sum {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : Node Γ Spec.Shape.scalar

Sum all entries of a context tensor into a scalar tensor.

noncomputable def Proofs.Autograd.TapeNodes.sumFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) : NodeFDerivCorrect (sum idx)

NodeFDerivCorrect for sum: derivative is the composite of context projection and coordinate sum.

def Proofs.Autograd.TapeNodes.Broadcast.broadcastToIndex {s₁ s₂ : Spec.Shape} : s₁.CanBroadcastTo s₂ → Fin s₂.size → Fin s₁.size

Compute the source index in s₁ that corresponds to a target index in s₂ under broadcasting.

noncomputable def Proofs.Autograd.TapeNodes.Broadcast.broadcastToVec {s₁ s₂ : Spec.Shape} (cb : s₁.CanBroadcastTo s₂) : Vec s₁.size → Vec s₂.size

Broadcast a vector Vec (size s₁) into Vec (size s₂) using the CanBroadcastTo index map.

noncomputable def Proofs.Autograd.TapeNodes.Broadcast.broadcastToCLM {s₁ s₂ : Spec.Shape} (cb : s₁.CanBroadcastTo s₂) : Vec s₁.size →L[ℝ] Vec s₂.size

Continuous-linear-map form of broadcastToVec.

@[simp]

theorem Proofs.Autograd.TapeNodes.Broadcast.broadcastToCLM_apply {s₁ s₂ : Spec.Shape} (cb : s₁.CanBroadcastTo s₂) (v : Vec s₁.size) : (broadcastToCLM cb) v = broadcastToVec cb v

noncomputable def Proofs.Autograd.TapeNodes.broadcastTo {Γ : List Spec.Shape} {s₁ s₂ : Spec.Shape} (idx : Idx Γ s₁) (cb : s₁.CanBroadcastTo s₂) : Node Γ s₂

General shape broadcast node s₁ → s₂ (linear).

noncomputable def Proofs.Autograd.TapeNodes.broadcastToFderiv {Γ : List Spec.Shape} {s₁ s₂ : Spec.Shape} (idx : Idx Γ s₁) (cb : s₁.CanBroadcastTo s₂) : NodeFDerivCorrect (broadcastTo idx cb)

NodeFDerivCorrect for broadcastTo (broadcasting is linear).

noncomputable def Proofs.Autograd.TapeNodes.reduceSum {Γ : List Spec.Shape} {s : Spec.Shape} (axis : ℕ) [valid : Spec.Shape.valid_axis_inst axis s] [wf : s.WellFormed] (idx : Idx Γ s) : Node Γ (Spec.Tensor.shapeAfterSum s axis)

Sum reduction along axis (linear; adjoint is broadcast back).

noncomputable def Proofs.Autograd.TapeNodes.reduceSumFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (axis : ℕ) [valid : Spec.Shape.valid_axis_inst axis s] [wf : s.WellFormed] (idx : Idx Γ s) : NodeFDerivCorrect (reduceSum axis idx)

NodeFDerivCorrect for reduce_sum.

noncomputable def Proofs.Autograd.TapeNodes.reduceMean {Γ : List Spec.Shape} {s : Spec.Shape} (axis : ℕ) [valid : Spec.Shape.valid_axis_inst axis s] [wf : s.WellFormed] (idx : Idx Γ s) : Node Γ (Spec.Tensor.shapeAfterSum s axis)

Mean reduction along axis (linear; adjoint is broadcast+scale).

noncomputable def Proofs.Autograd.TapeNodes.reduceMeanFderiv {Γ : List Spec.Shape} {s : Spec.Shape} (axis : ℕ) [valid : Spec.Shape.valid_axis_inst axis s] [wf : s.WellFormed] (idx : Idx Γ s) : NodeFDerivCorrect (reduceMean axis idx)

NodeFDerivCorrect for reduce_mean.

theorem Proofs.Autograd.TapeNodes.castVec_proof_irrel {n m : ℕ} (h₁ h₂ : n = m) (v : Vec n) : castVec h₁ v = castVec h₂ v

castVec does not depend on the particular proof of n = m (proof irrelevance).

noncomputable def Proofs.Autograd.TapeNodes.takeLeftVec {m n : ℕ} (v : Vec (m + n)) : Vec m

Take the left m entries of a length m+n vector.

noncomputable def Proofs.Autograd.TapeNodes.takeRightVec {m n : ℕ} (v : Vec (m + n)) : Vec n

Take the right n entries of a length m+n vector.

noncomputable def Proofs.Autograd.TapeNodes.concatVectors {Γ : List Spec.Shape} {n m : ℕ} (a : Idx Γ (Spec.Shape.dim n Spec.Shape.scalar)) (b : Idx Γ (Spec.Shape.dim m Spec.Shape.scalar)) : Node Γ (Spec.Shape.dim (n + m) Spec.Shape.scalar)

Concatenate two context vectors into a single (n+m)-vector node (dim-0 concat).

noncomputable def Proofs.Autograd.TapeNodes.concatVectorsFderiv {Γ : List Spec.Shape} {n m : ℕ} (a : Idx Γ (Spec.Shape.dim n Spec.Shape.scalar)) (b : Idx Γ (Spec.Shape.dim m Spec.Shape.scalar)) : NodeFDerivCorrect (concatVectors a b)

NodeFDerivCorrect for concat_vectors.

noncomputable def Proofs.Autograd.TapeNodes.concatDim0 {Γ : List Spec.Shape} {n m : ℕ} {s : Spec.Shape} (a : Idx Γ (Spec.Shape.dim n s)) (b : Idx Γ (Spec.Shape.dim m s)) : Node Γ (Spec.Shape.dim (n + m) s)

Concatenate two tensors along dimension 0 (dim-0 concat), using flattened vectors internally.

noncomputable def Proofs.Autograd.TapeNodes.concatDim0Fderiv {Γ : List Spec.Shape} {n m : ℕ} {s : Spec.Shape} (a : Idx Γ (Spec.Shape.dim n s)) (b : Idx Γ (Spec.Shape.dim m s)) : NodeFDerivCorrect (concatDim0 a b)

NodeFDerivCorrect for concat_dim0 (concat is linear).