OAI/Probability/Perceptron/Cavity/BulkCompactGG.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.bulkOverlap_continuous line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.bulkBlockTest_measurable line 16
  3. lemma OAI.SphericalPerceptronFreeEnergy.bulk_compact_gg_defect line 24
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulk_compact_gg_bound line 37
  5. lemma OAI.SphericalPerceptronFreeEnergy.omitted_bulk_monomial_tendsto line 45
  6. lemma OAI.SphericalPerceptronFreeEnergy.compactScalarGG_zero line 58
  7. lemma OAI.SphericalPerceptronFreeEnergy.omitted_bulk_limit_gg line 67
  8. lemma OAI.SphericalPerceptronFreeEnergy.bulk_monomial_tendsto line 83
  9. lemma OAI.SphericalPerceptronFreeEnergy.bulk_limit_gg line 96
  10. def OAI.SphericalPerceptronFreeEnergy.bulkJointDeviation line 111
  11. lemma OAI.SphericalPerceptronFreeEnergy.bulkJointDeviation_nonneg line 114
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulkJointDeviation_measurable line 117
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulkJointDeviation_integrable line 120
  14. lemma OAI.SphericalPerceptronFreeEnergy.bulkJointDeviation_integral_tendsto line 124
  15. def OAI.SphericalPerceptronFreeEnergy.bulkJointGoodSet line 136
  16. lemma OAI.SphericalPerceptronFreeEnergy.bulkJointGoodSet_measurable line 139
  17. lemma OAI.SphericalPerceptronFreeEnergy.bulkJointGoodSet_compl_measure line 145
  18. theorem OAI.SphericalPerceptronFreeEnergy.exists_bulkJointGoodParameters line 156