OAI/Probability/SLE/Gauge/PrescribedAdaptedBatch.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact chronological batch is adapted to its preceding endpoints. The intervening gap remains available for finite-centered angle mixing; the half-probability bound is conditioned before that gap.

  1. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.prescribed_adapted_batch_failure line 23