OAI/Probability/SLE/Stochastic/IndependentPlanarIncrements.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Independence of the two-coordinate Wiener increment from its full original past. Product coordinates retain both original pasts.

  1. lemma OAI.SLEExactGauge.measurePreserving_shuffle line 14
  2. lemma OAI.SLEExactGauge.independent_product_pairs line 30