OAI/Probability/SKGap/Localization/PhiAlgebra.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SKGap.Stein.KernelExpr line 13
  2. def OAI.SKGap.Stein.KernelExpr.eval line 22
  3. def OAI.SKGap.Stein.KernelExpr.mass line 29
  4. lemma OAI.SKGap.Stein.KernelExpr.mass_nonneg line 36
  5. lemma OAI.SKGap.Stein.KernelExpr.relative_bound line 39
  6. def OAI.SKGap.Stein.KernelExpr.dz line 59
  7. def OAI.SKGap.Stein.KernelExpr.dr line 66
  8. def OAI.SKGap.Stein.KernelExpr.da line 73
  9. lemma OAI.SKGap.Stein.KernelExpr.hasDerivAt_z line 80
  10. lemma OAI.SKGap.Stein.KernelExpr.hasDerivAt_r line 92
  11. lemma OAI.SKGap.Stein.KernelExpr.hasDerivAt_a line 104
  12. inductive OAI.SKGap.Stein.Axis line 115
  13. def OAI.SKGap.Stein.coordinateDeriv line 117
  14. def OAI.SKGap.Stein.mixed line 122
  15. def OAI.SKGap.Stein.KernelExpr.d line 128
  16. def OAI.SKGap.Stein.KernelExpr.mixedExpr line 131
  17. lemma OAI.SKGap.Stein.KernelExpr.partial_eval line 135
  18. lemma OAI.SKGap.Stein.KernelExpr.mixed_eval line 142
  19. theorem OAI.SKGap.Stein.KernelExpr.all_mixed_relative_bound line 147