Savický and Woods (The Number of Boolean Functions Computed by Formulas of a Given Size) prove the following result.
Theorem[SW98]: For every constant $k>1$, almost all boolean functions with formula complexity at most $n^k$ have circuit complexity at least $n^k/k$.
The proof consists of deriving a lower bound on $B(n,n^k)$, the number of boolean functions on $n$ inputs computed by formulas of size $n^k$. By comparing $B(n,n^k)$ to the number of circuits of size $C = n^k/k$, which is at most $C^{C}e^{C+4n}$, it can be realized that for large $n$, $C^{C}e^{C+4n} << B(n,n^k)$, and the result follows.
It looks to me that the result could be strengthened by noting that the number of nondeterministic circuits of size $n^k$ with $m$ nondeterministic inputs is not much larger than the number of deterministic circuits of size $n^k$ (for $m$ not too large, say $m=n$). Hence, I think the following corollary holds:
Corollary: For every constant $k>1$, almost all boolean functions with formula complexity at most $n^k$ have nondeterministic circuit complexity at least $n^k/k$ (for nondeterministic circuits with $n$ nondeterministic inputs).
(Recall that a nondeterministic circuit has, in addition to the ordinary inputs $x = (x_1,\dots,x_n)$, a set of "nondeterministic" inputs $y=(y_1,\dots,y_m)$. A nondeterministic circuit $C$ accepts input $x$ if there exists $y$ such that the circuit output $1$ on $(x,y)$).
Obviously, the lower bound on $B(n,n^k)$ is also a lower bound on the number of boolean functions on $n$ inputs computed by circuits of size $n^k$, hence "formula complexity at most $n^k$" can be replaced by "circuit complexity at most $n^k$" in the corollary. The corollary can also be stated as: for functions with polynomial circuit complexity, switching to nondeterministic circuits cannot, on average, decrease the complexity by more than a constant factor.
Questions:
(1) Are there any interesting implications/consequences of the corollary above?
(2) Are there any other results in the same direction? For example, what is known about the following proposition? For problems in P, switching from TMs to NTMs cannot, on average, decrease the complexity by more than a constant factor.
(Gil Kalai also has a question somewhat related to this one.)