OAI/Probability/InvariantIsing/Magnetic/RestrictedPhysicalLogCoefficients.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic coefficient replacement specialized to the actual base-system Gibbs probability and its physical spectral-group vectors.

  1. theorem OAI.InvariantIsing.restricted_physical_penalized_log_coefficients line 17