OAI/NumberTheory/CubicMoment/Estimates/ThinCellCutoff.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

An actual nonnegative cutoff supported in a cell of width 1/J, with a plateau on the central half of that cell.

  1. def OAI.CubicFirstMoment.thinBaseBump line 13
  2. def OAI.CubicFirstMoment.thinBaseSchwartz line 16
  3. lemma OAI.CubicFirstMoment.thinBaseSchwartz_apply line 20
  4. lemma OAI.CubicFirstMoment.thinBaseSchwartz_compact line 23
  5. def OAI.CubicFirstMoment.thinCellCutoff line 26
  6. lemma OAI.CubicFirstMoment.thinCellCutoff_nonneg line 29
  7. lemma OAI.CubicFirstMoment.thinCellCutoff_le_one line 31
  8. lemma OAI.CubicFirstMoment.thinCellCutoff_eq_affine line 33
  9. lemma OAI.CubicFirstMoment.thinCellCutoff_compact line 37
  10. lemma OAI.CubicFirstMoment.thinCellCutoff_smooth line 42
  11. lemma OAI.CubicFirstMoment.thinCellCutoff_norm line 47
  12. lemma OAI.CubicFirstMoment.thinCellCutoff_support line 51
  13. lemma OAI.CubicFirstMoment.thinCellCutoff_one line 66