OAI/NumberTheory/CubicMoment/Estimates/LogSmoothWeights.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic full factors are exact linear combinations of two smooth weights. No logarithmic coefficient is silently discarded.

  1. def OAI.CubicFirstMoment.logSmoothWeight line 13
  2. lemma OAI.CubicFirstMoment.logSmoothWeight_compact line 15
  3. lemma OAI.CubicFirstMoment.logSmoothWeight_positive line 19
  4. lemma OAI.CubicFirstMoment.logSmoothWeight_smooth line 22
  5. lemma OAI.CubicFirstMoment.primary_weighted_smooth_finite line 37
  6. theorem OAI.CubicFirstMoment.primary_log_smooth_decomposition line 54
  7. lemma OAI.CubicFirstMoment.primary_log_smooth_sq_le line 76