OAI/NumberTheory/CubicMoment/Estimates/CubeModelOverlap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The difference between the full model square and its coprime pair sum is supported on shared-prime pairs.

  1. def OAI.CubicFirstMoment.cubeModelTerm line 13
  2. theorem OAI.CubicFirstMoment.cube_model_coprimality_error line 17