OAI/Probability/SLE/Mass/RadonPathCertificates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Countable compact-test certificates for order and continuous Radon paths. The cutoff coordinates in the determining family supply local mass bounds.

  1. lemma OAI.SLEExactGauge.positive_part_error line 19
  2. theorem OAI.SLEExactGauge.LocalTestFamily.measure_le_of_positive_tests line 27
  3. theorem OAI.SLEExactGauge.LocalTestFamily.continuous_integrals_of_tests line 52