OAI/Probability/InvariantIsing/Arrays/TensorContactZeroBoundary.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The genuine zero-temperature boundary differs from the entropy contact bound only by the already controlled finite perturbation cost.

  1. lemma OAI.InvariantIsing.tensorContact_zero_temperature_bound line 17