OAI/NumberTheory/CubicMoment/Estimates/ComplementAbsoluteWeight.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Nonnegative uncollected tuple weights. These retain the absolute complementary mass; no cancellation of collected coefficients is used.

  1. def OAI.CubicFirstMoment.complementAbsoluteWeight line 13
  2. lemma OAI.CubicFirstMoment.complementAbsoluteWeight_nonneg line 18
  3. lemma OAI.CubicFirstMoment.complementAbsoluteWeight_bound line 23
  4. lemma OAI.CubicFirstMoment.complementAbsoluteWeight_rough line 39