HalaszBalancedMoment.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Equal total moments bound each mixed moment. This will be applied to the ordinary polynomial sum and its doubled-frequency version.