OAI/Probability/SLE/Multipoint/MultipointStateBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Deterministic compact bounds for the adapted state and its discount. Only the Brownian coordinate needs a separate stopping bound.

  1. lemma OAI.SLEExactGauge.Multipoint.lipschitz_state_norm_le line 14
  2. lemma OAI.SLEExactGauge.Multipoint.discounted_state_norm_bound line 26