OAI/Probability/SLE/Geometry/SingleCrossingObstruction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The local crossing obstruction in the parameter square. Clamping extends the difference map to the plane; the four-side logarithm supplies its outer boundary logarithm.

  1. def OAI.SLEExactGauge.unitClamp line 16
  2. lemma OAI.SLEExactGauge.continuous_unitClamp line 18
  3. lemma OAI.SLEExactGauge.unitClamp_coe line 20
  4. lemma OAI.SLEExactGauge.unitClamp_eq_interior line 22
  5. def OAI.SLEExactGauge.crossingSquareParam line 42
  6. lemma OAI.SLEExactGauge.continuous_crossingSquareParam line 45
  7. def OAI.SLEExactGauge.crossingSquareMap line 49
  8. lemma OAI.SLEExactGauge.continuous_crossingSquareMap line 52
  9. lemma OAI.SLEExactGauge.crossingSquareMap_zero_iff line 56
  10. lemma OAI.SLEExactGauge.crossingSquareParam_on_outer_circle line 70
  11. lemma OAI.SLEExactGauge.no_single_locally_injective_crossing line 92