Documentation

Complexity.Probability.Isolation

The isolation lemma #

Give every element i of a finite universe U a weight val (w i), where the labels w i are chosen independently and uniformly from a finite set W and val is injective, and give a set the sum of the weights of its elements. The isolation lemma of Mulmuley, Vazirani and Vazirani says that a nonempty family F of subsets of U then has a unique set of minimum weight, except with probability at most |U| / |W| (Cslib.Probability.dens_minWeightSets_card_ne_one_le) Mulmuley, Vazirani and Vazirani. With weights 1, …, N for N ≥ 2 |U| the minimum is unique with probability at least 1 / 2 (Cslib.Probability.half_le_dens_minWeightSets_card_eq_one). The family is arbitrary: it need not be given explicitly, and it may be exponentially large.

The proof follows Mulmuley, Vazirani and Vazirani. If two sets have minimum weight, some element i lies in one and not in the other, so i is ambiguous: some minimum-weight set contains it and some does not. Fixing the labels of all other elements, at most one label of i makes it ambiguous, since changing the weight of i shifts the weights of exactly the sets containing i. A union bound over the elements finishes the proof. Only cancellation of addition is used, so the weights may be natural numbers.

Main definitions #

Main results #

References #

source
def Cslib.Probability.setWeight {U : Type u_1} {W : Type u_2} {G : Type u_3} [AddCommMonoid G] (val : W → G) (w : U → W) (S : Finset U) :
G

The weight of a set: the sum of the values val (w i) of the labels of its elements.

Instances For
    source
    def Cslib.Probability.minWeightSets {U : Type u_1} {W : Type u_2} {G : Type u_3} [AddCommMonoid G] [LinearOrder G] (val : W → G) (w : U → W) (F : Finset (Finset U)) :
    Finset (Finset U)

    The sets of minimum weight in the family F.

    Instances For
      source
      theorem Cslib.Probability.mem_minWeightSets {U : Type u_1} {W : Type u_2} {G : Type u_3} [AddCommMonoid G] [LinearOrder G] {val : W → G} {w : U → W} {F : Finset (Finset U)} {S : Finset U} :
      S ∈ minWeightSets val w F ↔ S ∈ F ∧ ∀ T ∈ F, setWeight val w S ≤ setWeight val w T

      S is a set of minimum weight in F exactly when S ∈ F and no set of F has smaller weight.

      source
      theorem Cslib.Probability.minWeightSets_nonempty {U : Type u_1} {W : Type u_2} {G : Type u_3} [AddCommMonoid G] [LinearOrder G] (val : W → G) (w : U → W) {F : Finset (Finset U)} (hF : F.Nonempty) :
      (minWeightSets val w F).Nonempty

      A nonempty finite family has a set of minimum weight.

      source
      def Cslib.Probability.Ambiguous {U : Type u_1} {W : Type u_2} {G : Type u_3} [AddCommMonoid G] [LinearOrder G] (val : W → G) (w : U → W) (F : Finset (Finset U)) (i : U) :
      Prop

      An element is ambiguous when some set of minimum weight contains it and some does not.

      Instances For
        source
        theorem Cslib.Probability.setWeight_eq_of_notMem {U : Type u_1} {W : Type u_2} {G : Type u_3} [AddCommMonoid G] {val : W → G} {w w' : U → W} {i : U} (hw : ∀ (j : U), j ≠ i → w j = w' j) {S : Finset U} (hi : i ∉ S) :
        setWeight val w S = setWeight val w' S

        Labels that differ only at i give the same weight to the sets without i.

        source
        theorem Cslib.Probability.setWeight_add_eq_of_mem {U : Type u_1} {W : Type u_2} {G : Type u_3} [AddCommMonoid G] {val : W → G} {w w' : U → W} {i : U} (hw : ∀ (j : U), j ≠ i → w j = w' j) {S : Finset U} (hi : i ∈ S) :
        setWeight val w S + val (w' i) = setWeight val w' S + val (w i)

        Labels that differ only at i shift the weights of the sets with i by the same amount.

        source
        theorem Cslib.Probability.val_eq_of_ambiguous {U : Type u_1} {W : Type u_2} {G : Type u_3} [AddCommMonoid G] [LinearOrder G] [IsOrderedCancelAddMonoid G] {val : W → G} {w w' : U → W} {F : Finset (Finset U)} {i : U} (hw : ∀ (j : U), j ≠ i → w j = w' j) (h : Ambiguous val w F i) (h' : Ambiguous val w' F i) :
        val (w i) = val (w' i)

        At most one label makes an element ambiguous, once the other labels are fixed: both labels give the sets containing i the minimum weight of the sets without i.

        source
        theorem Cslib.Probability.dens_minWeightSets_card_ne_one_le {U : Type u_1} {W : Type u_2} {G : Type u_3} [AddCommMonoid G] [LinearOrder G] [IsOrderedCancelAddMonoid G] [Fintype U] [DecidableEq U] [Fintype W] {val : W → G} [Nonempty W] (hval : Function.Injective val) {F : Finset (Finset U)} (hF : F.Nonempty) :
        {w : U → W | (minWeightSets val w F).card ≠ 1}.dens ≤ ↑(Fintype.card U) / ↑(Fintype.card W)

        The isolation lemma Mulmuley, Vazirani and Vazirani: for every nonempty family F of subsets of U, and labels w i drawn uniformly and independently from W with injective values val, the probability that F has more than one set of minimum weight is at most |U| / |W|.

        source
        theorem Cslib.Probability.one_sub_le_dens_minWeightSets_card_eq_one {U : Type u_1} {W : Type u_2} {G : Type u_3} [AddCommMonoid G] [LinearOrder G] [IsOrderedCancelAddMonoid G] [Fintype U] [DecidableEq U] [Fintype W] {val : W → G} [Nonempty W] (hval : Function.Injective val) {F : Finset (Finset U)} (hF : F.Nonempty) :
        1 - ↑(Fintype.card U) / ↑(Fintype.card W) ≤ {w : U → W | (minWeightSets val w F).card = 1}.dens

        The isolation lemma, for success: a nonempty family has a unique set of minimum weight with probability at least 1 - |U| / |W|.

        source
        theorem Cslib.Probability.half_le_dens_minWeightSets_card_eq_one {U : Type u_1} [Fintype U] [DecidableEq U] {N : ℕ} [NeZero N] (hN : 2 * Fintype.card U ≤ N) {F : Finset (Finset U)} (hF : F.Nonempty) :
        1 / 2 ≤ {w : U → Fin N | (minWeightSets (fun (x : Fin N) => ↑x + 1) w F).card = 1}.dens

        Mulmuley, Vazirani and Vazirani: with weights drawn uniformly and independently from 1, …, N for some N ≥ 2 |U|, a nonempty family has a unique set of minimum weight with probability at least 1 / 2.