TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.MLTheory.CROWN.Proofs.DirectedIBPCoordinates

Coordinates of the directed pooling iterator #

The executable average-pool transfer enumerates flattened windows. Its quotient/remainder loop recovers the same row-major coordinates as the tensor specification.

source
def NN.MLTheory.CROWN.Graph.DirectedBackward.flatCoordEquiv (s : Spec.Shape) :
Fin s.size ≃ s.Coord

The usual row-major tensor coordinate represented by a flat graph index.

Instances For
    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.linearize_flatCoordEquiv (s : Spec.Shape) (i : Fin s.size) :
    ↑(TorchLean.Tensor.Internal.Coord.linearize ((flatCoordEquiv s) i)) = ↑i
    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.getScalar_flatten_coord {β : Type} [TorchLean.Storage β] {s : Spec.Shape} (x : TorchLean.Tensor β s) (i : Fin s.size) :
    x.flattenSpec.getScalar i = TorchLean.Tensor.Internal.Rep.get x ((flatCoordEquiv s) i)