OAI/Probability/Perceptron/Variational/StableMassKernel.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.stableMassKernel line 21
  2. instance OAI.SphericalPerceptronFreeEnergy.stableMassKernel_finite line 25
  3. def OAI.SphericalPerceptronFreeEnergy.stableCountKernel line 32
  4. instance OAI.SphericalPerceptronFreeEnergy.stableCountKernel_sFinite line 35
  5. lemma OAI.SphericalPerceptronFreeEnergy.stableCountKernel_eq line 38
  6. lemma OAI.SphericalPerceptronFreeEnergy.stableJumpMomentE_one_add_dirac line 64
  7. lemma OAI.SphericalPerceptronFreeEnergy.stableCountKernel_add_dirac line 68
  8. lemma OAI.SphericalPerceptronFreeEnergy.cascadeMeasurableSet_exists line 77
  9. lemma OAI.SphericalPerceptronFreeEnergy.measurable_fin_cons line 83
  10. def OAI.SphericalPerceptronFreeEnergy.stableDistinctMoment line 92
  11. lemma OAI.SphericalPerceptronFreeEnergy.stableDistinctMoment_measurable line 97
  12. lemma OAI.SphericalPerceptronFreeEnergy.stableDistinctMoment_add_dirac line 113
  13. instance OAI.SphericalPerceptronFreeEnergy.stableLogIntensity_noAtoms line 128
  14. lemma OAI.SphericalPerceptronFreeEnergy.stableDistinctMoment_palm_laplace line 132
  15. lemma OAI.SphericalPerceptronFreeEnergy.stableLaplaceProduct_shape line 194
  16. lemma OAI.SphericalPerceptronFreeEnergy.list_length_mul_le_sum line 219
  17. lemma OAI.SphericalPerceptronFreeEnergy.stableDistinctMoment_palm_mellin_mul line 229
  18. lemma OAI.SphericalPerceptronFreeEnergy.gamma_stable_product line 298
  19. lemma OAI.SphericalPerceptronFreeEnergy.stable_eppf_scalar line 317
  20. lemma OAI.SphericalPerceptronFreeEnergy.list_prod_map_const_mul line 340
  21. lemma OAI.SphericalPerceptronFreeEnergy.list_prod_map_div_const line 346
  22. lemma OAI.SphericalPerceptronFreeEnergy.list_prod_ofReal line 350
  23. theorem OAI.SphericalPerceptronFreeEnergy.stableDistinctMoment_eppf line 358
  24. def OAI.SphericalPerceptronFreeEnergy.stableEppfValue line 418