OAI/NumberTheory/CubicMoment/Estimates/CorrectedBilinearMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Cauchy--Schwarz with the true squarefree corrected mass.

  1. lemma OAI.CubicFirstMoment.norm_gauss_sq_eq_moebius_sq line 11
  2. theorem OAI.CubicFirstMoment.corrected_bilinear_mass_bound_sq line 16