OAI/Probability/SKGap/Gaussian/GaussianProductPower.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.gaussianProduct_integrable_exp_lipschitz line 14
  2. lemma OAI.SKGap.gaussianProduct_integrable_abs_pow_lipschitz line 21
  3. lemma OAI.SKGap.gaussianProduct_integrable_pow_lipschitz line 34
  4. def OAI.SKGap.matrixEntryMean line 52
  5. def OAI.SKGap.matrixCentered line 54
  6. lemma OAI.SKGap.matrixCentered_lipschitz line 57
  7. lemma OAI.SKGap.matrixEntry_lip line 63
  8. lemma OAI.SKGap.diagonalCentered_lip line 67
  9. lemma OAI.SKGap.offDiagonalCentered_lip line 70
  10. lemma OAI.SKGap.matrixCentered_even_moment line 74
  11. lemma OAI.SKGap.diagonalCentered_second_moment line 81
  12. lemma OAI.SKGap.offDiagonalCentered_fourth_moment line 90
  13. lemma OAI.SKGap.gaussianProduct_jensen_pow line 112
  14. def OAI.SKGap.matrixNormConstant line 120
  15. lemma OAI.SKGap.matrixNormConstant_bounds line 123
  16. lemma OAI.SKGap.gaussianProduct_centered_matrix_norms line 133