OAI/Probability/SLE/Stochastic/BrownianFiniteSmallBall.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive probability of a uniformly small real Brownian driver on any fixed finite time interval, using its actual based path law.

  1. def OAI.SLEExactGauge.driverUnitSmallBall line 17
  2. lemma OAI.SLEExactGauge.isOpen_driverUnitSmallBall line 20
  3. lemma OAI.SLEExactGauge.driverUnitSmallBall_positive line 37
  4. theorem OAI.SLEExactGauge.brownian_finite_smallBall_positive line 47