OAI/Probability/SKGap/Gaussian/SquareTail.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.gaussian_exp_quadratic_integrable line 35
  2. def OAI.SKGap.squareTail line 60
  3. lemma OAI.SKGap.measurable_squareTail line 62
  4. lemma OAI.SKGap.squareTail_nonneg line 67
  5. lemma OAI.SKGap.squareTail_le line 71
  6. lemma OAI.SKGap.tendsto_squareTail line 75
  7. lemma OAI.SKGap.tendsto_gaussian_tail_tilt line 80
  8. lemma OAI.SKGap.integrable_gaussian_tail_test line 103
  9. lemma OAI.SKGap.product_general_test_integrable line 114
  10. lemma OAI.SKGap.product_general_test_integral line 121
  11. theorem OAI.SKGap.gaussian_covered_tail_laplace line 139