OAI/Probability/Perceptron/Cavity/FreshReplicaKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.freshKernel_extension_exists line 11
  2. def OAI.SphericalPerceptronFreeEnergy.freshReplicaMatrixKernel line 20
  3. lemma OAI.SphericalPerceptronFreeEnergy.freshReplicaMatrixKernel_gram line 23
  4. def OAI.SphericalPerceptronFreeEnergy.freshReplicaArrayKernel line 29
  5. lemma OAI.SphericalPerceptronFreeEnergy.freshReplicaArrayKernel_source line 33
  6. lemma OAI.SphericalPerceptronFreeEnergy.freshReplicaArrayKernel_tendsto line 42
  7. lemma OAI.SphericalPerceptronFreeEnergy.freshPattern_moment_measurable_spins line 49
  8. lemma OAI.SphericalPerceptronFreeEnergy.freshPattern_gibbs_moment line 85
  9. def OAI.SphericalPerceptronFreeEnergy.sourceFreshMoment line 101
  10. lemma OAI.SphericalPerceptronFreeEnergy.sourceFreshMoment_array line 108
  11. theorem OAI.SphericalPerceptronFreeEnergy.sourceFreshMoment_tendsto line 131