OAI/Probability/SLE/Angle/TargetFlowIdentification.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Identification of the prescribed Euler flow with an actual capacity-two Loewner witness, including its geometric surviving domain.

  1. lemma OAI.SLEExactGauge.Target.negative_clock_coefficient line 15
  2. lemma OAI.SLEExactGauge.Target.surviving_cutoff_identifies line 28
  3. lemma OAI.SLEExactGauge.Target.rescaled_witness_trajectory line 78
  4. lemma OAI.SLEExactGauge.Target.surviving_iff_witness line 117
  5. lemma OAI.SLEExactGauge.Target.flow_eq_witness line 131
  6. lemma OAI.SLEExactGauge.Target.surviving_iff_witness_real_time line 143
  7. lemma OAI.SLEExactGauge.Target.flow_eq_witness_real_time line 154
  8. lemma OAI.SLEExactGauge.Target.inverseFlow_eq_witness line 166
  9. lemma OAI.SLEExactGauge.Target.trace_eq_witness line 191