OAI/NumberTheory/TwoPoint/ShortIntervals/MRTSparseMajorant.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing the artificial smooth coefficient weight on the original finite polynomial support. The majorant need only be at least one there.

  1. theorem OAI.TwoPointCorrelations.mrt_sparse_majorized_energy line 13