OAI/NumberTheory/CubicMoment/Estimates/FarLogCellHeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summing the actual far cells after height integration by parts. The only loss in their diagonal mass is the proved number of populated cells.

  1. def OAI.CubicFirstMoment.logCellHeightSum line 15
  2. theorem OAI.CubicFirstMoment.far_logCell_integrated_bound line 20