TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.MLTheory.CROWN.Proofs.DirectedIBPAxisSemantics

The real evaluator and the backward flat permutation #

The forward evaluator lowers an axis array to adjacent swaps. The backward operation inverts the same array and linearizes its coordinates. Both implementations therefore describe one bijection of real tensor entries, including tensors with arbitrary rank and zero-length dimensions.

source
theorem NN.MLTheory.CROWN.Graph.DirectedBackward.adjacentShape_axisMap (s : Spec.Shape) (swaps : List ℕ) (e : Equiv.Perm (Fin (List.length s))) (haxes : List.foldl Spec.Shape.swapAdjacentAxes (List.range (List.length s)) swaps = (axisArray e).toList) :
s.applyAdjacentSwaps swaps = axisMap e s
source
theorem NN.MLTheory.CROWN.Graph.DirectedBackward.adjacentCoordinateEquiv_axisMap (s : Spec.Shape) (swaps : List ℕ) (e : Equiv.Perm (Fin (List.length s))) (haxes : List.foldl Spec.Shape.swapAdjacentAxes (List.range (List.length s)) swaps = (axisArray e).toList) (c : s.Coord) :
Spec.Shape.Coord.toList (s.applyAdjacentSwaps swaps) ((adjacentCoordinateEquiv s swaps) c) = axisMap e (Spec.Shape.Coord.toList s c)
source
noncomputable def NN.MLTheory.CROWN.Graph.DirectedBackward.adjacentFlatEquiv (s : Spec.Shape) (swaps : List ℕ) :
Fin s.size ≃ Fin (s.applyAdjacentSwaps swaps).size

The forward permutation of flat tensor coordinates, obtained from the actual adjacent swaps.

Instances For
    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.flatCoordEquiv_symm_val (s : Spec.Shape) (c : s.Coord) :
    ↑((flatCoordEquiv s).symm c) = ↑(TorchLean.Tensor.Internal.Coord.linearize c)
    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.flatAxisPermutation?_adjacent (s : Spec.Shape) (swaps : List ℕ) (e : Equiv.Perm (Fin (List.length s))) (haxes : List.foldl Spec.Shape.swapAdjacentAxes (List.range (List.length s)) swaps = (axisArray e).toList) {flat : Fin (s.applyAdjacentSwaps swaps).size → Fin (s.applyAdjacentSwaps swaps).size} (hflat : flatAxisPermutation? (s.applyAdjacentSwaps swaps) (axisArray (Equiv.symm e)) (s.applyAdjacentSwaps swaps).size = some flat) :
    flat = ⇑((finCongr ⋯).trans (adjacentFlatEquiv s swaps))

    The checked backward flat permutation is the inverse-read form of the forward swaps.

    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.realTensor_coord (s : Spec.Shape) (f : ℕ → ℝ) (c : s.Coord) :
    TorchLean.Tensor.Internal.Rep.get (realTensor s f) c = f ↑((flatCoordEquiv s).symm c)
    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.adjacentFlatEquiv_values (s : Spec.Shape) (swaps : List ℕ) (f g : ℕ → ℝ) (hvalues : (realTensor s f).permuteByAdjacentSwaps swaps = realTensor (s.applyAdjacentSwaps swaps) g) (i : Fin s.size) :
    g ↑((adjacentFlatEquiv s swaps) i) = f ↑i
    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.permuteSomeTensor_flatEquation {s t : Spec.Shape} {forward : Array ℕ} {f g : ℕ → ℝ} (heval : IR.Graph.permuteSomeTensor { shape := s, tensor := realTensor s f } forward = Except.ok { shape := t, tensor := realTensor t g }) :
    s.size = t.size ∧ ∀ (inverse : Array ℕ), (IR.OpContracts.inversePerm forward).toOption = some inverse → ∀ (flat : Fin t.size → Fin t.size), flatAxisPermutation? t inverse t.size = some flat → Function.Bijective flat ∧ ∀ (i : Fin t.size), g ↑(flat i) = f ↑i

    A successful real permutation evaluator supplies exactly the backward coordinate equation.