OAI/Probability/Perceptron/Cavity/CavityBulkCoefficients.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptronFreeEnergy.CavityBulkNoiseIndex line 11
  2. def OAI.SphericalPerceptronFreeEnergy.cavityBulkBase line 14
  3. def OAI.SphericalPerceptronFreeEnergy.cavityBulkFeature line 21
  4. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkFeature_measurable line 26
  5. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkFeature_inner line 39
  6. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkFeature_gram line 89
  7. lemma OAI.SphericalPerceptronFreeEnergy.cavity_gibbs_moment line 98
  8. def OAI.SphericalPerceptronFreeEnergy.cavityBulkPartition line 115
  9. lemma OAI.SphericalPerceptronFreeEnergy.cavity_rows_joint_measurable line 120
  10. lemma OAI.SphericalPerceptronFreeEnergy.cavity_partition_joint_measurable line 132
  11. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkPartition_measurable line 147
  12. def OAI.SphericalPerceptronFreeEnergy.cavityBulkMoment line 154
  13. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkMoment_array line 158
  14. theorem OAI.SphericalPerceptronFreeEnergy.cavityBulkMoment_tendsto line 194