OAI/Probability/Perceptron/Cavity/BulkModel.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.bulkScale line 11
  2. def OAI.SphericalPerceptronFreeEnergy.bulkDegree line 12
  3. abbrev OAI.SphericalPerceptronFreeEnergy.BulkMark line 13
  4. def OAI.SphericalPerceptronFreeEnergy.bulkAmplitude line 15
  5. def OAI.SphericalPerceptronFreeEnergy.bulkFeature line 18
  6. def OAI.SphericalPerceptronFreeEnergy.bulkCovariance line 21
  7. def OAI.SphericalPerceptronFreeEnergy.bulkHamiltonian line 24
  8. def OAI.SphericalPerceptronFreeEnergy.bulkLogPartition line 28
  9. def OAI.SphericalPerceptronFreeEnergy.bulkDisorderLaw line 33
  10. instance OAI.SphericalPerceptronFreeEnergy.bulkDisorderLaw_probability line 36
  11. def OAI.SphericalPerceptronFreeEnergy.bulkExpectedLog line 40
  12. def OAI.SphericalPerceptronFreeEnergy.bulkB line 43
  13. def OAI.SphericalPerceptronFreeEnergy.bulkC line 47
  14. lemma OAI.SphericalPerceptronFreeEnergy.bulkFeature_continuous line 52
  15. lemma OAI.SphericalPerceptronFreeEnergy.bulkFeature_inner line 55
  16. lemma OAI.SphericalPerceptronFreeEnergy.bulkFeature_norm_sq line 65
  17. lemma OAI.SphericalPerceptronFreeEnergy.bulkLogPartition_eq line 70
  18. lemma OAI.SphericalPerceptronFreeEnergy.bulkB_bound line 77
  19. abbrev OAI.SphericalPerceptronFreeEnergy.BulkDisorder line 90
  20. def OAI.SphericalPerceptronFreeEnergy.bulkFeatureBound line 92
  21. lemma OAI.SphericalPerceptronFreeEnergy.bulkFeature_norm line 94
  22. lemma OAI.SphericalPerceptronFreeEnergy.bulkHamiltonian_continuous line 99
  23. lemma OAI.SphericalPerceptronFreeEnergy.bulkHamiltonian_bound line 107
  24. lemma OAI.SphericalPerceptronFreeEnergy.bulkHamiltonian_exp_integrable line 114
  25. def OAI.SphericalPerceptronFreeEnergy.bulkSpinKernel line 125
  26. instance OAI.SphericalPerceptronFreeEnergy.bulkSpinKernel_markov line 128
  27. def OAI.SphericalPerceptronFreeEnergy.bulkOverlap line 131
  28. lemma OAI.SphericalPerceptronFreeEnergy.bulkOverlap_measurable line 134
  29. def OAI.SphericalPerceptronFreeEnergy.bulkGibbsArrayLaw line 138
  30. lemma OAI.SphericalPerceptronFreeEnergy.bulkGibbsArray_block line 144