OAI/Probability/SLE/Gauge/PrescribedOrdinaryTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Transfer of the exact prescribed-gauge criterion from a regular Brownian presentation to the original ordinary SLE probability space.

  1. theorem OAI.SLEExactGauge.RegularSLEPresentation.prescribed_main_of_canonical_angle_bounds line 16
  2. theorem OAI.SLEExactGauge.ordinary_prescribed_main_of_canonical_angle_bounds line 58