OAI/NumberTheory/CubicMoment/Estimates/DispersionMixedAlgebra.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The mixed term in the corrected square is the genuine Type-I sum. No coprimality restriction is silently removed.

  1. lemma OAI.CubicFirstMoment.moebius_sq_mul_gauss line 12
  2. lemma OAI.CubicFirstMoment.dispersion_mixed_finite line 19