OAI/Probability/SLE/Geometry/CompactPlanarGaussian.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact smooth planar tests have one uniform Gaussian-generator error constant. These are the tests needed for Brownian localization.

  1. lemma OAI.SLEExactGauge.compact_planar_test_bounds line 14
  2. def OAI.SLEExactGauge.planarGenerator line 55
  3. lemma OAI.SLEExactGauge.compact_planar_gaussian_generator line 59