OAI/NumberTheory/CubicMoment/Decomposition/StoppedProductProfile.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A fixed Schwartz function localized in a genuine dyadic height window. The normalized profile and its scaled second derivative decay like 1/T.

  1. lemma OAI.CubicFirstMoment.heightWindow_compact line 12
  2. def OAI.CubicFirstMoment.heightWindowSchwartz line 21
  3. def OAI.CubicFirstMoment.schwartzHeightWindow line 24
  4. lemma OAI.CubicFirstMoment.schwartzHeightWindow_smooth line 27
  5. lemma OAI.CubicFirstMoment.schwartzHeightWindow_zero line 31
  6. lemma OAI.CubicFirstMoment.schwartzHeightWindow_tsupport line 35
  7. lemma OAI.CubicFirstMoment.schwartzHeightWindow_compact line 42
  8. lemma OAI.CubicFirstMoment.schwartzHeightWindow_derivatives line 47
  9. lemma OAI.CubicFirstMoment.schwartzHeightWindow_second_zero line 61
  10. lemma OAI.CubicFirstMoment.schwartzHeightWindow_norm_bound line 68
  11. lemma OAI.CubicFirstMoment.heightWindow_iteratedDeriv_bound line 88
  12. lemma OAI.CubicFirstMoment.schwartz_derivative_on_height line 102
  13. lemma OAI.CubicFirstMoment.schwartzHeightWindow_second_bound line 113