OAI/NumberTheory/CubicMoment/Estimates/LowFiniteProfile.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The derivative family is selected independently of the requested logarithmic saving. This order is needed for shrinking norm cutoffs.

  1. theorem OAI.CubicFirstMoment.low_variance_remainder_finite_seminorm line 12