OAI/Probability/Perceptron/Cavity/BulkRestorationLimit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.twoFreshDisorderLaw line 12
  2. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 15) line 15
  3. def OAI.SphericalPerceptronFreeEnergy.bulkFreshCompactDenominator line 19
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulkFreshCompactDenominator_measurable line 22
  5. lemma OAI.SphericalPerceptronFreeEnergy.bulkFreshNumerator_integrable line 26
  6. lemma OAI.SphericalPerceptronFreeEnergy.bulkFresh_weighted_integrable line 35
  7. lemma OAI.SphericalPerceptronFreeEnergy.bulkFresh_annealed_polynomial line 47
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulkFresh_moment_tendsto line 59
  9. lemma OAI.SphericalPerceptronFreeEnergy.bulkFresh_exact_restoration line 73
  10. lemma OAI.SphericalPerceptronFreeEnergy.bulkFresh_annealed_restoration line 90
  11. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_sum line 112
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_const_mul line 134
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_bound line 141
  14. lemma OAI.SphericalPerceptronFreeEnergy.bulk_two_row_exchange line 155
  15. lemma OAI.SphericalPerceptronFreeEnergy.bulk_pattern_sum_first line 182
  16. lemma OAI.SphericalPerceptronFreeEnergy.bulk_pattern_sum_second line 197