OAI/Probability/InvariantIsing/Magnetic/RestrictedConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The published SO(N) concentration input for every fixed nonempty spin constraint, with constants independent of its cardinality.

  1. theorem OAI.InvariantIsing.haar_restricted_pressure_median_tail line 13