OAI/NumberTheory/CubicMoment/Estimates/PartitionMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summing the explicit smooth norm partition loses only a small part of an established power saving.

  1. lemma OAI.CubicFirstMoment.finite_piece_moment line 13
  2. theorem OAI.CubicFirstMoment.norm_partition_moment_power line 27