OAI/Probability/Perceptron/Cavity/BulkRadialLimit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.bulk_single_mean_of_L2 line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.bulk_diagonal_mean_add line 20
  3. lemma OAI.SphericalPerceptronFreeEnergy.bulk_radial_limit_relation line 32
  4. lemma OAI.SphericalPerceptronFreeEnergy.isClosed_covarianceMatrix line 63
  5. lemma OAI.SphericalPerceptronFreeEnergy.cavity_extension_exists line 79
  6. def OAI.SphericalPerceptronFreeEnergy.cavityMatrixKernel line 89
  7. lemma OAI.SphericalPerceptronFreeEnergy.cavityMatrixKernel_posSemidef line 93
  8. lemma OAI.SphericalPerceptronFreeEnergy.sphericalExp_continuous line 98
  9. def OAI.SphericalPerceptronFreeEnergy.cappedSphericalExp line 105
  10. abbrev OAI.SphericalPerceptronFreeEnergy.CavityReplicaIndex line 116
  11. def OAI.SphericalPerceptronFreeEnergy.cavityVectorProjection line 118
  12. def OAI.SphericalPerceptronFreeEnergy.cavityReplicaTest line 122
  13. lemma OAI.SphericalPerceptronFreeEnergy.cavityReplicaTest_apply line 128
  14. def OAI.SphericalPerceptronFreeEnergy.cavityBlockCovariance line 135
  15. lemma OAI.SphericalPerceptronFreeEnergy.cavityBlockCovariance_continuous line 140
  16. def OAI.SphericalPerceptronFreeEnergy.cavityArrayKernel line 152
  17. lemma OAI.SphericalPerceptronFreeEnergy.cavityArrayKernel_tendsto line 157