OAI/Probability/SLE/Geometry/NormalizedDiskAngle.lean
6 declarations, 0 contain sorry, 0 declared as axioms
Normalization preserves the full stopped argument, which is the state variable needed by the finite-centered transition kernel.
- lemma
OAI.SLEExactGauge.IsCapacityTwoWitness.normalized_restart_stopped_argline 15 - def
OAI.SLEExactGauge.canonicalStoppedAngleline 55 - lemma
OAI.SLEExactGauge.canonicalStoppedAngle_measurableline 58 - lemma
OAI.SLEExactGauge.canonicalStoppedAngle_eqline 62 - lemma
OAI.SLEExactGauge.extendedMarkedAngle_at_finite_radiusline 73 - lemma
OAI.SLEExactGauge.IsCapacityTwoWitness.normalized_disk_stopped_argline 93