OAI/Probability/SKGap/Localization/PhiFrechet.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKGap.Stein.Triple line 14
  2. def OAI.SKGap.Stein.eval3 line 15
  3. def OAI.SKGap.Stein.grad2 line 17
  4. def OAI.SKGap.Stein.grad3 line 19
  5. lemma OAI.SKGap.Stein.grad2_eq line 22
  6. lemma OAI.SKGap.Stein.grad3_eq line 25
  7. lemma OAI.SKGap.Stein.continuous_grad2 line 30
  8. lemma OAI.SKGap.Stein.continuous_grad3 line 32
  9. lemma OAI.SKGap.Stein.hasFDerivAt_of_three_partials line 35
  10. lemma OAI.SKGap.Stein.continuous_momentNum line 64
  11. lemma OAI.SKGap.Stein.continuous_moment line 72
  12. lemma OAI.SKGap.Stein.continuous_tanh line 79
  13. lemma OAI.SKGap.Stein.KernelExpr.continuous_eval line 83
  14. def OAI.SKGap.Stein.KernelExpr.gradient line 91
  15. lemma OAI.SKGap.Stein.KernelExpr.hasFDerivAt_eval line 94
  16. lemma OAI.SKGap.Stein.grad3_norm line 101
  17. lemma OAI.SKGap.Stein.grad3_sub line 118
  18. def OAI.SKGap.Stein.strip line 125
  19. lemma OAI.SKGap.Stein.convex_strip line 126
  20. lemma OAI.SKGap.Stein.KernelExpr.absolute_bound line 136
  21. def OAI.SKGap.Stein.KernelExpr.dBudget line 141
  22. lemma OAI.SKGap.Stein.KernelExpr.dBudget_nonneg line 143
  23. lemma OAI.SKGap.Stein.KernelExpr.gradient_bound line 147
  24. lemma OAI.SKGap.Stein.KernelExpr.lipschitz_strip line 153
  25. def OAI.SKGap.Stein.KernelExpr.ddBudget line 160
  26. lemma OAI.SKGap.Stein.KernelExpr.ddBudget_nonneg line 162
  27. lemma OAI.SKGap.Stein.KernelExpr.gradient_lipschitz line 165
  28. lemma OAI.SKGap.Stein.RatioExpr.continuous_eval line 175
  29. def OAI.SKGap.Stein.RatioExpr.gradient line 185
  30. lemma OAI.SKGap.Stein.RatioExpr.hasFDerivAt_eval line 187
  31. def OAI.SKGap.Stein.RatioExpr.dBudget line 193
  32. lemma OAI.SKGap.Stein.RatioExpr.gradient_bound line 194
  33. lemma OAI.SKGap.Stein.RatioExpr.lipschitz_global line 197
  34. def OAI.SKGap.Stein.RatioExpr.ddBudget line 202
  35. lemma OAI.SKGap.Stein.RatioExpr.gradient_lipschitz line 203