OAI/Probability/SLE/Mass/CanonicalMassContinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual rational construction extends to an adapted, locally continuous family, with simultaneous support of every finite increment.

  1. structure OAI.SLEExactGauge.Multipoint.ContinuousMassPath line 19
  2. theorem OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.exists_continuous_progressive_extension line 35