Balancing unbounded fanin formulas

In Section 6.1 (page 163) of the book we mentioned that Lozhkin (1981) has proved the following result. Let $D(f)$ denote the minimal depth of a DeMorgan formula computing $f$. Recall that these formula consist of fanin-$2$ AND and OR gates; inputs are literals (variables and their negations).

Theorem (Lozhkin 1981): If a boolean function $f$ can be computed by a depth-$d$ DeMorgan formula using unbounded fanin AND and OR gates and having $L$ leaves, then $ D(f)\leq d-1+\lceil\log_2 L\rceil. $
Note that a trivial upper bound, obtained by simulating each gate by a tree, is only $D(f)=O(d\log L)$.

Proof: We use induction on $d$. For the induction step, assume that the claim holds for all formulas of depth at most $d-1$, and take a depth-$d$ DeMorgan formula $F$. Assume w.l.o.g. that the last gate of $F$ is an AND gate, an let $F_1,\ldots,F_t$ be the formulas entering this gate. Let $L_i$ be the number of leaves in $F_i$, $i=1,\ldots,t$. Since each of these formulas has depth at most $d-1$, the induction hypothesis implies that, for every $i=1,\ldots,t$, there is a DeMorgan formula $F_i^*$ which is equivalent to $F_i$ and has depth $$ D_i\leq d-2+\lceil\log_2 L_i\rceil\,.\qquad\qquad\qquad\qquad (1) $$ Set $$ D:=\left\lceil\log_2\sum_{i=1}^t2^{D_i}\right\rceil\,.\qquad\qquad\qquad\qquad (2) $$ Since $L=\sum_{i=1}^t L_i$, we obtain from (1) and (2) that \[ \begin{align} D&\leq 1+\log_2\sum_{i=1}^t2^{D_i}\\ &\leq 1+\log_2\sum_{i=1}^t2^{d-2+\lceil\log_2 L_i\rceil}\\ &\leq 1+ (d-2)+ \log_2\sum_{i=1}^t 2^{1+\log_2 L_i}\\ &\leq d-1 + \lceil\log_2 L\rceil. \end{align} \] We now construct the desired DeMorgan formula $F^*$ of depth $D$ which is equivalent to our original (unbounded fanin) formula. For this, take a formula $T$ over the basis $\{\land\}$, whose underlying graph is a complete binary tree of depth $D$. By the definition (2) of the depth $D$ of our tree, for every $i=1,\ldots,t$, there is a subformula $T_i$ of $T$ of depth $D_i$ and with $2^{D_i}$ leaves (we have enough distinct subtrees at each level). Replace by constant $1$ each leaf of $T$ which is not a leaf of any of the subformulas $T_1,\ldots,T_t$. After that replace each subformula $T_i$ by the (balanced) DeMorgan formula $F_i^*$ (whose existence was ensured by the induction hypothesis). The resulting DeMorgan $F^*$ has depth $D\leq d-1 + \lceil\log_2 L\rceil$ and computes the same boolean function as the original formula $F$. $\Box$