OAI/Probability/SLE/Loewner/ActualApproach.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The one-point approach estimate conditional on an actual finite stopped past. The density on that past is the exact terminal finite-centered law.

  1. lemma OAI.SLEExactGauge.greenDensity_radius_factor line 23
  2. theorem OAI.SLEExactGauge.actual_conditional_radius_approach line 33