OAI/NumberTheory/CubicMoment/Estimates/LogCellMajorant.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A concrete dispersion majorant for each actual log-norm cell. The cell is contained in the plateau of a cutoff at a comparable scale.

  1. def OAI.CubicFirstMoment.logCellScale line 11
  2. lemma OAI.CubicFirstMoment.exp_inv_le_one_add line 14
  3. lemma OAI.CubicFirstMoment.logCellScale_pos line 26
  4. lemma OAI.CubicFirstMoment.log_cell_plateau line 29
  5. lemma OAI.CubicFirstMoment.logNormCell_cutoff_one line 68
  6. lemma OAI.CubicFirstMoment.logCellScale_bounds line 75