Flipping bits

BitString.flipOn T x flips the bits of the Boolean vector x at the positions in T. Flipping one bit is Function.update x i (!x i) (BitString.flipOn_singleton), and flipping twice at the same positions changes nothing (BitString.flipOn_flipOn). Flips are the moves of sensitivity and block sensitivity, and they span the subcubes of the Boolean cube.

Sensitivity and certificate measures use CSLib's Computability.QueryComplexity.Measures.

An input x of a Boolean function g is isolated when flipping any one of its bits changes the value of g (BitString.isolatedInputs). A formula in disjunctive normal form needs a term for each isolated true input, and parity has only isolated inputs.

Main definitions

• Cslib.BitString.flipOn: flip the bits at a set of positions.
• Cslib.BitString.isolatedInputs: the isolated inputs of a Boolean function with a given value.

Main results

• Cslib.BitString.flipOn_apply: coordinatewise evaluation of flipOn.
• Cslib.BitString.flipOn_congr_decidableEq: flipOn is independent of the DecidableEq instance.
• Cslib.BitString.flipOn_singleton, Cslib.BitString.flipOn_singleton_self, Cslib.BitString.flipOn_singleton_of_ne: flipping one bit.
• Cslib.BitString.flipOn_flipOn, Cslib.BitString.flipOn_involutive: flipping is an involution.
• Cslib.BitString.flipOn_insert: flipping insert i T for i ∉ T.
• Cslib.BitString.flipOn_false: flipping the all-false vector gives the indicator of the set.
• Cslib.BitString.flipOn_filter_ne: flipping the positions where two vectors differ turns one into the other.
• Cslib.BitString.flipOn_prod_same, Cslib.BitString.flipOn_prod_of_ne: row projections of a single-coordinate flip on a product index type.
• Cslib.BitString.flipOn_reindex, Cslib.BitString.flipOn_reindex_singleton: reindexing a flip along an equivalence.
• Cslib.BitString.eq_of_singleton_invariant: a function invariant under all single-coordinate flips is constant.

References

• N. Nisan, CREW PRAMs and decision trees
• Adapted in part from OpenAI's formalization [OAI26b] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Combinatorics/Sensitivity/Basic.lean), via the complexitylib port [Sch26e] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

def Cslib.BitString.flipOn {ι : Type u_1} [DecidableEq ι] (T : Finset ι) (x : ι → Bool) : ι → Bool

Flip the bits of x at the positions in T.

theorem Cslib.BitString.flipOn_apply {ι : Type u_1} [DecidableEq ι] (T : Finset ι) (x : ι → Bool) (i : ι) : flipOn T x i = if i ∈ T then !x i else x i

Coordinatewise, flipOn T x negates the bits in T and keeps the others.

theorem Cslib.BitString.flipOn_congr_decidableEq {ι : Type u_1} {inst₁ inst₂ : DecidableEq ι} (T : Finset ι) (x : ι → Bool) : flipOn T x = flipOn T x

flipOn is independent of the DecidableEq instance.

theorem Cslib.BitString.flipOn_eq_piecewise {ι : Type u_1} [DecidableEq ι] (T : Finset ι) (x : ι → Bool) : flipOn T x = T.piecewise (fun (i : ι) => !x i) x

flipOn T x is x with its bits at the positions in T replaced by their negations.

theorem Cslib.BitString.flipOn_apply_of_mem {ι : Type u_1} [DecidableEq ι] {T : Finset ι} {x : ι → Bool} {i : ι} (h : i ∈ T) : flipOn T x i = !x i

At a position in T, flipOn T x has the negated bit of x.

theorem Cslib.BitString.flipOn_apply_of_notMem {ι : Type u_1} [DecidableEq ι] {T : Finset ι} {x : ι → Bool} {i : ι} (h : i ∉ T) : flipOn T x i = x i

At a position outside T, flipOn T x has the bit of x.

@[simp]

theorem Cslib.BitString.flipOn_empty {ι : Type u_1} [DecidableEq ι] (x : ι → Bool) : flipOn ∅ x = x

Flipping at no positions changes nothing.

theorem Cslib.BitString.flipOn_singleton {ι : Type u_1} [DecidableEq ι] (i : ι) (x : ι → Bool) : flipOn {i} x = Function.update x i !x i

Flipping one bit.

theorem Cslib.BitString.flipOn_apply_eq_of_iff {ι : Type u_1} [DecidableEq ι] {T U : Finset ι} {x : ι → Bool} {i : ι} (h : i ∈ T ↔ i ∈ U) : flipOn T x i = flipOn U x i

Flipping at T and at U gives the same bit at any position i that lies in T exactly when it lies in U.

@[simp]

theorem Cslib.BitString.flipOn_flipOn {ι : Type u_1} [DecidableEq ι] (T : Finset ι) (x : ι → Bool) : flipOn T (flipOn T x) = x

Flipping twice at the same positions changes nothing.

theorem Cslib.BitString.flipOn_involutive {ι : Type u_1} [DecidableEq ι] (T : Finset ι) : Function.Involutive (flipOn T)

Flipping at a fixed set of positions is an involution.

@[simp]

theorem Cslib.BitString.flipOn_singleton_self {ι : Type u_1} [DecidableEq ι] (i : ι) (x : ι → Bool) : flipOn {i} x i = !x i

Flipping {i} negates bit i.

theorem Cslib.BitString.flipOn_singleton_of_ne {ι : Type u_1} [DecidableEq ι] {i j : ι} (h : j ≠ i) (x : ι → Bool) : flipOn {i} x j = x j

Flipping {i} leaves every bit j ≠ i unchanged.

theorem Cslib.BitString.flipOn_insert {ι : Type u_1} [DecidableEq ι] {x : ι → Bool} {i : ι} {T : Finset ι} (hi : i ∉ T) : flipOn (insert i T) x = flipOn {i} (flipOn T x)

For i ∉ T, flipping insert i T is flipping T and then {i}.

@[simp]

theorem Cslib.BitString.flipOn_false {ι : Type u_1} [DecidableEq ι] (T : Finset ι) (i : ι) : flipOn T (fun (x : ι) => false) i = decide (i ∈ T)

Flipping the bits of the all-false vector in T gives the indicator of T.

@[simp]

theorem Cslib.BitString.flipOn_filter_ne {ι : Type u_1} [DecidableEq ι] [Fintype ι] (x y : ι → Bool) : flipOn {i : ι | x i ≠ y i} x = y

Flipping x at the positions where x and y differ gives y.

theorem Cslib.BitString.flipOn_prod_same {ι : Type u_1} [DecidableEq ι] {κ : Type u_2} [DecidableEq (κ × ι)] (x : κ × ι → Bool) (j : κ) (i : ι) : (fun (a : ι) => flipOn {(j, i)} x (j, a)) = flipOn {i} fun (a : ι) => x (j, a)

On a product index type κ × ι, row j of flipOn {(j, i)} x is row j of x with coordinate i flipped.

theorem Cslib.BitString.flipOn_prod_of_ne {ι : Type u_1} {κ : Type u_2} [DecidableEq (κ × ι)] (x : κ × ι → Bool) {j k : κ} (i : ι) (hk : k ≠ j) : (fun (a : ι) => flipOn {(j, i)} x (k, a)) = fun (a : ι) => x (k, a)

On a product index type κ × ι, every row k ≠ j of flipOn {(j, i)} x is row k of x.

theorem Cslib.BitString.flipOn_reindex {ι : Type u_1} [DecidableEq ι] {ι' : Type u_2} (e : ι ≃ ι') (x : ι' → Bool) (B : Finset ι) : (fun (i : ι) => flipOn (Finset.map e.toEmbedding B) x (e i)) = flipOn B fun (i : ι) => x (e i)

Pulling back along e the input x with the image block B.map e.toEmbedding flipped gives the pullback fun i => x (e i) with B flipped.

theorem Cslib.BitString.flipOn_reindex_singleton {ι : Type u_1} [DecidableEq ι] {ι' : Type u_2} (e : ι ≃ ι') (x : ι' → Bool) (i : ι) : (fun (a : ι) => flipOn {e i} x (e a)) = flipOn {i} fun (a : ι) => x (e a)

Singleton case of flipOn_reindex: pulling back flipOn {e i} x along e gives the pullback of x with i flipped.

theorem Cslib.BitString.eq_of_singleton_invariant {ι : Type u_1} [DecidableEq ι] [Finite ι] (f : (ι → Bool) → Bool) (h : ∀ (x : ι → Bool) (i : ι), f (flipOn {i} x) = f x) (x y : ι → Bool) : f x = f y

Over a finite index type, a function invariant under every single-coordinate flip is constant.

def Cslib.BitString.isolatedInputs {ι : Type u_1} [DecidableEq ι] [Fintype ι] (g : (ι → Bool) → Bool) (b : Bool) : Finset (ι → Bool)

The isolated inputs of g with value b: the inputs x with g x = b at which flipping any one bit changes the value of g.

@[simp]

theorem Cslib.BitString.mem_isolatedInputs {ι : Type u_1} [DecidableEq ι] {x : ι → Bool} [Fintype ι] {g : (ι → Bool) → Bool} {b : Bool} : x ∈ isolatedInputs g b ↔ g x = b ∧ ∀ (i : ι), g (Function.update x i !x i) = !b

x is an isolated input of g with value b exactly when g x = b and flipping any one bit of x gives the value !b.

theorem Cslib.BitString.isolatedInputs_not {ι : Type u_1} [DecidableEq ι] [Fintype ι] (g : (ι → Bool) → Bool) (b : Bool) : isolatedInputs (fun (x : ι → Bool) => !g x) b = isolatedInputs g !b

The isolated inputs of the negation of g with value b are those of g with value !b.