EntropyReduction
Abstract
Summing the cubic majorant reduces entropy to the second and third spectral moments. Newton’s identity replaces the third moment by purity and the third elementary symmetric polynomial.
The Lean objects in this component are dotProduct v v, C, entropy_spectral_bound, entropy_three_spectra.