OAI/Probability/Perceptron/Cavity/BulkRestoredObservables.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptronFreeEnergy.TwoFreshDisorder line 13
  2. def OAI.SphericalPerceptronFreeEnergy.bulkMarkedTest line 16
  3. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarkedTest_continuous line 23
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarkedTest_bound line 44
  5. def OAI.SphericalPerceptronFreeEnergy.bulkFreshNumerator line 53
  6. def OAI.SphericalPerceptronFreeEnergy.bulkFreshDenominator line 59
  7. lemma OAI.SphericalPerceptronFreeEnergy.twoFreshHamiltonian_measurable line 64
  8. lemma OAI.SphericalPerceptronFreeEnergy.twoFreshMarkedTest_measurable line 71
  9. lemma OAI.SphericalPerceptronFreeEnergy.bulkFreshNumerator_measurable line 79
  10. lemma OAI.SphericalPerceptronFreeEnergy.bulkFreshDenominator_measurable line 91
  11. lemma OAI.SphericalPerceptronFreeEnergy.bulkFreshNumerator_bound line 101
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulkFreshDenominator_mem line 112
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarked_replica_moment line 121
  14. lemma OAI.SphericalPerceptronFreeEnergy.bulkFresh_polynomial_moment line 156