OAI/Probability/Perceptron/Cavity/CavityCompensator.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.cavity_exp_local_lipschitz line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.cavity_log_local_lipschitz line 20
  3. lemma OAI.SphericalPerceptronFreeEnergy.cavity_compensator_bound line 31
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulkC_measurable line 95
  5. lemma OAI.SphericalPerceptronFreeEnergy.bulkC_bound line 100
  6. def OAI.SphericalPerceptronFreeEnergy.cavityBulkCompPartition line 105
  7. lemma OAI.SphericalPerceptronFreeEnergy.cavity_comp_partition_joint_measurable line 111
  8. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkCompPartition_measurable line 128
  9. def OAI.SphericalPerceptronFreeEnergy.cavityCompensatorConstant line 135
  10. lemma OAI.SphericalPerceptronFreeEnergy.cavityCompensatorConstant_nonneg line 139
  11. lemma OAI.SphericalPerceptronFreeEnergy.tilt_cavity_compensator_bound line 145
  12. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkSingleWeight_measurable line 157
  13. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkCompPartition_error line 165
  14. lemma OAI.SphericalPerceptronFreeEnergy.bulkC_L1_of_L2 line 181