OAI/Probability/SLE/Angle/TargetPathNormalization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A measurable normalization of arbitrary continuous paths. On based paths it is inverse to the physical-time unnormalization.

  1. def OAI.SLEExactGauge.normalizePath line 18
  2. lemma OAI.SLEExactGauge.measurable_normalizePath line 23
  3. lemma OAI.SLEExactGauge.normalize_unnormalize line 30
  4. lemma OAI.SLEExactGauge.measurableEmbedding_unnormalizeDriver line 39
  5. lemma OAI.SLEExactGauge.unnormalizeDriver_law line 44