OAI/NumberTheory/CubicMoment/Estimates/SharpHeightPartition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Smooth height windows with ratio 3/2. Their support lies in [T,2T] in absolute value, exactly the range of the proved bilinear estimates. The finite telescoping identity keeps the actual truncation multiplier.

  1. def OAI.CubicFirstMoment.heightPartitionBump line 14
  2. lemma OAI.CubicFirstMoment.heightPartitionBump_one line 20
  3. lemma OAI.CubicFirstMoment.heightPartitionBump_zero line 25
  4. def OAI.CubicFirstMoment.heightWindow line 30
  5. lemma OAI.CubicFirstMoment.heightWindow_smooth line 33
  6. lemma OAI.CubicFirstMoment.heightWindow_norm_le line 38
  7. lemma OAI.CubicFirstMoment.heightWindow_zero line 44
  8. lemma OAI.CubicFirstMoment.heightWindow_telescope line 75
  9. lemma OAI.CubicFirstMoment.cutoffHeightMultiplier_partition line 86
  10. lemma OAI.CubicFirstMoment.integrable_cutoffHeightMultiplier_window line 104
  11. lemma OAI.CubicFirstMoment.cutoffHeightMultiplier_integral_partition line 110