OAI/Probability/SLE/Gauge/PrescribedCandidateCover.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual finite candidate and missed-cell covers for a prescribed batch. Candidate selection uses the terminal spatial measure. No terminal event is inserted into the adapted finite change of law.

  1. def OAI.SLEExactGauge.prescribedCandidateIndices line 18
  2. def OAI.SLEExactGauge.prescribedMissedIndices line 29
  3. theorem OAI.SLEExactGauge.prescribed_candidates_finite_cover line 39