OAI/Probability/SLE/Loewner/RawForwardHeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuity and height monotonicity of the exact raw forward flow on each surviving interval, without a geometric trace witness.

  1. lemma OAI.SLEExactGauge.Target.flow_continuousOn_of_survival line 14
  2. lemma OAI.SLEExactGauge.Target.flow_height_antitone_of_survival line 22