Tensor-instance alphabet padding

DefinitionAlphabet padding of a tensor instance#✓fully proved

Rename the active edge alphabet of an instance through dec, returning zero when any off-diagonal target label is outside D. The diagonal coordinate is replaced by sourceDefault.

def pad [Fintype J] [DecidableEq J] [DecidableEq A'] (R : Instance J A)
    (sourceDefault : A) (D : Finset A') (dec : A' → A) : Instance J A' :=
  fun v θ =>
    if ∀ w, w ≠ v → θ w ∈ D then
      R v (fun w => if w = v then sourceDefault else dec (θ w))
    else 0

Uses 1 · Used by 3

Statement usesInteger-valued complete-graph tensor instance

Used byFactoring and unfactoring a tensor instance gives its padding · Factoring round trip with the full source alphabet · Bijective alphabet padding preserves instance value

TheoremFactoring and unfactoring a tensor instance gives its padding#✓fully proved

Factoring an instance and converting it back through constant edge names gives its padded version. The decoder must send every admitted target name into the explicit source alphabet.

theorem toInstance_toFactored_eq_pad [Fintype J] [LinearOrder J]
    [DecidableEq A] [DecidableEq A'] (R : Instance J A) (sourceLabels : Finset A)
    (sourceDefault : A) (D : Finset A') (dec : A' → A)
    (hdec : Set.MapsTo dec D sourceLabels) :
    (R.toFactored sourceLabels sourceDefault).toInstance (fun _ _ => D) (fun _ _ => dec) =
      R.pad sourceDefault D dec

Uses 7 · Used by 2

Statement usesComplete-graph instance of a factored network · Integer-valued complete-graph tensor instance · Alphabet padding of a tensor instance · Half-edge factored presentation of a tensor instance

Proof usesMembership in default-padded finite tuples · Finite tuples with prescribed default values · Integer-valued factored tensor network

Used byFactoring round trip with the full source alphabet · Bijective alphabet padding preserves instance value

TheoremFactoring round trip with the full source alphabet#✓fully proved

The source conversion theorem with the full finite source alphabet.

theorem toInstance_toFactored_univ_eq_pad [Fintype J] [LinearOrder J] [Fintype A]
    [DecidableEq A] [DecidableEq A'] (R : Instance J A) (sourceDefault : A)
    (D : Finset A') (dec : A' → A) :
    (R.toFactored univ sourceDefault).toInstance (fun _ _ => D) (fun _ _ => dec) =
      R.pad sourceDefault D dec

Uses 5

Statement usesComplete-graph instance of a factored network · Integer-valued complete-graph tensor instance · Alphabet padding of a tensor instance · Half-edge factored presentation of a tensor instance

Proof usesFactoring and unfactoring a tensor instance gives its padding

TheoremBijective alphabet padding preserves instance value#✓fully proved

Padding through a bijective renaming of an explicit source alphabet preserves instance value.

theorem value_pad [Fintype J] [LinearOrder J] [DecidableEq A] [DecidableEq A']
    (R : Instance J A) (sourceLabels : Finset A) (sourceDefault : A)
    (targetLabels : Finset A') (targetDefault : A') (D : Finset A') (dec : A' → A)
    (hD : D ⊆ targetLabels) (hdec : Set.BijOn dec D sourceLabels) :
    (R.pad sourceDefault D dec).value targetLabels targetDefault =
      R.value sourceLabels sourceDefault

Uses 10

Statement usesInteger-valued complete-graph tensor instance · Alphabet padding of a tensor instance · Value of a complete-graph tensor instance

Proof usesInteger-valued factored tensor network · Complete-graph instance of a factored network · Value of a factored tensor network · Converting a factored network to an instance preserves value · Half-edge factored presentation of a tensor instance · Factoring and unfactoring a tensor instance gives its padding · Half-edge presentation preserves instance value

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.