OAI/Probability/Perceptron/Cavity/CavityShellLimit.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussian_prefix_preserving line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussian_prefix_norm line 19
  3. def OAI.SphericalPerceptronFreeEnergy.cavitySphereLaw line 24
  4. def OAI.SphericalPerceptronFreeEnergy.cavityCoupledBlock line 32
  5. lemma OAI.SphericalPerceptronFreeEnergy.cavityCoupledBlock_measurable line 35
  6. lemma OAI.SphericalPerceptronFreeEnergy.cavitySphereLaw_coupled line 38
  7. lemma OAI.SphericalPerceptronFreeEnergy.cavityCoupledBlock_tendsto_ae line 56
  8. def OAI.SphericalPerceptronFreeEnergy.cavityGaussianLaw line 67
  9. theorem OAI.SphericalPerceptronFreeEnergy.cavitySphereLaw_tendsto line 69
  10. def OAI.SphericalPerceptronFreeEnergy.cavityShell line 91
  11. lemma OAI.SphericalPerceptronFreeEnergy.cavityShell_measurable line 93
  12. lemma OAI.SphericalPerceptronFreeEnergy.stdGaussian_sphere_null line 96
  13. lemma OAI.SphericalPerceptronFreeEnergy.cavityShell_frontier_null line 101
  14. lemma OAI.SphericalPerceptronFreeEnergy.stdGaussian_open_pos line 117
  15. def OAI.SphericalPerceptronFreeEnergy.cavityShellMass line 125
  16. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellMass_pos line 127
  17. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellMass_le_one line 140
  18. lemma OAI.SphericalPerceptronFreeEnergy.cavitySphereLaw_shell_tendsto line 143
  19. lemma OAI.SphericalPerceptronFreeEnergy.cavitySphereLaw_shell_log_tendsto line 149