MarkedTubeHarmonicMeasure.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Convert the two explicit marked-point Brownian tubes into lower bounds for both conformal exit arcs. Every geometric condition concerns actual paths in the surviving domain; the only probabilistic input here is the generic published conformal Brownian exit law.

lemma OAI.SLEExactGauge.Serpentine.marked_window_tubes_opposite_sides line 18
theorem OAI.SLEExactGauge.Serpentine.marked_tubes_harmonic_bounds line 34

theorem OAI.SLEExactGauge.Serpentine.marked_tube_first_exit_geometry line 82

Source documentation

Early survival, a final exit and avoidance of the actual complete guide imply the geometric hypotheses in the harmonic-measure theorem.

theorem marked_tube_first_exit_geometry
    (D : Set ℂ) (hD : IsOpen D) (g : ℂ → ℂ) (h : ℂ ≃ₜ ℂ)
    (α : ℝ≥0 → ℂ)
    (hzero : ∀ z ∈ D, (h (g z)).re = 0 → ∃ u : ℝ≥0, 0 < u ∧ α u = z)
    (ζ : ℝ → ℂ) (hc : Continuous ζ)
    (hearly : MapsTo ζ (Icc (0 : ℝ) (1 / 64)) D)
    (hlast : ζ 3 ∉ D)
    (havoid : ∀ t ∈ Icc (1 / 64 : ℝ) 3, ∀ u : ℝ≥0, 0 < u → ζ t ≠ α u) :
    ∃ τ : ℝ, UnitWindowFirstExit D ζ τ ∧ (1 / 64 : ℝ) < τ ∧
      ∀ t ∈ Ico (1 / 64 : ℝ) τ, (h (g (ζ t))).re ≠ 0 := by
…

Mentions: OAI.SLEExactGauge.UnitWindowFirstExit