OAI/Probability/SLE/Geometry/RationalTestPath.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A Borel certificate that rational test values extend to a continuous real path. This makes the good-path event countably measurable.

  1. def OAI.SLEExactGauge.rationalTestPathValues line 18
  2. lemma OAI.SLEExactGauge.rationalTestPathValues_embedding line 20
  3. def OAI.SLEExactGauge.HasContinuousRationalTests line 30
  4. lemma OAI.SLEExactGauge.measurableSet_hasContinuousRationalTests line 34
  5. theorem OAI.SLEExactGauge.HasContinuousRationalTests.continuous_extension line 45