OAI/Probability/SKGap/Gaussian/GaussianGramMomentsJoined.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.scalarGramVariance line 18
  2. def OAI.SKGap.spinMixed line 20
  3. lemma OAI.SKGap.spinVariance_nonneg line 22
  4. lemma OAI.SKGap.abs_spinVariance_le_one line 25
  5. lemma OAI.SKGap.abs_spinMixed_le_one line 30
  6. lemma OAI.SKGap.integrable_spinVariance line 37
  7. lemma OAI.SKGap.integrable_spinMixed line 41
  8. lemma OAI.SKGap.gaussian_nishimori_variance line 45
  9. lemma OAI.SKGap.hasDerivAt_spinVariance line 69
  10. lemma OAI.SKGap.hasDerivAt_oddVariance line 73
  11. lemma OAI.SKGap.integrable_center_spinVariance line 78
  12. lemma OAI.SKGap.integrable_center_oddVariance line 85
  13. lemma OAI.SKGap.integrable_center_sq_spinVariance line 92
  14. theorem OAI.SKGap.gaussian_weighted_gram_moments line 101
  15. def OAI.SKGap.scalarGramVector line 143
  16. theorem OAI.SKGap.gaussian_weighted_gram_matrix line 145