OAI/Probability/Perceptron/Variational/CompactGGEvents.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.compactGG_events line 12
  2. def OAI.SphericalPerceptronFreeEnergy.compactPairReal line 50
  3. def OAI.SphericalPerceptronFreeEnergy.compactArrayReal line 51
  4. def OAI.SphericalPerceptronFreeEnergy.compactBlockReal line 53
  5. lemma OAI.SphericalPerceptronFreeEnergy.compactPairReal_measurable line 56
  6. lemma OAI.SphericalPerceptronFreeEnergy.compactArrayReal_measurable line 57
  7. lemma OAI.SphericalPerceptronFreeEnergy.compactBlockReal_measurable line 60
  8. def OAI.SphericalPerceptronFreeEnergy.compactRealLaw line 64
  9. instance OAI.SphericalPerceptronFreeEnergy.compactRealLaw_probability line 67
  10. lemma OAI.SphericalPerceptronFreeEnergy.compactRealLaw_gg line 71
  11. lemma OAI.SphericalPerceptronFreeEnergy.compactRealLaw_exchangeable line 90
  12. lemma OAI.SphericalPerceptronFreeEnergy.compactRealLaw_gram line 101
  13. lemma OAI.SphericalPerceptronFreeEnergy.compactRealLaw_diagonals line 112
  14. lemma OAI.SphericalPerceptronFreeEnergy.compact_gg_no_crossing line 121