OAI/Probability/Perceptron/Cavity/BulkConcentration.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.bulkFeatureBound_sq line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.bulkFeatureBound_sq_le line 15
  3. lemma OAI.SphericalPerceptronFreeEnergy.bulkLogPartition_measurable line 38
  4. lemma OAI.SphericalPerceptronFreeEnergy.bulkLogPartition_bound line 46
  5. lemma OAI.SphericalPerceptronFreeEnergy.bulkLogPartition_memLp line 56
  6. lemma OAI.SphericalPerceptronFreeEnergy.bulkLogPartition_variance line 69
  7. lemma OAI.SphericalPerceptronFreeEnergy.enrichedFeature_cross_inner line 84
  8. def OAI.SphericalPerceptronFreeEnergy.bulkDirection line 100
  9. def OAI.SphericalPerceptronFreeEnergy.bulkCoefficient line 103
  10. def OAI.SphericalPerceptronFreeEnergy.bulkY line 105
  11. lemma OAI.SphericalPerceptronFreeEnergy.bulkDirection_continuous line 108
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulkDirection_norm line 111
  13. lemma OAI.SphericalPerceptronFreeEnergy.bulkDirection_inner line 119
  14. lemma OAI.SphericalPerceptronFreeEnergy.bulkFeature_direction_inner line 126
  15. lemma OAI.SphericalPerceptronFreeEnergy.bulkY_bound line 133
  16. lemma OAI.SphericalPerceptronFreeEnergy.bulkY_measurable line 136
  17. lemma OAI.SphericalPerceptronFreeEnergy.bulkAmplitude_update line 139
  18. lemma OAI.SphericalPerceptronFreeEnergy.bulkFeature_update line 148
  19. lemma OAI.SphericalPerceptronFreeEnergy.bulkHamiltonian_update line 161
  20. lemma OAI.SphericalPerceptronFreeEnergy.bulkCoefficient_pos line 170
  21. lemma OAI.SphericalPerceptronFreeEnergy.bulkHamiltonian_section_measurable line 175