OAI/Probability/SLE/Angle/AngleHarmonicStopped.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bounded stopping for smooth harmonic tests of the logarithmic Loewner state and Brownian driver. This supplies the angular eigenfunction moments.

  1. lemma OAI.SLEExactGauge.compact_harmonic_field line 14
  2. lemma OAI.SLEExactGauge.harmonic_pair_directional line 39
  3. lemma OAI.SLEExactGauge.ClippedLogSolution.stopped_harmonic_compact line 50