ActualSequencePassage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual joint guide compactness theorem retains the whole normalized parameter-guide family. Uniform convergence of that family supplies the common access point and the small physical radius needed by the proved sequence passage theorem. No separate access-radius hypothesis is needed.

theorem OAI.SLEExactGauge.SequencePassage.small_initial_access_segment line 20

Source documentation

Uniform guide convergence and simplicity of the limiting guide give a nonzero common access point at an arbitrarily small positive guide time.

theorem small_initial_access_segment
    (C : ℝ≥0) (r : ℝ) (hr : 0 < r)
    (βₙ : ℕ → ℝ → ℂ) (β : ℝ → ℂ)
    (hβ0 : β 0 = 0) (hβi : InjOn β (Icc 0 2))
    (hconv : TendstoUniformlyOn βₙ β atTop (Icc 0 2)) :
    ∃ δ : ℝ, 0 < δ ∧ δ ≤ 2 ∧ (C : ℝ) * δ ≤ r ∧ β δ ≠ 0 ∧
      Tendsto (fun n => βₙ n δ) atTop (𝓝 (β δ)) := by
…

theorem OAI.SLEExactGauge.SequencePassage.localized_sequence_success_of_uniform_guide_limit line 42

Source documentation

A convergent normalized guide family gives the full sequence passage estimate, with hypotheses on deterministic continuation tubes and ribbon coordinate regions.

theorem localized_sequence_success_of_uniform_guide_limit
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (B₀ : ℝ≥0 → Ω → ℝ) (hB₀ : IsBrownianReal B₀ P)
    (hm : ∀ t, Measurable (B₀ t)) (hc : ∀ ω, Continuous (fun t => B₀ t ω))
    (γ : Ω → ℝ≥0 → ℂ) (G F₀ : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B₀ t ω)
      (γ ω) (G ω) (F₀ ω))
    (hboundary : PublishedLoewnerBoundaryExtension)
    (hsupport : PublishedGeometricTubeSupport P γ)
    (Fₙ : ℕ → ℂ → ℂ) (Fbar : ℕ → ℂ → OnePoint ℂ)
    (hFn : ∀ n, DifferentiableOn ℂ (Fₙ n) upperHalfPlane)
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedLoewnerBoundaryExtension, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.upperHalfPlane