OAI/Probability/InvariantIsing/Haar/HaarConcentrationInput.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact Gromov--Milman specialization used by the pressure proof. The proof uses the actual polynomial heat operator on SO(N), its proved curvature bound, positive polynomial convolution, and the scalar entropy argument.

  1. theorem OAI.InvariantIsing.haarConcentration_proved line 15