OAI/Probability/SphericalField/Poisson/RandomMeasure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.poissonRandomMeasureLaw_laplace line 17
  2. lemma OAI.SphericalPerceptron.poissonLaplace_map line 25
  3. lemma OAI.SphericalPerceptron.poissonRandomMeasureLaw_map line 31
  4. lemma OAI.SphericalPerceptron.stableLogDensity_translate line 46
  5. lemma OAI.SphericalPerceptron.stableLogIntensity_lintegral_translate line 55
  6. lemma OAI.SphericalPerceptron.stableLogIntensity_translate line 78
  7. def OAI.SphericalPerceptron.logMarkShift line 86
  8. lemma OAI.SphericalPerceptron.logMarkShift_measurable line 89
  9. lemma OAI.SphericalPerceptron.stableLogIntensity_mark_shift line 93
  10. lemma OAI.SphericalPerceptron.stablePoisson_mark_shift line 111
  11. lemma OAI.SphericalPerceptron.poissonMeasure_atom_succ line 121
  12. lemma OAI.SphericalPerceptron.poissonMeasure_mean line 135