OAI/Probability/SLE/Mass/LevelRadonKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Passage of the conditional Green kernel to the actual common Radon limits. The hypotheses on the limits are exactly those furnished by the common convex extraction, including its retained L² pairings.

  1. lemma OAI.SLEExactGauge.Multipoint.level_radon_mean_finite_on_compacts line 19
  2. theorem OAI.SLEExactGauge.Multipoint.level_radon_conditional_kernel line 43