OAI/Probability/SLE/Gauge/PrescribedCoverExpectation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual prescribed finite covers reduce the Hausdorff expectation to the fixed terminal-mass charge and vanishing expected missed-cell cost. The stochastic missed-cell estimate is kept explicit in this reduction.

  1. def OAI.SLEExactGauge.prescribedMissedCost line 18
  2. theorem OAI.SLEExactGauge.expected_prescribed_hausdorff_le_of_missed_cost line 24