OAI/NumberTheory/CubicMoment/Estimates/ExplicitMomentAbsorption.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Explicit error exponents, independent of the coefficient-bound constants.

  1. lemma OAI.CubicFirstMoment.absorb_prime_coordinate_error_explicit line 10