OAI/Probability/SLE/Multipoint/MultipointActualProbability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed-order radius estimate in an arbitrary conformal image. The only analytic input not proved here is the stated disk growth bound.

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