OAI/NumberTheory/CubicMoment/Estimates/TypeILogCoefficients.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Fixed logarithmic coefficient factors can be retained in the actual weight family. This is the form used by short logarithmic convolutions.

  1. def OAI.CubicFirstMoment.logPowerWeight line 11
  2. def OAI.CubicFirstMoment.LogarithmicWeightFamily.logPower line 14
  3. theorem OAI.CubicFirstMoment.typeI_low_log_coefficients line 43