OAI/Probability/Perceptron/Cavity/BulkMarkedPairLimit.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.bulk_marked_ratio_tendsto_of_reference line 12
  2. theorem OAI.SphericalPerceptronFreeEnergy.bulk_marked_pair_limit_exists line 58
  3. def OAI.SphericalPerceptronFreeEnergy.pairFieldMark line 103
  4. lemma OAI.SphericalPerceptronFreeEnergy.pairFieldMark_measurable line 104
  5. lemma OAI.SphericalPerceptronFreeEnergy.pairFieldMark_bound line 107
  6. def OAI.SphericalPerceptronFreeEnergy.bulkPairAverage line 111
  7. lemma OAI.SphericalPerceptronFreeEnergy.bulkPairAverage_measurable line 115
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulkPairAverage_bound line 120
  9. def OAI.SphericalPerceptronFreeEnergy.bulkPairOverlapTest line 128
  10. lemma OAI.SphericalPerceptronFreeEnergy.bulkPairOverlapTest_measurable line 130
  11. lemma OAI.SphericalPerceptronFreeEnergy.bulk_last_two_fields line 134
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulk_marked_last_pair line 144
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulkPairAverage_first line 158
  14. lemma OAI.SphericalPerceptronFreeEnergy.bulkPairAverage_second line 173
  15. lemma OAI.SphericalPerceptronFreeEnergy.bulkPairAverage_diagonal_bound line 197