They're fairly standard theorems, I thought they'd be well-known as they trivially imply Sperner's theorem/lemma about the maximal size of an antichain.
The LYM inequality states that given an antichain on [n], let i.e the number of sets of size in Then
.
Now the local LYM inequality states that if then , where is the lower shadow of the antichain , in symbols .
In the above notation, . Each implies the other, but I'm struggling to show properly that the first inequality implies the second.