Contraction of factored tensor networks

DefinitionMerging vertices of a factored tensor network#✓fully proved

Merge vertices along χ, retaining source states and labels on their classes and padding all other coordinates with the supplied defaults.

def merge [Fintype J] [LinearOrder J] [LinearOrder J'] (N : Factored J σ τ)
    (χ : J → J') (defaultState : σ) (defaultLabel : τ) :
    Factored J' (J → σ) (J × J → τ) where
  S G := Fintype.piFinsetOn (fun a => χ a = G) N.S defaultState
  W G z :=
    (∏ a with χ a = G, N.W a (z a)) *
      ∏ p ∈ orderedPairs J with χ p.1 = G ∧ χ p.2 = G,
        N.interaction p.1 p.2 (z p.1) (z p.2)
  Θ G G' := Fintype.piFinsetOn (fun p : J × J => χ p.1 = G ∧ χ p.2 = G')
    (fun p => N.labelSet p.1 p.2) defaultLabel
  f G G' z t :=
    ∏ p : J × J with χ p.1 = G ∧ χ p.2 = G',
      N.f p.1 p.2 (z p.1) (t (if G < G' then p else p.swap))
  c G G' := ∑ p : J × J with χ p.1 = G ∧ χ p.2 = G', N.c p.1 p.2

Uses 5 · Used by 6

Statement usesFinite tuples with prescribed default values · Integer-valued factored tensor network · Interaction of two states in a factored network · Label set of an unordered vertex pair · Ordered pairs representing unordered pairs

Used byShape bound for contracted tensor networks · Size bound for contracted tensor networks · Number of states of a merged vertex · Interaction of two distinct merged classes · Interaction of merged classes in increasing order · Merging vertices preserves network value

TheoremInteraction of merged classes in increasing order#✓fully proved

The interaction of two increasingly ordered classes is the product of all source interactions crossing between them.

theorem merge_interaction_lt [Fintype J] [LinearOrder J] [LinearOrder J']
    (N : Factored J σ τ) (χ : J → J') (defaultState : σ) (defaultLabel : τ)
    {G G' : J'} (h : G < G') (z z' : J → σ) :
    (N.merge χ defaultState defaultLabel).interaction G G' z z' =
      ∏ p : J × J with χ p.1 = G ∧ χ p.2 = G',
        N.interaction p.1 p.2 (z p.1) (z' p.2)

Uses 7 · Used by 2

Statement usesInteger-valued factored tensor network · Interaction of two states in a factored network · Merging vertices of a factored tensor network

Proof usesFinite tuples with prescribed default values · Products of factorized functions over label tuples · Label set of an unordered vertex pair · Ordered pairs representing unordered pairs

Used byInteraction of two distinct merged classes · Merging vertices preserves network value

TheoremInteraction of two distinct merged classes#✓fully proved

The interaction of two distinct classes is the product of all source interactions crossing between them, oriented from the first class to the second.

theorem merge_interaction [Fintype J] [LinearOrder J] [LinearOrder J']
    (N : Factored J σ τ) (χ : J → J') (defaultState : σ) (defaultLabel : τ)
    {G G' : J'} (h : G ≠ G') (z z' : J → σ) :
    (N.merge χ defaultState defaultLabel).interaction G G' z z' =
      ∏ p : J × J with χ p.1 = G ∧ χ p.2 = G',
        N.interaction p.1 p.2 (z p.1) (z' p.2)

Uses 5 · Used by 1

Statement usesInteger-valued factored tensor network · Interaction of two states in a factored network · Merging vertices of a factored tensor network

Proof usesInteraction is symmetric under swapping endpoints · Interaction of merged classes in increasing order

Used bySize bound for contracted tensor networks

TheoremMerging vertices preserves network value#✓fully proved

Merging along any map preserves the exact integer-valued network value.

theorem value_merge [Fintype J] [LinearOrder J] [Fintype J'] [LinearOrder J']
    (N : Factored J σ τ) (χ : J → J') (defaultState : σ) (defaultLabel : τ) :
    (N.merge χ defaultState defaultLabel).value = N.value

Uses 9

Statement usesInteger-valued factored tensor network · Merging vertices of a factored tensor network · Value of a factored tensor network

Proof usesMembership in default-padded finite tuples · Finite tuples with prescribed default values · Interaction of two states in a factored network · Interaction is symmetric under swapping endpoints · Interaction of merged classes in increasing order · Ordered pairs representing unordered pairs

TheoremNumber of states of a merged vertex#✓fully proved

The number of merged states is the product of the state-set sizes in the class.

theorem card_merge_S [Fintype J] [LinearOrder J] [LinearOrder J']
    (N : Factored J σ τ) (χ : J → J') (defaultState : σ) (defaultLabel : τ)
    (G : J') :
    ((N.merge χ defaultState defaultLabel).S G).card =
      ∏ a with χ a = G, (N.S a).card

Uses 3 · Used by 1

Statement usesInteger-valued factored tensor network · Merging vertices of a factored tensor network

Proof usesNumber of default-padded finite tuples

Used byShape bound for contracted tensor networks

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.