OAI/NumberTheory/CubicMoment/Estimates/PrimeLogWindow.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A genuine smooth approximation to the dyadic interval in logarithmic coordinates. The two endpoint transitions have width exactly 1/J.

  1. def OAI.CubicFirstMoment.primeLogWindow line 12
  2. lemma OAI.CubicFirstMoment.primeLogWindow_smooth line 15
  3. lemma OAI.CubicFirstMoment.primeLogWindow_one line 18
  4. lemma OAI.CubicFirstMoment.primeLogWindow_zero_left line 25
  5. lemma OAI.CubicFirstMoment.primeLogWindow_zero_right line 38
  6. lemma OAI.CubicFirstMoment.primeLogWindow_support line 50
  7. lemma OAI.CubicFirstMoment.primeLogWindow_tsupport line 59
  8. lemma OAI.CubicFirstMoment.primeLogWindow_compact line 63
  9. def OAI.CubicFirstMoment.primeLogWindowSchwartz line 66
  10. lemma OAI.CubicFirstMoment.primeLogWindow_support_two line 69
  11. lemma OAI.CubicFirstMoment.primeLogWindow_derivative_bound line 78