OAI/Probability/Perceptron/Cavity/CavityLabelPartition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SphericalPerceptronFreeEnergy.cavityIndexMeasurableSingleton line 12
  2. def OAI.SphericalPerceptronFreeEnergy.cavityLabelPartition line 18
  3. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabelPartition_measurable line 25
  4. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabelPartition_mem line 45
  5. def OAI.SphericalPerceptronFreeEnergy.cavityLabelPartitionLaw line 64
  6. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabelPartitionLaw_integral line 71
  7. theorem OAI.SphericalPerceptronFreeEnergy.cavityLabelPartitionLaw_moment line 80
  8. def OAI.SphericalPerceptronFreeEnergy.cavityIndexedRootPartition line 107
  9. lemma OAI.SphericalPerceptronFreeEnergy.cavityIndexedRootPartition_measurable line 116
  10. lemma OAI.SphericalPerceptronFreeEnergy.cavityIndexedRootPartition_log_bound line 146
  11. lemma OAI.SphericalPerceptronFreeEnergy.cavityIndexedRoot_disorder_preserving line 161
  12. theorem OAI.SphericalPerceptronFreeEnergy.cavityLabelPartitionLaw_log_recursion line 175