OAI/Probability/SLE/Mass/RationalTraceMassSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The trace support of rational increments passes simultaneously to every real interval, using only monotonicity and continuity of the trace.

  1. lemma OAI.SLEExactGauge.exists_rational_trace_enclosure_avoiding line 18
  2. theorem OAI.SLEExactGauge.HalfPlaneTraceIncrements.extension_increment_carried line 48