OAI/Probability/Perceptron/Cavity/CavityBulkLog.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.cavitySingleTest_bounds line 11
  2. abbrev OAI.SphericalPerceptronFreeEnergy.CavityPartitionRange line 30
  3. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkPartition_mem line 33
  4. def OAI.SphericalPerceptronFreeEnergy.cavityBulkPartitionLaw line 65
  5. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkPartitionLaw_integral line 72
  6. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkPartition_power_integrable line 80
  7. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkPartitionLaw_moment line 91
  8. def OAI.SphericalPerceptronFreeEnergy.cavityPartitionLogTest line 99
  9. def OAI.SphericalPerceptronFreeEnergy.cavityBulkLog line 103
  10. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkPartitionLaw_log line 107
  11. theorem OAI.SphericalPerceptronFreeEnergy.cavityBulkLog_tendsto line 119
  12. lemma OAI.SphericalPerceptronFreeEnergy.log_sub_le_div_sub line 137
  13. lemma OAI.SphericalPerceptronFreeEnergy.cavity_cap_tail line 144
  14. lemma OAI.SphericalPerceptronFreeEnergy.cavity_capped_log_bound line 153