OAI/Probability/Perceptron/Cavity/CavityShellPerturbation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptronFreeEnergy.CavityShellSpin line 12
  2. def OAI.SphericalPerceptronFreeEnergy.cavityShellFeature line 14
  3. lemma OAI.SphericalPerceptronFreeEnergy.cavityRho_measurable line 17
  4. lemma OAI.SphericalPerceptronFreeEnergy.cavityNormalizedVec_measurable line 21
  5. lemma OAI.SphericalPerceptronFreeEnergy.ambientBulkFeature_measurable_comp line 28
  6. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellFeature_measurable line 33
  7. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellFeature_norm line 41
  8. theorem OAI.SphericalPerceptronFreeEnergy.cavity_shell_perturbation_comparison line 52
  9. lemma OAI.SphericalPerceptronFreeEnergy.cavity_shell_perturbation_error_tendsto line 79
  10. def OAI.SphericalPerceptronFreeEnergy.cavityShellProbability line 84
  11. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellProbability_probability line 87
  12. def OAI.SphericalPerceptronFreeEnergy.cavityShellBaseLaw line 97
  13. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellBaseLaw_probability line 100
  14. lemma OAI.SphericalPerceptronFreeEnergy.cavityShell_probability_eventually line 107
  15. def OAI.SphericalPerceptronFreeEnergy.cavityShellSpinEmbedding line 113
  16. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellSpinEmbedding_measurable line 121
  17. def OAI.SphericalPerceptronFreeEnergy.cavityShellPatternEnergy line 127
  18. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellPatternEnergy_measurable line 131
  19. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellPatternEnergy_bound line 137
  20. theorem OAI.SphericalPerceptronFreeEnergy.cavity_true_shell_perturbation line 142