OAI/Probability/SLE/Gauge/PrescribedCoverEvents.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite terminal candidate family has measurable missed-cell cost. Only this cost envelope is integrated; the spatial selection itself need not be chosen measurably.

  1. lemma OAI.SLEExactGauge.trace_inter_nonempty line 16
  2. theorem OAI.SLEExactGauge.prescribedMissedIndices_measurable line 24
  3. theorem OAI.SLEExactGauge.prescribed_missed_cost_measurable line 55