Fiberwise differential identities

The finite tensor pairing makes push and pull adjoint. General fiberwise directional derivatives and reverse maps are likewise adjoint when each local fiber rule satisfies the corresponding scalar identity.

def TorchLean.Tensor.Internal.Rep.dot {R : Type u} [Storage R] [Semiring R] {s : Shape} (x y : Rep R s) : R

The standard bilinear pairing of two finite coordinate tensors.

theorem TorchLean.Tensor.Internal.Rep.dot_stack {R : Type u} [Storage R] [Semiring R] {n : ℕ} {s : Shape} (components : Fin n → Rep R s) (tensor : Rep R (n :: s)) : (stack components).dot tensor = ∑ component : Fin n, (components component).dot (tensor.unstack component)

Stacking and leading-axis slicing are adjoint for the finite tensor pairing.

The pairing of a stacked family with a tensor is the sum of the pairings with each corresponding leading-axis slice.

theorem TorchLean.Tensor.Internal.Rep.dot_reindex_eq_dot_reindex_symm {R : Type u} [Storage R] [Semiring R] {s t : Shape} (e : Coord t ≃ Coord s) (x : Rep R s) (y : Rep R t) : (reindex e x).dot y = x.dot (reindex e.symm y)

Reindexing and inverse reindexing are adjoint for the finite tensor pairing.

The proof changes the finite summation index along the coordinate equivalence; it does not require an ordering or positivity assumption on shape dimensions.

theorem TorchLean.Tensor.Internal.Rep.dot_reindex_reindex {R : Type u} [Storage R] [Semiring R] {s t : Shape} (e : Coord t ≃ Coord s) (x y : Rep R s) : (reindex e x).dot (reindex e y) = x.dot y

Applying the same coordinate reindexing to both tensors preserves their pairing.

theorem TorchLean.Tensor.Internal.Rep.dot_push_eq_dot_pull {R : Type u} [Storage R] [Semiring R] {s t : Shape} (f : Coord s → Coord t) (x : Rep R s) (y : Rep R t) : (push f x).dot y = x.dot (pull f y)

Fiber aggregation is adjoint to pullback for the standard finite dot product.

theorem TorchLean.Tensor.Internal.Rep.dot_fiberwiseDifferential_eq_dot_fiberwiseVjp {R : Type u} [Storage R] [Semiring R] {s t : Shape} (f : Coord s → Coord t) (fiberDifferential : (outputCoordinate : Coord t) → (Fiber f outputCoordinate → R) → (Fiber f outputCoordinate → R) → R) (fiberVjp : (outputCoordinate : Coord t) → (Fiber f outputCoordinate → R) → R → Fiber f outputCoordinate → R) (fiber_adjoint : ∀ (outputCoordinate : Coord t) (fiberInput fiberTangent : Fiber f outputCoordinate → R) (outputCotangent : R), fiberDifferential outputCoordinate fiberInput fiberTangent * outputCotangent = ∑ inputCoordinate : Fiber f outputCoordinate, fiberTangent inputCoordinate * fiberVjp outputCoordinate fiberInput outputCotangent inputCoordinate) (inputTensor inputTangent : Rep R s) (outputCotangent : Rep R t) : (ofFn fun (outputCoordinate : Coord t) => fiberDifferential outputCoordinate (fun (inputCoordinate : Fiber f outputCoordinate) => inputTensor.get ↑inputCoordinate) fun (inputCoordinate : Fiber f outputCoordinate) => inputTangent.get ↑inputCoordinate).dot outputCotangent = inputTangent.dot (ofFn fun (inputCoordinate : Coord s) => fiberVjp (f inputCoordinate) (fun (fiberCoordinate : Fiber f (f inputCoordinate)) => inputTensor.get ↑fiberCoordinate) (outputCotangent.get (f inputCoordinate)) ⟨inputCoordinate, ⋯⟩)

Lift a local differential/VJP adjunction on each reduction fiber to the corresponding tensor-level adjunction.

The two operators are ordinary dependent functions rather than a certificate structure. fiberDifferential receives the primal values and tangent values in one output fiber. fiberVjp receives the same primal values and one output cotangent, and returns one cotangent for every input in that fiber. The fiber_adjoint hypothesis is the complete local proof obligation.

This theorem deliberately does not claim that fiberDifferential is the derivative of a particular aggregate. A custom reducer establishes that fact separately using the derivative notion appropriate to its scalar domain, then uses this theorem to obtain the global VJP law. No permutation order is chosen: both local functions act directly on the finite fiber.