OAI/NumberTheory/CubicMoment/Estimates/ComplementAbsoluteCollection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact collection of absolute tuple weights by their primary product. This is a finite identity, before any cancellation estimate.

  1. lemma OAI.CubicFirstMoment.complement_absolute_collection line 13
  2. theorem OAI.CubicFirstMoment.complement_absolute_tuple_mass line 33