OAI/Probability/SLE/Loewner/SlitPhysicalTrace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The capacity-two curve has exactly the prescribed initial ranges and no additional swallowed points.

  1. def OAI.SLEExactGauge.slitCapacityCurve line 14
  2. lemma OAI.SLEExactGauge.slitCapacityCurve_continuous line 18
  3. lemma OAI.SLEExactGauge.slitCapacityCurve_zero line 23
  4. lemma OAI.SLEExactGauge.slitCapacityCurve_initial_range line 28
  5. lemma OAI.SLEExactGauge.slitCapacityCurve_injOn line 37
  6. lemma OAI.SLEExactGauge.slitCapacityCurve_positive line 48
  7. theorem OAI.SLEExactGauge.slitCapacityCurve_free_complement line 59