OAI/Probability/SLE/Gauge/CanonicalLateGridLower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The lower bound only needs the centered tail comparison in sufficiently late batches. Every earlier entry is controlled by its finite probability law.

  1. def OAI.SLEExactGauge.prescribedCompactGridCell line 16
  2. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.ae_positive_prescribed_of_late_disk_tails line 28