PassageSuccess.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The same retained continuation certifies the whole passage, its terminal position, and its sausage mass. No success or stopping-window event is assumed.

theorem OAI.SLEExactGauge.PassageSuccess.eventual_retained_success_probability line 17

Source documentation

A single finite retention preserves a positive fraction of the varying probability and certifies every eventual success property of the retained sets.

theorem eventual_retained_success_probability
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsFiniteMeasure P]
    (E : Set Ω) (D : ℕ → Set Ω) (G S : ℕ → Set Ω)
    (hE : MeasurableSet E) (hD : ∀ i, MeasurableSet (D i))
    (hcover : P (E \ ⋃ i, D i) = 0) (q : ℝ) (hq : 0 < q)
    (hG : ∀ᶠ n in atTop, ENNReal.ofReal q ≤ P (G n ∩ E))
    (hS : ∀ i, ∀ᶠ n in atTop, ∀ᵐ ω ∂P, ω ∈ G n ∩ E ∩ D i → ω ∈ S n) :
    ∀ᶠ n in atTop, ENNReal.ofReal (q / 2) ≤ P ((G n ∩ S n) ∩ E) := by
…

def OAI.SLEExactGauge.PassageSuccess.FrontSuccess line 54

Source documentation

Concrete success of the first front stop, including the full preceding path and the required terminal offset.

def FrontSuccess {Ω : Type*}
    (η : ℕ → Ω → ℝ≥0 → ℂ) (pₙ : ℕ → ℂ → ℝ) (σ : Ω → ℝ≥0)
    (Vₙ : ℕ → Set ℂ) (aₙ : ℕ → ℂ) (ε : ℝ) (n : ℕ) : Set Ω :=
…

theorem OAI.SLEExactGauge.PassageSuccess.retained_tube_firstFront_success_mass line 62

Source documentation

Actual successful passage and sausage mass from the same retained tube.

theorem retained_tube_firstFront_success_mass
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (f : Ω → C(ℝ≥0, ℂ)) (hf : Measurable f)
    (hSLE : IsOrdinaryChordalSLE κ (fun ω => f ω) P)
    (σ : Ω → ℝ≥0) (hσ : Measurable σ)
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ)
    (hFn : ∀ n, DifferentiableOn ℂ (Fₙ n) upperHalfPlane)
    (hinj : ∀ n, InjOn (Fₙ n) upperHalfPlane)
    (hF : DifferentiableOn ℂ F upperHalfPlane)
    (hne : ∀ z ∈ upperHalfPlane, deriv F z ≠ 0)
    (hconv : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
…

Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.upperHalfPlane