OAI/Probability/SLE/Stochastic/DriverLawKernelTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A deterministic-time kernel specified by the original Brownian past transfers to another Brownian realization with the same continuous path law.

  1. lemma OAI.SLEExactGauge.source_driver_integral_of_same_law_kernel line 21
  2. lemma OAI.SLEExactGauge.source_driver_bind_of_same_law_kernel line 51