OAI/Probability/SLE/Gauge/PrescribedCostConvergence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The source's pointwise missed-cell bounds imply vanishing expected cleanup cost for the exact prescribed gauge.

  1. theorem OAI.SLEExactGauge.expected_prescribed_missed_cost_le line 15
  2. theorem OAI.SLEExactGauge.prescribed_missed_cost_tendsto_zero line 49