OAI/Probability/SLE/Geometry/NormalizedRawAllTimes.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Random normalization commutes with the raw mass process on one event for every finite horizon. Future-dependent horizons may then be used.

  1. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.normalized_raw_scaling_all_times line 38
  2. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.normalized_raw_restart_all_times line 79