OAI/NumberTheory/CubicMoment/Estimates/LargeTupleCoordinateWeights.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual independently smoothed prime coordinates of a large row belong to one uniform family, for every norm partition and roughness scale.

  1. def OAI.CubicFirstMoment.largeTupleNormScale line 13
  2. lemma OAI.CubicFirstMoment.largeTupleNormScale_pos line 16
  3. def OAI.CubicFirstMoment.largeTupleCoordinateWeight line 21
  4. def OAI.CubicFirstMoment.largeTupleCoordinateWeights line 28
  5. lemma OAI.CubicFirstMoment.roughSmoothWeight_at_prime line 46
  6. lemma OAI.CubicFirstMoment.largeTupleCoordinateWeight_distinguished line 56
  7. lemma OAI.CubicFirstMoment.largeTupleCoordinateWeight_rough line 66
  8. lemma OAI.CubicFirstMoment.largeTupleCoordinateWeight_norm line 76
  9. lemma OAI.CubicFirstMoment.largeTupleCoordinateWeight_low line 83
  10. lemma OAI.CubicFirstMoment.largeTupleCoordinateWeight_high line 90