OAI/Probability/Perceptron/Interpolation/ArrayGeometry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianCovariance_posSemidef line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.sourceSpinArray_posSemidef line 30
  3. lemma OAI.SphericalPerceptronFreeEnergy.sourceTreeArray_posSemidef line 34
  4. lemma OAI.SphericalPerceptronFreeEnergy.sourceJointArray_diagonal line 50
  5. lemma OAI.SphericalPerceptronFreeEnergy.isClosed_matrix_posSemidef line 56
  6. lemma OAI.SphericalPerceptronFreeEnergy.pi_iid_reindex_preserving line 72
  7. lemma OAI.SphericalPerceptronFreeEnergy.infinite_iid_reindex_preserving line 81
  8. lemma OAI.SphericalPerceptronFreeEnergy.gibbsReplicaMean_reindex line 91
  9. lemma OAI.SphericalPerceptronFreeEnergy.gibbsReplicaMean_fresh_last line 106
  10. lemma OAI.SphericalPerceptronFreeEnergy.annealedInfiniteReplica_reindex line 119
  11. def OAI.SphericalPerceptronFreeEnergy.compactRelabel line 138
  12. lemma OAI.SphericalPerceptronFreeEnergy.compactRelabel_continuous line 141
  13. lemma OAI.SphericalPerceptronFreeEnergy.sourceGibbsArray_exchangeable line 144
  14. lemma OAI.SphericalPerceptronFreeEnergy.compact_exchangeability_limit line 167