BoundedSpliceProbability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Passage from the actual bounded first-height event. The geometry of the stopped past is derived from the measurable certificate, rather than imposed separately on the stopped Loewner realization.

theorem OAI.SLEExactGauge.brownian_capacity_trace_adapted line 16
theorem OAI.SLEExactGauge.bounded_firstHeight_splice_positive line 31

theorem OAI.SLEExactGauge.bounded_firstHeight_splice_varying_probability line 75

Source documentation

Actual bounded-height splice support combined with varying early events produces one positive probability for the whole sequence of charts.

theorem bounded_firstHeight_splice_varying_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