OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Box.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCauchyTail.box line 18
  2. def OAI.OrdinaryCauchyTail.cauchy line 20
  3. def OAI.OrdinaryCauchyTail.tailWeight line 22
  4. lemma OAI.OrdinaryCauchyTail.box_nonneg line 24
  5. lemma OAI.OrdinaryCauchyTail.box_integrable line 25
  6. lemma OAI.OrdinaryCauchyTail.cauchy_nonneg line 27
  7. lemma OAI.OrdinaryCauchyTail.cauchy_integrable line 28
  8. lemma OAI.OrdinaryCauchyTail.measurable_tail line 29
  9. lemma OAI.OrdinaryCauchyTail.tail_nonneg line 30
  10. lemma OAI.OrdinaryCauchyTail.tail_integrable line 31
  11. lemma OAI.OrdinaryCauchyTail.box_shift_integral line 33
  12. lemma OAI.OrdinaryCauchyTail.box_reflect_integral line 42
  13. lemma OAI.OrdinaryCauchyTail.cauchy_close line 51
  14. lemma OAI.OrdinaryCauchyTail.tail_close line 59
  15. lemma OAI.OrdinaryCauchyTail.tail_convolution_lower line 72
  16. theorem OAI.OrdinaryCauchyTail.tail_bound line 84
  17. lemma OAI.OrdinaryCauchyTail.tendsto_tail_integral line 115
  18. lemma OAI.OrdinaryCauchyTail.cauchy_le_one line 131
  19. lemma OAI.OrdinaryCauchyTail.tail_decomposition line 135
  20. theorem OAI.OrdinaryCauchyTail.small_of_compact line 151