OAI/Probability/SLE/Loewner/TraceRestrictionContinuity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Rational first-visit identities extend simultaneously to all finite times by local total-variation continuity.

  1. theorem OAI.SLEExactGauge.Multipoint.trace_restriction_of_rational_times line 16