OAI/Probability/InvariantIsing/Pressure/RandomSqrtLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Continuous square-root transport with uniform integrability.

  1. lemma OAI.InvariantIsing.uniformIntegrable_add_real line 11
  2. lemma OAI.InvariantIsing.uniformIntegrable_abs_real line 21
  3. lemma OAI.InvariantIsing.random_sqrt_scaled_limit line 30