OAI/Probability/SLE/Gauge/CanonicalBatchSuccess.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The prescribed finite batch level supplies the successful-test budget. This uses its exact retained moment and the next limiting moment bound.

  1. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.centeredDiskLaw_batch_success line 19