OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/BumpMass.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryGaussianWindow.bumpMass line 25
  2. def OAI.OrdinaryGaussianWindow.bumpMoment line 26
  3. def OAI.OrdinaryGaussianWindow.dilateKernel line 27
  4. lemma OAI.OrdinaryGaussianWindow.bump_nonneg line 29
  5. lemma OAI.OrdinaryGaussianWindow.bump_integrable line 31
  6. lemma OAI.OrdinaryGaussianWindow.bumpMoment_integrable line 34
  7. lemma OAI.OrdinaryGaussianWindow.bumpMass_pos line 41
  8. lemma OAI.OrdinaryGaussianWindow.bumpMoment_nonneg line 46
  9. lemma OAI.OrdinaryGaussianWindow.dilateKernel_integrable line 49
  10. lemma OAI.OrdinaryGaussianWindow.dilateKernel_mass line 54
  11. lemma OAI.OrdinaryGaussianWindow.dilateKernel_moment_eq line 60
  12. lemma OAI.OrdinaryGaussianWindow.dilateKernel_moment_integrable line 66
  13. lemma OAI.OrdinaryGaussianWindow.dilateKernel_moment line 74
  14. lemma OAI.OrdinaryGaussianWindow.scaledWindow_square_integrable line 85
  15. lemma OAI.OrdinaryGaussianWindow.kernelWindow_dilate line 93
  16. lemma OAI.OrdinaryGaussianWindow.scaledWindow_l1_concentration line 96