OAI/Probability/SLE/Gauge/RibbonStepPatch.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A fixed compact coordinate patch for the actual one-step ribbon.

  1. def OAI.SLEExactGauge.RibbonCoordinates.ribbonStepPatch line 16

    Source documentation

    The length-four patch used for one step and its two-sided waypoint routes.

    def ribbonStepPatch (k : ℝ) : Set ℂ :=
…
  2. def OAI.SLEExactGauge.RibbonCoordinates.ribbonStepCompact line 20

    Source documentation

    A padded compact patch in coordinates relative to the current front.

    def ribbonStepCompact : Set ℂ :=
…
  3. theorem OAI.SLEExactGauge.RibbonCoordinates.ribbonStepCompact_isCompact line 23
  4. theorem OAI.SLEExactGauge.RibbonCoordinates.ribbonStepCompact_interior line 35
  5. theorem OAI.SLEExactGauge.RibbonCoordinates.ribbonStepCompact_zero line 47
  6. theorem OAI.SLEExactGauge.RibbonCoordinates.ribbonStepCompact_core line 51
  7. theorem OAI.SLEExactGauge.RibbonCoordinates.ribbonStepCompact_passage line 59
  8. theorem OAI.SLEExactGauge.RibbonCoordinates.guidePatch_subset_ribbonStepPatch line 67
  9. theorem OAI.SLEExactGauge.RibbonCoordinates.crossingPatch_subset_ribbonStepPatch line 72
  10. theorem OAI.SLEExactGauge.RibbonCoordinates.translate_ribbonStepCompact line 77
  11. theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_translate line 82