OAI/NumberTheory/CubicMoment/Estimates/PairOverlapEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The elementary symmetric pair bound used to remove shared-prime pairs from the quadratic cube model.

  1. lemma OAI.CubicFirstMoment.symmetric_pair_energy_le line 12