OAI/MathematicalPhysics/CriticalSK/GaussianMoments.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.gaussian_square_density line 23
  2. lemma OAI.CriticalSK.gaussian_square_integral line 31
  3. lemma OAI.CriticalSK.gaussian_square_integrable line 51
  4. def OAI.CriticalSK.chiSquare line 58
  5. def OAI.CriticalSK.standardGaussianProduct line 60
  6. def OAI.CriticalSK.gaussianScalarPi line 69
  7. instance OAI.CriticalSK.(instance at line 71) line 71
  8. def OAI.CriticalSK.gaussianLinear line 73
  9. lemma OAI.CriticalSK.gaussianLinear_continuous line 75
  10. lemma OAI.CriticalSK.gaussian_exp_integrable line 79
  11. lemma OAI.CriticalSK.gaussian_exp_integral line 84
  12. lemma OAI.CriticalSK.gaussianLinear_neg line 96
  13. lemma OAI.CriticalSK.gaussianLinear_add line 99
  14. lemma OAI.CriticalSK.gaussianLinear_sub line 102
  15. lemma OAI.CriticalSK.gaussian_cosh_integrable line 105
  16. lemma OAI.CriticalSK.gaussian_cosh_integral line 110
  17. lemma OAI.CriticalSK.cosh_mul_cosh_identity line 117
  18. lemma OAI.CriticalSK.gaussian_cosh_product_integrable line 121
  19. lemma OAI.CriticalSK.gaussian_cosh_product_integral line 126
  20. lemma OAI.CriticalSK.cosh_pow_exp_bound line 147
  21. lemma OAI.CriticalSK.gaussian_cosh_pow_bound line 163
  22. lemma OAI.CriticalSK.cosh_sub_one_quadratic line 186
  23. def OAI.CriticalSK.coshMixture line 200
  24. lemma OAI.CriticalSK.coshMixture_continuous line 203
  25. lemma OAI.CriticalSK.coshMixture_nonneg line 209
  26. lemma OAI.CriticalSK.coshMixture_integrable line 212
  27. lemma OAI.CriticalSK.coshMixture_integral line 216
  28. lemma OAI.CriticalSK.coshMixture_pow_integrable_bound line 224
  29. lemma OAI.CriticalSK.coshMixture_square line 248
  30. lemma OAI.CriticalSK.coshMixture_square_integral line 257
  31. lemma OAI.CriticalSK.coshMixture_centered_integrable_bound line 272