OAI/Probability/InvariantIsing/Cavity/CavityHaarRestrictedFloor.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The physical Haar prior supplies the quantitative denominator-floor error. No inverse partition moment or full tilted Haar moment is assumed.

  1. theorem OAI.InvariantIsing.cavity_haar_restricted_floor_error line 17