Tensor-network contraction

• Integer-valued factored tensor networks
• Contraction of factored tensor networks
• Bounds for contraction of factored tensor networks
• Equivalent presentations of finite tensor networks
• Tensor-instance alphabet padding
• Finite rectangular-grid tensor evaluation
• Finite row networks for grid tensors
• Bounds for finite grid row networks
• Transposition of finite grid tensor evaluations
• State padding preserves tensor-network values

TheoremGrid value expanded over kernel choices#✓fully proved

If every active rectangle kernel is a finite sum, the grid value is the sum over one kernel choice for each active rectangle. Raw rectangle indices outside gridRectangles retain the original kernel, which does not affect gridValue.

theorem gridValue_eq_sum_choices [Fintype ρ] [LinearOrder ρ]
    [Fintype γ] [LinearOrder γ] [DecidableEq A]
    {κ : {ω // ω ∈ gridRectangles ρ γ} → Type*}
    (labels diagonalLabels : Finset A) (R : Instance (ρ × γ) A)
    (G : ((ρ × ρ) × (γ × γ)) → A → A → A → A → ℤ)
    (choices : (ω : {ω // ω ∈ gridRectangles ρ γ}) → Finset (κ ω))
    (K : (ω : {ω // ω ∈ gridRectangles ρ γ}) → κ ω → A → A → A → A → ℤ)
    (hG : ∀ (ω : {ω // ω ∈ gridRectangles ρ γ}) x y u v,
      G ω x y u v = ∑ k ∈ choices ω, K ω k x y u v) :
    gridValue labels diagonalLabels R G =
      ∑ choice ∈ Fintype.piFinset choices,
        gridValue labels diagonalLabels R fun ω =>
          if hω : ω ∈ gridRectangles ρ γ then K ⟨ω, hω⟩ (choice ⟨ω, hω⟩) else G ω

Uses 6

Statement usesInteger-valued complete-graph tensor instance · Ordered rectangles of a finite grid · Finite grid tensor evaluation

Proof usesDirected labelings of a finite grid · Ordered pairs representing unordered pairs · Applying a rectangle kernel to its diagonal ends

TheoremEntry bound for a converted tensor instance#✓fully proved

A converted tensor entry is a sum of at most 2 ^ P terms, each containing one weight and Fintype.card J - 1 off-diagonal factors.

theorem abs_toInstance_le [Fintype J] [LinearOrder J] [DecidableEq A]
    (N : Factored J σ τ) (D : J → J → Finset A) (dec : J → J → A → τ)
    {P B : ℕ} (h : N.Sized P B) (a : J) (theta : J → A) :
    |N.toInstance D dec a theta| ≤ 2 ^ (P + B * Fintype.card J)

Uses 4

Statement usesInteger-valued factored tensor network · Shaped tensor network with bounded entries · Complete-graph instance of a factored network

Proof usesFactored tensor network with shape parameter

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.