Existential convolution on the Boolean cube

BitString.orConvolution f g x asks whether x = a + b for accepted inputs a of f and b of g. The group operation is coordinatewise exclusive or, and the aggregation is existential disjunction. Thus its accepted set is the sumset of the accepted sets of f and g. It does not count representations or take their parity.

Main definitions

• Cslib.BitString.orConvolution: existential convolution of Boolean functions.

Main results

• Cslib.BitString.orConvolution_eq_true_iff_exists_add: the sumset characterization.
• Cslib.BitString.orConvolution_comm: existential convolution is commutative.

def Cslib.BitString.orConvolution {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → Bool) (x : ι → Bool) : Bool

Existential XOR convolution: some accepted input of f, added to some accepted input of g, equals the requested output.

@[simp]

theorem Cslib.BitString.orConvolution_eq_true {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → Bool) (x : ι → Bool) : orConvolution f g x = true ↔ ∃ (a : ι → Bool), f a = true ∧ g (x + a) = true

The defining existential condition for convolution.

theorem Cslib.BitString.orConvolution_eq_true_iff_exists_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → Bool) (x : ι → Bool) : orConvolution f g x = true ↔ ∃ (a : ι → Bool) (b : ι → Bool), f a = true ∧ g b = true ∧ a + b = x

Existential convolution accepts exactly the sums of accepted inputs.

theorem Cslib.BitString.orConvolution_comm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → Bool) : orConvolution f g = orConvolution g f

Swapping the two input functions preserves existential convolution.

@[simp]

theorem Cslib.BitString.orConvolution_false_left {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → Bool) : orConvolution (fun (x : ι → Bool) => false) g = fun (x : ι → Bool) => false

An empty accepted set has empty convolution with every Boolean function.

@[simp]

theorem Cslib.BitString.orConvolution_false_right {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) : (orConvolution f fun (x : ι → Bool) => false) = fun (x : ι → Bool) => false

An empty accepted set on the right also has empty convolution.

@[simp]

theorem Cslib.BitString.orConvolution_point_left {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a : ι → Bool) (g : (ι → Bool) → Bool) : orConvolution (fun (y : ι → Bool) => decide (y = a)) g = fun (x : ι → Bool) => g (x + a)

Convolving a point indicator with g translates g.