OAI/Probability/Perceptron/Variational/TiltedVisitKernel.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.tiltedMarkKernel line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.tiltedMarkKernel_markov line 16
  3. def OAI.SphericalPerceptronFreeEnergy.tiltedStateStep line 27
  4. lemma OAI.SphericalPerceptronFreeEnergy.tiltedStateStep_markov line 31
  5. lemma OAI.SphericalPerceptronFreeEnergy.tiltedStateStep_lintegral line 39
  6. def OAI.SphericalPerceptronFreeEnergy.pathOneKernel line 52
  7. def OAI.SphericalPerceptronFreeEnergy.pathPairKernel line 56
  8. lemma OAI.SphericalPerceptronFreeEnergy.pathOneKernel_markov line 62
  9. lemma OAI.SphericalPerceptronFreeEnergy.pathPairKernel_markov line 71
  10. lemma OAI.SphericalPerceptronFreeEnergy.path_bounded_integrable line 84
  11. lemma OAI.SphericalPerceptronFreeEnergy.bounded_probability_mean_sq line 88
  12. def OAI.SphericalPerceptronFreeEnergy.pathMean line 111
  13. def OAI.SphericalPerceptronFreeEnergy.pathCorrelation line 114
  14. lemma OAI.SphericalPerceptronFreeEnergy.pathMean_measurable line 118
  15. lemma OAI.SphericalPerceptronFreeEnergy.pathCorrelation_measurable line 122
  16. lemma OAI.SphericalPerceptronFreeEnergy.pathMean_bound line 127
  17. lemma OAI.SphericalPerceptronFreeEnergy.pathCorrelation_bound line 134
  18. lemma OAI.SphericalPerceptronFreeEnergy.pathMean_succ line 144
  19. lemma OAI.SphericalPerceptronFreeEnergy.pathCorrelation_zero line 151
  20. lemma OAI.SphericalPerceptronFreeEnergy.pathCorrelation_succ line 168
  21. lemma OAI.SphericalPerceptronFreeEnergy.pathCorrelation_nonneg line 183
  22. lemma OAI.SphericalPerceptronFreeEnergy.pathCorrelation_monotone line 199