OAI/Probability/SLE/Gauge/PrescribedCanonicalTests.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual adapted tests use canonical mass at the finite test endpoint. Terminal candidate failure implies failure of all these earlier tests.

  1. def OAI.SLEExactGauge.Multipoint.CanonicalMass.prescribedBallTest line 21
  2. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.prescribedBallTest_measurable line 25
  3. def OAI.SLEExactGauge.Multipoint.CanonicalMass.prescribedTestFailures line 36
  4. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.prescribedTestFailures_measurable_at_end line 42
  5. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.prescribed_missed_implies_test_failures line 57