OAI/Analysis/KadisonKastler/DoubleGaussianCovariance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Covariance of double Gaussian smearing

  1. theorem OAI.KadisonKastler.unitaryRealGroup_commute line 13
  2. theorem OAI.KadisonKastler.doubleGaussian_conjugate line 23
  3. theorem OAI.KadisonKastler.doubleGaussian_first_covariance line 34
  4. theorem OAI.KadisonKastler.doubleGaussian_second_covariance line 41