OAI/Probability/SLE/Mass/CanonicalMassPositiveReduction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The remaining scaling link in positive canonical mass: equal nonzero-mass probabilities at positive times suffice, with the Green mean and the Brownian germ argument already proved.

  1. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.positive_all_times_of_scaling line 21