OAI/Probability/SLE/Loewner/CanonicalTraceCandidate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The raw inverse-flow trace candidate has a measurable continuous-path modification under the actual Wiener law. No trace-generation input is used.

  1. def OAI.SLEExactGauge.unnormalizeDriver line 19
  2. lemma OAI.SLEExactGauge.measurable_unnormalizeDriver line 22
  3. lemma OAI.SLEExactGauge.unnormalize_normalizedDriver line 27
  4. theorem OAI.SLEExactGauge.exists_canonical_trace_candidate_modification line 36