OAI/NumberTheory/CubicMoment/Decomposition/StoppedOuterEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual stopped outer coefficient has logarithmic energy in the same X-normalization as the stopped corrected-dispersion theorem.

  1. theorem OAI.CubicFirstMoment.stopped_outer_log_energy line 11