ActualRadiusStops.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Geometric conformal-radius levels have increasing stopping-time versions. Running maxima make the versions increasing on every outcome, while preserving the actual geometric times almost surely.

lemma OAI.SLEExactGauge.exists_live_level_of_radiusLevelTime_lt_top line 16
lemma OAI.SLEExactGauge.live_radius_level_before line 24
lemma OAI.SLEExactGauge.radiusLevelTime_mono line 52
def OAI.SLEExactGauge.runningMaxStops line 66
lemma OAI.SLEExactGauge.runningMaxStops_stopping line 71
lemma OAI.SLEExactGauge.runningMaxStops_monotone line 78
lemma OAI.SLEExactGauge.runningMaxStops_eq_of_monotone line 83

theorem OAI.SLEExactGauge.exists_monotone_radiusLevel_stops line 94

Source documentation

One increasing stopping sequence represents all prescribed radius levels simultaneously, including outcomes on which a level is never hit.

theorem exists_monotone_radiusLevel_stops
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t))
    (hBm : Measurable (fun p : ℝ≥0 × Ω => B p.1 p.2))
    (hBc : ∀ ω, Continuous (fun t => B t ω)) (hB0 : ∀ ω, B 0 ω = 0)
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ᵐ ω ∂P, IsCapacityTwoWitness
      (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
    (z : ℂ) (hz : z ∈ upperHalfPlane)
    (u : ℕ → ℝ) (hu : ∀ j, 0 ≤ u j) (hmono : Monotone u) :
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upperHalfPlane