OAI/NumberTheory/CubicMoment/Estimates/NormFourierSeminorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite seminorm control survives the norm-denominator multiplier and Fourier transform, uniformly before choosing a shrinking profile.

  1. theorem OAI.CubicFirstMoment.normDenominatorFourier_seminorm_control line 14