Skip to content

Finite rectangular-grid tensor evaluation

9 fully proved

Tensor Network

DefinitionOrdered rectangles of a finite grid#✓fully proved

Ordered grid rectangles, indexed by an increasing row pair and increasing column pair.

def gridRectangles (ρ γ : Type*) [Fintype ρ] [LinearOrder ρ]
    [Fintype γ] [LinearOrder γ] : Finset ((ρ × ρ) × (γ × γ)) :=
  orderedPairs ρ ×ˢ orderedPairs γ
Uses 1 · Used by 7
Statement usesOrdered pairs representing unordered pairs
Used byTotal capacity of the grid row network · Number of ordered grid rectangles · Finite grid tensor evaluation · Complete-graph tensor value as a crossing grid evaluation · Grid row network computes the grid value · Grid value expanded over kernel choices · Transposition preserves the grid evaluation

DefinitionApplying a rectangle kernel to its diagonal ends#✓fully proved

Apply a rectangle kernel to its four directed diagonal ends x, y, u, v.

def rectangleApply (G : A → A → A → A → ℤ)
    (ℓ : Matrix (ρ × γ) (ρ × γ) A) (ω : (ρ × ρ) × (γ × γ)) : ℤ :=
  G (ℓ (ω.1.1, ω.2.1) (ω.1.2, ω.2.2))
    (ℓ (ω.1.1, ω.2.2) (ω.1.2, ω.2.1))
    (ℓ (ω.1.2, ω.2.1) (ω.1.1, ω.2.2))
    (ℓ (ω.1.2, ω.2.2) (ω.1.1, ω.2.1))
Used by 5
Used byFinite grid tensor evaluation · Complete-graph tensor value as a crossing grid evaluation · Grid row network computes the grid value · Grid value expanded over kernel choices · Transposition preserves the grid evaluation

DefinitionDirected labelings of a finite grid#✓fully proved

Directed grid labelings with independent finite choices on edges and diagonal entries.

def gridLabelings [Fintype ρ] [Fintype γ] [DecidableEq (ρ × γ)] [DecidableEq A]
    (labels diagonalLabels : Finset A) : Finset (Matrix (ρ × γ) (ρ × γ) A) :=
  (Fintype.piFinset fun w =>
    Fintype.piFinset fun w' => if w' = w then diagonalLabels else labels).map
      Matrix.of.toEmbedding
Used by 6
Used byFinite grid tensor evaluation · Characterization of directed grid labelings · Complete-graph tensor value as a crossing grid evaluation · Grid row network computes the grid value · Grid value expanded over kernel choices · Transposition preserves the grid evaluation

TheoremCharacterization of directed grid labelings#✓fully proved

Membership in gridLabelings means precisely that diagonal and edge coordinates use their respective finite choice sets.

@[simp] theorem mem_gridLabelings [Fintype ρ] [Fintype γ] [DecidableEq (ρ × γ)]
    [DecidableEq A]
    (labels diagonalLabels : Finset A) (ℓ : Matrix (ρ × γ) (ρ × γ) A) :
    ℓ ∈ gridLabelings labels diagonalLabels ↔
      ∀ w w', (w' = w → ℓ w w' ∈ diagonalLabels) ∧ (w' ≠ w → ℓ w w' ∈ labels)
Uses 1 · Used by 3
Statement usesDirected labelings of a finite grid
Used byComplete-graph tensor value as a crossing grid evaluation · Grid row network computes the grid value · Transposition preserves the grid evaluation

DefinitionFinite grid tensor evaluation#✓fully proved

The finite grid evaluation: local tensors, row and column edge equalities, and one kernel per ordered rectangle, summed over all directed labelings.

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 ω) ℓ ω)
Uses 5 · Used by 4
Statement usesInteger-valued complete-graph tensor instance · Directed labelings of a finite grid · Ordered rectangles of a finite grid · Ordered pairs representing unordered pairs · Applying a rectangle kernel to its diagonal ends
Used byComplete-graph tensor value as a crossing grid evaluation · Grid row network computes the grid value · Grid value expanded over kernel choices · Transposition preserves the grid evaluation

Transport to a grid

DefinitionTransporting a tensor instance to a grid#✓fully proved

Transport an instance to a grid, returning zero unless the self-label is the chosen default.

def onGrid [DecidableEq A] (R : Instance J A) (default : A) (e : J ≃ ρ × γ) :
    Instance (ρ × γ) A :=
  fun w h => if h w = default then R (e.symm w) (fun v => h (e v)) else 0
Uses 1 · Used by 1
Statement usesInteger-valued complete-graph tensor instance
Used byComplete-graph tensor value as a crossing grid evaluation

Tensor Network

DefinitionCrossing kernel on grid rectangles#✓fully proved

The crossing kernel requires opposite directed copies on both rectangle diagonals to agree.

def crossing [DecidableEq A] (x y u v : A) : ℤ :=
  if x = v ∧ y = u then 1 else 0
Used by 1
Used byComplete-graph tensor value as a crossing grid evaluation

TheoremComplete-graph tensor value as a crossing grid evaluation#✓fully proved

Complete-graph tensor evaluation is the crossing grid evaluation after transport. The transport gates diagonal entries at default; other allowed diagonal labels therefore contribute zero. The default need not belong to the edge-label set.

theorem Instance.value_eq_gridValue_crossing [Fintype J] [LinearOrder J]
    [Fintype ρ] [LinearOrder ρ] [Fintype γ] [LinearOrder γ] [DecidableEq A]
    (R : Instance J A) (labels diagonalLabels : Finset A) (default : A)
    (hdefault : default ∈ diagonalLabels) (e : J ≃ ρ × γ) :
    R.value labels default =
      gridValue labels diagonalLabels (R.onGrid default e) (fun _ => crossing)
Uses 15
Statement usesInteger-valued complete-graph tensor instance · Transporting a tensor instance to a grid · Value of a complete-graph tensor instance · Crossing kernel on grid rectangles · Finite grid tensor evaluation
Proof usesMembership in default-padded finite tuples · Finite tuples with prescribed default values · Symmetry criterion for matrices indexed by a product · Instance value as a sum over half-edge vectors · Directed 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

TheoremNumber of ordered grid rectangles#✓fully proved

The number of ordered grid rectangles is the product of the two pair counts.

theorem card_gridRectangles [Fintype ρ] [LinearOrder ρ] [Fintype γ] [LinearOrder γ] :
    (gridRectangles ρ γ).card =
      (Fintype.card ρ).choose 2 * (Fintype.card γ).choose 2
Uses 3
Statement usesOrdered rectangles of a finite grid
Proof usesMembership in the ordered pairs · Ordered pairs representing unordered pairs

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.