OAI/NumberTheory/TwoPoint/Fourier/MinorArcTypicalSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The minor-arc short-integral estimate for the actual MRT typical set.

  1. theorem OAI.TwoPointCorrelations.minor_arc_typical_log_saving line 13