OAI/NumberTheory/TwoPoint/Fourier/MinorArcTypicalIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual typical-set short-sum integral, reduced to the bounded bilinear window plus its single prime-square error.

  1. theorem OAI.TwoPointCorrelations.minor_arc_typical_integral_le line 14