Depth lower bounds from bounded fan-in #
At depth d, a fan-in-r output can depend on at most r ^ d inputs.
Essential inputs therefore give a lower bound on circuit depth.
theorem
Cslib.Circuits.Circuit.card_inputSupport_le_depth
{σ : Signature}
{n m : ℕ}
(c : Circuit σ n m)
{r : ℕ}
(bounded : c.FanInAtMost r)
:
A fan-in-r circuit has at most m * (max 1 r) ^ c.depth supporting
inputs. The maximum accounts for direct output wires when r = 0.
theorem
Cslib.Circuits.Circuit.essential_le_depth
{σ : Signature}
{n m : ℕ}
{U : Type u_2}
(c : Circuit σ n m)
{interpretation : Interpretation σ U}
{target : (Fin n → U) → Fin m → U}
{selected : Finset (Fin n)}
{r : ℕ}
(computes : c.ComputesWith interpretation target)
(essential : ∀ k ∈ selected, Algebraic.EssentialAt target k)
(bounded : c.FanInAtMost r)
:
If a circuit has fan-in at most r, computes target, and every input in
selected is essential to target, then selected has at most
m * (max 1 r) ^ c.depth elements.