Bounds for finite grid row networks

TheoremCapacity bound between grid rows#✓fully proved

The capacity between two grid rows is at most g²mL when every active rectangle is charged at most 2mL and there are g columns.

theorem gridRowNetwork_capacity_le [Fintype ρ] [LinearOrder ρ]
    [Fintype γ] [LinearOrder γ] [DecidableEq A]
    {g L m : ℕ} (hm : 1 ≤ m) (hγ : Fintype.card γ = g)
    (labels diagonalLabels : Finset A) (R : Instance (ρ × γ) A)
    (cutLabels : ((ρ × ρ) × (γ × γ)) → Finset T)
    (top bottom : ((ρ × ρ) × (γ × γ)) → A → A → T → ℤ)
    (cap : ((ρ × ρ) × (γ × γ)) → ℕ)
    (hcap : ∀ ω, cap ω ≤ 2 * m * L) (a b : ρ) :
    (gridRowNetwork labels diagonalLabels R cutLabels top bottom cap L).c a b ≤
      g ^ 2 * (m * L)

Uses 5 · Used by 1

Statement usesInteger-valued factored tensor network · Integer-valued complete-graph tensor instance · Row network of a grid tensor · Ordered pairs representing unordered pairs

Proof usesMembership in the ordered pairs

Used byShape bound for the grid row network

TheoremShape bound for the grid row network#✓fully proved

The grid row network has shape m g³ L when both raw-state alphabets have at most 2^L elements and every rectangle label set and capacity obeys its declared bound.

theorem gridRowNetwork_shaped [Fintype ρ] [LinearOrder ρ]
    [Fintype γ] [LinearOrder γ] [DecidableEq A]
    {g L m : ℕ} (hm : 1 ≤ m) (hρ : Fintype.card ρ = g)
    (hγ : Fintype.card γ = g)
    (labels diagonalLabels : Finset A) (hlabels : labels.card ≤ 2 ^ L)
    (hdiagonal : diagonalLabels.card ≤ 2 ^ L) (R : Instance (ρ × γ) A)
    (cutLabels : ((ρ × ρ) × (γ × γ)) → Finset T)
    (top bottom : ((ρ × ρ) × (γ × γ)) → A → A → T → ℤ)
    (cap : ((ρ × ρ) × (γ × γ)) → ℕ)
    (hcut : ∀ ω, (cutLabels ω).card ≤ 2 ^ cap ω)
    (hcap : ∀ ω, cap ω ≤ 2 * m * L) :
    (gridRowNetwork labels diagonalLabels R cutLabels top bottom cap L).Shaped
      (m * (g ^ 3 * L))

Uses 8 · Used by 1

Statement usesFactored tensor network with shape parameter · Integer-valued complete-graph tensor instance · Row network of a grid tensor · Ordered pairs representing unordered pairs

Proof usesInteger-valued factored tensor network · Label set of an unordered vertex pair · Capacity bound between grid rows · Membership in the ordered pairs

Used bySize bound for the grid row network

TheoremSize bound for the grid row network#✓fully proved

Under uniform raw tensor and factor bounds, the grid row network has exact source exponents m g³ L for shape and g B + g² b for integer magnitudes.

TensorNetwork.gridRowNetwork_sized · 20 lines

theorem gridRowNetwork_sized [Fintype ρ] [LinearOrder ρ]
    [Fintype γ] [LinearOrder γ] [DecidableEq A]
    {g L m B b : ℕ} (hm : 1 ≤ m) (hρ : Fintype.card ρ = g)
    (hγ : Fintype.card γ = g)
    (labels diagonalLabels : Finset A) (hlabels : labels.card ≤ 2 ^ L)
    (hdiagonal : diagonalLabels.card ≤ 2 ^ L) (R : Instance (ρ × γ) A)
    (hR : ∀ w h, |R w h| ≤ 2 ^ B)
    (G : ((ρ × ρ) × (γ × γ)) → A → A → A → A → ℤ)
    (cutLabels : ((ρ × ρ) × (γ × γ)) → Finset T)
    (top bottom : ((ρ × ρ) × (γ × γ)) → A → A → T → ℤ)
    (cap : ((ρ × ρ) × (γ × γ)) → ℕ)
    (hfactor : ∀ ω x y u v,
      G ω x y u v = ∑ θ ∈ cutLabels ω, top ω x y θ * bottom ω u v θ)
    (hcut : ∀ ω, (cutLabels ω).card ≤ 2 ^ cap ω)
    (hcap : ∀ ω, cap ω ≤ 2 * m * L)
    (htop : ∀ ω x y θ, |top ω x y θ| ≤ 2 ^ b)
    (hbottom : ∀ ω u v θ, |bottom ω u v θ| ≤ 2 ^ b)
    (hG : ∀ ω x y u v, |G ω x y u v| ≤ 2 ^ b) :
    (gridRowNetwork labels diagonalLabels R cutLabels top bottom cap L).Sized
      (m * (g ^ 3 * L)) (g * B + g ^ 2 * b)

Uses 10

Statement usesShaped tensor network with bounded entries · Integer-valued complete-graph tensor instance · Row network of a grid tensor · Ordered pairs representing unordered pairs

Proof usesInteger-valued factored tensor network · Factored tensor network with shape parameter · Interaction of two states in a factored network · Interaction is symmetric under swapping endpoints · Interaction between rows of the grid row network · Shape bound for the grid row network

TheoremTotal capacity of the grid row network#✓fully proved

The directed total capacity consists of all vertical row edges plus twice the active rectangle capacity; diagonal row capacities are excluded.

theorem gridRowNetwork_totalCapacity [Fintype ρ] [LinearOrder ρ]
    [Fintype γ] [LinearOrder γ] [DecidableEq A]
    {g L : ℕ} (hρ : Fintype.card ρ = g) (hγ : Fintype.card γ = g)
    (labels diagonalLabels : Finset A) (R : Instance (ρ × γ) A)
    (cutLabels : ((ρ × ρ) × (γ × γ)) → Finset T)
    (top bottom : ((ρ × ρ) × (γ × γ)) → A → A → T → ℤ)
    (cap : ((ρ × ρ) × (γ × γ)) → ℕ) :
    (gridRowNetwork labels diagonalLabels R cutLabels top bottom cap L).totalCapacity =
      g ^ 2 * (g - 1) * L +
        2 * ∑ ω ∈ gridRectangles ρ γ, cap ω

Uses 7

Statement usesDirected total capacity of a factored network · Integer-valued complete-graph tensor instance · Ordered rectangles of a finite grid · Row network of a grid tensor · Ordered pairs representing unordered pairs

Proof usesInteger-valued factored tensor network · Membership in the ordered pairs

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.