OAI/Probability/SLE/Mass/CanonicalMassNontrivial.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positive initial Green mass and terminal exhaustion give a positive probability of nonzero canonical mass at a finite deterministic time.

  1. lemma OAI.SLEExactGauge.Multipoint.initialGreenMeasure_univ_pos line 16
  2. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.exists_nonzero_finite_time line 44