OAI/NumberTheory/CubicMoment/Estimates/LowThinBilinear.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The thin diagonal keeps the actual coefficient energy, while only the off-diagonal remainder uses the uniform coefficient bound.

  1. theorem OAI.CubicFirstMoment.low_thinCell_bilinear_height_square line 12