OAI/NumberTheory/CubicGauss/PowerBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Power-bound formulations and squarefree-to-cubic extensions.

  1. def OAI.CubicFirstMoment.CubicPowerBound line 17
  2. lemma OAI.CubicFirstMoment.SieveOperator.Bound.restrict_coeff line 24
  3. lemma OAI.CubicFirstMoment.cubic_power_bound_transposed line 45
  4. theorem OAI.CubicFirstMoment.cubic_power_bound_two line 75
  5. lemma OAI.CubicFirstMoment.squarefreePrimaryBall_eq_empty_of_lt_one line 124
  6. lemma OAI.CubicFirstMoment.cube_envelope_sum_bound line 132
  7. def OAI.CubicFirstMoment.CubicFullPowerBound line 189
  8. theorem OAI.CubicFirstMoment.cubic_power_full_extension line 197