OAI/Probability/Perceptron/Cavity/CavityGeometry.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.gaussianBlockJoin line 13
  2. lemma OAI.SphericalPerceptronFreeEnergy.gaussianBlockJoin_measurable line 16
  3. lemma OAI.SphericalPerceptronFreeEnergy.gaussianBlockSplit_join line 22
  4. lemma OAI.SphericalPerceptronFreeEnergy.gaussianBlockJoin_split line 26
  5. lemma OAI.SphericalPerceptronFreeEnergy.gaussianBlockJoin_norm_sq line 31
  6. lemma OAI.SphericalPerceptronFreeEnergy.gaussianBlockJoin_inner line 35
  7. def OAI.SphericalPerceptronFreeEnergy.cavityRho line 43
  8. def OAI.SphericalPerceptronFreeEnergy.cavityNormalizedVec line 45
  9. lemma OAI.SphericalPerceptronFreeEnergy.cavityRho_bounds line 48
  10. lemma OAI.SphericalPerceptronFreeEnergy.cavityNormalizedVec_norm line 62
  11. lemma OAI.SphericalPerceptronFreeEnergy.cavityNormalizedVec_inner line 76
  12. lemma OAI.SphericalPerceptronFreeEnergy.cavityNormalizedVec_overlap_error line 88
  13. lemma OAI.SphericalPerceptronFreeEnergy.cavityNormalizedVec_covariance line 123
  14. def OAI.SphericalPerceptronFreeEnergy.gaussianSumSplit line 143
  15. def OAI.SphericalPerceptronFreeEnergy.gaussianInl line 145
  16. def OAI.SphericalPerceptronFreeEnergy.gaussianInr line 147
  17. lemma OAI.SphericalPerceptronFreeEnergy.gaussianSumSplit_measurable line 150
  18. lemma OAI.SphericalPerceptronFreeEnergy.gaussianInl_measurable line 153
  19. lemma OAI.SphericalPerceptronFreeEnergy.gaussianInr_measurable line 158
  20. lemma OAI.SphericalPerceptronFreeEnergy.gaussianSumSplit_preserving line 163
  21. lemma OAI.SphericalPerceptronFreeEnergy.gaussianInl_inner line 176
  22. lemma OAI.SphericalPerceptronFreeEnergy.gaussianInr_inner line 182
  23. lemma OAI.SphericalPerceptronFreeEnergy.gaussianInl_Inr_inner line 188
  24. lemma OAI.SphericalPerceptronFreeEnergy.gaussianInl_norm line 192
  25. lemma OAI.SphericalPerceptronFreeEnergy.gaussianInr_norm line 196
  26. lemma OAI.SphericalPerceptronFreeEnergy.gaussianInl_linear line 200
  27. lemma OAI.SphericalPerceptronFreeEnergy.gaussianInr_linear line 206
  28. lemma OAI.SphericalPerceptronFreeEnergy.gaussianLogPartition_measurable_finite line 214
  29. lemma OAI.SphericalPerceptronFreeEnergy.gaussianInl_log_integral line 223
  30. lemma OAI.SphericalPerceptronFreeEnergy.gaussianInr_log_integral line 238
  31. theorem OAI.SphericalPerceptronFreeEnergy.independentGaussian_covariance_comparison line 253