OAI/NumberTheory/CubicMoment/Estimates/DispersionAbsoluteModel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Absolute model mass controls both the model and the coprimality error in its Type-I replacement.

  1. def OAI.CubicFirstMoment.dispersionAbsoluteModel line 12
  2. lemma OAI.CubicFirstMoment.dispersionAbsoluteModel_nonneg line 15
  3. lemma OAI.CubicFirstMoment.norm_dispersionModel_le_absolute line 19
  4. lemma OAI.CubicFirstMoment.dispersionAbsoluteModel_sq_le line 27
  5. theorem OAI.CubicFirstMoment.logarithmic_dispersionAbsoluteModel_energy line 41