OAI/Probability/SLE/Loewner/RawReverseComposition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A tail of a reverse trajectory is the raw inverse at the earlier capacity time. This identity needs no geometric trace.

  1. lemma OAI.SLEExactGauge.reverse_height_mono_nonneg line 14
  2. lemma OAI.SLEExactGauge.Target.raw_reverse_tail_inverse line 25