TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.MLTheory.CROWN.Proofs.DirectedIBPAxisInverse

Checked inverse axis arrays #

A valid axis array represents a finite permutation. The executable inverse-table builder returns its inverse, so applying that builder twice recovers the original axis array.

source
def NN.MLTheory.CROWN.Graph.axisArray {rank : ℕ} (e : Equiv.Perm (Fin rank)) :
Array ℕ

List the image of each axis under the permutation, in source-axis order.

Instances For
    source
    @[simp]
    theorem NN.MLTheory.CROWN.Graph.axisArray_size {rank : ℕ} (e : Equiv.Perm (Fin rank)) :
    (axisArray e).size = rank
    source
    @[simp]
    theorem NN.MLTheory.CROWN.Graph.axisArray_getElem {rank : ℕ} (e : Equiv.Perm (Fin rank)) (i : ℕ) (hi : i < (axisArray e).size) :
    (axisArray e)[i] = ↑(e ⟨i, ⋯⟩)
    source
    @[simp]
    theorem NN.MLTheory.CROWN.Graph.axisArray_getElem! {rank : ℕ} (e : Equiv.Perm (Fin rank)) (i : Fin rank) :
    (axisArray e)[↑i]! = ↑(e i)
    source
    def NN.MLTheory.CROWN.Graph.axisMap {rank : ℕ} (e : Equiv.Perm (Fin rank)) (xs : List ℕ) :
    List ℕ

    Read a natural-number list in the axis order encoded by a finite permutation.

    Instances For
      source
      @[simp]
      theorem NN.MLTheory.CROWN.Graph.axisMap_length {rank : ℕ} (e : Equiv.Perm (Fin rank)) (xs : List ℕ) :
      (axisMap e xs).length = rank
      source
      @[simp]
      theorem NN.MLTheory.CROWN.Graph.axisMap_getElem! {rank : ℕ} (e : Equiv.Perm (Fin rank)) (xs : List ℕ) (i : Fin rank) :
      (axisMap e xs)[↑i]! = xs[↑(e i)]!
      source
      theorem NN.MLTheory.CROWN.Graph.axisMap_symm {rank : ℕ} (e : Equiv.Perm (Fin rank)) (xs : List ℕ) (hlen : xs.length = rank) :
      axisMap (Equiv.symm e) (axisMap e xs) = xs
      source
      theorem NN.MLTheory.CROWN.Graph.exists_axisArray {perm : Array ℕ} {rank : ℕ} (hperm : perm.toList.Perm (List.range rank)) :
      ∃ (e : Equiv.Perm (Fin rank)), perm = axisArray e

      An axis list obtained by swaps has an ordinary finite permutation representation.

      source
      theorem NN.MLTheory.CROWN.Graph.inversePerm_axisArray {rank : ℕ} (e : Equiv.Perm (Fin rank)) :
      IR.OpContracts.inversePerm (axisArray e) = Except.ok (axisArray (Equiv.symm e))

      The checked inverse-table algorithm computes the inverse finite permutation.

      source
      theorem NN.MLTheory.CROWN.Graph.permuteShape_properties {s t : Spec.Shape} {perm : Array ℕ} (h : s.permute? perm.toList = some t) :
      perm.size = s.rank ∧ perm.toList.Nodup ∧ t = List.map (fun (i : ℕ) => s[i]!) perm.toList

      A successful shape check has the declared rank and reads precisely its requested axes.