OAI/Probability/Perceptron/Interpolation/CompactArrayMap.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.compactMapArray line 13
  2. def OAI.SphericalPerceptronFreeEnergy.compactMapBlock line 14
  3. lemma OAI.SphericalPerceptronFreeEnergy.compactMapArray_continuous line 16
  4. lemma OAI.SphericalPerceptronFreeEnergy.compactMapBlock_continuous line 19
  5. def OAI.SphericalPerceptronFreeEnergy.compactDiagonalMapArray line 24
  6. def OAI.SphericalPerceptronFreeEnergy.compactDiagonalMapBlock line 26
  7. lemma OAI.SphericalPerceptronFreeEnergy.compactDiagonalMapArray_continuous line 29
  8. lemma OAI.SphericalPerceptronFreeEnergy.compactDiagonalMapBlock_continuous line 34
  9. lemma OAI.SphericalPerceptronFreeEnergy.compactDiagonalMapBlock_compactBlock line 41
  10. def OAI.SphericalPerceptronFreeEnergy.compactMapLaw line 50
  11. lemma OAI.SphericalPerceptronFreeEnergy.compactMapLaw_integral line 56
  12. lemma OAI.SphericalPerceptronFreeEnergy.compactMapLaw_gg line 62
  13. lemma OAI.SphericalPerceptronFreeEnergy.compactMapLaw_pair line 85
  14. def OAI.SphericalPerceptronFreeEnergy.compactDiagonalMapLaw line 94
  15. lemma OAI.SphericalPerceptronFreeEnergy.compactDiagonalMapLaw_integral line 100
  16. lemma OAI.SphericalPerceptronFreeEnergy.compactDiagonalMapLaw_gg line 106