Transposition of finite grid tensor evaluations

5 fully proved

Transposition

DefinitionTranspose of a grid tensor instance#✓fully proved

Swap the row and column coordinates of a grid tensor instance.

def transpose (R : Instance (ρ × γ) A) : Instance (γ × ρ) A :=
  fun w h => R w.swap fun w' => h w'.swap

Uses 1 · Used by 2

Statement usesInteger-valued complete-graph tensor instance

Used byTransposition preserves the grid evaluation · Transposing a grid tensor instance is an involution

TheoremTransposing a grid tensor instance is an involution#✓fully proved

Transposing a grid tensor instance twice recovers the original instance.

@[simp] theorem transpose_transpose (R : Instance (ρ × γ) A) : R.transpose.transpose = R

Uses 2

Statement usesInteger-valued complete-graph tensor instance · Transpose of a grid tensor instance

Tensor Network

DefinitionTranspose of a rectangle kernel#✓fully proved

Transpose a rectangle kernel, exchanging the y and u directed diagonal ends.

def transposeRectangleKernel
    (G : ((ρ × ρ) × (γ × γ)) → A → A → A → A → ℤ) :
    ((γ × γ) × (ρ × ρ)) → A → A → A → A → ℤ :=
  fun ω x y u v => G (ω.2, ω.1) x u y v

Used by 2

Used byTransposition preserves the grid evaluation · Transposing a rectangle kernel is an involution

TheoremTransposing a rectangle kernel is an involution#✓fully proved

Transposing a rectangle kernel twice recovers the original kernel.

@[simp] theorem transposeRectangleKernel_transposeRectangleKernel
    (G : ((ρ × ρ) × (γ × γ)) → A → A → A → A → ℤ) :
    transposeRectangleKernel (transposeRectangleKernel G) = G

def transposeRectangleKernel
    (G : ((ρ × ρ) × (γ × γ)) → A → A → A → A → ℤ) :
    ((γ × γ) × (ρ × ρ)) → A → A → A → A → ℤ :=
  fun ω x y u v => G (ω.2, ω.1) x u y v

MathlibExt/Combinatorics/TensorNetwork/GridTranspose.lean:53

Uses 1

Statement usesTranspose of a rectangle kernel

TheoremTransposition preserves the grid evaluation#✓fully proved

Transposing the grid coordinates, local tensors, and rectangle kernels preserves the finite grid evaluation. Edge and diagonal label choices remain independent.

theorem gridValue_transpose [Fintype ρ] [LinearOrder ρ] [Fintype γ] [LinearOrder γ]
    [DecidableEq A] (labels diagonalLabels : Finset A) (R : Instance (ρ × γ) A)
    (G : ((ρ × ρ) × (γ × γ)) → A → A → A → A → ℤ) :
    gridValue labels diagonalLabels R.transpose (transposeRectangleKernel G) =
      gridValue labels diagonalLabels R G

abbrev Instance (J A : Type*) := J → (J → A) → ℤ

MathlibExt/Combinatorics/TensorNetwork/Basic.lean:67

def gridValue [Fintype ρ] [LinearOrder ρ] [Fintype γ] [LinearOrder γ]
    [DecidableEq A] (labels diagonalLabels : Finset A) (R : Instance (ρ × γ) A)
    (G : ((ρ × ρ) × (γ × γ)) → A → A → A → A → ℤ) : ℤ :=
  ∑ ℓ ∈ gridLabelings labels diagonalLabels,
    (∏ w, R w (ℓ w)) *
      ((∏ a, ∏ q ∈ orderedPairs γ,
          if ℓ (a, q.1) (a, q.2) = ℓ (a, q.2) (a, q.1) then 1 else 0) *
        (∏ i, ∏ p ∈ orderedPairs ρ,
          if ℓ (p.1, i) (p.2, i) = ℓ (p.2, i) (p.1, i) then 1 else 0) *
        ∏ ω ∈ gridRectangles ρ γ, rectangleApply (G ω) ℓ ω)

MathlibExt/Combinatorics/TensorNetwork/Grid.lean:89

def transposeRectangleKernel
    (G : ((ρ × ρ) × (γ × γ)) → A → A → A → A → ℤ) :
    ((γ × γ) × (ρ × ρ)) → A → A → A → A → ℤ :=
  fun ω x y u v => G (ω.2, ω.1) x u y v

MathlibExt/Combinatorics/TensorNetwork/GridTranspose.lean:53

Uses 10

Statement usesInteger-valued complete-graph tensor instance · Transpose of a grid tensor instance · Finite grid tensor evaluation · Transpose of a rectangle kernel

Proof usesDirected labelings of a finite grid · Ordered rectangles of a finite grid · Characterization of directed grid labelings · Membership in the ordered pairs · Ordered pairs representing unordered pairs · Applying a rectangle kernel to its diagonal ends

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.