OAI/Probability/SLE/Loewner/TargetCutoffMeasurability.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Joint measurability and finite-prefix dependence of the prescribed cutoff flow. The variable initial point is encoded as a displacement in the already constructed measurable Picard equation.

  1. lemma OAI.SLEExactGauge.Target.measurable_cutoffField line 16
  2. lemma OAI.SLEExactGauge.Target.measurable_cutoffFlow line 27
  3. def OAI.SLEExactGauge.Target.stopDriver line 61
  4. lemma OAI.SLEExactGauge.Target.stopDriver_apply line 66
  5. lemma OAI.SLEExactGauge.Target.stopDriver_measurable_past line 69
  6. lemma OAI.SLEExactGauge.Target.cutoffFlow_eq_of_driver_prefix line 83
  7. lemma OAI.SLEExactGauge.Target.cutoffFlow_stopDriver line 98
  8. lemma OAI.SLEExactGauge.Target.cutoffFlow_measurable_past line 106