OAI/Probability/SLE/Loewner/TargetEulerConvergence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The prescribed dyadic Euler definition converges to the bounded cutoff ODE. Only continuity in time and a global Lipschitz bound in space are used.

  1. def OAI.SLEExactGauge.Target.eulerSlope line 14
  2. lemma OAI.SLEExactGauge.Target.euler_pairs_mem line 18
  3. lemma OAI.SLEExactGauge.Target.euler_pairs_dist_lt line 36
  4. lemma OAI.SLEExactGauge.Target.eulerSlope_error_tendsto line 57
  5. lemma OAI.SLEExactGauge.Target.eulerFlow_tendsto_solution line 78
  6. lemma OAI.SLEExactGauge.Target.cutoffFlow_eq_solution line 114