OAI/Probability/SKValue/GroundState/StandardGaussian.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValueG.standardGaussian line 12
  2. def OAI.SKValueG.gaussianProduct line 13
  3. instance OAI.SKValueG.(instance at line 16) line 16
  4. instance OAI.SKValueG.(instance at line 17) line 17
  5. lemma OAI.SKValueG.density_hasDerivAt line 20
  6. lemma OAI.SKValueG.density_mul_integrable line 33
  7. lemma OAI.SKValueG.standardGaussian_integrable_id line 40
  8. lemma OAI.SKValueG.gaussian_stein_bounded line 44
  9. lemma OAI.SKValueG.gaussian_coordinate_integrable line 80
  10. lemma OAI.SKValueG.gaussian_pi_stein_bounded line 85
  11. def OAI.SKValueG.partition line 126
  12. def OAI.SKValueG.gibbsWeight line 129
  13. def OAI.SKValueG.logPartition line 132
  14. lemma OAI.SKValueG.partition_pos line 135
  15. lemma OAI.SKValueG.gibbsWeight_nonneg line 138
  16. lemma OAI.SKValueG.sum_gibbsWeight line 141
  17. lemma OAI.SKValueG.gibbsWeight_le_one line 147
  18. lemma OAI.SKValueG.continuous_partition line 153
  19. lemma OAI.SKValueG.continuous_gibbsWeight line 157
  20. lemma OAI.SKValueG.hasDerivAt_partition line 161
  21. lemma OAI.SKValueG.hasDerivAt_logPartition line 166
  22. lemma OAI.SKValueG.hasDerivAt_gibbsWeight line 176
  23. lemma OAI.SKValueG.abs_gibbsMean_le line 188
  24. def OAI.SKValueG.linearProcess line 196
  25. lemma OAI.SKValueG.continuous_linearProcess line 199
  26. lemma OAI.SKValueG.hasDerivAt_linearProcess_update line 204
  27. lemma OAI.SKValueG.continuous_linear_gibbsWeight line 217
  28. lemma OAI.SKValueG.integrable_linear_gibbsWeight line 221
  29. lemma OAI.SKValueG.coordinate_gibbsWeight_integrable line 226
  30. lemma OAI.SKValueG.gaussian_coordinate_gibbsWeight line 232
  31. lemma OAI.SKValueG.le_logPartition line 260
  32. lemma OAI.SKValueG.logPartition_le line 265
  33. lemma OAI.SKValueG.abs_logPartition_le line 276
  34. lemma OAI.SKValueG.continuous_logPartition line 288
  35. lemma OAI.SKValueG.linearProcess_integrable line 292
  36. lemma OAI.SKValueG.logPartition_integrable line 296
  37. lemma OAI.SKValueG.gibbsWeight_mul_integrable line 303
  38. lemma OAI.SKValueG.gaussian_linear_gibbsWeight line 309
  39. lemma OAI.SKValueG.weighted_covariance_pairs line 349