OAI/Probability/SLE/Gauge/PrescribedDiskConditional.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The normalized disk success probability is a genuine conditional lower bound under the actual finite centered law, tested against its full past.

  1. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.prescribed_disk_conditional_bound line 16