PassageSuccessRegions.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual front-success theorem with moving middle regions. The physical neighborhoods are selected only after finitely many compact middle certificates have been retained.

theorem OAI.SLEExactGauge.PassageSuccess.retained_tube_firstFront_success_mass_middle_regions line 20

Source documentation

Full front success and mass in the moving middle strip. Local uniform coordinate convergence supplies its margin on every retained compact; there is no inclusion assumption on the whole limiting open strip.

theorem retained_tube_firstFront_success_mass_middle_regions
    {Ω : 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