OAI/Probability/SLE/Geometry/PublishedFiniteBoundaryExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite-valued form of Rohde--Schramm, Basic properties of SLE, Annals of Mathematics 161 (2005), Theorem 4.1, pp. 898--899. The theorem extends the inverse Loewner map continuously to the closed half-plane. Keeping its values in ℂ allows arbitrary deterministic stopped charts to act on an entire fresh continuous trace, before any passage event is selected. This is an explicit published input, not a continuation or passage estimate.

  1. def OAI.SLEExactGauge.PublishedFiniteLoewnerBoundaryExtension line 26
  2. theorem OAI.SLEExactGauge.PublishedFiniteLoewnerBoundaryExtension.to_onePoint line 34
  3. theorem OAI.SLEExactGauge.normalized_finite_capacity_inverse_boundary_extension line 42
  4. def OAI.SLEExactGauge.finiteBoundaryPath line 69

    Source documentation

    A finite boundary chart acts measurably on continuous trace paths.

    def finiteBoundaryPath (Fbar : C(closedHalfPlane, ℂ))
    (p : C(ℝ≥0, ℂ)) : C(ℝ≥0, ℂ) := Fbar.comp (liftClosedPath p)

    Mentions: OAI.SLEExactGauge.closedHalfPlane, OAI.SLEExactGauge.liftClosedPath

  5. theorem OAI.SLEExactGauge.measurable_finiteBoundaryPath line 72
  6. theorem OAI.SLEExactGauge.finiteBoundaryPath_apply line 79