OAI/Probability/SLE/Gauge/UniformRecenteredPassage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform passage constants for actual recentered ribbon configurations. The finite chart realization and normalization law are constructed, and subsequence compactness supplies the diagonal estimate.

  1. theorem OAI.SLEExactGauge.uniform_recentered_passage_from_geometry line 20