OAI/NumberTheory/CubicMoment/Decomposition/StoppedProductMellinPhase.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact phases in the product Mellin integral. The scale oscillation is kept outside the fixed Schwartz profile, so its derivative cost is uniform.

  1. def OAI.CubicFirstMoment.reflectedZeroMellinProfile line 13
  2. lemma OAI.CubicFirstMoment.reflectedZeroMellinProfile_apply line 20
  3. lemma OAI.CubicFirstMoment.zeroLineMellinWeight_reflected_phase line 29
  4. lemma OAI.CubicFirstMoment.gaussProduct_shift line 43
  5. lemma OAI.CubicFirstMoment.norm_twisted_coefficient line 57