OAI/Probability/InvariantIsing/Cavity/CavityHaarPenalty.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removal of the geometric quadratic penalty for the physical fresh-Haar model. Its required moments come from the actual Haar frame.

  1. theorem OAI.InvariantIsing.cavity_haar_quadratic_penalty line 15