Skip to content

Equivalent presentations of finite tensor networks

5 fully proved

Factored

DefinitionComplete-graph instance of a factored network#✓fully proved

Turn a factored network into a complete-graph tensor instance.

The finite set D a b names the source labels on the edge {a, b} through dec a b. Labels outside D a b make the corresponding directed factor zero.

def toInstance [Fintype J] [LinearOrder J] [DecidableEq A] (N : Factored J σ τ)
    (D : J → J → Finset A) (dec : J → J → A → τ) : Instance J A :=
  fun a θ => ∑ z ∈ N.S a, N.W a z *
    ∏ b ∈ univ.erase a,
      if θ b ∈ D (min a b) (max a b) then
        N.f a b z (dec (min a b) (max a b) (θ b))
      else 0
Uses 2 · Used by 6
Statement usesInteger-valued factored tensor network · Integer-valued complete-graph tensor instance
Used byEntry bound for a converted tensor instance · Half-edge presentation preserves instance value · Converting a factored network to an instance preserves value · Factoring and unfactoring a tensor instance gives its padding · Factoring round trip with the full source alphabet · Bijective alphabet padding preserves instance value

TheoremConverting a factored network to an instance preserves value#✓fully proved

Naming every source edge alphabet bijectively inside labels preserves network value.

theorem value_toInstance [Fintype J] [LinearOrder J] [DecidableEq A]
    (N : Factored J σ τ) (labels : Finset A) (default : A)
    (D : J → J → Finset A) (dec : J → J → A → τ)
    (hD : ∀ a b, a < b → D a b ⊆ labels)
    (hdec : ∀ a b, a < b → Set.BijOn (dec a b) (D a b) (N.Θ a b)) :
    (N.toInstance D dec).value labels default = N.value
Uses 13 · Used by 2
Statement usesInteger-valued factored tensor network · Complete-graph instance of a factored network · Value of a factored tensor network · Value of a complete-graph tensor instance
Proof usesFinite tuples with prescribed default values · Product of sums over default-padded tuples · Interaction of two states in a factored network · Label set of an unordered vertex pair · Edge labelings of the complete graph · Edge labels incident to a vertex · Membership in the ordered pairs · Ordered pairs representing unordered pairs · Ordered representative of an unordered pair
Used byHalf-edge presentation preserves instance value · Bijective alphabet padding preserves instance value

Half-edge presentations

DefinitionHalf-edge factored presentation of a tensor instance#✓fully proved

Present an instance as a half-edge network.

A state at v chooses one label for every off-diagonal half-edge from v; the two sides of each edge are constrained to agree. The capacities are zero because this construction makes no size claim.

def toFactored [Fintype J] [DecidableEq J] [DecidableEq A]
    (R : Instance J A) (labels : Finset A) (default : A) :
    Factored J (J → A) A where
  S v := Fintype.piFinsetOn (fun w => w ≠ v) (fun _ => labels) default
  W := R
  Θ _ _ := labels
  f _ w z θ := if z w = θ then 1 else 0
  c _ _ := 0
Uses 3 · Used by 5
Statement usesFinite tuples with prescribed default values · Integer-valued factored tensor network · Integer-valued complete-graph tensor instance
Used byInstance value as a sum over half-edge vectors · Half-edge presentation preserves instance value · Factoring and unfactoring a tensor instance gives its padding · Factoring round trip with the full source alphabet · Bijective alphabet padding preserves instance value

TheoremHalf-edge presentation preserves instance value#✓fully proved

The half-edge presentation of an instance has the same value.

theorem value_toFactored [Fintype J] [LinearOrder J] [DecidableEq A]
    (R : Instance J A) (labels : Finset A) (default : A) :
    R.value labels default = (R.toFactored labels default).value
Uses 13 · Used by 2
Statement usesValue of a factored tensor network · Integer-valued complete-graph tensor instance · Half-edge factored presentation of a tensor instance · Value of a complete-graph tensor instance
Proof usesMembership in default-padded finite tuples · Finite tuples with prescribed default values · Integer-valued factored tensor network · Complete-graph instance of a factored network · Converting a factored network to an instance preserves value · Edge labelings of the complete graph · Edge labels incident to a vertex · Characterization of complete-graph edge labelings · Ordered representative of an unordered pair
Used byInstance value as a sum over half-edge vectors · Bijective alphabet padding preserves instance value

TheoremInstance value as a sum over half-edge vectors#✓fully proved

Expand an instance value as a sum over directed half-edge vectors with equality factors.

theorem value_eq_halfEdges [Fintype J] [LinearOrder J] [DecidableEq A]
    (R : Instance J A) (labels : Finset A) (default : A) :
    R.value labels default =
      ∑ ℓ ∈ Fintype.piFinset fun w : J =>
        Fintype.piFinsetOn (fun w' => w' ≠ w) (fun _ => labels) default,
        (∏ w, R w (ℓ w)) * ∏ p ∈ orderedPairs J,
          if ℓ p.1 p.2 = ℓ p.2 p.1 then 1 else 0
Uses 12 · Used by 1
Statement usesFinite tuples with prescribed default values · Integer-valued complete-graph tensor instance · Value of a complete-graph tensor instance · Ordered pairs representing unordered pairs
Proof usesMembership in default-padded finite tuples · Integer-valued factored tensor network · Interaction of two states in a factored network · Label set of an unordered vertex pair · Value of a factored tensor network · Half-edge factored presentation of a tensor instance · Half-edge presentation preserves instance value · Membership in the ordered pairs
Used byComplete-graph tensor value as a crossing grid evaluation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.