OAI/Probability/InvariantIsing/Pressure/GroundStateLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The deterministic ground-state limit, almost surely and in expectation, and the existence of the full real-temperature variational limit.

  1. def OAI.InvariantIsing.thermalVariationalValue line 16

    Also declared: ComparatorChallenges/InvariantIsing.lean:214 (same declaration text).

  2. theorem OAI.InvariantIsing.ground_state_limit line 19