OAI/Probability/SLE/Mass/StrictPastMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The expected terminal mass arriving strictly after a deterministic past is its current Green mass, including arbitrary events in that past.

  1. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.strict_past_mass_kernel line 18