OAI/Probability/SLE/Gauge/SerpentineActualRadius.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Successful physical prefixes leave a definite ball around the marked point in the actual surviving domain, hence finish before a fixed radius level.

  1. lemma OAI.SLEExactGauge.Serpentine.good_physicalFit_ball_survives line 18
  2. theorem OAI.SLEExactGauge.Serpentine.good_physicalExperiment_ball_survives line 36
  3. def OAI.SLEExactGauge.Serpentine.experimentRadiusLevel line 61
  4. lemma OAI.SLEExactGauge.Serpentine.experimentRadiusLevel_nonneg line 63
  5. lemma OAI.SLEExactGauge.Serpentine.experimentRadiusLevel_cutoff line 68
  6. theorem OAI.SLEExactGauge.Serpentine.good_physicalExperiment_before_radius line 74