OAI/Probability/SLE/Geometry/ContinuousRangeCompletion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Continuous images of Baire space are measurable in the completion of a finite measure. This supplies the uncountable-time projection step for SLE.

  1. def OAI.SLEExactGauge.prefixCylinder line 13
  2. lemma OAI.SLEExactGauge.prefixCylinder_nil line 16
  3. lemma OAI.SLEExactGauge.prefixCylinder_children line 20
  4. lemma OAI.SLEExactGauge.prefixCylinder_res line 30
  5. theorem OAI.SLEExactGauge.nullMeasurableSet_continuous_baire_range line 34
  6. theorem OAI.SLEExactGauge.nullMeasurableSet_of_analytic_finite line 101