OAI/NumberTheory/CubicMoment/Estimates/LogNormCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual disjoint log-norm partition used in the integrated bilinear estimate. Its finite fibers preserve both the sum and coefficient energy.

  1. def OAI.CubicFirstMoment.logNormCell line 12
  2. def OAI.CubicFirstMoment.logNormCellSupport line 15
  3. lemma OAI.CubicFirstMoment.logNormCell_bounds line 18
  4. lemma OAI.CubicFirstMoment.logNormCell_mem_range line 23
  5. lemma OAI.CubicFirstMoment.logNormCell_count line 30
  6. lemma OAI.CubicFirstMoment.sum_logNormCells line 39
  7. lemma OAI.CubicFirstMoment.logNormCell_energy line 45
  8. lemma OAI.CubicFirstMoment.logNormCell_bilinear_partition line 52