OAI/Probability/InvariantIsing/Pressure/RandomPressureAlmostSure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The almost-sure random-spectrum pressure theorem, under the conditional orbit law in Proposition gen:random. No global integrability is assumed.

  1. theorem OAI.InvariantIsing.random_pressure_tendsto_ae line 13