OAI/Probability/InvariantIsing/Gaussian/GaussianTestVariance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The proved regular-potential Poincare inequality at the standard Gaussian.

  1. theorem OAI.InvariantIsing.gaussian_test_variance_le line 12