OAI/NumberTheory/CubicMoment/Estimates/ThinCellStoppedBilinear.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The thin-cell estimate for literal stopped coefficients. Their energies are proved from the divisor moment and roughness, rather than assumed.

  1. lemma OAI.CubicFirstMoment.outer_log_energy_conversion_cubic line 12
  2. theorem OAI.CubicFirstMoment.thinCell_stopped_bilinear_log_saving line 34