WaypointBrownianPassages.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform Brownian waypoint tube events stay initially in the surviving domain, then avoid the complete access guide and hit the stopped past.

theorem OAI.SLEExactGauge.RibbonCoordinates.early_waypoint_coordinate_ball_safe line 15
theorem OAI.SLEExactGauge.RibbonCoordinates.physical_early_waypoint_tube_survives line 55

theorem OAI.SLEExactGauge.RibbonCoordinates.uniform_brownian_waypoint_passage_geometry line 99

Source documentation

One positive probability gives the complete route geometry: the early part survives, the later part avoids the full guide, and the final leg hits the actual stopped past. No harmonic-measure labels are assumed.

theorem uniform_brownian_waypoint_passage_geometry
    (hopen : PublishedPlanarDiskOpenness) (hsupport : PublishedPlanarWienerUnitSupport)
    (W : WienerLaw) (hW : IsWiener W) (C K : ℝ≥0) (hK : 0 < (K : ℝ)) :
    ∃ q : ℝ≥0∞, 0 < q ∧ ∀ P : ℂ → ℂ,
      ContinuousOn P closedRibbon → InjOn P closedRibbon →
      (∀ z ∈ closedRibbon, 0 < z.re → P z ∈ upperHalfPlane) →
      ∀ k ε x side : ℝ, 1 ≤ k → 0 < ε → ε ≤ 1 / 8 → |x| ≤ 1 / 16 →
      (side = -1 ∨ side = 1) → LipschitzOnWith C P (crossingPatch k) →
      (∀ u ∈ crossingPatch k, ∀ v ∈ crossingPatch k,
        dist u v ≤ K * dist (P u) (P v)) →
      ∀ (γ xp : ℝ≥0 → ℂ) (T : ℝ≥0), 0 < T →
      ContinuousOn xp (Icc 0 T) → EqOn γ (P ∘ xp) (Icc 0 T) →
…

Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.PublishedPlanarWienerUnitSupport, OAI.SLEExactGauge.RibbonCoordinates.closedRibbon, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.RibbonCoordinates.crossingPatch