OAI/Probability/SLE/Geometry/RegularSlitTube.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Open-tube support for a deterministic slit with regular real characteristics. The slit geometry and the existence of these characteristics remain explicit deterministic obligations.

  1. def OAI.SLEExactGauge.RegularRealCharacteristics line 16
  2. lemma OAI.SLEExactGauge.regular_slit_driver_trace_containment line 22
  3. theorem OAI.SLEExactGauge.regular_slit_driver_tube line 48
  4. theorem OAI.SLEExactGauge.regular_slit_tube_positive line 77
  5. theorem OAI.SLEExactGauge.ordinary_regular_slit_tube_positive line 97