OAI/NumberTheory/CubicMoment/Estimates/HeightBilinear.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Genuine Gauss-sum bilinear forms inherit the full height variance bound by finite Cauchy--Schwarz, retaining the original coefficients.

  1. lemma OAI.CubicFirstMoment.bilinear_full_variance_bound_sq line 12
  2. lemma OAI.CubicFirstMoment.height_bilinear_full_variance_bound_sq line 39