Functions with prescribed values

DefinitionFinite tuples with prescribed default values#✓fully proved

Finite tuples constrained on P and equal to a prescribed default elsewhere.

def piFinsetOn (P : ι → Prop) [DecidablePred P] (T : ι → Finset σ) (d : σ) :
    Finset (ι → σ) :=
  piFinset fun i => if P i then T i else {d}

Used by 17

Used byNumber of default-padded finite tuples · Unique default completion of active coordinates · Membership in default-padded finite tuples · Products of factorized functions over label tuples · Product of sums over default-padded tuples · Shape bound for contracted tensor networks · Merging vertices of a factored tensor network · Interaction of merged classes in increasing order · Merging vertices preserves network value · Half-edge factored presentation of a tensor instance · Instance value as a sum over half-edge vectors · Half-edge presentation preserves instance value · Converting a factored network to an instance preserves value · Complete-graph tensor value as a crossing grid evaluation · Edge labelings of the complete graph · Characterization of complete-graph edge labelings · Factoring and unfactoring a tensor instance gives its padding

TheoremMembership in default-padded finite tuples#✓fully proved

Membership gives the allowed values on the active indices and the default off them.

@[simp] theorem mem_piFinsetOn (P : ι → Prop) [DecidablePred P]
    (T : ι → Finset σ) (d : σ) (t : ι → σ) :
    t ∈ piFinsetOn P T d ↔ ∀ i, (P i → t i ∈ T i) ∧ (¬P i → t i = d)

Uses 1 · Used by 7

Statement usesFinite tuples with prescribed default values

Used byUnique default completion of active coordinates · Merging vertices preserves network value · Instance value as a sum over half-edge vectors · Half-edge presentation preserves instance value · Complete-graph tensor value as a crossing grid evaluation · Characterization of complete-graph edge labelings · Factoring and unfactoring a tensor instance gives its padding

TheoremNumber of default-padded finite tuples#✓fully proved

Inactive coordinates contribute one choice, so only active coordinates enter the product.

theorem card_piFinsetOn (P : ι → Prop) [DecidablePred P]
    (T : ι → Finset σ) (d : σ) :
    (piFinsetOn P T d).card = ∏ i with P i, (T i).card

Uses 1 · Used by 2

Statement usesFinite tuples with prescribed default values

Used byShape bound for contracted tensor networks · Number of states of a merged vertex

TheoremProduct of sums over default-padded tuples#✓fully proved

Distribute a product of finite sums over the default-padded tuples of choices.

theorem sum_piFinsetOn_prod {R : Type*} [CommSemiring R]
    (P : ι → Prop) [DecidablePred P] (T : ι → Finset σ) (d : σ) (H : ι → σ → R) :
    ∑ t ∈ piFinsetOn P T d, ∏ i with P i, H i (t i) =
      ∏ i with P i, ∑ x ∈ T i, H i x

Uses 1 · Used by 2

Statement usesFinite tuples with prescribed default values

Used byProducts of factorized functions over label tuples · Converting a factored network to an instance preserves value

TheoremProducts of factorized functions over label tuples#✓fully proved

Products of factorized functions factor through the tuples of their labels.

theorem prod_sum_eq_sum_piFinsetOn_mul {R : Type*} [CommSemiring R]
    (P : ι → Prop) [DecidablePred P] (T : ι → Finset σ) (d : σ)
    (f g : ι → σ → R) :
    ∏ i with P i, ∑ x ∈ T i, f i x * g i x =
      ∑ t ∈ piFinsetOn P T d, (∏ i with P i, f i (t i)) * ∏ i with P i, g i (t i)

Uses 2 · Used by 1

Statement usesFinite tuples with prescribed default values

Proof usesProduct of sums over default-padded tuples

Used byInteraction of merged classes in increasing order

TheoremUnique default completion of active coordinates#✓fully proved

Prescribed active coordinates have exactly one completion with the chosen default.

theorem existsUnique_piFinsetOn (P : ι → Prop) [DecidablePred P]
    (T : ι → Finset σ) (d : σ) (t : ι → σ) (ht : ∀ i, P i → t i ∈ T i) :
    ∃! b : ι → σ, b ∈ piFinsetOn P T d ∧ ∀ i, P i → b i = t i

Uses 2

Statement usesFinite tuples with prescribed default values

Proof usesMembership in default-padded finite tuples

TheoremNumber of dependent functions with prescribed values#✓fully proved

The number of dependent functions in piFinset s with prescribed values on S is the product of the numbers of choices outside S.

theorem card_filter_piFinset_eqOn_of_mem (s : (i : ι) → Finset (α i)) (S : Finset ι)
    (f : (i : {i // i ∈ S}) → α i.1) (hf : ∀ i, f i ∈ s i.1) :
    {g ∈ piFinset s | ∀ i, g i.1 = f i}.card =
      ∏ i ∈ Finset.univ \ S, (s i).card

Used by 1

Used byNumber of functions agreeing with a given one on a set

TheoremNumber of functions agreeing with a given one on a set#✓fully proved

The number of functions agreeing with f on S is the number of unrestricted choices on the remaining coordinates.

theorem card_filter_univ_eqOn (S : Finset ι) (f : {i // i ∈ S} → κ) :
    (Finset.univ.filter fun g : ι → κ => ∀ i, g i.1 = f i).card =
      Fintype.card κ ^ (Fintype.card ι - S.card)

Uses 1 · Used by 2

Proof usesNumber of dependent functions with prescribed values

Used byDivision-free count of functions with prescribed values · Counting satisfying assignments over a larger variable range

TheoremDivision-free count of functions with prescribed values#✓fully proved

Division-free count of finite functions with prescribed values on a set of coordinates.

theorem card_filter_univ_eqOn_mul_pow_card (S : Finset ι) (f : {i // i ∈ S} → κ) :
    (Finset.univ.filter fun g : ι → κ => ∀ i, g i.1 = f i).card *
      Fintype.card κ ^ S.card =
      Fintype.card κ ^ Fintype.card ι

Uses 1 · Used by 1

Proof usesNumber of functions agreeing with a given one on a set

Used byBalanced coloring of a weighted symmetric matrix

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.