OAI/Probability/Perceptron/Cascade/PoissonLaplace.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.expNegENNReal_finite line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.expNegENNReal_top line 20
  3. def OAI.SphericalPerceptronFreeEnergy.poissonLaplace line 22
  4. lemma OAI.SphericalPerceptronFreeEnergy.poissonLaplace_measurable line 25
  5. lemma OAI.SphericalPerceptronFreeEnergy.poissonLaplace_bounds line 29
  6. lemma OAI.SphericalPerceptronFreeEnergy.poissonLaplace_finitePointMeasure line 33
  7. lemma OAI.SphericalPerceptronFreeEnergy.finitePoissonLaw_laplace line 43
  8. lemma OAI.SphericalPerceptronFreeEnergy.expNegENNReal_zero line 68
  9. lemma OAI.SphericalPerceptronFreeEnergy.expNegENNReal_add line 70
  10. lemma OAI.SphericalPerceptronFreeEnergy.expNegENNReal_sum line 80
  11. lemma OAI.SphericalPerceptronFreeEnergy.measureSum_measurable line 87
  12. lemma OAI.SphericalPerceptronFreeEnergy.poissonLaplace_finsetSum line 94
  13. lemma OAI.SphericalPerceptronFreeEnergy.poissonLaplace_sum_tendsto line 99
  14. def OAI.SphericalPerceptronFreeEnergy.countablePoissonLaw line 107
  15. instance OAI.SphericalPerceptronFreeEnergy.countablePoissonLaw_probability line 111
  16. lemma OAI.SphericalPerceptronFreeEnergy.finitePoissonLaw_laplace_nonneg line 117
  17. lemma OAI.SphericalPerceptronFreeEnergy.countablePoissonLaw_laplace line 138
  18. lemma OAI.SphericalPerceptronFreeEnergy.measure_eq_of_additive_test_family line 185
  19. lemma OAI.SphericalPerceptronFreeEnergy.expNegENNReal_injective line 234
  20. def OAI.SphericalPerceptronFreeEnergy.laplaceTest line 243
  21. lemma OAI.SphericalPerceptronFreeEnergy.laplaceTest_zero line 250
  22. lemma OAI.SphericalPerceptronFreeEnergy.laplaceTest_add line 255
  23. lemma OAI.SphericalPerceptronFreeEnergy.laplaceTest_separates line 262
  24. lemma OAI.SphericalPerceptronFreeEnergy.measure_eq_of_laplace_tests line 271
  25. lemma OAI.SphericalPerceptronFreeEnergy.measure_eq_of_map_eq_comap line 277
  26. lemma OAI.SphericalPerceptronFreeEnergy.measureLaw_eval_comap line 286
  27. lemma OAI.SphericalPerceptronFreeEnergy.laplaceTest_eval_eq line 302
  28. lemma OAI.SphericalPerceptronFreeEnergy.measureLaw_eq_of_laplace line 320
  29. def OAI.SphericalPerceptronFreeEnergy.countablePoissonIntensity line 350
  30. lemma OAI.SphericalPerceptronFreeEnergy.countablePoissonLaw_laplace_intensity line 354
  31. def OAI.SphericalPerceptronFreeEnergy.finiteIntensityMarks line 377
  32. instance OAI.SphericalPerceptronFreeEnergy.finiteIntensityMarks_probability line 380
  33. lemma OAI.SphericalPerceptronFreeEnergy.finiteIntensityMarks_smul line 388
  34. def OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw line 397
  35. instance OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_probability line 402
  36. lemma OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_laplace line 407