OAI/Probability/SLE/Gauge/PrescribedGaugeCost.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The prescribed quadratic envelope directly pays for enlarged candidate balls and for final cells. Its infinite-diameter convention gives the same Hausdorff outer measure, since the defining limit uses small covers.

  1. lemma OAI.SLEExactGauge.Target.hausdorff_eq_hausdorffGauge line 15
  2. lemma OAI.SLEExactGauge.Target.gauge_le_entry line 26
  3. lemma OAI.SLEExactGauge.Target.gauge_scaled_entry_le line 32
  4. lemma OAI.SLEExactGauge.Target.enlarged_candidate_gauge_cost line 42
  5. lemma OAI.SLEExactGauge.Target.cleanup_cell_gauge_cost line 71