OAI/Probability/SLE/Geometry/HarmonicMaximal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite maximal estimate used to control a harmonic test between two of the actual domain-localization stops.

  1. lemma OAI.SLEExactGauge.martingale_abs_sub_initial line 13
  2. lemma OAI.SLEExactGauge.martingale_finite_maximal line 28