OAI/Probability/Perceptron/Cavity/BulkMarkedArray.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.bulkB_measurable line 13
  2. lemma OAI.SphericalPerceptronFreeEnergy.bulkB_pairAverage line 19
  3. lemma OAI.SphericalPerceptronFreeEnergy.bulkB_symm line 24
  4. def OAI.SphericalPerceptronFreeEnergy.bulkMarkedEntry line 29
  5. def OAI.SphericalPerceptronFreeEnergy.bulkMarkedArray line 34
  6. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarkedArray_measurable line 39
  7. def OAI.SphericalPerceptronFreeEnergy.bulkGibbsHamiltonian line 46
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulkGibbsHamiltonian_measurable line 50
  9. def OAI.SphericalPerceptronFreeEnergy.bulkMarkedArrayLaw line 54
  10. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarkedArray_block line 61
  11. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarkedArray_exchangeable line 84
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarkedArray_overlap line 99
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarkedArray_pair line 108
  14. def OAI.SphericalPerceptronFreeEnergy.markedTangentR line 133
  15. def OAI.SphericalPerceptronFreeEnergy.markedTangentPair line 135
  16. def OAI.SphericalPerceptronFreeEnergy.markedTangentTriple line 137
  17. lemma OAI.SphericalPerceptronFreeEnergy.bulk_tangent_pair_sum line 140
  18. lemma OAI.SphericalPerceptronFreeEnergy.bulk_tangent_triple_sum line 169
  19. lemma OAI.SphericalPerceptronFreeEnergy.bulk_marked_tangent_bound line 198