OAI/Probability/SLE/Angle/AngleEigenStopped.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact stopped mean identities for every angular eigenpolynomial.

  1. lemma OAI.SLEExactGauge.ClippedLogSolution.stopped_harmonic_bounded line 14
  2. lemma OAI.SLEExactGauge.logEigenDensity_bound line 61
  3. lemma OAI.SLEExactGauge.AngularLocalization.mean_eigen line 78