OAI/Probability/Perceptron/Variational/StableTotalBiasedLaw.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.stableEppfValue_singleton_one line 21
  2. lemma OAI.SphericalPerceptronFreeEnergy.stableEppfValue_join line 27
  3. lemma OAI.SphericalPerceptronFreeEnergy.stableEppfValue_new line 40
  4. def OAI.SphericalPerceptronFreeEnergy.stableTotalBiasedLaw line 57
  5. lemma OAI.SphericalPerceptronFreeEnergy.stableTotalBias_mass line 61
  6. lemma OAI.SphericalPerceptronFreeEnergy.stableTotalBiasedLaw_probability line 70
  7. def OAI.SphericalPerceptronFreeEnergy.stableOrderedDistinctMass line 81
  8. lemma OAI.SphericalPerceptronFreeEnergy.stableOrderedDistinctMass_measurable line 84
  9. lemma OAI.SphericalPerceptronFreeEnergy.stableOrderedDistinctMass_biased line 88
  10. lemma OAI.SphericalPerceptronFreeEnergy.stableOrderedDistinctMass_eppf line 109
  11. lemma OAI.SphericalPerceptronFreeEnergy.stableCountAtom_measurable line 118
  12. lemma OAI.SphericalPerceptronFreeEnergy.stablePoissonCount_simple line 131
  13. lemma OAI.SphericalPerceptronFreeEnergy.stableMassKernel_atom_eq line 164
  14. lemma OAI.SphericalPerceptronFreeEnergy.stableMassAtom_measurable line 175
  15. lemma OAI.SphericalPerceptronFreeEnergy.stableMassAtom_measurable_comp line 188
  16. def OAI.SphericalPerceptronFreeEnergy.stableBlockProbability line 194
  17. lemma OAI.SphericalPerceptronFreeEnergy.stableBlockProbability_measurable line 199
  18. lemma OAI.SphericalPerceptronFreeEnergy.stableBlockProbability_moment line 217
  19. lemma OAI.SphericalPerceptronFreeEnergy.stableTotalBiasedLaw_absolutelyContinuous line 266
  20. lemma OAI.SphericalPerceptronFreeEnergy.stableBlockProbability_ordered line 270
  21. lemma OAI.SphericalPerceptronFreeEnergy.stableBlockProbability_eppf line 284
  22. def OAI.SphericalPerceptronFreeEnergy.markedStableTotalE line 307
  23. lemma OAI.SphericalPerceptronFreeEnergy.markedStableTotalE_measurable line 310
  24. def OAI.SphericalPerceptronFreeEnergy.markedStableTotal line 313
  25. lemma OAI.SphericalPerceptronFreeEnergy.markedStableTotal_measurable line 315
  26. lemma OAI.SphericalPerceptronFreeEnergy.markedStableTotalE_projection line 318
  27. lemma OAI.SphericalPerceptronFreeEnergy.markedStableTotal_projection line 323
  28. def OAI.SphericalPerceptronFreeEnergy.markedStableMassKernel line 327
  29. instance OAI.SphericalPerceptronFreeEnergy.markedStableMassKernel_finite line 331
  30. def OAI.SphericalPerceptronFreeEnergy.markedStableCountKernel line 338
  31. instance OAI.SphericalPerceptronFreeEnergy.markedStableCountKernel_sfinite line 341
  32. lemma OAI.SphericalPerceptronFreeEnergy.markedStableCountKernel_eq line 344
  33. lemma OAI.SphericalPerceptronFreeEnergy.markedStableTotalE_add_dirac line 370
  34. lemma OAI.SphericalPerceptronFreeEnergy.markedStableTotal_add_dirac line 375
  35. lemma OAI.SphericalPerceptronFreeEnergy.markedStableCountKernel_add_dirac line 382
  36. lemma OAI.SphericalPerceptronFreeEnergy.markedStable_project_law line 390
  37. lemma OAI.SphericalPerceptronFreeEnergy.markedStable_regular line 396
  38. lemma OAI.SphericalPerceptronFreeEnergy.markedStable_laplace line 407
  39. def OAI.SphericalPerceptronFreeEnergy.markedDistinctMoment line 417
  40. lemma OAI.SphericalPerceptronFreeEnergy.markedDistinctMoment_measurable line 424