OAI/Probability/Perceptron/Cavity/BulkSingleLimit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.bulk_single_ratio_tendsto_of_reference line 12
  2. theorem OAI.SphericalPerceptronFreeEnergy.bulk_single_limit_exists line 58
  3. def OAI.SphericalPerceptronFreeEnergy.singleFieldMark line 85
  4. lemma OAI.SphericalPerceptronFreeEnergy.singleFieldMark_measurable line 86
  5. lemma OAI.SphericalPerceptronFreeEnergy.singleFieldMark_bound line 88
  6. def OAI.SphericalPerceptronFreeEnergy.bulkSingleAverage line 90
  7. lemma OAI.SphericalPerceptronFreeEnergy.bulkSingleAverage_measurable line 94
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulkSingleAverage_bound line 99
  9. lemma OAI.SphericalPerceptronFreeEnergy.bulk_marked_last_single line 107
  10. lemma OAI.SphericalPerceptronFreeEnergy.bulkSingleAverage_first line 124
  11. lemma OAI.SphericalPerceptronFreeEnergy.bulkSingleAverage_second line 139
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulkSingleAverage_diagonal_bound line 165