OAI/NumberTheory/CubicMoment/Estimates/TypeIMixedDyads.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A fixed number of relative norm dyads covers the full product support. The number is independent of the product length.

  1. def OAI.CubicFirstMoment.typeIMixedDyadIndex line 12
  2. def OAI.CubicFirstMoment.typeIMixedDyad line 15
  3. lemma OAI.CubicFirstMoment.typeIMixedDyadIndex_bounds line 18
  4. lemma OAI.CubicFirstMoment.typeIMixedDyadIndex_lt line 32
  5. lemma OAI.CubicFirstMoment.typeIMixedDyad_partition line 39