EarlyPassageLocalization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Early physical containment of the narrow first-height past. The event is measurable in the stopped past, and failure is an actual conformal localization escape event.

def OAI.SLEExactGauge.EarlyPassageLocalization.stoppedImageEvent line 25
Source documentation
Physical containment of the entire trace segment through a finite stop.
```
def stoppedImageEvent {Ω : Type*} (γ : Ω → ℝ≥0 → ℂ) (σ : Ω → ℝ≥0)
    (Fbar : ℂ → OnePoint ℂ) (a : ℂ) (r : ℝ) : Set Ω :=
…
```
theorem OAI.SLEExactGauge.EarlyPassageLocalization.stoppedImageEvent_measurable line 30

theorem OAI.SLEExactGauge.EarlyPassageLocalization.stoppedImage_failure_subset_escape line 70

Source documentation

Containment failure before a bounded parameter-radius stop is exactly an escape covered by conformal localization.

theorem stoppedImage_failure_subset_escape
    {Ω : Type*} (γ : Ω → ℝ≥0 → ℂ) (σ : Ω → ℝ≥0)
    (E : Set Ω) (Fbar : ℂ → OnePoint ℂ) (a : ℂ) (r A : ℝ)
    (hbound : ∀ ω ∈ E, ∀ t ∈ Icc 0 (σ ω), ‖γ ω t‖ < A) :
    E \ stoppedImageEvent γ σ Fbar a r ⊆
      {ω | ∃ t : ℝ≥0, BeforeFirstModulus (γ ω) A t ∧
        Fbar (γ ω t) ∉ (fun z : ℂ => (z : OnePoint ℂ)) '' ball a r} := by
…

Mentions: OAI.SLEExactGauge.EarlyPassageLocalization.stoppedImageEvent, OAI.SLEExactGauge.BeforeFirstModulus

theorem OAI.SLEExactGauge.EarlyPassageLocalization.bounded_firstHeight_norm line 88

Source documentation

A bounded first-height certificate stays strictly inside the ball of half the rectangle scale.

theorem bounded_firstHeight_norm
    (p : C(ℝ≥0, ℂ)) (hp0 : p 0 = 0) (hpH : ∀ t, 0 ≤ (p t).im)
    {B : ℝ} (hB : 0 < B) (T : ℝ≥0)
    (hcert : let σ := boundedFirstHeightTime p B T
…

theorem OAI.SLEExactGauge.EarlyPassageLocalization.unit_guide_localization line 118

Source documentation

Conformal localization controls a stopped containment failure whenever the past remains below its parameter-radius threshold.

theorem unit_guide_localization
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8) :
    ∃ b C c L₀ : ℝ, 0 < b ∧ 0 < C ∧ 0 < c ∧ 1 < L₀ ∧
    ∀ (Ω : Type*) [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
      (γ : Ω → ℝ≥0 → ℂ), IsOrdinaryChordalSLE κ γ P →
    ∀ (F : ℂ → ℂ) (Fbar : ℂ → OnePoint ℂ),
      DifferentiableOn ℂ F upperHalfPlane → InjOn F upperHalfPlane →
      ContinuousOn Fbar closedHalfPlane →
      (∀ z ∈ upperHalfPlane, Fbar z = (F z : OnePoint ℂ)) →
    ∀ (a : ℂ) (r : ℝ), 0 < r →
    ∀ (η : ℝ → ℂ) (S : ℝ), 0 < S → ContinuousOn η (Icc 0 S) →
      η 0 = 0 → ‖η S‖ = 1 → (∀ t ∈ Icc 0 S, 0 ≤ (η t).im) →
…

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

theorem OAI.SLEExactGauge.EarlyPassageLocalization.escape_under_scaling line 143

Source documentation

Actual capacity scaling transports an escape event, including its strict before-first-modulus condition.

theorem escape_under_scaling
    {Ω : Type*} (γ : Ω → ℝ≥0 → ℂ) (Fbar : ℂ → OnePoint ℂ)
    (c : ℝ≥0) (hc : 0 < c) (A r : ℝ) (a : ℂ) :
    {ω | ∃ t : ℝ≥0, BeforeFirstModulus (γ ω) A t ∧
      Fbar (γ ω t) ∉ (fun z : ℂ => (z : OnePoint ℂ)) '' ball a r} ⊆
    {ω | ∃ t : ℝ≥0, BeforeFirstModulus (sourceScaleTrace c (γ ω)) ((c : ℝ) * A) t ∧
      Fbar (sourceScaleTrace c (γ ω) t / (c : ℂ)) ∉
        (fun z : ℂ => (z : OnePoint ℂ)) '' ball a r} := by
…

Mentions: OAI.SLEExactGauge.BeforeFirstModulus, OAI.SLEExactGauge.sourceScaleTrace

theorem OAI.SLEExactGauge.EarlyPassageLocalization.localization_at_guide_radius line 167

Source documentation

The localization estimate with a guide ending at an arbitrary positive parameter radius, derived by capacity scaling of ordinary SLE.

theorem localization_at_guide_radius
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8) :
    ∃ b C c L₀ : ℝ, 0 < b ∧ 0 < C ∧ 0 < c ∧ 1 < L₀ ∧
    ∀ (Ω : Type*) [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
      (γ : Ω → ℝ≥0 → ℂ), IsOrdinaryChordalSLE κ γ P →
    ∀ (F : ℂ → ℂ) (Fbar : ℂ → OnePoint ℂ),
      DifferentiableOn ℂ F upperHalfPlane → InjOn F upperHalfPlane →
      ContinuousOn Fbar closedHalfPlane →
      (∀ z ∈ upperHalfPlane, Fbar z = (F z : OnePoint ℂ)) →
    ∀ (a : ℂ) (r : ℝ), 0 < r →
    ∀ (η : ℝ → ℂ) (S b₀ : ℝ), 0 < S → 0 < b₀ → ContinuousOn η (Icc 0 S) →
      η 0 = 0 → ‖η S‖ = b₀ → (∀ t ∈ Icc 0 S, 0 ≤ (η t).im) →
…

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

theorem OAI.SLEExactGauge.EarlyPassageLocalization.bounded_firstHeight_localization line 240

Source documentation

The precise early-passage estimate: the bounded narrow first-height past fails physical containment with probability at most the localization power tail.

theorem bounded_firstHeight_localization
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8) :
    ∃ b C c L₀ : ℝ, 0 < b ∧ 0 < C ∧ 0 < c ∧ 1 < L₀ ∧
    ∀ (Ω : Type*) [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
      (γ : Ω → ℝ≥0 → ℂ), IsOrdinaryChordalSLE κ γ P →
      (∀ ω, Continuous (γ ω)) → (∀ ω, γ ω 0 = 0) → (∀ ω t, 0 ≤ (γ ω t).im) →
    ∀ (F : ℂ → ℂ) (Fbar : ℂ → OnePoint ℂ),
      DifferentiableOn ℂ F upperHalfPlane → InjOn F upperHalfPlane →
      ContinuousOn Fbar closedHalfPlane →
      (∀ z ∈ upperHalfPlane, Fbar z = (F z : OnePoint ℂ)) →
    ∀ (a : ℂ) (r : ℝ), 0 < r →
    ∀ (η : ℝ → ℂ) (S b₀ : ℝ), 0 < S → 0 < b₀ → ContinuousOn η (Icc 0 S) →
…

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