OAI/NumberTheory/CubicMoment/Estimates/FarLogNormCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Far cells are the exact complement of the actual near-cell graph. Every product in such a cell has the lower frequency bound needed for IBP.

  1. def OAI.CubicFirstMoment.allLogNormCells line 11
  2. def OAI.CubicFirstMoment.farLogNormCells line 14
  3. lemma OAI.CubicFirstMoment.nearLogNormCells_subset line 17
  4. lemma OAI.CubicFirstMoment.farLogNormCells_subset line 21
  5. lemma OAI.CubicFirstMoment.farLogNormCells_frequency line 25
  6. lemma OAI.CubicFirstMoment.sum_near_farLogNormCells line 45