OAI/MathematicalPhysics/CriticalSK/Covariance.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.euclideanMatrix_norm_le_frobenius line 14
  2. lemma OAI.CriticalSK.covariance_continuous line 32
  3. lemma OAI.CriticalSK.covarianceNorm_continuous line 42
  4. lemma OAI.CriticalSK.variance_linear_quadratic line 49
  5. lemma OAI.CriticalSK.variance_linear_le_norm line 65
  6. lemma OAI.CriticalSK.variance_linear_smallBall line 75
  7. lemma OAI.CriticalSK.sum_four_exchange line 90
  8. lemma OAI.CriticalSK.gibbsOverlap_nonneg line 110
  9. lemma OAI.CriticalSK.gibbsOverlap_continuous line 115
  10. lemma OAI.CriticalSK.finite_gram_frobenius line 123
  11. lemma OAI.CriticalSK.covariance_frobenius_overlap line 139
  12. lemma OAI.CriticalSK.covarianceNorm_sq_le_overlap line 163
  13. lemma OAI.CriticalSK.rotatedCubeOverlap_eq line 172
  14. lemma OAI.CriticalSK.haar_gibbsOverlap_bound line 194
  15. lemma OAI.CriticalSK.natural_gibbsOverlap_probability line 215
  16. lemma OAI.CriticalSK.naturalOverlapConstant_pos line 249
  17. lemma OAI.CriticalSK.natural_GibbsOverlap_tight line 253
  18. lemma OAI.CriticalSK.two_thirds_cube line 297
  19. lemma OAI.CriticalSK.covariance_lower_tight line 301
  20. lemma OAI.CriticalSK.covariance_upper_tight line 317
  21. lemma OAI.CriticalSK.tight_interval_limit line 344
  22. theorem OAI.CriticalSK.covariance_natural_scale line 386