Documentation

Complexity.Foundations.Data.BitString.Flip

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.

On Fin n, flipOn is definitionally equal to CSLib's BitString.flipBlock. 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 #

Main results #

References #

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

Flip the bits of x at the positions in T.

Instances For
    source
    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.

    source
    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.

    source
    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.

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

    Flipping at no positions changes nothing.

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

    Flipping one bit.

    source
    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.

    source
    @[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.

    source
    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.

    source
    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.

    Instances For
      source
      @[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.

      source
      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.