OAI/Probability/SphericalField/Poisson/Intensity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.poisson_power_integral line 16
  2. def OAI.SphericalPerceptron.expNegENNReal line 34
  3. lemma OAI.SphericalPerceptron.expNegENNReal_bound line 36
  4. lemma OAI.SphericalPerceptron.expNegENNReal_continuous line 41
  5. lemma OAI.SphericalPerceptron.expNegENNReal_finite line 50
  6. lemma OAI.SphericalPerceptron.expNegENNReal_top line 56
  7. def OAI.SphericalPerceptron.poissonLaplace line 58
  8. lemma OAI.SphericalPerceptron.poissonLaplace_measurable line 61
  9. lemma OAI.SphericalPerceptron.poissonLaplace_bounds line 65
  10. lemma OAI.SphericalPerceptron.poissonLaplace_finitePointMeasure line 69
  11. lemma OAI.SphericalPerceptron.finitePoissonLaw_laplace line 79
  12. lemma OAI.SphericalPerceptron.expNegENNReal_zero line 103
  13. lemma OAI.SphericalPerceptron.expNegENNReal_add line 105
  14. lemma OAI.SphericalPerceptron.expNegENNReal_sum line 115