Documentation

Complexity.Foundations.Data.BitString.PartialAssignment.Counting

Counting partial assignments and random restrictions #

Over a finite index type ι, the partial assignments extending ρ₀ with exactly ℓ free coordinates number (m choose ℓ) 2 ^ (m - ℓ) for the m free coordinates of ρ₀ (PartialAssignment.card_extensions), so (|ι| choose ℓ) 2 ^ (|ι| - ℓ) partial assignments leave exactly ℓ coordinates free (PartialAssignment.card_withFree). Drawing such a partial assignment uniformly is drawing a set of ℓ free coordinates and a word for the others (PartialAssignment.sum_card_filter_outside), and double counting relates partial assignments with different numbers of free coordinates (PartialAssignment.sum_card_filter_extensions, PartialAssignment.sum_extensions_update); these are the random restrictions of Subbotovskaya's method and Håstad's switching lemma.

Main definitions #

Main results #

References #

Counting extensions #

source
def Cslib.BitString.PartialAssignment.extensions {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ₀ : PartialAssignment ι) (ℓ : ℕ) :
Finset (PartialAssignment ι)

The extensions of ρ₀ leaving exactly ℓ coordinates free.

Instances For
    source
    @[simp]
    theorem Cslib.BitString.PartialAssignment.mem_extensions {ι : Type u_1} {ρ : PartialAssignment ι} [Fintype ι] [DecidableEq ι] {ρ₀ : PartialAssignment ι} {ℓ : ℕ} :
    ρ ∈ ρ₀.extensions ℓ ↔ ρ.Extends ρ₀ ∧ ρ.free.card = ℓ

    ρ is in ρ₀.extensions ℓ exactly when it extends ρ₀ and leaves exactly ℓ coordinates free.

    source
    theorem Cslib.BitString.PartialAssignment.card_extensions {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ₀ : PartialAssignment ι) (ℓ : ℕ) :
    (ρ₀.extensions ℓ).card = ρ₀.free.card.choose ℓ * 2 ^ (ρ₀.free.card - ℓ)

    There are (m choose ℓ) 2 ^ (m - ℓ) extensions of ρ₀ leaving ℓ of the m free coordinates of ρ₀ free.

    source
    theorem Cslib.BitString.PartialAssignment.card_filter_extensions_free_subset {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ₀ : PartialAssignment ι) (ℓ : ℕ) {U : Finset ι} (hU : U ⊆ ρ₀.free) :
    {ρ ∈ ρ₀.extensions ℓ | ρ.free ⊆ U}.card = U.card.choose ℓ * 2 ^ (ρ₀.free.card - ℓ)

    The number of extensions in ρ₀.extensions ℓ whose free coordinates lie inside U ⊆ ρ₀.free is C(|U|, ℓ) * 2 ^ (#ρ₀.free - ℓ).

    source
    @[reducible, inline]
    abbrev Cslib.BitString.PartialAssignment.withFree (ι : Type u_1) [Fintype ι] [DecidableEq ι] (ℓ : ℕ) :
    Finset (PartialAssignment ι)

    The partial assignments leaving exactly ℓ coordinates free: the extensions of the one fixing nothing.

    Instances For
      source
      theorem Cslib.BitString.PartialAssignment.mem_withFree {ι : Type u_1} {ρ : PartialAssignment ι} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} :
      ρ ∈ withFree ι ℓ ↔ ρ.free.card = ℓ

      ρ is in withFree ι ℓ exactly when it leaves exactly ℓ coordinates free.

      source
      theorem Cslib.BitString.PartialAssignment.card_withFree {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ℓ : ℕ) :
      (withFree ι ℓ).card = (Fintype.card ι).choose ℓ * 2 ^ (Fintype.card ι - ℓ)

      There are (|ι| choose ℓ) 2 ^ (|ι| - ℓ) partial assignments leaving exactly ℓ coordinates free.

      Drawing random restrictions #

      source
      theorem Cslib.BitString.PartialAssignment.sum_card_filter_outside {ι : Type u_1} [Fintype ι] [DecidableEq ι] (Q : PartialAssignment ι → Prop) [DecidablePred Q] (ℓ : ℕ) :
      ∑ J ∈ Finset.powersetCard ℓ Finset.univ, {z : ι → Bool | Q (outside J z)}.card = 2 ^ ℓ * {ρ ∈ withFree ι ℓ | Q ρ}.card

      Drawing a free set and a word: fixing the coordinates outside a set J of ℓ coordinates to a word z draws every partial assignment with ℓ free coordinates 2 ^ ℓ times.

      source
      theorem Cslib.BitString.PartialAssignment.sum_card_filter_extensions {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : PartialAssignment ι → Prop) [DecidablePred P] {ℓ ℓ' : ℕ} (hℓ : ℓ' ≤ ℓ) :
      ∑ ρ ∈ withFree ι ℓ, {ρ' ∈ ρ.extensions ℓ' | P ρ'}.card = {ρ' ∈ withFree ι ℓ' | P ρ'}.card * (Fintype.card ι - ℓ').choose (ℓ - ℓ')

      Double counting extensions. Summed over the partial assignments with ℓ free coordinates, the extensions with ℓ' ≤ ℓ free coordinates satisfying P count each partial assignment with ℓ' free coordinates satisfying P once for each of the C(|ι| - ℓ', ℓ - ℓ') ones it extends.

      source
      theorem Cslib.BitString.PartialAssignment.sum_extensions_update {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ₀ : PartialAssignment ι) {t : ℕ} (ht1 : 1 ≤ t) (g : PartialAssignment ι → ℕ) :
      ∑ ρ ∈ ρ₀.extensions t, ∑ i ∈ ρ.free, (g (Function.update ρ i (some false)) + g (Function.update ρ i (some true))) = (ρ₀.free.card - (t - 1)) * ∑ ρ' ∈ ρ₀.extensions (t - 1), g ρ'

      Double counting one-step extensions. Summing g (update ρ i (some b)) over all extensions ρ ∈ ρ₀.extensions t, free coordinates i ∈ ρ.free, and constants b : Bool counts each extension ρ' ∈ ρ₀.extensions (t - 1) once for each of the #ρ₀.free - (t - 1) coordinates of ρ₀.free fixed by ρ'.

      source
      theorem Cslib.BitString.PartialAssignment.mul_card_extensions_sub_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ₀ : PartialAssignment ι) {t : ℕ} (ht1 : 1 ≤ t) :
      (ρ₀.free.card - (t - 1)) * (ρ₀.extensions (t - 1)).card = 2 * t * (ρ₀.extensions t).card

      Relating the number of extensions with t - 1 and t free coordinates: (#ρ₀.free - (t - 1)) * #(ρ₀.extensions (t - 1)) = 2 * t * #(ρ₀.extensions t).

      source
      theorem Cslib.BitString.PartialAssignment.card_extensions_le_two_mul_card_filter_forall_nonempty {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ₀ : PartialAssignment ι) {b m : ℕ} (hb : 1 ≤ b) (hfree : ρ₀.free.card = b * m) {B : Fin b → Finset ι} (hBsub : ∀ (j : Fin b), B j ⊆ ρ₀.free) (hBcard : ∀ (j : Fin b), (B j).card = m) {r : ℕ} (hbr : 2 * b ≤ 2 ^ r) :
      (ρ₀.extensions (b * r)).card ≤ 2 * {ρ ∈ ρ₀.extensions (b * r) | ∀ (j : Fin b), (ρ.free ∩ B j).Nonempty}.card

      Union bound for block survival: if ρ₀ has b * m free coordinates and B 0, …, B (b - 1) are b subsets of ρ₀.free of size m, then for 1 ≤ b and 2 * b ≤ 2 ^ r, at least half of all extensions in ρ₀.extensions (b * r) leave at least one free coordinate in every block B j.

      source
      theorem Cslib.BitString.PartialAssignment.mul_card_filter_withFree_le {n c G H G' ℓ ℓ' : ℕ} (hℓ'ℓ : ℓ' ≤ ℓ) (hℓn : ℓ ≤ n) {B B' : PartialAssignment (Fin n) → Prop} [DecidablePred B] [DecidablePred B'] (h₁ : c * {ρ ∈ withFree (Fin n) ℓ | B ρ}.card ≤ G * (withFree (Fin n) ℓ).card) (h₂ : ∀ ρ ∈ withFree (Fin n) ℓ, ¬B ρ → c * {ρ' ∈ ρ.extensions ℓ' | B' ρ'}.card ≤ H * (ρ.extensions ℓ').card) (hG : G + H ≤ G') :
      c * {ρ ∈ withFree (Fin n) ℓ' | B' ρ}.card ≤ G' * (withFree (Fin n) ℓ').card

      Two stages of restrictions, counted. Drawing a restriction with ℓ' free bits by first drawing one with ℓ ≥ ℓ' free bits and then an extension of it: if at most a G / c fraction of the restrictions with ℓ free bits satisfy B, and for each other one at most an H / c fraction of its extensions with ℓ' free bits satisfy B', then at most a (G + H) / c fraction of the restrictions with ℓ' free bits satisfy B'.