OAI/Probability/SLE/Gauge/StrictPastTilted.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The strict past-mass formula expressed through finite centered laws. Every spatial integrand is identified before applying monotone convergence.

  1. lemma OAI.SLEExactGauge.Multipoint.finiteCenteredLaw_tests_spatial_tendsto line 26
  2. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.finite_strict_past_tilted_limit line 86