OAI/Probability/SLE/Multipoint/MultipointFieldBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Drift and Brownian cross bounds for the concrete regularized fields.

  1. theorem OAI.SLEExactGauge.Multipoint.regularizedLogFactor_relative_drift line 12
  2. lemma OAI.SLEExactGauge.Multipoint.regularizedLogFactor_relative_spatial line 35
  3. theorem OAI.SLEExactGauge.Multipoint.regularizedLogFactor_pair_absorption line 47