OAI/NumberTheory/CubicMoment/Estimates/SmallBStoppedEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The energy of the actual stopped inner coefficient follows from rough distinguished divisors and the lattice count, without any mean-square hypothesis on the collected coefficient.

  1. theorem OAI.CubicFirstMoment.smallB_stopped_beta_energy line 13