OAI/NumberTheory/CubicMoment/Estimates/TypeICutoffWindow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual cutoff window of the Type-I polynomial is the difference of its two normalized endpoint integrals.

  1. def OAI.CubicFirstMoment.typeIHeightPolynomial line 12
  2. lemma OAI.CubicFirstMoment.continuous_typeIHeightPolynomial line 16
  3. def OAI.CubicFirstMoment.typeICutoffWindow line 26
  4. theorem OAI.CubicFirstMoment.typeICutoffWindow_endpoints line 31
  5. theorem OAI.CubicFirstMoment.typeICutoffWindow_le_mean line 66