OAI/NumberTheory/CubicMoment/Estimates/PrimeLogCutoffEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A power saving for the exact higher-prime-power replacement error. Both the sparse support and the coefficient amplitude are proved.

  1. theorem OAI.CubicFirstMoment.primeLogConvolutionError_cutoff_energy line 13