OAI/NumberTheory/CubicMoment/Theta/CubicThetaCentralStoppedCenteredBilinear.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual stopped coefficients satisfy the centered bilinear estimate. Both energies and the shared-prime correction are derived from their finite formulas; the early-label roughness condition remains explicit.

  1. theorem OAI.CubicFirstMoment.stopped_centered_bilinear_log_saving_actual line 17