OAI/Probability/SLE/Geometry/HarmonicPathMaximum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Passing the finite mesh maximal estimate to all times between two compact localization stops.

  1. lemma OAI.SLEExactGauge.mul_measure_le_of_eventually_mem line 14
  2. theorem OAI.SLEExactGauge.harmonic_path_maximal line 31