OAI/Probability/SLE/Mass/PositiveTraceMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positive increments and trace support force positive canonical mass in each open set visited at a positive time.

  1. lemma OAI.SLEExactGauge.Multipoint.positive_trace_mass_of_positive_increments line 15
  2. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.positive_open_visited line 54