OAI/Probability/Perceptron/Pressure/CountableTerminalRestoration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptronFreeEnergy.TripleGaussianState line 13
  2. abbrev OAI.SphericalPerceptronFreeEnergy.TripleGaussianMark line 14
  3. abbrev OAI.SphericalPerceptronFreeEnergy.TripleGaussianData line 15
  4. def OAI.SphericalPerceptronFreeEnergy.tripleGaussianStep line 20
  5. lemma OAI.SphericalPerceptronFreeEnergy.tripleGaussianStep_measurable line 28
  6. def OAI.SphericalPerceptronFreeEnergy.tripleGaussianTerminal line 38
  7. def OAI.SphericalPerceptronFreeEnergy.tripleGaussianObservable line 42
  8. def OAI.SphericalPerceptronFreeEnergy.tripleGaussianRoot line 45
  9. def OAI.SphericalPerceptronFreeEnergy.tripleGaussianPair line 52
  10. lemma OAI.SphericalPerceptronFreeEnergy.tripleGaussianPair_measurable line 66
  11. theorem OAI.SphericalPerceptronFreeEnergy.countable_three_terminal_pair_value line 91