OAI/Probability/SLE/Geometry/HarmonicLimitData.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A bounded measurable terminal variable for each localized harmonic test, with the L1 error required in the full-path maximal estimate.

  1. theorem OAI.SLEExactGauge.SmoothDomainExhaustion.harmonic_limit_data line 16