OAI/Probability/Perceptron/Variational/MarkedTotalBiasedLaw.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.markedDistinctMoment_add_dirac line 23
  2. lemma OAI.SphericalPerceptronFreeEnergy.markedDistinctMoment_palm_laplace line 51
  3. lemma OAI.SphericalPerceptronFreeEnergy.markedDistinctMoment_laplace_factor line 129
  4. lemma OAI.SphericalPerceptronFreeEnergy.mellin_weighted_identity line 145
  5. lemma OAI.SphericalPerceptronFreeEnergy.markedDistinctMoment_mellin_factor line 170
  6. def OAI.SphericalPerceptronFreeEnergy.markedTotalBiasedLaw line 215
  7. lemma OAI.SphericalPerceptronFreeEnergy.markedStableTotal_momentE line 219
  8. lemma OAI.SphericalPerceptronFreeEnergy.markedTotalBiasedLaw_probability line 226
  9. def OAI.SphericalPerceptronFreeEnergy.markedOrderedDistinctMass line 244
  10. lemma OAI.SphericalPerceptronFreeEnergy.markedOrderedDistinctMass_measurable line 248
  11. lemma OAI.SphericalPerceptronFreeEnergy.markedOrderedDistinctMass_biased line 253
  12. lemma OAI.SphericalPerceptronFreeEnergy.markedOrderedDistinctMass_eppf line 275
  13. lemma OAI.SphericalPerceptronFreeEnergy.normalizedMeasure_map line 291
  14. lemma OAI.SphericalPerceptronFreeEnergy.markedStableMassKernel_projection line 298
  15. def OAI.SphericalPerceptronFreeEnergy.markedBlockProbability line 305
  16. lemma OAI.SphericalPerceptronFreeEnergy.markedBlockProbability_measurable line 312
  17. lemma OAI.SphericalPerceptronFreeEnergy.markedBlockProbability_moment line 332
  18. lemma OAI.SphericalPerceptronFreeEnergy.markedBlockProbability_ordered line 388
  19. lemma OAI.SphericalPerceptronFreeEnergy.markedTotalBiasedLaw_absolutelyContinuous line 402
  20. lemma OAI.SphericalPerceptronFreeEnergy.markedBlockProbability_factor line 406
  21. lemma OAI.SphericalPerceptronFreeEnergy.markedStableTotal_map_shift line 438