OAI/Probability/SLE/Gauge/PrescribedVisitBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The ordinary one-point estimate bounds every actual missed cell, including the bottom half-row of the shifted grid.

  1. theorem OAI.SLEExactGauge.prescribed_missed_cell_visit_bound line 14