Documentation

Complexity.Foundations.Combinatorics.SubsetPairCount

Truncated subset-pair counts #

Counts the pairs (E, U) of subsets of an n-element set with #E ≤ q and U ⊆ E (OpenAI, The Exponential Time Hypothesis is False, eq. (3.14), p. 25): C_q = ∑_{s = 0}^{min(q, n)} 2 ^ s * n.choose s.

Main definitions #

Main results #

References #

source
def Cslib.subsetPairCount (n q : ℕ) :
ℕ

Number of subset pairs (E, U) of an n-element set with #E ≤ q and U ⊆ E ([OAI26c], eq. (3.14), p. 25): C_q = ∑_{s = 0}^{min(q, n)} 2^s C(n, s).

Instances For
    source
    @[simp]
    theorem Cslib.subsetPairCount_zero_right (n : ℕ) :
    subsetPairCount n 0 = 1

    At q = 0, only (∅, ∅) is retained, so C_0 = 1.

    source
    @[simp]
    theorem Cslib.subsetPairCount_zero_left (q : ℕ) :
    subsetPairCount 0 q = 1

    On an empty ground set (n = 0), C_q = 1 for every q.

    source
    theorem Cslib.subsetPairCount_mono_right (n : ℕ) {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂) :
    subsetPairCount n q₁ ≤ subsetPairCount n q₂

    subsetPairCount is monotone in the truncation order q.

    source
    theorem Cslib.subsetPairCount_pos (n q : ℕ) :
    0 < subsetPairCount n q

    Every subsetPairCount is strictly positive.

    source
    theorem Cslib.subsetPairCount_eq_three_pow {n q : ℕ} (hq : n ≤ q) :
    subsetPairCount n q = 3 ^ n

    When n ≤ q, all subset sizes occur and C_q = 3 ^ n ([OAI26c], p. 25).

    source
    theorem Cslib.subsetPairCount_le_three_pow (n q : ℕ) :
    subsetPairCount n q ≤ 3 ^ n

    subsetPairCount n q ≤ 3 ^ n for all n, q : ℕ.

    source
    theorem Cslib.sum_powerset_filter_card_le_two_pow {ι : Type u_1} [Fintype ι] (q : ℕ) :
    ∑ E ∈ Finset.univ.powerset with E.card ≤ q, 2 ^ E.card = subsetPairCount (Fintype.card ι) q

    Summing 2 ^ #E over E ⊆ univ with #E ≤ q equals subsetPairCount (Fintype.card ι) q.

    source
    theorem Cslib.subsetPairCount_eq_sum_powerset_fin (n q : ℕ) :
    subsetPairCount n q = ∑ E ∈ Finset.univ.powerset with E.card ≤ q, 2 ^ E.card

    subsetPairCount n q equals ∑_{E ⊆ Fin n, #E ≤ q} 2 ^ #E.

    source
    theorem Cslib.card_subsetPairs_eq_subsetPairCount {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℕ) :
    {p : Finset ι × Finset ι | p.1.card ≤ q ∧ p.2 ⊆ p.1}.card = subsetPairCount (Fintype.card ι) q

    subsetPairCount (Fintype.card ι) q counts {p : Finset ι × Finset ι | #p.1 ≤ q ∧ p.2 ⊆ p.1} ([OAI26c], eq. (3.14), p. 25).

    source
    theorem Cslib.card_subsetPairs_eq_subsetPairCount_of_card {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (hn : Fintype.card ι = n) (q : ℕ) :
    {p : Finset ι × Finset ι | p.1.card ≤ q ∧ p.2 ⊆ p.1}.card = subsetPairCount n q

    Specialization of card_subsetPairs_eq_subsetPairCount when Fintype.card ι = n.