OAI/Probability/SLE/Loewner/RawLifetimeFlowLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Both coordinates of the raw forward flow approach the driver at a finite lifetime. Updating the terminal value gives a continuous path.

  1. theorem OAI.SLEExactGauge.Target.flow_tendsto_driver_at_lifetime line 15
  2. theorem OAI.SLEExactGauge.Target.continuousOn_flow_with_terminal_driver line 36