OAI/Probability/SKGap/Localization/PhiRatio.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SKGap.Stein.RatioExpr line 11
  2. def OAI.SKGap.Stein.RatioExpr.eval line 18
  3. def OAI.SKGap.Stein.RatioExpr.mass line 24
  4. lemma OAI.SKGap.Stein.RatioExpr.mass_nonneg line 30
  5. lemma OAI.SKGap.Stein.RatioExpr.bounded line 37
  6. def OAI.SKGap.Stein.RatioExpr.d line 50
  7. lemma OAI.SKGap.Stein.RatioExpr.kernel_deriv_z line 57
  8. lemma OAI.SKGap.Stein.RatioExpr.kernel_deriv_r line 67
  9. lemma OAI.SKGap.Stein.RatioExpr.kernel_deriv_a line 77
  10. lemma OAI.SKGap.Stein.RatioExpr.hasDerivAt_z line 87
  11. lemma OAI.SKGap.Stein.RatioExpr.hasDerivAt_r line 95
  12. lemma OAI.SKGap.Stein.RatioExpr.hasDerivAt_a line 103
  13. lemma OAI.SKGap.Stein.RatioExpr.partial_eval line 111
  14. def OAI.SKGap.Stein.RatioExpr.mixedExpr line 118
  15. lemma OAI.SKGap.Stein.RatioExpr.mixed_eval line 122
  16. theorem OAI.SKGap.Stein.RatioExpr.all_mixed_ratio_bounded line 127