OAI/Probability/SLE/Stochastic/PlanarGeneratorRegularity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compact smooth tests retain bounded smoothness and Lipschitz control under the planar Brownian generator.

  1. lemma OAI.SLEExactGauge.planarGenerator_partial_formula line 13
  2. lemma OAI.SLEExactGauge.planarGenerator_smooth line 24
  3. lemma OAI.SLEExactGauge.planarGenerator_compact line 34
  4. lemma OAI.SLEExactGauge.planarGenerator_bounded_lipschitz line 42