RetainedRegionMargins.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Physical middle-strip margins are chosen separately for each retained compact set. A finite probability retention then permits their finite union; no inclusion of the entire limiting open strip in every moving strip is used.

theorem OAI.SLEExactGauge.RetainedTubeSausage.eventual_middle_neighborhood line 17

Source documentation

Each compact subset of the limiting middle strip has one open physical neighborhood lying in every sufficiently late moving middle strip.

theorem eventual_middle_neighborhood
    (pₙ : ℕ → ℂ → ℝ) (p : ℂ → ℝ) (U : Set ℂ) (hU : IsOpen U)
    (hp : ContinuousOn p U) (hconv : TendstoLocallyUniformlyOn pₙ p atTop U)
    (K : Set ℂ) (hK : IsCompact K)
    (hband : K ⊆ U ∩ {z | (1 / 3 : ℝ) < p z ∧ p z < 2 / 3}) :
    ∃ R : Set ℂ, IsOpen R ∧ K ⊆ R ∧
      ∀ᶠ n in atTop, R ⊆ U ∩ {z | (1 / 3 : ℝ) < pₙ n z ∧ pₙ n z < 2 / 3} := by
…

theorem OAI.SLEExactGauge.RetainedTubeSausage.countable_stopped_mass_ae_window_compact_regions line 48

Source documentation

Finite retention permits compact-dependent physical neighborhoods.

theorem countable_stopped_mass_ae_window_compact_regions
    {Ω : 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)
    (R : ℕ → Set ℂ) (hR : ∀ i, IsOpen (R i)) (himage : ∀ i, F '' K i ⊆ R i)
…

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

theorem OAI.SLEExactGauge.RetainedTubeSausage.countable_stopped_mass_ae_window_middle_regions line 148

Source documentation

Local coordinate convergence supplies the compact-dependent physical margins needed by the retained stopped-mass theorem.

theorem countable_stopped_mass_ae_window_middle_regions
    {Ω : 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)
    (pₙ : ℕ → ℂ → ℝ) (p : ℂ → ℝ) (U : Set ℂ) (hU : IsOpen U)
…

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