OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/BoxAddWidth.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OrdinarySharpWindow.box_add_width line 23
  2. lemma OAI.OrdinarySharpWindow.sharpWindow_width_add line 45
  3. lemma OAI.OrdinarySharpWindow.sharpWindow_width_subadditive line 57
  4. lemma OAI.OrdinarySharpWindow.sharpWindow_width_nat_mul line 75
  5. lemma OAI.OrdinarySharpWindow.sharpWindow_l1_mass line 91
  6. lemma OAI.OrdinarySharpWindow.sharpWindow_long_from_short line 107