OAI/Probability/SLE/Angle/TargetLevelDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The prescribed finite-level density is the actual normalized stopped Green density, with no change to its finite/infinite-time convention.

  1. lemma OAI.SLEExactGauge.Target.alpha_eq line 16
  2. lemma OAI.SLEExactGauge.Target.p_eq line 21
  3. lemma OAI.SLEExactGauge.Target.disk_center_sin_arg line 25
  4. lemma OAI.SLEExactGauge.Target.levelDensity_eq_stoppedGreen line 31
  5. lemma OAI.SLEExactGauge.Target.levelDensity_eq_canonicalFiniteDensity line 84
  6. theorem OAI.SLEExactGauge.Target.levelDensity_integrable_mean line 95