OAI/NumberTheory/CubicMoment/Estimates/DominantSmoothSizes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Explicit eventual scale margins for the dominant smooth dyad.

  1. theorem OAI.CubicFirstMoment.eventual_dominant_smooth_scales line 10