OAI/Probability/InvariantIsing/Magnetic/MagneticPhysicalFieldUpper.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-field upper bound for physical orthogonal Haar matrices, with arbitrary finite eigenvalue and field labelings at every dimension.

  1. theorem OAI.InvariantIsing.finite_physical_field_pressure_upper line 14