OAI/Probability/Perceptron/Variational/GaussianMarkRecursion.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_integrable_exp_linear_shift line 18
  2. def OAI.SphericalPerceptronFreeEnergy.gaussianLinearEntropic line 28
  3. lemma OAI.SphericalPerceptronFreeEnergy.gaussianLinearEntropic_lipschitz line 31
  4. def OAI.SphericalPerceptronFreeEnergy.gaussianLinearBackward line 43
  5. lemma OAI.SphericalPerceptronFreeEnergy.gaussianLinearBackward_lipschitz line 47
  6. def OAI.SphericalPerceptronFreeEnergy.gaussianLinearMarkStep line 61
  7. lemma OAI.SphericalPerceptronFreeEnergy.gaussianLinearMarkStep_measurable line 65
  8. def OAI.SphericalPerceptronFreeEnergy.linearCascadeWord line 72
  9. lemma OAI.SphericalPerceptronFreeEnergy.linearCascadeWord_nonneg line 77
  10. lemma OAI.SphericalPerceptronFreeEnergy.gaussianLinearRecursion_realization line 87
  11. def OAI.SphericalPerceptronFreeEnergy.gaussianMarkLaw line 118
  12. lemma OAI.SphericalPerceptronFreeEnergy.lipschitz_memLp_stdGaussian line 120
  13. def OAI.SphericalPerceptronFreeEnergy.gaussianLinearCascadeLog line 131
  14. lemma OAI.SphericalPerceptronFreeEnergy.gaussianLinearCascadeLog_measurable line 137
  15. lemma OAI.SphericalPerceptronFreeEnergy.gaussianLinearCascadeLog_mean line 148