OAI/NumberTheory/CubicMoment/Estimates/IndependentMellinMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-row L2 transfer for independently separated norm weights, with a proved tail outside the simultaneous height window.

  1. lemma OAI.CubicFirstMoment.finite_box_integral_moment line 15
  2. theorem OAI.CubicFirstMoment.independent_mellin_integral_moment line 33