OAI/Probability/InvariantIsing/Magnetic/RestrictedCompressionLogLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual random compression and its explicit geometric error give the canonical logarithm with fixed coefficients in the large-system limit.

  1. theorem OAI.InvariantIsing.restricted_compression_log_limit line 16