OAI/Probability/SLE/Gauge/PrescribedCoverLimits.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The missed-cell error in the prescribed cover vanishes, including the bottom rows whose centers approach the real boundary.

  1. lemma OAI.SLEExactGauge.prescribed_cleanup_radius_le_exp line 14
  2. lemma OAI.SLEExactGauge.prescribed_cover_diameter_tendsto_zero line 22
  3. lemma OAI.SLEExactGauge.prescribed_batch_failure_cost_tendsto_zero line 36
  4. lemma OAI.SLEExactGauge.prescribed_boundary_cost_tendsto_zero line 51
  5. lemma OAI.SLEExactGauge.prescribed_cleanup_error_tendsto_zero line 80