SequencePassage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Sequencewise ribbon passage from the actual bounded first-height event. The early event is stopped-image containment, and the retained mass window is the actual first front crossing constructed from the continuation.

theorem OAI.SLEExactGauge.SequencePassage.eventual_bounded_splice_probability line 20

Source documentation

The actual stopped-image events give one positive splice probability. The finite initial part of the sequence does not need an early-loss estimate.

theorem eventual_bounded_splice_probability
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (B₀ : ℝ≥0 → Ω → ℝ) (hB₀ : IsBrownianReal B₀ P)
    (hm : ∀ t, Measurable (B₀ t)) (hc : ∀ ω, Continuous (fun t => B₀ t ω))
    (γ : Ω → ℝ≥0 → ℂ) (G F₀ : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B₀ t ω)
      (γ ω) (G ω) (F₀ ω))
    (hboundary : PublishedLoewnerBoundaryExtension)
    (hsupport : PublishedGeometricTubeSupport P γ)
    (B r : ℝ) (hB : 0 < B) (hr : 0 < r) (Tc : ℝ≥0)
    (F : ℂ → ℂ) (hF : ContinuousOn F upperHalfPlane) (a : ℂ)
…

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

theorem OAI.SLEExactGauge.SequencePassage.uniform_bounded_firstHeight_real_probability line 98

Source documentation

The published support input and proved scaling law give a real positive lower probability, uniformly in the first-height scale.

theorem uniform_bounded_firstHeight_real_probability
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (B₀ : ℝ≥0 → Ω → ℝ) (hB₀ : IsBrownianReal B₀ P)
    (hm : ∀ t, Measurable (B₀ t)) (hc : ∀ ω, Continuous (fun t => B₀ t ω))
    (γ : Ω → ℝ≥0 → ℂ) (G F₀ : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B₀ t ω)
      (γ ω) (G ω) (F₀ ω))
    (hsupport : PublishedGeometricTubeSupport P γ) :
    ∃ T₀ : ℝ≥0, 0 < T₀ ∧ ∃ q : ℝ, 0 < q ∧ ∀ B : ℝ, 0 < B →
      ENNReal.ofReal q ≤ P (stoppedNarrowCertificate γ
        (fun ω => boundedFirstHeightTime (γ ω) B (T₀ * (Real.toNNReal B) ^ 2))
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedGeometricTubeSupport