OAI/Probability/SLE/Stochastic/WienerGridSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Nondegenerate independent Gaussian increments give positive probability to every based finite grid tube.

  1. lemma OAI.SLEExactGauge.gaussianReal_ball_pos line 14
  2. lemma OAI.SLEExactGauge.nat_path_error_le line 21
  3. lemma OAI.SLEExactGauge.wienerGridTime_strictMono line 37
  4. theorem OAI.SLEExactGauge.wienerGrid_tube_pos line 43