Average monotonicity of pure-state entanglement entropy (${\sum }_r{p}_{r}S({\rho }_{A,r})\le S({\rho }_A)$)

For a bipartite pure state, entanglement entropy is the Von Neumann entropy of either reduced density matrix. When Alice makes a local measurement with pure conditional branches, Bob's reductions average to his original reduction. Concavity of Von Neumann entropy therefore gives ${\sum }_r{p}_{r}S({\rho }_{B,r})\le S({\rho }_B)$. When Bob measures, apply concavity to Alice's reductions. In each pure branch the two reduced entropies coincide by the Schmidt decomposition. Refining measurement outcomes to individual Kraus operators and iterating proves the inequality for arbitrary finite-round LOCC. Discarded local systems can be measured and their outcomes refined as well, so discarding does not evade the bound.