PublishedWienerSupport.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The finite-window planar Brownian support input.

Millet--Sanz-Sole (1994), A simple proof of the support theorem for diffusion processes, Seminaire de Probabilites XXVIII, Theorem 3.5, p. 47: specialize to dimension two, identity diffusion and zero drift. Only positivity of uniform tubes about based continuous paths on [0,1] is retained. The product of two real Wiener laws is the planar law. The Hölder support statement implies this weaker uniform-topology consequence, using density of polygonal Cameron--Martin paths. https://www.numdam.org/article/SPS_1994__28__36_0.pdf

def OAI.SLEExactGauge.planarUnitPath line 32
theorem OAI.SLEExactGauge.continuous_planarUnitPath line 37
def OAI.SLEExactGauge.PublishedPlanarWienerUnitSupport line 50
Source documentation
A precise published input about ordinary planar Brownian motion, without any ribbon geometry or uniform-in-route probability conclusion.
```
def PublishedPlanarWienerUnitSupport : Prop :=
…
```

theorem OAI.SLEExactGauge.uniform_planarWiener_tube_probability line 56

Source documentation

The uniform probability needed for the bounded-speed physical route family is derived from the pointwise published support statement.

theorem uniform_planarWiener_tube_probability
    (hpublished : PublishedPlanarWienerUnitSupport)
    (W : WienerLaw) (hW : IsWiener W) (C : ℝ≥0) {ε : ℝ} (hε : 0 < ε) :
    ∃ q : ℝ≥0∞, 0 < q ∧ ∀ f : unitInterval →ᵇ ℂ,
      LipschitzWith C f → f 0 = 0 → q ≤ (W.prod W)
        {b | ∀ t : unitInterval, dist (planarUnitPath b t) (f t) < ε} := by
…

Mentions: OAI.SLEExactGauge.PublishedPlanarWienerUnitSupport, OAI.SLEExactGauge.planarUnitPath