OAI/NumberTheory/CubicMoment/Estimates/MellinConjugation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Reflection of the actual Mellin kernel is obtained by conjugating its original radial weight. This handles the reverse character row without adding an analytic hypothesis.

  1. lemma OAI.CubicFirstMoment.star_fourierChar line 13
  2. lemma OAI.CubicFirstMoment.traceFourier_conj line 18
  3. lemma OAI.CubicFirstMoment.normProfileFourier_conj line 30
  4. lemma OAI.CubicFirstMoment.normDenominatorLogSchwartz_conj line 43
  5. lemma OAI.CubicFirstMoment.real_fourier_conj line 54
  6. lemma OAI.CubicFirstMoment.arithmeticMellinCoefficient_conj line 66