OAI/Probability/SLE/Mass/RawRadonGoodPaths.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A countably measurable event guaranteeing zero initial mass, monotone growth, and continuous compact-test paths for the raw rational reconstruction.

  1. def OAI.SLEExactGauge.RawRadonGood line 16
  2. lemma OAI.SLEExactGauge.measurableSet_rawRadonGood line 22
  3. theorem OAI.SLEExactGauge.RawRadonGood.reconstructed_paths line 40
  4. theorem OAI.SLEExactGauge.rawRadonGood_of_continuous_path line 88