OAI/Probability/InvariantIsing/Gaussian/BilinearGaussianComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite bilinear Gaussian comparison behind the sharp rectangular upper edge.

  1. abbrev OAI.InvariantIsing.BilinearGaussianIndex line 12
  2. def OAI.InvariantIsing.bilinearMatrixCoefficient line 14
  3. def OAI.InvariantIsing.bilinearVectorCoefficient line 21
  4. lemma OAI.InvariantIsing.bilinearMatrix_covariance line 28
  5. lemma OAI.InvariantIsing.bilinearVector_covariance line 45
  6. theorem OAI.InvariantIsing.bilinear_gaussian_maximum_comparison line 52