OAI/Probability/Perceptron/Cavity/BulkGoodParameters.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.bulkDeviationAt line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.bulkDeviationAt_nonneg line 15
  3. lemma OAI.SphericalPerceptronFreeEnergy.bulkDeviationAt_measurable line 22
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulkDeviationAt_integrable line 29
  5. lemma OAI.SphericalPerceptronFreeEnergy.bulkDeviationAt_integral_tendsto line 36
  6. def OAI.SphericalPerceptronFreeEnergy.omittedBulkDeviation line 46
  7. lemma OAI.SphericalPerceptronFreeEnergy.omittedBulkDeviation_integral_tendsto line 49
  8. def OAI.SphericalPerceptronFreeEnergy.bulkGoodSet line 57
  9. lemma OAI.SphericalPerceptronFreeEnergy.bulkGoodSet_measurable line 60
  10. lemma OAI.SphericalPerceptronFreeEnergy.bulkGoodSet_compl_measure line 66
  11. theorem OAI.SphericalPerceptronFreeEnergy.exists_bulkGoodParameters line 77
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulk_pairTest_measurable line 96
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulk_pairTest_bound line 102
  14. lemma OAI.SphericalPerceptronFreeEnergy.bulk_replica_ibp line 109
  15. lemma OAI.SphericalPerceptronFreeEnergy.bulk_energy_factorization line 128
  16. def OAI.SphericalPerceptronFreeEnergy.bulkGGDefect line 151
  17. lemma OAI.SphericalPerceptronFreeEnergy.bulkGG_weighted_bound line 157
  18. lemma OAI.SphericalPerceptronFreeEnergy.bulkGG_bound line 168