OAI/Probability/SphericalField/Cascade/MarkedStable.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.markedStableTotalE_projection line 27
  2. lemma OAI.SphericalPerceptron.markedStableTotal_projection line 32
  3. instance OAI.SphericalPerceptron.markedStableCountKernel_sfinite line 36
  4. lemma OAI.SphericalPerceptron.markedStableCountKernel_eq line 39
  5. lemma OAI.SphericalPerceptron.markedStableTotalE_add_dirac line 65
  6. lemma OAI.SphericalPerceptron.markedStableTotal_add_dirac line 70
  7. lemma OAI.SphericalPerceptron.markedStableCountKernel_add_dirac line 77
  8. lemma OAI.SphericalPerceptron.markedStable_project_law line 85
  9. lemma OAI.SphericalPerceptron.markedStable_regular line 91
  10. lemma OAI.SphericalPerceptron.markedStable_laplace line 102
  11. def OAI.SphericalPerceptron.markedDistinctMoment line 112
  12. lemma OAI.SphericalPerceptron.markedDistinctMoment_measurable line 119
  13. lemma OAI.SphericalPerceptron.markedDistinctMoment_add_dirac line 139
  14. lemma OAI.SphericalPerceptron.markedDistinctMoment_palm_laplace line 167