OAI/NumberTheory/CubicMoment/Estimates/CorrectedSquareTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transfer the proved complex variance and Type-I estimates to the actual nonnegative corrected square.

  1. theorem OAI.CubicFirstMoment.correctedSquareMass_le_of_errors line 12