OAI/Probability/Perceptron/Cavity/BulkLimitGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.bulkJointEmbedding line 15
  2. lemma OAI.SphericalPerceptronFreeEnergy.bulkJointEmbedding_continuous line 16
  3. def OAI.SphericalPerceptronFreeEnergy.bulkJointLaw line 19
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulkGibbsArray_exchangeable line 23
  5. lemma OAI.SphericalPerceptronFreeEnergy.bulkGibbsArray_closed_full line 28
  6. lemma OAI.SphericalPerceptronFreeEnergy.compact_scalar_gram_closed line 34
  7. lemma OAI.SphericalPerceptronFreeEnergy.bulkGibbsArray_limit_gram line 38
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulkGibbsArray_limit_diagonal line 51
  9. lemma OAI.SphericalPerceptronFreeEnergy.bulkJointLaw_gram line 65
  10. lemma OAI.SphericalPerceptronFreeEnergy.bulkJointLaw_diagonal line 77
  11. lemma OAI.SphericalPerceptronFreeEnergy.omitted_bulk_limit_geometry line 86
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulkJointLaw_scalarGram_integral line 105
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulk_pair_restoration_ratio_tendsto line 112