OAI/NumberTheory/CubicMoment/Estimates/PrimeModelCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The undecomposed prime model in the actual cutoff windows. The power saving comes from ordinary mean value, with the endpoint phases and the angular character retained exactly.

  1. lemma OAI.CubicFirstMoment.finite_cutoff_window_endpoints line 14
  2. theorem OAI.CubicFirstMoment.prime_model_cutoff_power_saving line 47