OAI/Probability/SLE/Mass/LevelApproximationSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-level mass is carried near the actual past trace. On an interior compact, the neighborhood shrinks as the level tends to infinity.

  1. lemma OAI.SLEExactGauge.Multipoint.levelApproximationDensity_eq_zero_of_avoidance line 14