Skip to content

Integer-valued factored tensor networks

17 fully proved

Tensor Network

DefinitionOrdered pairs representing unordered pairs#✓fully proved

Pairs (a, b) with a < b, representing unordered pairs once.

def orderedPairs (J : Type*) [Fintype J] [LinearOrder J] : Finset (J × J) :=
  univ.filter fun p => p.1 < p.2
Used by 24
Used byShape bound for contracted tensor networks · Size bound for contracted tensor networks · Capacity bound between grid rows · Shape bound for the grid row network · Size bound for the grid row network · Total capacity of the grid row network · Merging vertices of a factored tensor network · Interaction of merged classes in increasing order · Merging vertices preserves network value · Instance value as a sum over half-edge vectors · Converting a factored network to an instance preserves value · Number of ordered grid rectangles · Ordered rectangles of a finite grid · Finite grid tensor evaluation · Complete-graph tensor value as a crossing grid evaluation · Row network of a grid tensor · Interaction between rows of the grid row network · Row interaction for enumerated left states · Grid row network computes the grid value · Grid value expanded over kernel choices · Membership in the ordered pairs · Value of a factored tensor network · State padding preserves the weighted pair sum · Transposition preserves the grid evaluation

TheoremMembership in the ordered pairs#✓fully proved

Membership in orderedPairs is strict ordering of the two coordinates.

@[simp] theorem mem_orderedPairs [Fintype J] [LinearOrder J] (p : J × J) :
    p ∈ orderedPairs J ↔ p.1 < p.2
Uses 1 · Used by 10
Statement usesOrdered pairs representing unordered pairs
Used byCapacity bound between grid rows · Shape bound for the grid row network · Total capacity of the grid row network · Instance value as a sum over half-edge vectors · Converting a factored network to an instance preserves value · Number of ordered grid rectangles · Complete-graph tensor value as a crossing grid evaluation · Grid row network computes the grid value · State padding preserves the weighted pair sum · Transposition preserves the grid evaluation

DefinitionOrdered representative of an unordered pair#✓fully proved

The ordered representative (min a b, max a b) of the pair {a, b}.

def pairIndex [LinearOrder J] (a b : J) : J × J :=
  (min a b, max a b)
Used by 3
Used byHalf-edge presentation preserves instance value · Converting a factored network to an instance preserves value · Edge labels incident to a vertex

DefinitionEdge labelings of the complete graph#✓fully proved

Complete-graph edge labelings, free on orderedPairs and default elsewhere.

def edgeLabelings (J : Type*) [Fintype J] [LinearOrder J]
    (labels : Finset A) (default : A) : Finset (J × J → A) :=
  Fintype.piFinsetOn (fun p : J × J => p.1 < p.2) (fun _ => labels) default
Uses 1 · Used by 4
Statement usesFinite tuples with prescribed default values
Used byHalf-edge presentation preserves instance value · Converting a factored network to an instance preserves value · Characterization of complete-graph edge labelings · Value of a complete-graph tensor instance

TheoremCharacterization of complete-graph edge labelings#✓fully proved

A labeling belongs to edgeLabelings exactly when active edges use allowed labels and all other coordinates contain the default.

@[simp] theorem mem_edgeLabelings [Fintype J] [LinearOrder J]
    (labels : Finset A) (default : A) (labeling : J × J → A) :
    labeling ∈ edgeLabelings J labels default ↔
      ∀ p, (p.1 < p.2 → labeling p ∈ labels) ∧ (¬p.1 < p.2 → labeling p = default)
Uses 3 · Used by 1
Statement usesEdge labelings of the complete graph
Proof usesMembership in default-padded finite tuples · Finite tuples with prescribed default values
Used byHalf-edge presentation preserves instance value

DefinitionEdge labels incident to a vertex#✓fully proved

Labels incident to v, indexed by the other endpoint.

def incidentLabels [LinearOrder J] (labeling : J × J → A) (v : J) : J → A :=
  fun w => labeling (pairIndex v w)
Uses 1 · Used by 3
Statement usesOrdered representative of an unordered pair
Used byHalf-edge presentation preserves instance value · Converting a factored network to an instance preserves value · Value of a complete-graph tensor instance

AbbreviationInteger-valued complete-graph tensor instance#✓fully proved

An integer-valued local tensor at each vertex.

abbrev Instance (J A : Type*) := J → (J → A) → ℤ
Used by 24
Used byCapacity bound between grid rows · Shape bound for the grid row network · Size bound for the grid row network · Total capacity of the grid row network · Half-edge factored presentation of a tensor instance · Complete-graph instance of a factored network · Instance value as a sum over half-edge vectors · Half-edge presentation preserves instance value · Finite grid tensor evaluation · Transporting a tensor instance to a grid · Complete-graph tensor value as a crossing grid evaluation · Row network of a grid tensor · Interaction between rows of the grid row network · Row interaction for enumerated left states · Grid row network computes the grid value · Grid value expanded over kernel choices · Value of a complete-graph tensor instance · Alphabet padding of a tensor instance · Factoring and unfactoring a tensor instance gives its padding · Factoring round trip with the full source alphabet · Bijective alphabet padding preserves instance value · Transposition preserves the grid evaluation · Transpose of a grid tensor instance · Transposing a grid tensor instance is an involution

Complete-graph instances

DefinitionValue of a complete-graph tensor instance#✓fully proved

The sum, over complete-graph edge labelings, of the product of local tensors.

def value [Fintype J] [LinearOrder J] (labels : Finset A) (default : A)
    (R : Instance J A) : ℤ :=
  ∑ labeling ∈ edgeLabelings J labels default,
    ∏ v, R v (incidentLabels labeling v)
Uses 3 · Used by 5
Statement usesInteger-valued complete-graph tensor instance · Edge labelings of the complete graph · Edge labels incident to a vertex
Used byInstance value as a sum over half-edge vectors · Half-edge presentation preserves instance value · Converting a factored network to an instance preserves value · Complete-graph tensor value as a crossing grid evaluation · Bijective alphabet padding preserves instance value

Tensor Network

StructureInteger-valued factored tensor network#✓fully proved

An integer-valued factored tensor network.

Only Θ a b with a < b supplies labels. The factors f a b and f b a are the two sides of the same interaction. Capacities c are metadata used by totalCapacity, Shaped, and Sized; value does not read them.

structure Factored (J σ τ : Type*) where
  /-- The finite set of states allowed at each vertex. -/
  S : J → Finset σ
  /-- The integer weight of a state at a vertex. -/
  W : J → σ → ℤ
  /-- The finite label set stored in increasing vertex order. -/
  Θ : J → J → Finset τ
  /-- The factor contributed on one vertex's side of an edge label. -/
  f : J → J → σ → τ → ℤ
  /-- The directed capacity table; the bare structure does not require symmetry. -/
  c : J → J → ℕ
Used by 33
Used byEntry bound for a converted tensor instance · Shape bound for contracted tensor networks · Size bound for contracted tensor networks · Capacity bound between grid rows · Shape bound for the grid row network · Size bound for the grid row network · Total capacity of the grid row network · Number of states of a merged vertex · Merging vertices of a factored tensor network · Interaction of two distinct merged classes · Interaction of merged classes in increasing order · Merging vertices preserves network value · Half-edge factored presentation of a tensor instance · Complete-graph instance of a factored network · Instance value as a sum over half-edge vectors · Half-edge presentation preserves instance value · Converting a factored network to an instance preserves value · Row network of a grid tensor · Interaction between rows of the grid row network · Row interaction for enumerated left states · Grid row network computes the grid value · Interaction of two states in a factored network · Interaction is symmetric under swapping endpoints · Label set of an unordered vertex pair · Label set is symmetric in its endpoints · Factored tensor network with shape parameter · Shaped tensor network with bounded entries · Directed total capacity of a factored network · Value of a factored tensor network · State padding of a factored tensor network · State padding preserves value and total capacity · Factoring and unfactoring a tensor instance gives its padding · Bijective alphabet padding preserves instance value

Factored

DefinitionLabel set of an unordered vertex pair#✓fully proved

The label set of an unordered vertex pair.

def labelSet [LinearOrder J] (N : Factored J σ τ) (a b : J) : Finset τ :=
  N.Θ (min a b) (max a b)
Uses 1 · Used by 12
Statement usesInteger-valued factored tensor network
Used byShape bound for contracted tensor networks · Shape bound for the grid row network · Merging vertices of a factored tensor network · Interaction of merged classes in increasing order · Instance value as a sum over half-edge vectors · Converting a factored network to an instance preserves value · Interaction between rows of the grid row network · Interaction of two states in a factored network · Interaction is symmetric under swapping endpoints · Label set is symmetric in its endpoints · Factored tensor network with shape parameter · State padding of a factored tensor network

TheoremLabel set is symmetric in its endpoints#✓fully proved

The label set is independent of endpoint order.

theorem labelSet_comm [LinearOrder J] (N : Factored J σ τ) (a b : J) :
    N.labelSet a b = N.labelSet b a
Uses 2 · Used by 2
Statement usesInteger-valued factored tensor network · Label set of an unordered vertex pair
Used byShape bound for contracted tensor networks · Interaction is symmetric under swapping endpoints

DefinitionInteraction of two states in a factored network#✓fully proved

The interaction of two states, summed over their shared edge labels.

def interaction [LinearOrder J] (N : Factored J σ τ)
    (a b : J) (z z' : σ) : ℤ :=
  ∑ θ ∈ N.labelSet a b, N.f a b z θ * N.f b a z' θ
Uses 2 · Used by 17
Statement usesInteger-valued factored tensor network · Label set of an unordered vertex pair
Used byShape bound for contracted tensor networks · Size bound for contracted tensor networks · Size bound for the grid row network · Merging vertices of a factored tensor network · Interaction of two distinct merged classes · Interaction of merged classes in increasing order · Merging vertices preserves network value · Instance value as a sum over half-edge vectors · Converting a factored network to an instance preserves value · Interaction between rows of the grid row network · Row interaction for enumerated left states · Grid row network computes the grid value · Interaction is symmetric under swapping endpoints · Shaped tensor network with bounded entries · Value of a factored tensor network · State padding of a factored tensor network · State padding preserves value and total capacity

TheoremInteraction is symmetric under swapping endpoints#✓fully proved

Reading an interaction from the other endpoint swaps its states.

theorem interaction_comm [LinearOrder J] (N : Factored J σ τ)
    (a b : J) (z z' : σ) :
    N.interaction a b z z' = N.interaction b a z' z
Uses 4 · Used by 3
Statement usesInteger-valued factored tensor network · Interaction of two states in a factored network
Proof usesLabel set of an unordered vertex pair · Label set is symmetric in its endpoints
Used bySize bound for the grid row network · Interaction of two distinct merged classes · Merging vertices preserves network value

DefinitionValue of a factored tensor network#✓fully proved

The network value: sum over states of vertex weights times all pair interactions.

def value [Fintype J] [LinearOrder J] (N : Factored J σ τ) : ℤ :=
  ∑ z ∈ Fintype.piFinset N.S,
    (∏ a, N.W a (z a)) *
      ∏ p ∈ orderedPairs J, N.interaction p.1 p.2 (z p.1) (z p.2)
Uses 3 · Used by 7
Statement usesInteger-valued factored tensor network · Interaction of two states in a factored network · Ordered pairs representing unordered pairs
Used byMerging vertices preserves network value · Instance value as a sum over half-edge vectors · Half-edge presentation preserves instance value · Converting a factored network to an instance preserves value · Grid row network computes the grid value · State padding preserves value and total capacity · Bijective alphabet padding preserves instance value

DefinitionDirected total capacity of a factored network#✓fully proved

The directed total capacity Σ_{a ≠ b} c a b; both orientations are counted.

def totalCapacity [Fintype J] [DecidableEq J] (N : Factored J σ τ) : ℕ :=
  ∑ a, ∑ b ∈ univ.erase a, N.c a b
Uses 1 · Used by 2
Statement usesInteger-valued factored tensor network
Used byTotal capacity of the grid row network · State padding preserves value and total capacity

StructureFactored tensor network with shape parameter#✓fully proved

A network of shape parameter P: at most 2 ^ P states per vertex, symmetric capacities summing to at most P at each vertex, and at most 2 ^ c labels per edge.

structure Shaped [Fintype J] [LinearOrder J]
    (N : Factored J σ τ) (P : ℕ) : Prop where
  card_S : ∀ a, (N.S a).card ≤ 2 ^ P
  c_symm : ∀ a b, N.c a b = N.c b a
  sum_c : ∀ a, ∑ b ∈ univ.erase a, N.c a b ≤ P
  card_labelSet : ∀ a b, a ≠ b → (N.labelSet a b).card ≤ 2 ^ N.c a b
Uses 2 · Used by 6
Statement usesInteger-valued factored tensor network · Label set of an unordered vertex pair
Used byEntry bound for a converted tensor instance · Shape bound for contracted tensor networks · Size bound for contracted tensor networks · Shape bound for the grid row network · Size bound for the grid row network · Shaped tensor network with bounded entries

StructureShaped tensor network with bounded entries#✓fully proved

A shaped network whose weights, factors and off-diagonal interactions are bounded by 2 ^ B in absolute value.

structure Sized [Fintype J] [LinearOrder J]
    (N : Factored J σ τ) (P B : ℕ) : Prop extends Shaped N P where
  abs_W : ∀ a z, |N.W a z| ≤ 2 ^ B
  abs_f : ∀ a b z θ, |N.f a b z θ| ≤ 2 ^ B
  abs_interaction : ∀ a b z z', a ≠ b → |N.interaction a b z z'| ≤ 2 ^ B
Uses 3 · Used by 3
Statement usesInteger-valued factored tensor network · Factored tensor network with shape parameter · Interaction of two states in a factored network
Used byEntry bound for a converted tensor instance · Size bound for contracted tensor networks · Size bound for the grid row network

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.