OAI/Probability/SKGap/Gaussian/PhiStein.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.Stein.hasDerivAt_integral01 line 13
  2. def OAI.SKGap.Stein.weight line 35
  3. def OAI.SKGap.Stein.numerator line 36
  4. def OAI.SKGap.Stein.numeratorZ line 37
  5. def OAI.SKGap.Stein.phi line 38
  6. def OAI.SKGap.Stein.phiZ line 40
  7. lemma OAI.SKGap.Stein.continuous_weight line 42
  8. lemma OAI.SKGap.Stein.phi_eq line 44
  9. lemma OAI.SKGap.Stein.numerator_hasDerivAt line 47
  10. lemma OAI.SKGap.Stein.phi_hasDerivAt line 59
  11. lemma OAI.SKGap.Stein.weight_hasDerivAt line 68
  12. lemma OAI.SKGap.Stein.boundary_hasDerivAt line 75
  13. lemma OAI.SKGap.Stein.numerator_boundary line 83
  14. theorem OAI.SKGap.Stein.phi_stein line 102
  15. lemma OAI.SKGap.Stein.phi_pos line 113
  16. lemma OAI.SKGap.Stein.phiZ_at_diagonal line 122
  17. lemma OAI.SKGap.Stein.phi_stein_deriv line 125