OAI/Probability/SLE/Angle/AngleEigenSource.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Identification of the localized harmonic eigenfunctions with the actual stopped Green weight and angle, including paths missing the level.

  1. lemma OAI.SLEExactGauge.logPolynomialDensity_green_factor line 14
  2. lemma OAI.SLEExactGauge.logCosine_logCoordinates line 25
  3. lemma OAI.SLEExactGauge.logCosine_initial line 36
  4. lemma OAI.SLEExactGauge.logPolynomialDensity_initial line 44
  5. lemma OAI.SLEExactGauge.AngularLocalization.eigen_eq_source_of_hit line 62
  6. lemma OAI.SLEExactGauge.AngularLocalization.eigen_small_of_not_hit line 83
  7. lemma OAI.SLEExactGauge.localization_eigen_tendsto line 105