OAI/Probability/SLE/Multipoint/MultipointLocalIdentification.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Safe clipped coordinates identify the actual Loewner flow separately up to each point's completion or the common localization time.

  1. theorem OAI.SLEExactGauge.Multipoint.clipped_multipoint_identification line 16
  2. theorem OAI.SLEExactGauge.Multipoint.stopped_height_gives_local_identification line 34