OAI/Probability/Perceptron/Cavity/BulkSingleEmpiricalLimit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.bulkSingleAverage_first_limit line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.bulkSingleAverage_second_limit line 24
  3. theorem OAI.SphericalPerceptronFreeEnergy.bulk_single_empirical_limits line 43
  4. abbrev OAI.SphericalPerceptronFreeEnergy.bulkAnnealedReplicaLaw line 64
  5. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_annealed line 68
  6. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaPrefix_integrable line 78
  7. lemma OAI.SphericalPerceptronFreeEnergy.bulkReplicaMean_centered_square line 88
  8. def OAI.SphericalPerceptronFreeEnergy.Jet3.dilationMark line 113
  9. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.dilationMark_apply line 117
  10. lemma OAI.SphericalPerceptronFreeEnergy.bulkC_singleAverage line 120
  11. lemma OAI.SphericalPerceptronFreeEnergy.bulkB_diagonal_singleAverage line 125
  12. theorem OAI.SphericalPerceptronFreeEnergy.bulk_single_L2_concentration line 130
  13. theorem OAI.SphericalPerceptronFreeEnergy.bulk_diagonal_C_concentration line 152