OAI/Probability/Perceptron/Cascade/StableCascade.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.StableCascade line 20
  2. instance OAI.SphericalPerceptronFreeEnergy.stableCascadeNonempty line 24
  3. def OAI.SphericalPerceptronFreeEnergy.cascadeTotalE line 29
  4. lemma OAI.SphericalPerceptronFreeEnergy.cascadeTotalE_measurable line 34
  5. def OAI.SphericalPerceptronFreeEnergy.cascadeTotal line 41
  6. lemma OAI.SphericalPerceptronFreeEnergy.cascadeTotal_measurable line 43
  7. def OAI.SphericalPerceptronFreeEnergy.cascadeLaw line 46
  8. lemma OAI.SphericalPerceptronFreeEnergy.poissonWeightedTotal_identDistrib line 51
  9. lemma OAI.SphericalPerceptronFreeEnergy.poissonWeightedTotal_pos line 63
  10. lemma OAI.SphericalPerceptronFreeEnergy.poissonWeightedTotal_rpow_integrable line 72
  11. lemma OAI.SphericalPerceptronFreeEnergy.poissonRandomMeasureLaw_ae_ae line 87
  12. lemma OAI.SphericalPerceptronFreeEnergy.cascadeTotal_succ_eq line 93
  13. theorem OAI.SphericalPerceptronFreeEnergy.cascadeTotal_regular line 116
  14. lemma OAI.SphericalPerceptronFreeEnergy.lintegral_comp_exp_all line 149
  15. lemma OAI.SphericalPerceptronFreeEnergy.stableLogIntensity_laplace_moment line 156
  16. lemma OAI.SphericalPerceptronFreeEnergy.one_sub_exp_neg_lintegral line 189
  17. lemma OAI.SphericalPerceptronFreeEnergy.lintegral_rpow_unit line 206
  18. lemma OAI.SphericalPerceptronFreeEnergy.stableLaplaceConstant_eq_gamma line 216
  19. lemma OAI.SphericalPerceptronFreeEnergy.stablePoissonTotal_add_dirac line 243
  20. lemma OAI.SphericalPerceptronFreeEnergy.stablePoissonTotal_laplace_lintegral line 250
  21. lemma OAI.SphericalPerceptronFreeEnergy.stablePoisson_palm_laplace line 266
  22. lemma OAI.SphericalPerceptronFreeEnergy.gamma_lintegral_rpow_scale line 297
  23. def OAI.SphericalPerceptronFreeEnergy.stableJumpMomentE line 305
  24. lemma OAI.SphericalPerceptronFreeEnergy.stableJumpMomentE_measurable line 308
  25. lemma OAI.SphericalPerceptronFreeEnergy.stablePoisson_palm_laplace' line 311
  26. lemma OAI.SphericalPerceptronFreeEnergy.stablePoisson_palm_mellin_mul line 321
  27. lemma OAI.SphericalPerceptronFreeEnergy.stablePoissonTotal_rpow_lintegral_mul line 379
  28. lemma OAI.SphericalPerceptronFreeEnergy.stablePoissonTotal_rpow_integral line 405