OAI/Probability/SLE/Stochastic/PlanarGaussianMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The two-coordinate Gaussian generator estimate. Its error is uniform under the compact smooth test bounds used for stopped planar Brownian motion.

  1. def OAI.SLEExactGauge.planarGaussianMean line 13
  2. lemma OAI.SLEExactGauge.planar_gaussian_generator_error line 16