CompactConformalPassageMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The compact-retention and sausage part of the uniform ribbon step, assembled for actual locally convergent conformal maps and actual SLE. Only the passage event and its retained intervals are supplied by geometry.

theorem OAI.SLEExactGauge.compact_conformal_ribbon_mass line 18

theorem OAI.SLEExactGauge.countable_compact_conformal_ribbon_mass line 67

Source documentation

A countable family of actual retained compact intervals is enough. The finite extraction, common mesh, derivative constants, and unconditional small-sausage subtraction are all performed here.

theorem countable_compact_conformal_ribbon_mass
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (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)
    (K : ℕ → Set ℂ) (hK : ∀ i, IsCompact (K i))
    (hKH : ∀ i, K i ⊆ upperHalfPlane)
…

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