Bounds for contraction of factored tensor networks

TheoremShape bound for contracted tensor networks#✓fully proved

If every contraction class has at most m vertices, contraction multiplies the network's shape parameter by m.

theorem merge_shaped [Fintype J] [LinearOrder J] [Fintype J'] [LinearOrder J']
    (N : Factored J σ τ) (chi : J → J') (defaultState : σ) (defaultLabel : τ) {P m : ℕ}
    (h : N.Shaped P) (hm : ∀ G, (univ.filter fun a => chi a = G).card ≤ m) :
    (N.merge chi defaultState defaultLabel).Shaped (P * m)

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 → ℕ

MathlibExt/Combinatorics/TensorNetwork/Basic.lean:84

Uses 10 · Used by 1

Statement usesInteger-valued factored tensor network · Factored tensor network with shape parameter · Merging vertices of a factored tensor network

Proof usesNumber of default-padded finite tuples · Finite tuples with prescribed default values · Number of states of a merged vertex · Interaction of two states in a factored network · Label set of an unordered vertex pair · Label set is symmetric in its endpoints · Ordered pairs representing unordered pairs

Used bySize bound for contracted tensor networks

TheoremSize bound for contracted tensor networks#✓fully proved

If every contraction class has at most m vertices, contraction multiplies the shape parameter by m and changes the absolute-value exponent from B to B * (m + m * m).

theorem merge_sized [Fintype J] [LinearOrder J] [Fintype J'] [LinearOrder J']
    (N : Factored J σ τ) (chi : J → J') (defaultState : σ) (defaultLabel : τ)
    {P B m : ℕ} (h : N.Sized P B)
    (hm : ∀ G, (univ.filter fun a => chi a = G).card ≤ m) :
    (N.merge chi defaultState defaultLabel).Sized (P * m) (B * (m + m * m))

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 → ℕ

MathlibExt/Combinatorics/TensorNetwork/Basic.lean:84

Uses 8

Statement usesInteger-valued factored tensor network · Shaped tensor network with bounded entries · Merging vertices of a factored tensor network

Proof usesFactored tensor network with shape parameter · Interaction of two states in a factored network · Interaction of two distinct merged classes · Shape bound for contracted tensor networks · Ordered pairs representing unordered pairs

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.