Partial assignments

A partial assignment of the coordinates ι fixes some of them and leaves the others free: a map ρ : ι → Option Bool with ρ i = some b when coordinate i is fixed to b. In circuit complexity it is called a restriction, Jukna's ρ : ι → {0, 1, *} Jukna, Section 1.6, [Has86]. Restricting a function f on ι → Bool by ρ gives f ∘ ρ.fill, Jukna's f↾ρ, where ρ.fill x takes the fixed coordinates from ρ and the free ones from x.

The subfunctions of f on a set Y of coordinates are its restrictions by the partial assignments that fix exactly the coordinates outside Y (subfunctions, mem_subfunctions_iff); counting them is the method of Nechiporuk.

Main definitions

• Cslib.BitString.PartialAssignment: partial assignments of the coordinates ι, and Cslib.BitString.PartialAssignment.empty the one fixing nothing.
• Cslib.BitString.PartialAssignment.fill: complete an input by the fixed coordinates.
• Cslib.BitString.PartialAssignment.Agrees: an input agrees with a partial assignment.
• Cslib.BitString.PartialAssignment.free, Cslib.BitString.PartialAssignment.support: the free and the fixed coordinates.
• Cslib.BitString.PartialAssignment.assign, Cslib.BitString.PartialAssignment.unassign: fix the coordinates of a set to the values of a word, and free the coordinates of a set.
• Cslib.BitString.PartialAssignment.outside: the partial assignment fixing the coordinates outside a set to the values of a word.
• Cslib.BitString.PartialAssignment.Extends: the information order on partial assignments.
• Cslib.BitString.subfunctions: the subfunctions of a function on a set of coordinates.

Main results

• Cslib.BitString.PartialAssignment.agrees_iff_fill_eq: an input agrees with a partial assignment when filling it changes nothing.
• Cslib.BitString.PartialAssignment.extends_iff_ofOption_le: extension is the pointwise order of Part Bool.
• Cslib.BitString.PartialAssignment.Extends.update_some, Cslib.BitString.PartialAssignment.Extends.update_none: updating a free coordinate of ρ₀ preserves extending ρ₀.
• Cslib.BitString.mem_subfunctions_iff: subfunctions are restrictions.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers
• J. Håstad, Almost optimal lower bounds for small depth circuits

@[reducible, inline]

abbrev Cslib.BitString.PartialAssignment (ι : Type u_1) : Type u_1

A partial assignment (a restriction, in circuit complexity) of the coordinates ι: some b fixes a coordinate to b, and none leaves it free.

Being an abbreviation of ι → Option Bool, a partial assignment inherits the pointwise order of the order of core on Option Bool, in which none < some false < some true. That order is not the information order: ρ ≤ ρ' does not say that ρ' extends ρ. The information order is PartialAssignment.Extends, the pointwise order on Part Bool (PartialAssignment.extends_iff_ofOption_le).

def Cslib.BitString.PartialAssignment.empty {ι : Type u_1} : PartialAssignment ι

The partial assignment fixing nothing.

@[simp]

theorem Cslib.BitString.PartialAssignment.empty_apply {ι : Type u_1} (i : ι) : empty i = none

The partial assignment fixing nothing leaves every coordinate free.

def Cslib.BitString.PartialAssignment.fill {ι : Type u_1} (ρ : PartialAssignment ι) (x : ι → Bool) : ι → Bool

Complete x by the coordinates fixed by ρ.

@[simp]

theorem Cslib.BitString.PartialAssignment.fill_of_eq_none {ι : Type u_1} {ρ : PartialAssignment ι} {i : ι} (hi : ρ i = none) (x : ι → Bool) : ρ.fill x i = x i

At a coordinate left free by ρ, ρ.fill x takes the bit of x.

@[simp]

theorem Cslib.BitString.PartialAssignment.fill_of_eq_some {ι : Type u_1} {ρ : PartialAssignment ι} {i : ι} {b : Bool} (hi : ρ i = some b) (x : ι → Bool) : ρ.fill x i = b

At a coordinate that ρ fixes to b, ρ.fill x is b.

@[simp]

theorem Cslib.BitString.PartialAssignment.fill_empty {ι : Type u_1} (x : ι → Bool) : empty.fill x = x

Fixing nothing changes nothing.

@[simp]

theorem Cslib.BitString.PartialAssignment.fill_none {ι : Type u_1} (x : ι → Bool) : fill (fun (x : ι) => none) x = x

fill_empty, for the partial assignment fixing nothing written as a function.

Agreement

def Cslib.BitString.PartialAssignment.Agrees {ι : Type u_1} (ρ : PartialAssignment ι) (x : ι → Bool) : Prop

The input x agrees with ρ: it takes the value fixed by ρ at every fixed coordinate.

@[instance_reducible]

instance Cslib.BitString.PartialAssignment.instDecidableAgreesOfFintype {ι : Type u_1} [Fintype ι] (ρ : PartialAssignment ι) (x : ι → Bool) : Decidable (ρ.Agrees x)

Agreement with a partial assignment of finitely many coordinates is decidable.

theorem Cslib.BitString.PartialAssignment.agrees_iff_fill_eq {ι : Type u_1} {ρ : PartialAssignment ι} {x : ι → Bool} : ρ.Agrees x ↔ ρ.fill x = x

An input agrees with ρ exactly when filling it from ρ does not change it.

theorem Cslib.BitString.PartialAssignment.agrees_fill {ι : Type u_1} (ρ : PartialAssignment ι) (x : ι → Bool) : ρ.Agrees (ρ.fill x)

A filled input agrees with the partial assignment it was filled from.

@[simp]

theorem Cslib.BitString.PartialAssignment.agrees_empty {ι : Type u_1} (x : ι → Bool) : empty.Agrees x

Every input agrees with the partial assignment fixing nothing.

theorem Cslib.BitString.PartialAssignment.fill_eq_fill_of_forall_ne {ι : Type u_1} {ρ : PartialAssignment ι} {i : ι} {x y : ι → Bool} (h : ∀ (j : ι), j ≠ i → x j = y j) (j : ι) (hj : j ≠ i) : ρ.fill x j = ρ.fill y j

Filling preserves agreement away from coordinate i.

theorem Cslib.BitString.PartialAssignment.dependsOn_comp_fill {ι : Type u_1} {i : ι} {β : Type u_2} {f : (ι → Bool) → β} (hf : DependsOn f {i}ᶜ) (ρ : PartialAssignment ι) : DependsOn (f ∘ ρ.fill) {i}ᶜ

A function that ignores coordinate i still ignores it once coordinates are hardwired.

Fixing and freeing coordinates

@[simp]

theorem Cslib.BitString.PartialAssignment.fill_update {ι : Type u_1} [DecidableEq ι] (ρ : PartialAssignment ι) (i : ι) (b : Bool) (x : ι → Bool) : fill (Function.update ρ i (some b)) x = Function.update (ρ.fill x) i b

Filling after fixing coordinate i to b updates the filled input at i.

theorem Cslib.BitString.PartialAssignment.fill_update_empty {ι : Type u_1} [DecidableEq ι] (i : ι) (b : Bool) (x : ι → Bool) : fill (Function.update empty i (some b)) x = Function.update x i b

Fixing a single coordinate i to b in the empty partial assignment updates the input at i.

theorem Cslib.BitString.PartialAssignment.fill_fill_update {ι : Type u_1} {ρ : PartialAssignment ι} {i : ι} [DecidableEq ι] (hi : ρ i = none) (b : Bool) (x : ι → Bool) : ρ.fill (fill (Function.update ρ i (some b)) x) = fill (Function.update ρ i (some b)) x

Filling after fixing one more free coordinate is filling twice.

theorem Cslib.BitString.PartialAssignment.fill_update_of_ne_none {ι : Type u_1} {ρ : PartialAssignment ι} {i : ι} [DecidableEq ι] (hi : ρ i ≠ none) (x : ι → Bool) (c : Bool) : ρ.fill (Function.update x i c) = ρ.fill x

Changing a fixed coordinate does not change the filled input.

theorem Cslib.BitString.PartialAssignment.fill_update_of_eq_none {ι : Type u_1} {ρ : PartialAssignment ι} {i : ι} [DecidableEq ι] (hi : ρ i = none) (x : ι → Bool) (c : Bool) : ρ.fill (Function.update x i c) = Function.update (ρ.fill x) i c

Changing a free coordinate changes the filled input there.

def Cslib.BitString.PartialAssignment.assign {ι : Type u_1} [DecidableEq ι] (ρ : PartialAssignment ι) (S : Finset ι) (a : ι → Bool) : PartialAssignment ι

Fix the coordinates of S to their values in a.

@[simp]

theorem Cslib.BitString.PartialAssignment.assign_of_mem {ι : Type u_1} {ρ : PartialAssignment ι} {i : ι} [DecidableEq ι] {S : Finset ι} (hi : i ∈ S) (a : ι → Bool) : ρ.assign S a i = some (a i)

ρ.assign S a fixes each coordinate of S to its value in a.

@[simp]

theorem Cslib.BitString.PartialAssignment.assign_of_notMem {ι : Type u_1} {ρ : PartialAssignment ι} {i : ι} [DecidableEq ι] {S : Finset ι} (hi : i ∉ S) (a : ι → Bool) : ρ.assign S a i = ρ i

ρ.assign S a agrees with ρ outside S.

@[simp]

theorem Cslib.BitString.PartialAssignment.assign_assign {ι : Type u_1} [DecidableEq ι] (ρ : PartialAssignment ι) (S : Finset ι) (a b : ι → Bool) : (ρ.assign S a).assign S b = ρ.assign S b

Fixing the coordinates of S twice keeps the values of the second assignment.

theorem Cslib.BitString.PartialAssignment.assign_eq_self {ι : Type u_1} {ρ : PartialAssignment ι} [DecidableEq ι] {S : Finset ι} {a : ι → Bool} (h : ∀ i ∈ S, ρ i = some (a i)) : ρ.assign S a = ρ

Fixing coordinates to the values they already have changes nothing.

def Cslib.BitString.PartialAssignment.unassign {ι : Type u_1} [DecidableEq ι] (ρ : PartialAssignment ι) (S : Finset ι) : PartialAssignment ι

Free the coordinates of S.

@[simp]

theorem Cslib.BitString.PartialAssignment.unassign_of_mem {ι : Type u_1} {ρ : PartialAssignment ι} {i : ι} [DecidableEq ι] {S : Finset ι} (hi : i ∈ S) : ρ.unassign S i = none

ρ.unassign S leaves the coordinates of S free.

@[simp]

theorem Cslib.BitString.PartialAssignment.unassign_of_notMem {ι : Type u_1} {ρ : PartialAssignment ι} {i : ι} [DecidableEq ι] {S : Finset ι} (hi : i ∉ S) : ρ.unassign S i = ρ i

ρ.unassign S agrees with ρ outside S.

@[simp]

theorem Cslib.BitString.PartialAssignment.unassign_empty {ι : Type u_1} [DecidableEq ι] (ρ : PartialAssignment ι) : ρ.unassign ∅ = ρ

Freeing no coordinates changes nothing.

def Cslib.BitString.PartialAssignment.outside {ι : Type u_1} [DecidableEq ι] (Y : Finset ι) (z : ι → Bool) : PartialAssignment ι

The partial assignment fixing the coordinates outside Y to their values in z.

@[simp]

theorem Cslib.BitString.PartialAssignment.fill_outside {ι : Type u_1} [DecidableEq ι] (Y : Finset ι) (z x : ι → Bool) : (outside Y z).fill x = Y.piecewise x z

Filling x from outside Y z takes the coordinates in Y from x and the others from z.

Free coordinates

def Cslib.BitString.PartialAssignment.free {ι : Type u_1} [Fintype ι] (ρ : PartialAssignment ι) : Finset ι

The coordinates left free by ρ.

@[simp]

theorem Cslib.BitString.PartialAssignment.mem_free {ι : Type u_1} {ρ : PartialAssignment ι} {i : ι} [Fintype ι] : i ∈ ρ.free ↔ ρ i = none

A coordinate is free in ρ exactly when ρ maps it to none.

@[simp]

theorem Cslib.BitString.PartialAssignment.free_empty {ι : Type u_1} [Fintype ι] : empty.free = Finset.univ

The partial assignment fixing nothing leaves every coordinate free.

@[simp]

theorem Cslib.BitString.PartialAssignment.free_none {ι : Type u_1} [Fintype ι] : (free fun (x : ι) => none) = Finset.univ

free_empty, for the partial assignment fixing nothing written as a function.

def Cslib.BitString.PartialAssignment.support {ι : Type u_1} [Fintype ι] (ρ : PartialAssignment ι) : Finset ι

The coordinates fixed by ρ, the complement of its free coordinates (compl_free).

@[simp]

theorem Cslib.BitString.PartialAssignment.mem_support {ι : Type u_1} {ρ : PartialAssignment ι} {i : ι} [Fintype ι] : i ∈ ρ.support ↔ (ρ i).isSome = true

A coordinate is in the support of ρ exactly when ρ fixes it.

@[simp]

theorem Cslib.BitString.PartialAssignment.support_empty {ι : Type u_1} [Fintype ι] : empty.support = ∅

The partial assignment fixing nothing has empty support.

theorem Cslib.BitString.PartialAssignment.dependsOn_comp_fill_free {ι : Type u_1} [Fintype ι] {β : Type u_2} (f : (ι → Bool) → β) (ρ : PartialAssignment ι) : DependsOn (f ∘ ρ.fill) ↑ρ.free

A restricted function f ∘ ρ.fill depends only on the free coordinates of ρ.

theorem Cslib.BitString.PartialAssignment.compl_free {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : PartialAssignment ι) : ρ.freeᶜ = ρ.support

The free coordinates are those outside the support.

theorem Cslib.BitString.PartialAssignment.compl_support {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : PartialAssignment ι) : ρ.supportᶜ = ρ.free

The coordinates outside the support are the free coordinates.

@[simp]

theorem Cslib.BitString.PartialAssignment.free_update {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : PartialAssignment ι) (i : ι) (b : Bool) : free (Function.update ρ i (some b)) = ρ.free.erase i

Fixing coordinate i removes it from the free coordinates.

@[simp]

theorem Cslib.BitString.PartialAssignment.free_update_none {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : PartialAssignment ι) (i : ι) : free (Function.update ρ i none) = insert i ρ.free

Freeing coordinate i adds it to the free coordinates.

@[simp]

theorem Cslib.BitString.PartialAssignment.free_assign {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : PartialAssignment ι) (S : Finset ι) (a : ι → Bool) : (ρ.assign S a).free = ρ.free \ S

Fixing the coordinates of S removes them from the free coordinates.

theorem Cslib.BitString.PartialAssignment.fill_assign {ι : Type u_1} {ρ : PartialAssignment ι} [Fintype ι] [DecidableEq ι] {S : Finset ι} (hS : S ⊆ ρ.free) {a x : ι → Bool} (h : ∀ i ∈ S, a i = x i) : (ρ.assign S a).fill x = ρ.fill x

Fixing free coordinates to the values of x does not change the input filled from x.

theorem Cslib.BitString.PartialAssignment.unassign_union_assign {ι : Type u_1} {ρ : PartialAssignment ι} [Fintype ι] [DecidableEq ι] {S Q : Finset ι} (hS : S ⊆ ρ.free) (a : ι → Bool) : (ρ.assign S a).unassign (Q ∪ S) = ρ.unassign Q

Fixing free coordinates and freeing them again gives back the partial assignment.

@[simp]

theorem Cslib.BitString.PartialAssignment.free_outside {ι : Type u_1} [Fintype ι] [DecidableEq ι] (Y : Finset ι) (z : ι → Bool) : (outside Y z).free = Y

The free coordinates of outside Y z are exactly those of Y.

theorem Cslib.BitString.PartialAssignment.comp_fill_update_empty_of_mem_free {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : Type u_2} {ρ : PartialAssignment ι} {i : ι} (hi : i ∈ ρ.free) (b : Bool) (f : (ι → Bool) → β) : (f ∘ ρ.fill) ∘ fill (Function.update empty i (some b)) = f ∘ fill (Function.update ρ i (some b))

Restricting f ∘ ρ.fill by fixing a free coordinate i of ρ to b is restricting f by update ρ i (some b).

Extensions

def Cslib.BitString.PartialAssignment.Extends {ι : Type u_1} (ρ' ρ : PartialAssignment ι) : Prop

ρ' extends ρ: it fixes every coordinate that ρ fixes, to the same value. This is the information order on partial assignments; the order on Option in core is a different one.

@[instance_reducible]

instance Cslib.BitString.PartialAssignment.instDecidableExtendsOfFintype {ι : Type u_1} [Fintype ι] (ρ' ρ : PartialAssignment ι) : Decidable (ρ'.Extends ρ)

Extension of partial assignments of finitely many coordinates is decidable.

theorem Cslib.BitString.PartialAssignment.Extends.refl {ι : Type u_1} (ρ : PartialAssignment ι) : ρ.Extends ρ

Every partial assignment extends itself.

theorem Cslib.BitString.PartialAssignment.Extends.trans {ι : Type u_1} {ρ ρ' ρ'' : PartialAssignment ι} (h₁ : ρ''.Extends ρ') (h₂ : ρ'.Extends ρ) : ρ''.Extends ρ

Extension is transitive: an extension of an extension of ρ extends ρ.

theorem Cslib.BitString.PartialAssignment.extends_iff_ofOption_le {ι : Type u_1} {ρ ρ' : PartialAssignment ι} : ρ'.Extends ρ ↔ (fun (i : ι) => ↑(ρ i)) ≤ fun (i : ι) => ↑(ρ' i)

The information order: ρ' extends ρ exactly when it is above ρ pointwise in the order of Part Bool, where an undefined value is below every value and distinct values are incomparable.

@[simp]

theorem Cslib.BitString.PartialAssignment.extends_empty {ι : Type u_1} (ρ : PartialAssignment ι) : ρ.Extends empty

Every partial assignment extends the one fixing nothing.

theorem Cslib.BitString.PartialAssignment.Extends.agrees {ι : Type u_1} {ρ ρ' : PartialAssignment ι} (h : ρ'.Extends ρ) {x : ι → Bool} (hx : ρ'.Agrees x) : ρ.Agrees x

An input agreeing with ρ' agrees with every partial assignment that ρ' extends.

theorem Cslib.BitString.PartialAssignment.fill_fill_of_extends {ι : Type u_1} {ρ ρ' : PartialAssignment ι} (h : ρ'.Extends ρ) (x : ι → Bool) : ρ.fill (ρ'.fill x) = ρ'.fill x

Filling from an extension of ρ is not changed by filling from ρ.

theorem Cslib.BitString.PartialAssignment.Extends.free_subset {ι : Type u_1} [Fintype ι] {ρ ρ' : PartialAssignment ι} (h : ρ'.Extends ρ) : ρ'.free ⊆ ρ.free

A free coordinate of an extension is free in the partial assignment it extends.

theorem Cslib.BitString.PartialAssignment.extends_assign {ι : Type u_1} {ρ : PartialAssignment ι} [Fintype ι] [DecidableEq ι] {S : Finset ι} (hS : S ⊆ ρ.free) (a : ι → Bool) : (ρ.assign S a).Extends ρ

Fixing free coordinates extends a partial assignment.

theorem Cslib.BitString.PartialAssignment.Extends.update_some {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ₀ ρ : PartialAssignment ι} (h : ρ.Extends ρ₀) {i : ι} (hi : i ∈ ρ₀.free) (b : Bool) : Extends (Function.update ρ i (some b)) ρ₀

Fixing a coordinate of ρ that is free in ρ₀ preserves extending ρ₀.

theorem Cslib.BitString.PartialAssignment.Extends.update_none {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ₀ ρ : PartialAssignment ι} (h : ρ.Extends ρ₀) {i : ι} (hi : i ∈ ρ₀.free) : Extends (Function.update ρ i none) ρ₀

Freeing a coordinate of ρ that is free in ρ₀ preserves extending ρ₀.

Subfunctions

def Cslib.BitString.subfunctions {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (Y : Finset ι) : Finset ((ι → Bool) → Bool)

The subfunctions of f on the coordinates Y: for each assignment z of the other coordinates, the function that reads the coordinates in Y from its input and the others from z.

@[simp]

theorem Cslib.BitString.mem_subfunctions {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f g : (ι → Bool) → Bool} {Y : Finset ι} : g ∈ subfunctions f Y ↔ ∃ (z : ι → Bool), (fun (x : ι → Bool) => f (Y.piecewise x z)) = g

g is a subfunction of f on Y exactly when, for some assignment z, g reads the coordinates in Y from its input and the others from z before applying f.

theorem Cslib.BitString.mem_subfunctions_iff {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f g : (ι → Bool) → Bool} {Y : Finset ι} : g ∈ subfunctions f Y ↔ ∃ (z : ι → Bool), f ∘ (PartialAssignment.outside Y z).fill = g

The subfunctions on Y are the restrictions by the partial assignments fixing exactly the coordinates outside Y.