OAI/Probability/InvariantIsing/Gaussian/GaussianFiniteColumnMinimum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Passing the row tests to the full unit sphere in Gordon's matrix comparison.

  1. lemma OAI.InvariantIsing.continuous_gaussianPattern_apply line 12
  2. theorem OAI.InvariantIsing.gaussian_finite_column_minimum line 19