OAI/Probability/InvariantIsing/Cavity/CavityHaarVariablePenalty.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removal of the geometric penalty before replacing the random compression blocks. The Haar fourth moment is uniform in those blocks.

  1. theorem OAI.InvariantIsing.cavity_haar_variable_quadratic_penalty line 15