OAI/NumberTheory/CubicMoment/Decomposition/StoppedProductGaussWindow.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A whole signed Mellin-height window for a fixed Schwartz multiplier. This is an application of the proved localized Gauss estimate, retaining its coefficient energies and its lower length/height ranges.

  1. theorem OAI.CubicFirstMoment.schwartz_gauss_window_log_saving line 14