OAI/Probability/SLE/Geometry/ActualWienerSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite-window planar Wiener support from finite Gaussian increments, independent interpolation residuals, and uniform continuity.

  1. def OAI.SLEExactGauge.wienerUnitClamp line 13
  2. lemma OAI.SLEExactGauge.continuous_wienerUnitClamp line 16
  3. lemma OAI.SLEExactGauge.wienerUnitClamp_unit line 20
  4. lemma OAI.SLEExactGauge.wienerUnitClamp_zero line 25
  5. theorem OAI.SLEExactGauge.actual_planarWienerUnitSupport line 31

    Source documentation

    The planar Wiener law gives positive probability to each uniform tube about a continuous based path, as in Millet--Sanz-Sole (1994), Theorem 3.5.

    theorem actual_planarWienerUnitSupport : PublishedPlanarWienerUnitSupport := by
…

    Mentions: OAI.SLEExactGauge.PublishedPlanarWienerUnitSupport