OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/BoxNonneg.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinarySharpWindow.box line 23
  2. lemma OAI.OrdinarySharpWindow.box_nonneg line 25
  3. lemma OAI.OrdinarySharpWindow.box_le_one line 29
  4. lemma OAI.OrdinarySharpWindow.box_integrable line 33
  5. lemma OAI.OrdinarySharpWindow.box_integral line 37
  6. lemma OAI.OrdinarySharpWindow.box_translation_pointwise line 42
  7. lemma OAI.OrdinarySharpWindow.box_translation_l1_nonneg line 73
  8. lemma OAI.OrdinarySharpWindow.box_translation_l1 line 86
  9. def OAI.OrdinarySharpWindow.sharpWindow line 101
  10. lemma OAI.OrdinarySharpWindow.sharpWindow_integrable line 104
  11. lemma OAI.OrdinarySharpWindow.sharpWindow_translation_l1 line 111