OAI/NumberTheory/CubicMoment/Estimates/TypeILowNegligible.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete central Type-I integral is negligible on the first-moment scale. All arithmetic support conditions refer to the actual selected sums.

  1. theorem OAI.CubicFirstMoment.typeI_low_integral_isLittleO line 12