OAI/Probability/SLE/Geometry/RandomSpatialTestingAE.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local random spatial testing only needs almost-sure finite compact masses. Infinite exceptional restrictions are set to zero measurably.

  1. lemma OAI.SLEExactGauge.finite_restriction_version line 14
  2. lemma OAI.SLEExactGauge.bind_restrict_right line 37
  3. theorem OAI.SLEExactGauge.conditional_random_spatial_test_on_ae line 53