OAI/Probability/Perceptron/Cavity/CavityProductLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.cavity_integral_preserving line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.cavity_prod_front_swap line 18
  3. lemma OAI.SphericalPerceptronFreeEnergy.cavity_product_shuffle line 27
  4. def OAI.SphericalPerceptronFreeEnergy.cavityRowsAppend line 40
  5. lemma OAI.SphericalPerceptronFreeEnergy.cavityRowsAppend_preserving line 43
  6. lemma OAI.SphericalPerceptronFreeEnergy.normalizedPatternEnergy_append line 56
  7. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellPatternEnergy_append line 64
  8. lemma OAI.SphericalPerceptronFreeEnergy.cavity_gaussian_joint_log_integrable line 71
  9. def OAI.SphericalPerceptronFreeEnergy.cavityShellLowLog line 94
  10. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellPatternEnergy_joint_measurable line 99
  11. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellLowLog_integrable line 107
  12. lemma OAI.SphericalPerceptronFreeEnergy.bulkExpectedLog_nested line 120
  13. theorem OAI.SphericalPerceptronFreeEnergy.cavity_expected_shell_restriction line 129