RetainedTubeSausage.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual open-tube passage certificates imply a positive stopped sausage mass. The retained time window is derived from the front coordinate, rather than supplied as a separate geometric hypothesis.

theorem OAI.SLEExactGauge.RetainedTubeSausage.eventually_front_lt_on_compact line 19

Source documentation

Uniformly convergent physical coordinates preserve a strict front bound on each compact retained parameter set.

theorem eventually_front_lt_on_compact
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ)
    (hF : ContinuousOn F upperHalfPlane)
    (hFconv : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
    (pₙ : ℕ → ℂ → ℝ) (p : ℂ → ℝ) (U : Set ℂ) (hU : IsOpen U)
    (hp : ContinuousOn p U) (hpconv : TendstoLocallyUniformlyOn pₙ p atTop U)
    (K : Set ℂ) (hK : IsCompact K) (hKH : K ⊆ upperHalfPlane)
    (hKU : F '' K ⊆ U) (q : ℝ) (hbound : ∀ z ∈ K, p (F z) < q) :
    ∀ᶠ n in atTop, ∀ z ∈ K, pₙ n (Fₙ n z) < q := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.RetainedTubeSausage.countable_stopped_mass_ae_window line 65

Source documentation

The countable stopped-mass reduction also permits almost-sure window and chart identities, as supplied by the actual boundary restart.

theorem countable_stopped_mass_ae_window
    {Ω : 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 : IsOpen R) (himage : ∀ i, F '' K i ⊆ R)
…

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

theorem OAI.SLEExactGauge.RetainedTubeSausage.countable_stopped_mass_ae_window_eventually line 139

Source documentation

The countable stopped-mass reduction also permits almost-sure window and chart identities, as supplied by the actual boundary restart.

theorem countable_stopped_mass_ae_window_eventually
    {Ω : 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 : IsOpen R) (himage : ∀ i, F '' K i ⊆ R)
…

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

theorem OAI.SLEExactGauge.RetainedTubeSausage.retained_tube_stopped_sausage_mass line 233

Source documentation

Actual tube passages produce retained sausage mass before the varying front stop. Compact intervals and stop windows are both derived here.

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

theorem OAI.SLEExactGauge.RetainedTubeSausage.retained_tube_stopped_sausage_mass_eventually line 323

Source documentation

Actual tube passages produce retained sausage mass before the varying front stop. Compact intervals and stop windows are both derived here.

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