OAI/NumberTheory/CubicMoment/Estimates/OrdinaryGroupRange.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A strict grouping gap above one third implies the actual logarithmic upper-length condition in the published-input bilinear theorem.

  1. theorem OAI.CubicFirstMoment.ordinary_group_upper_range line 11