[proofplan]
We decompose the antichain into its rank-level pieces and measure subsets of each level by normalized cardinality. The normalized matching property says that passing to the next upper shadow cannot decrease this normalized cardinality. We then inductively push all antichain elements from ranks at most $t$ up to a subset $B_t\subset P_t$, preserving at least the sum of their normalized weights. At the last rank, this weight is at most $1$, giving the [LYM inequality](/theorems/2586).
[/proofplan]
[step:Decompose the antichain into rank levels and define normalized weights]
For each $0\le i\le r$, define
\begin{align*}
A_i=A\cap P_i.
\end{align*}
Since the rank levels are pairwise disjoint, the set $A$ is the disjoint union of the sets $A_i$. Therefore
\begin{align*}
\sum_{x\in A}\frac{1}{|P_{\rho(x)}|}=\sum_{i=0}^r \frac{|A_i|}{|P_i|}.
\end{align*}
For each $0\le i\le r$, let $\mathcal{P}(P_i)$ denote the power set of $P_i$, and define the normalized weight map $\mu_i:\mathcal{P}(P_i)\to[0,1]$ by
\begin{align*}
\mu_i(B)=\frac{|B|}{|P_i|}
\end{align*}
for every $B\in\mathcal{P}(P_i)$. The denominators are nonzero because the rank levels $P_0,\dots,P_r$ are assumed nonempty, and the codomain is valid because every $B\in\mathcal{P}(P_i)$ satisfies $0\le |B|\le |P_i|$.
[guided]
We first separate the antichain according to rank. For each $0\le i\le r$, define $A_i=A\cap P_i$. Since $\rho$ is a rank function and $P_i=\{x\in P:\rho(x)=i\}$, the rank levels $P_0,\dots,P_r$ are pairwise disjoint. Hence the sets $A_i$ are pairwise disjoint and their union is $A$. Therefore the contribution of all elements of $A$ to the LYM sum can be grouped by rank:
\begin{align*}
\sum_{x\in A}\frac{1}{|P_{\rho(x)}|}=\sum_{i=0}^r \frac{|A_i|}{|P_i|}.
\end{align*}
The normalized matching property is expressed in terms of ratios of cardinalities inside a single rank level, so we package those ratios as functions. For each $0\le i\le r$, let $\mathcal{P}(P_i)$ be the power set of $P_i$, and define the map $\mu_i:\mathcal{P}(P_i)\to[0,1]$ by
\begin{align*}
\mu_i(B)=\frac{|B|}{|P_i|}
\end{align*}
for every subset $B\subset P_i$. This is well-defined because the theorem assumes $P_i$ is nonempty, so $|P_i|\ne0$, and because $0\le |B|\le |P_i|$ implies $0\le \mu_i(B)\le1$. With this notation, the desired inequality is exactly
\begin{align*}
\sum_{i=0}^r \mu_i(A_i)\le 1.
\end{align*}
[/guided]
[/step]
[step:Construct an upper-level representative for the first $t$ ranks]
We prove by induction on $t\in\{0,\dots,r\}$ that there exists a subset $B_t\subset P_t$ such that
\begin{align*}
\mu_t(B_t)\ge \sum_{i=0}^t \mu_i(A_i),
\end{align*}
and every element of $B_t$ lies above some element of $A_0\cup\cdots\cup A_t$.
For $t=0$, take $B_0=A_0$. Then
\begin{align*}
\mu_0(B_0)=\mu_0(A_0)=\sum_{i=0}^0\mu_i(A_i),
\end{align*}
and every element of $B_0$ lies above itself, which belongs to $A_0$.
[guided]
The goal of the induction is to replace all antichain elements in the lower ranks by a single subset sitting in one rank. For $t=0$, no replacement is needed. We define $B_0=A_0\subset P_0$. Its normalized weight is exactly
\begin{align*}
\mu_0(B_0)=\mu_0(A_0)=\sum_{i=0}^0\mu_i(A_i).
\end{align*}
The second invariant is also satisfied: if $b\in B_0$, then $b\in A_0$, so $b$ lies above the chosen element $b\in A_0$. This invariant is important because it will later force disjointness from the next antichain level.
[/guided]
[/step]
[step:Push the representative from rank $t-1$ to rank $t$ and add the new antichain layer]
Assume $1\le t\le r$ and suppose that $B_{t-1}\subset P_{t-1}$ has been constructed. Define
\begin{align*}
C_t=\nabla_{t-1}(B_{t-1})\subset P_t
\end{align*}
and
\begin{align*}
B_t=C_t\cup A_t.
\end{align*}
By the normalized matching property applied to $B_{t-1}\subset P_{t-1}$,
\begin{align*}
\mu_t(C_t)\ge \mu_{t-1}(B_{t-1}).
\end{align*}
We claim that $C_t\cap A_t=\varnothing$. If $y\in C_t\cap A_t$, then by the definition of $C_t$ there exists $b\in B_{t-1}$ with $b\le y$. By the induction invariant, there exists $a\in A_0\cup\cdots\cup A_{t-1}$ with $a\le b$. Hence $a\le y$. Since $a\in P_i$ for some $i<t$ and $y\in P_t$, we have $a\ne y$. Thus $a$ and $y$ are two distinct comparable elements of the antichain $A$, a contradiction.
Therefore the union defining $B_t$ is disjoint, and so
\begin{align*}
\mu_t(B_t)=\mu_t(C_t)+\mu_t(A_t).
\end{align*}
Using the normalized matching estimate and the induction hypothesis,
\begin{align*}
\mu_t(B_t)\ge \mu_{t-1}(B_{t-1})+\mu_t(A_t).
\end{align*}
Therefore
\begin{align*}
\mu_t(B_t)\ge \sum_{i=0}^{t-1}\mu_i(A_i)+\mu_t(A_t)=\sum_{i=0}^t\mu_i(A_i).
\end{align*}
Finally, every element of $B_t$ lies above an element of $A_0\cup\cdots\cup A_t$. Indeed, an element of $A_t$ lies above itself, while an element of $C_t$ lies above some element of $B_{t-1}$ and hence, by the induction invariant, above some element of $A_0\cup\cdots\cup A_{t-1}$.
[guided]
We now explain the induction step carefully. Suppose $B_{t-1}\subset P_{t-1}$ already represents the antichain elements in ranks $0,\dots,t-1$. To move it up one rank, define its upper shadow
\begin{align*}
C_t=\nabla_{t-1}(B_{t-1})=\{y\in P_t:b\le y \text{ for some } b\in B_{t-1}\}.
\end{align*}
The normalized matching property applies because $B_{t-1}\subset P_{t-1}$ and $0\le t-1<r$. It gives
\begin{align*}
\mu_t(C_t)\ge \mu_{t-1}(B_{t-1}).
\end{align*}
Thus pushing $B_{t-1}$ upward does not lose normalized weight.
Now we add the actual antichain elements in rank $t$ by setting
\begin{align*}
B_t=C_t\cup A_t.
\end{align*}
The key point is that this union is disjoint. Suppose, toward a contradiction, that $y\in C_t\cap A_t$. Since $y\in C_t$, there is some $b\in B_{t-1}$ with $b\le y$. Since $b\in B_{t-1}$, the induction invariant gives an element $a\in A_0\cup\cdots\cup A_{t-1}$ such that $a\le b$. Combining the inequalities gives $a\le y$. The element $a$ lies in some lower rank $P_i$ with $i<t$, while $y\in P_t$, so $a\ne y$. Hence $a$ and $y$ are distinct comparable elements of $A$, contradicting that $A$ is an antichain.
Because $C_t$ and $A_t$ are disjoint subsets of the same finite rank level $P_t$, cardinalities add:
\begin{align*}
\mu_t(B_t)=\frac{|C_t|+|A_t|}{|P_t|}=\mu_t(C_t)+\mu_t(A_t).
\end{align*}
Using normalized matching and then the induction hypothesis,
\begin{align*}
\mu_t(B_t)\ge \mu_{t-1}(B_{t-1})+\mu_t(A_t).
\end{align*}
Thus
\begin{align*}
\mu_t(B_t)\ge \sum_{i=0}^{t-1}\mu_i(A_i)+\mu_t(A_t)=\sum_{i=0}^t\mu_i(A_i).
\end{align*}
It remains to preserve the invariant about lying above an antichain element. If $y\in A_t$, then $y$ lies above itself. If $y\in C_t$, then by definition $b\le y$ for some $b\in B_{t-1}$, and by the induction invariant there is $a\in A_0\cup\cdots\cup A_{t-1}$ with $a\le b$. Hence $a\le y$. So every element of $B_t$ lies above some element of $A_0\cup\cdots\cup A_t$.
[/guided]
[/step]
[step:Apply the induction at the top rank]
Taking $t=r$ in the induction construction gives a subset $B_r\subset P_r$ such that
\begin{align*}
\mu_r(B_r)\ge \sum_{i=0}^r \mu_i(A_i).
\end{align*}
Since $B_r\subset P_r$, we have $|B_r|\le |P_r|$, and hence
\begin{align*}
\mu_r(B_r)=\frac{|B_r|}{|P_r|}\le 1.
\end{align*}
Therefore
\begin{align*}
\sum_{x\in A}\frac{1}{|P_{\rho(x)}|}=\sum_{i=0}^r\mu_i(A_i)\le \mu_r(B_r)\le 1.
\end{align*}
This proves the LYM inequality for every antichain $A\subset P$.
[guided]
The induction has pushed all antichain elements, rank by rank, into a single subset of the top rank while preserving at least their total normalized weight. Applying the induction statement with $t=r$ gives a subset $B_r\subset P_r$ satisfying
\begin{align*}
\mu_r(B_r)\ge \sum_{i=0}^r \mu_i(A_i).
\end{align*}
Now we use the fact that a normalized weight inside one rank level is at most $1$. Since $B_r\subset P_r$, finite cardinality gives $|B_r|\le |P_r|$. The rank level $P_r$ is nonempty by hypothesis, so division by $|P_r|$ is valid, and the definition of $\mu_r$ gives
\begin{align*}
\mu_r(B_r)=\frac{|B_r|}{|P_r|}\le 1.
\end{align*}
Finally, the first step rewrote the LYM sum as the sum of the normalized weights of the rank pieces of $A$:
\begin{align*}
\sum_{x\in A}\frac{1}{|P_{\rho(x)}|}=\sum_{i=0}^r\mu_i(A_i).
\end{align*}
Combining this identity with the top-rank induction estimate and the bound $\mu_r(B_r)\le1$ yields
\begin{align*}
\sum_{x\in A}\frac{1}{|P_{\rho(x)}|}=\sum_{i=0}^r\mu_i(A_i)\le \mu_r(B_r)\le 1.
\end{align*}
Thus every antichain $A\subset P$ satisfies the LYM inequality.
[/guided]
[/step]
