Local LYM inequality comparing a uniform family with its upper shadow

Fix $S\in [A{]}^k$. Since $A$ is the disjoint union of $S$ and $A\setminus S$, [L1] gives $\mathrm{\mid }A\setminus S\mathrm{\mid }=n-k$. The map $x\mapsto S\cup \{x\}$ is a bijection from $A\setminus S$ to the $(k+1)$-subsets of $A$ properly containing $S$: its inverse sends such a set to its unique element outside $S$. Thus every $S\in [A{]}^k$ has exactly $n-k$ one-element extensions.

Fix $T\in [A{]}^{k+1}$. The map $y\mapsto T\setminus \{y\}$ is a bijection from $T$ to its $k$-element subsets, with inverse sending a $k$-subset to its unique omitted element. Hence $T$ has exactly $k+1$ such subsets.

Count pairs $(S,T)$ with $S\in \mathcal{F}$, $T\in [A{]}^{k+1}$, and $S\subset T$. By step 1.1, there are $\mathrm{\mid }\mathcal{F}\mathrm{\mid }(n-k)$ pairs.

Every second coordinate lies in $\mathrm{\nabla }\mathcal{F}$, and step 1.2 shows that a fixed $T\in \mathrm{\nabla }\mathcal{F}$ contains at most $k+1$ members of $\mathcal{F}$. Thus the same number of pairs is at most $\mathrm{\mid }\mathrm{\nabla }\mathcal{F}\mathrm{\mid }(k+1)$.

Steps 2.1 and 2.2 give $\mathrm{\mid }\mathcal{F}\mathrm{\mid }(n-k)\le \mathrm{\mid }\mathrm{\nabla }\mathcal{F}\mathrm{\mid }(k+1)$. Using [L2] and dividing by the positive binomial coefficients gives the stated normalized inequality.

Equality in step 2.2 holds precisely when every $T\in \mathrm{\nabla }\mathcal{F}$ contributes all of its $k+1$ possible $k$-subsets, which is precisely the equality condition in the Statement.

Therefore the normalized local LYM inequality holds, with the asserted equality characterization.