OAI/Probability/Perceptron/Cascade/CavityFiniteRPC.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptronFreeEnergy.CavityRPCState line 12
  2. abbrev OAI.SphericalPerceptronFreeEnergy.CavityRPCMark line 13
  3. def OAI.SphericalPerceptronFreeEnergy.cavityRPCMarkLaw line 14
  4. def OAI.SphericalPerceptronFreeEnergy.cavityRPCStep line 17
  5. def OAI.SphericalPerceptronFreeEnergy.cavityRPCTerminal line 20
  6. lemma OAI.SphericalPerceptronFreeEnergy.cavityRPCStep_measurable line 23
  7. lemma OAI.SphericalPerceptronFreeEnergy.cavityRPCTerminal_measurable line 26
  8. theorem OAI.SphericalPerceptronFreeEnergy.cavity_finiteRPC_conditional line 34
  9. def OAI.SphericalPerceptronFreeEnergy.cavityScalarRootValue line 75
  10. def OAI.SphericalPerceptronFreeEnergy.cavityRPCRootState line 79
  11. lemma OAI.SphericalPerceptronFreeEnergy.cavity_scalar_recursion_bound line 82
  12. lemma OAI.SphericalPerceptronFreeEnergy.cavity_scalar_root_pi_mean line 90
  13. theorem OAI.SphericalPerceptronFreeEnergy.cavity_finiteRPC_roots line 120