OAI/Probability/FreeIsing/Gaussian/SmallBall.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.gaussianPDFReal_le_peak line 11
  2. theorem OAI.Problem367.gaussianReal_le_peak_mul_volume line 22
  3. theorem OAI.Problem367.gaussianReal_Icc_le line 34
  4. theorem OAI.Problem367.gaussianReal_abs_le line 42
  5. theorem OAI.Problem367.gaussianReal_abs_le_of_variance_ge line 53
  6. def OAI.Problem367.gaussianSmallRadius line 69
  7. lemma OAI.Problem367.gaussianSmallRadius_pos line 72
  8. lemma OAI.Problem367.gaussianReal_smallBall_le_half line 77
  9. theorem OAI.Problem367.smallBall_le_half_of_hasGaussianLaw line 95
  10. theorem OAI.Problem367.integral_le_one_sub_half_gap line 104
  11. theorem OAI.Problem367.integral_gaussian_le_one_sub_half_gap line 133