OAI/Probability/Perceptron/Variational/FixedCount.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptronFreeEnergy.SourceCountData line 13
  2. def OAI.SphericalPerceptronFreeEnergy.sourceCountLaw line 15
  3. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 18) line 18
  4. def OAI.SphericalPerceptronFreeEnergy.sourceCountEmbedding line 22
  5. lemma OAI.SphericalPerceptronFreeEnergy.sourceCountEmbedding_measurable line 25
  6. def OAI.SphericalPerceptronFreeEnergy.sourceCountKernel line 29
  7. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 31) line 31
  8. lemma OAI.SphericalPerceptronFreeEnergy.sourceCountKernel_apply line 35
  9. def OAI.SphericalPerceptronFreeEnergy.sourceCountHamiltonian line 40
  10. lemma OAI.SphericalPerceptronFreeEnergy.sourceCountHamiltonian_measurable line 44
  11. def OAI.SphericalPerceptronFreeEnergy.sourceCountLog line 57
  12. lemma OAI.SphericalPerceptronFreeEnergy.sourceCountLog_ae line 61
  13. lemma OAI.SphericalPerceptronFreeEnergy.sourceCountLog_memLp line 74
  14. lemma OAI.SphericalPerceptronFreeEnergy.sourceCountExpectedLog_eq line 85
  15. lemma OAI.SphericalPerceptronFreeEnergy.sourceCount_exp_ae line 100
  16. lemma OAI.SphericalPerceptronFreeEnergy.sourceCountHamiltonian_succ line 128
  17. lemma OAI.SphericalPerceptronFreeEnergy.sourceCountLog_succ line 138
  18. lemma OAI.SphericalPerceptronFreeEnergy.sourceCountFreshLog_prefix line 155
  19. lemma OAI.SphericalPerceptronFreeEnergy.sourceCountExpectedLog_fresh line 166