OAI/Probability/SLE/Stochastic/WienerBridge.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Independence of the Brownian endpoint and its pinned bridge, used in the finite-window Wiener support theorem.

  1. def OAI.SLEExactGauge.unitBridge line 14
  2. lemma OAI.SLEExactGauge.unitBridge_joint_gaussian line 18
  3. lemma OAI.SLEExactGauge.unitBridge_endpoint_covariance line 42
  4. lemma OAI.SLEExactGauge.unitBridge_independent_endpoint line 61