OAI/Probability/SLE/Angle/TargetBrownianNormalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The Brownian time scaling in the prescribed flow, and uniqueness of the based Wiener law used by its deterministic coefficient formula.

  1. def OAI.SLEExactGauge.Target.normalizedDriver line 17
  2. lemma OAI.SLEExactGauge.Target.normalizedDriver_measurable line 23
  3. lemma OAI.SLEExactGauge.Target.normalizedDriver_matches line 30
  4. theorem OAI.SLEExactGauge.Target.normalizedDriver_isBrownian line 37
  5. theorem OAI.SLEExactGauge.Target.normalizedDriver_isWiener line 48
  6. theorem OAI.SLEExactGauge.Target.isWiener_unique line 62
  7. theorem OAI.SLEExactGauge.Target.normalizedDriver_law line 84