OAI/Probability/SLE/Angle/TargetFlowInjectivity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The raw cutoff construction retains injectivity on the surviving domain. This is used to construct its inverse as a measurable map.

  1. lemma OAI.SLEExactGauge.Target.cutoffFlow_injective line 13
  2. lemma OAI.SLEExactGauge.Target.surviving_common_cutoff line 30
  3. lemma OAI.SLEExactGauge.Target.flow_injOn_surviving line 55