OAI/Probability/Perceptron/Cavity/BulkFreshRestore.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.bulkSeparateLast line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.bulkSeparateLast_preserving line 16
  3. lemma OAI.SphericalPerceptronFreeEnergy.bulkHamiltonian_last line 44
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulk_replica_restore_last line 54
  5. lemma OAI.SphericalPerceptronFreeEnergy.bulk_restoration_denominator_bounds line 69
  6. def OAI.SphericalPerceptronFreeEnergy.bulkSeparateTwo line 80
  7. lemma OAI.SphericalPerceptronFreeEnergy.bulkSeparateTwo_preserving line 86
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulkHamiltonian_two line 94
  9. lemma OAI.SphericalPerceptronFreeEnergy.bulk_replica_restore_two line 103
  10. lemma OAI.SphericalPerceptronFreeEnergy.bulk_two_denominator_bounds line 120
  11. def OAI.SphericalPerceptronFreeEnergy.bulkPermutePatterns line 135
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulkPermutePatterns_preserving line 138
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulkHamiltonian_permute line 154
  14. def OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean line 163
  15. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_permute line 168
  16. def OAI.SphericalPerceptronFreeEnergy.bulkPatternFields line 189
  17. lemma OAI.SphericalPerceptronFreeEnergy.bulkPatternFields_measurable line 192
  18. lemma OAI.SphericalPerceptronFreeEnergy.bulk_row_exchange line 199