OAI/NumberTheory/CubicMoment/Theta/CubicThetaCentralAngularStoppedProductLowSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full stopped product estimate integrated against the actual low-height multiplier. A finite logarithmic loss is paid explicitly.

  1. theorem OAI.CubicFirstMoment.angular_stopped_product_low_log_saving_actual line 16