OAI/Probability/InvariantIsing/Pressure/LocalizedAlmostSure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Eventual local exponential tails imply almost-sure convergence whenever the localizing random bound is eventually finite.

  1. lemma OAI.InvariantIsing.exponential_tail_extend_initial line 12
  2. lemma OAI.InvariantIsing.ae_tendsto_zero_of_localized_exponential_tail line 30