Almost-all circuit lower bounds

This file isolates the density language from any particular asymptotic gate budget. The primary predicate is division-free; the final theorem translates it to the conventional real-valued density limit.

Easy and hard members of a finite family

noncomputable def Cslib.Circuits.Circuit.easyInFamily {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) (G : ℕ) : Finset (Algebraic.Target U n m)

Members of a family that are easy at internal-gate budget G.

Equations

• Cslib.Circuits.Circuit.easyInFamily interpretation family G = {target ∈ family | target ∈ Cslib.Circuits.Circuit.functionsAtMost interpretation n m G}

noncomputable def Cslib.Circuits.Circuit.hardInFamily {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) (G : ℕ) : Finset (Algebraic.Target U n m)

Members of a family requiring more than G internal gates.

Equations

• Cslib.Circuits.Circuit.hardInFamily interpretation family G = {target ∈ family | target ∉ Cslib.Circuits.Circuit.functionsAtMost interpretation n m G}

noncomputable def Cslib.Circuits.Circuit.easyDensity {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) (G : ℕ) : ℝ

Proportion of a finite family computed within gate budget G.

Equations

• Cslib.Circuits.Circuit.easyDensity interpretation family G = ↑(Cslib.Circuits.Circuit.easyInFamily interpretation family G).card / ↑family.card

theorem Cslib.Circuits.Circuit.mem_hardInFamily_iff {U : Type u_1} {σ : Signature} {n m G : ℕ} [Fintype σ.Op] [Fintype U] {interpretation : Interpretation σ U} {family : Finset (Algebraic.Target U n m)} {target : Algebraic.Target U n m} : target ∈ hardInFamily interpretation family G ↔ target ∈ family ∧ GateHard interpretation G target

theorem Cslib.Circuits.Circuit.card_easyInFamily_le_sharpBudget {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) (G : ℕ) : (easyInFamily interpretation family G).card ≤ σ.sharpBudget n m G

theorem Cslib.Circuits.Circuit.card_family_sub_sharpBudget_le_hardInFamily {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) (G : ℕ) : family.card - σ.sharpBudget n m G ≤ (hardInFamily interpretation family G).card

Quantitative almost-all theorem: at most the sharp budget can be easy.

Division-free asymptotic density

def Cslib.Circuits.Circuit.AsymptoticallyAlmostAllHard {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (m : ℕ) (family : (n : ℕ) → Finset (Algebraic.Target U n m)) (gateBudget : ℕ → ℕ) : Prop

A sequence of easy subsets is asymptotically negligible when every fixed multiple of its cardinality is eventually bounded by the ambient family. This is a division-free finite-set formulation of density tending to zero.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Circuits.Circuit.asymptoticallyAlmostAllHard_of_sharpBudget {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (m : ℕ) (family : (n : ℕ) → Finset (Algebraic.Target U n m)) (gateBudget : ℕ → ℕ) (negligible : ∀ (K : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, K * σ.sharpBudget n m (gateBudget n) ≤ (family n).card) : AsymptoticallyAlmostAllHard interpretation m family gateBudget

Generic exact asymptotic Shannon theorem. Every fixed multiple of the sharp description budget being eventually smaller than the family implies that the easy subfamily has density zero.

theorem Cslib.Circuits.Circuit.asymptoticallyAlmostAllHard_of_finalTerm {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (m : ℕ) (family : (n : ℕ) → Finset (Algebraic.Target U n m)) (gateBudget : ℕ → ℕ) (enoughLines : ∀ᶠ (n : ℕ) in Filter.atTop, gateBudget n ≤ σ.lineCount (n + gateBudget n)) (negligible : ∀ (K : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ↑K * σ.finalTerm n m (gateBudget n) ≤ ↑(family n).card) : AsymptoticallyAlmostAllHard interpretation m family gateBudget

Analytic form of the almost-all transfer theorem. It replaces the exact sum of integer quotients by the real final-term envelope.

The full target space and conventional density

theorem Cslib.Circuits.Circuit.AsymptoticallyAlmostAllHard.eventually_exists_hard {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] {interpretation : Interpretation σ U} {m : ℕ} {family : (n : ℕ) → Finset (Algebraic.Target U n m)} {gateBudget : ℕ → ℕ} (hard : AsymptoticallyAlmostAllHard interpretation m family gateBudget) (nonempty : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < (family n).card) : ∀ᶠ (n : ℕ) in Filter.atTop, ∃ target ∈ family n, GateHard interpretation (gateBudget n) target

An asymptotically negligible easy subset leaves a hard target at every sufficiently large width, provided the ambient families are nonempty.

noncomputable def Cslib.Circuits.Circuit.fullFamily (U : Type u_1) [Fintype U] (m n : ℕ) : Finset (Algebraic.Target U n m)

The complete family of m-output functions on n inputs.

Equations

• Cslib.Circuits.Circuit.fullFamily U m n = Finset.univ

@[simp]

theorem Cslib.Circuits.Circuit.card_fullFamily (U : Type u_1) [Fintype U] (m n : ℕ) : (fullFamily U m n).card = Algebraic.Target.count U n m

theorem Cslib.Circuits.Circuit.AsymptoticallyAlmostAllHard.tendsto_easyDensity_zero {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] {interpretation : Interpretation σ U} {m : ℕ} {family : (n : ℕ) → Finset (Algebraic.Target U n m)} {gateBudget : ℕ → ℕ} (hard : AsymptoticallyAlmostAllHard interpretation m family gateBudget) (familyNonempty : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < (family n).card) : Filter.Tendsto (fun (n : ℕ) => easyDensity interpretation (family n) (gateBudget n)) Filter.atTop (nhds 0)

The division-free almost-all predicate implies the conventional statement that the real-valued density of easy functions tends to zero.