OAI/Probability/SLE/Gauge/PrescribedGridLower.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Eventual bounds on the exact prescribed grid imply an arbitrary-cover Hausdorff lower bound. Finitely many early batches are restored uniformly.

  1. lemma OAI.SLEExactGauge.prescribed_grid_ball_bound line 16
  2. lemma OAI.SLEExactGauge.Target.hausdorffGauge_le_hausdorff line 70
  3. lemma OAI.SLEExactGauge.prescribed_grid_mass_distribution line 80