Property density

The density of a property of n-bit Boolean functions: the fraction of the 2 ^ (2 ^ n) Boolean functions that the property contains, as an exact rational (roadmap track L3, toward natural-proofs largeness). This mirrors the random-bit eventProb layer but over the sample space of all Boolean functions.

Main results

• density with density_nonneg, density_le_one, the complement identity density_compl, and the union bound density_union_le

def Complexity.density {n : ℕ} (P : Finset ((Fin n → Bool) → Bool)) : ℚ

The density of a property P of n-bit Boolean functions: the fraction of all 2 ^ (2 ^ n) such functions that lie in P.

Equations

• Complexity.density P = ↑P.card / 2 ^ 2 ^ n

theorem Complexity.density_nonneg {n : ℕ} (P : Finset ((Fin n → Bool) → Bool)) : 0 ≤ density P

theorem Complexity.card_le_card_boolFunc {n : ℕ} (P : Finset ((Fin n → Bool) → Bool)) : P.card ≤ 2 ^ 2 ^ n

A property has at most as many members as there are Boolean functions.

theorem Complexity.density_le_one {n : ℕ} (P : Finset ((Fin n → Bool) → Bool)) : density P ≤ 1

theorem Complexity.density_compl {n : ℕ} (P : Finset ((Fin n → Bool) → Bool)) : density Pᶜ = 1 - density P

The density of the complement of a property is one minus its density.

theorem Complexity.density_union_le {n : ℕ} (P Q : Finset ((Fin n → Bool) → Bool)) : density (P ∪ Q) ≤ density P + density Q

The union bound for property density.