OAI/Probability/SLE/Loewner/TargetInverseMeasurability.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A measurable inverse of the raw surviving flow. The inverse is the prescribed inverseFlow, including its value zero outside its range.

  1. def OAI.SLEExactGauge.Target.survivingState line 16
  2. def OAI.SLEExactGauge.Target.survivingStateMap line 19
  3. lemma OAI.SLEExactGauge.Target.measurable_survivingStateMap line 22
  4. lemma OAI.SLEExactGauge.Target.survivingStateMap_injective line 26
  5. lemma OAI.SLEExactGauge.Target.measurableEmbedding_survivingStateMap line 36
  6. lemma OAI.SLEExactGauge.Target.inverseFlow_eq_extend line 41
  7. lemma OAI.SLEExactGauge.Target.measurable_inverseFlow line 75