OAI/Probability/Perceptron/Cavity/FreshThermalLaw.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptronFreeEnergy.FreshPartitionRange line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.freshPartition_lower_le_upper line 16
  3. def OAI.SphericalPerceptronFreeEnergy.freshPartitionClip line 19
  4. lemma OAI.SphericalPerceptronFreeEnergy.freshPartitionClip_measurable line 23
  5. lemma OAI.SphericalPerceptronFreeEnergy.freshPartitionClip_eq line 27
  6. def OAI.SphericalPerceptronFreeEnergy.freshThermalPartition line 39
  7. lemma OAI.SphericalPerceptronFreeEnergy.freshThermalPartition_measurable line 43
  8. lemma OAI.SphericalPerceptronFreeEnergy.freshThermalPartition_mem line 52
  9. def OAI.SphericalPerceptronFreeEnergy.freshThermalLaw line 74
  10. lemma OAI.SphericalPerceptronFreeEnergy.freshThermalLaw_integral line 79
  11. lemma OAI.SphericalPerceptronFreeEnergy.freshThermalPartition_power_integrable line 97
  12. lemma OAI.SphericalPerceptronFreeEnergy.freshThermalLaw_moment line 111
  13. lemma OAI.SphericalPerceptronFreeEnergy.freshThermalPartition_log_integrable line 120
  14. lemma OAI.SphericalPerceptronFreeEnergy.freshThermalLaw_log line 133
  15. lemma OAI.SphericalPerceptronFreeEnergy.log_tiltMean_exp_bound_general line 143