OAI/Probability/SLE/Mass/RationalCanonicalMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual common convex-tail construction at rational times, with adapted versions, positive trace increments and its conditional Green kernel.

  1. def OAI.SLEExactGauge.Multipoint.rationalMassTime line 19
  2. lemma OAI.SLEExactGauge.Multipoint.rationalMassTime_encode line 22
  3. structure OAI.SLEExactGauge.Multipoint.RationalCanonicalMass line 26
  4. theorem OAI.SLEExactGauge.Multipoint.exists_rationalCanonicalMass line 62