OAI/Probability/SKGap/Gaussian/PhiMoments.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.Stein.hyper line 12
  2. lemma OAI.SKGap.Stein.continuous_hyper line 13
  3. lemma OAI.SKGap.Stein.hyper_hasDerivAt line 14
  4. lemma OAI.SKGap.Stein.hyper_abs_le line 18
  5. def OAI.SKGap.Stein.momentNum line 23
  6. def OAI.SKGap.Stein.moment line 26
  7. lemma OAI.SKGap.Stein.moment_base line 29
  8. lemma OAI.SKGap.Stein.momentNum_hasDerivAt_d line 33
  9. lemma OAI.SKGap.Stein.momentNum_hasDerivAt_a line 52
  10. lemma OAI.SKGap.Stein.momentNum_abs_le line 69
  11. lemma OAI.SKGap.Stein.moment_relative_bound line 101
  12. lemma OAI.SKGap.Stein.moment_hasDerivAt_z line 107
  13. lemma OAI.SKGap.Stein.moment_hasDerivAt_r line 118
  14. lemma OAI.SKGap.Stein.moment_hasDerivAt_a line 129