OAI/Probability/InvariantIsing/Pressure/GibbsMap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pushforward of an integrable terminal Gibbs tilt.

  1. lemma OAI.InvariantIsing.gibbsProbability_map_normalize line 12