Final-term envelope for sharp circuit counting

The exact sharp budget is a sum of factorial-divided terms. This file bounds that sum by its final real-valued term, without yet invoking Stirling.

noncomputable def Cslib.Circuits.Signature.finalTerm (σ : Signature) [Fintype σ.Op] (n m G : ℕ) : ℝ

Real-valued envelope obtained by replacing every summand of the sharp budget by its final factorial-divided term.

Equations

• σ.finalTerm n m G = (↑G + 1) * ↑(σ.lineCount (n + G)) ^ G * (↑n + ↑G) ^ m / ↑G.factorial

theorem Algebraic.Nat.factorial_le_factorial_mul_pow {g G : ℕ} (bounded : g ≤ G) : G.factorial ≤ g.factorial * G ^ (G - g)

The tail of a factorial is bounded by replacing every factor by the final index.

theorem Cslib.Circuits.Signature.sharpBudget_cast_le_finalTerm (σ : Signature) [Fintype σ.Op] {n m G : ℕ} (enoughLines : G ≤ σ.lineCount (n + G)) : ↑(σ.sharpBudget n m G) ≤ σ.finalTerm n m G

Real-valued global form of the factorial-improved count. It bounds every summand by the final one whenever the final line count is at least G.

theorem Cslib.Circuits.Circuit.card_functionsAtMost_cast_le_finalTerm {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) {n m G : ℕ} (enoughLines : G ≤ σ.lineCount (n + G)) : ↑(functionsAtMost interpretation n m G).card ≤ σ.finalTerm n m G

Real-valued final-term bound on the number of functions computed with at most G gates.

theorem Cslib.Circuits.Circuit.exists_hard_in_family_of_finalTerm {U : Type u_1} {σ : Signature} {n m G : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) (enoughLines : G ≤ σ.lineCount (n + G)) (large : σ.finalTerm n m G < ↑family.card) : ∃ target ∈ family, GateHard interpretation G target

A finite family exceeding the real-valued final-term envelope contains a function requiring more than G gates.

theorem Cslib.Circuits.Circuit.exists_hard_of_finalTerm {U : Type u_1} {σ : Signature} {G n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (enoughLines : G ≤ σ.lineCount (n + G)) (large : σ.finalTerm n m G < ↑(Algebraic.Target.count U n m)) : ∃ (target : Algebraic.Target U n m), GateHard interpretation G target

Full-function-space Shannon theorem using the real-valued final-term envelope.