OAI/Probability/Perceptron/Brownian/CountableGaussianField.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.countableGaussianLaw line 11
  2. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 14) line 14
  3. def OAI.SphericalPerceptronFreeEnergy.gaussianCoordinatePrefix line 18
  4. lemma OAI.SphericalPerceptronFreeEnergy.gaussianCoordinatePrefix_measurePreserving line 20
  5. def OAI.SphericalPerceptronFreeEnergy.gaussianPrefixField line 30
  6. def OAI.SphericalPerceptronFreeEnergy.countableGaussianField line 33
  7. lemma OAI.SphericalPerceptronFreeEnergy.gaussianPrefixField_measurable line 36
  8. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianField_measurable line 43
  9. lemma OAI.SphericalPerceptronFreeEnergy.finiteGaussian_exp_integrable line 53
  10. lemma OAI.SphericalPerceptronFreeEnergy.finiteGaussian_exp_integral line 66
  11. lemma OAI.SphericalPerceptronFreeEnergy.gaussianPrefixField_exp_integrable line 91
  12. lemma OAI.SphericalPerceptronFreeEnergy.gaussianPrefixField_exp_integral line 96
  13. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianField_exp_integrable line 107
  14. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianField_exp_integral line 111
  15. def OAI.SphericalPerceptronFreeEnergy.maskedGaussianCoefficient line 116
  16. lemma OAI.SphericalPerceptronFreeEnergy.maskedGaussianCoefficient_measurable line 119
  17. lemma OAI.SphericalPerceptronFreeEnergy.sum_range_cutoff line 124
  18. def OAI.SphericalPerceptronFreeEnergy.truncatedCountableGaussianField line 138
  19. lemma OAI.SphericalPerceptronFreeEnergy.truncatedCountableGaussianField_eq line 141
  20. lemma OAI.SphericalPerceptronFreeEnergy.truncatedCountableGaussianField_eventually_eq line 154
  21. lemma OAI.SphericalPerceptronFreeEnergy.truncatedCountableGaussianField_measurable line 161
  22. lemma OAI.SphericalPerceptronFreeEnergy.gaussianCoefficient_prefix_sq_le line 166
  23. lemma OAI.SphericalPerceptronFreeEnergy.truncatedCountableGaussianField_exp_integral_le line 173
  24. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianField_exp_integral_le line 183