OAI/NumberTheory/CubicMoment/Estimates/LargeTupleWeightLengths.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The same actual coordinate weights are logarithmic families when the length is the product of any fixed group of their scales.

  1. def OAI.CubicFirstMoment.largeTupleBoxIndex line 12
  2. def OAI.CubicFirstMoment.largeTupleGroupLength line 16
  3. lemma OAI.CubicFirstMoment.largeTupleGroupLength_one line 19
  4. def OAI.CubicFirstMoment.largeTupleGroupWeight line 23
  5. def OAI.CubicFirstMoment.largeTupleGroupWeights line 27
  6. def OAI.CubicFirstMoment.largeTupleGroupLogWeights line 31