OAI/NumberTheory/CubicMoment/Estimates/WideMellinControl.lean

GitHub source file

2 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.wideGramFourier_seminorm_control line 14
  2. theorem OAI.CubicFirstMoment.wideGramMellinCoefficient_moment_control line 70