OAI/Probability/SLE/Mass/LevelRadonPairings.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The measurable common Radon versions retain the L² pairings. In particular expectations on any past event pass through the same limits.

  1. theorem OAI.SLEExactGauge.Multipoint.exists_measurable_level_radon_limits_with_pairings line 16