OAI/Probability/Perceptron/Variational/HeatGrid.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.gaussianGrid line 19
  2. lemma OAI.SphericalPerceptronFreeEnergy.gaussianGrid_lipschitz line 22
  3. lemma OAI.SphericalPerceptronFreeEnergy.gaussianGrid_succ line 30
  4. lemma OAI.SphericalPerceptronFreeEnergy.gaussianGrid_zero line 37
  5. lemma OAI.SphericalPerceptronFreeEnergy.gaussianGrid_absorb line 47
  6. def OAI.SphericalPerceptronFreeEnergy.gridVariance line 89
  7. lemma OAI.SphericalPerceptronFreeEnergy.gridVariance_nonneg line 92
  8. lemma OAI.SphericalPerceptronFreeEnergy.gridVariance_below line 102
  9. lemma OAI.SphericalPerceptronFreeEnergy.gridVariance_cons line 109
  10. lemma OAI.SphericalPerceptronFreeEnergy.gaussianBackward_compress line 119
  11. lemma OAI.SphericalPerceptronFreeEnergy.expectedCoordinateSphereLog_stationary_covariance line 137
  12. def OAI.SphericalPerceptronFreeEnergy.amplitudeCovarianceLevels line 196
  13. lemma OAI.SphericalPerceptronFreeEnergy.amplitudeCovarianceLevels_root line 200
  14. lemma OAI.SphericalPerceptronFreeEnergy.amplitudeCovarianceLevels_increment line 203
  15. lemma OAI.SphericalPerceptronFreeEnergy.amplitudeCovarianceLevels_monotone line 210
  16. lemma OAI.SphericalPerceptronFreeEnergy.amplitudeCovarianceLevels_nonneg line 217
  17. def OAI.SphericalPerceptronFreeEnergy.amplitudeSphereDual line 222
  18. lemma OAI.SphericalPerceptronFreeEnergy.amplitudeSphereValue_tendsto line 227
  19. def OAI.SphericalPerceptronFreeEnergy.finiteAmplitudeIncrement line 247
  20. def OAI.SphericalPerceptronFreeEnergy.finiteAmplitudeSphereValue line 250
  21. def OAI.SphericalPerceptronFreeEnergy.finiteAmplitudeSphereDual line 253
  22. lemma OAI.SphericalPerceptronFreeEnergy.finiteAmplitudeSphereValue_convex line 257
  23. lemma OAI.SphericalPerceptronFreeEnergy.finiteAmplitudeSphereValue_nonneg line 275
  24. lemma OAI.SphericalPerceptronFreeEnergy.finiteAmplitudeSphereValue_tendsto line 281