OAI/NumberTheory/CubicMoment/Estimates/LowStopped.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Low-height localization for the actual stopped coefficients. The outer and inner energies are derived from their divisor definitions.

  1. theorem OAI.CubicFirstMoment.low_localized_stopped_bilinear_log_saving line 13