GuideCompactness.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Joint compactness of conformal charts and physical/parameter access guides. The sole published input is the explicitly stated normalized univalent normal-family theorem. Normalization and guide identification use proved clearance, tip-collapse, and compact-inverse estimates.

theorem OAI.SLEExactGauge.GuideCompactness.limit_omits_tip line 24

Source documentation

The weak omitted-value derivative estimate proves that a nondegenerate locally uniform conformal limit still omits the limiting omitted value.

theorem limit_omits_tip
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ) (aₙ : ℕ → ℂ) (a : ℂ)
    (hFn : ∀ n, DifferentiableOn ℂ (Fₙ n) upperHalfPlane)
    (hinj : ∀ n, InjOn (Fₙ n) upperHalfPlane)
    (hconv : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
    (ha : Tendsto aₙ atTop (𝓝 a))
    (homit : ∀ n, aₙ n ∉ Fₙ n '' upperHalfPlane)
    (hne : ∀ z ∈ upperHalfPlane, deriv F z ≠ 0) :
    a ∉ F '' upperHalfPlane := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.GuideCompactness.locallyUniform_subsequence line 50

Source documentation

Reindexing a locally uniform limit along a subsequence.

theorem locallyUniform_subsequence
    {Fₙ : ℕ → ℂ → ℂ} {F : ℂ → ℂ} {S : Set ℂ}
    (h : TendstoLocallyUniformlyOn Fₙ F atTop S)
    {φ : ℕ → ℕ} (hφ : StrictMono φ) :
    TendstoLocallyUniformlyOn (fun n => Fₙ (φ n)) F atTop S := by
…

theorem OAI.SLEExactGauge.GuideCompactness.normalized_waypoint_of_uniform_limit line 61

Source documentation

The unit-semicircle waypoint normalization survives uniform guide convergence on the closed time interval.

theorem normalized_waypoint_of_uniform_limit
    {βₙ : ℕ → ℝ → ℂ} {β : ℝ → ℂ} {I : Set ℝ} {tw s : ℝ}
    (hu : TendstoUniformlyOn βₙ β atTop I) (htw : tw ∈ I)
    (hway : ∀ n, ‖βₙ n tw‖ = 1 ∧ s ≤ (βₙ n tw).im) :
    ‖β tw‖ = 1 ∧ s ≤ (β tw).im := by
…

theorem OAI.SLEExactGauge.GuideCompactness.compact_parameter_family_of_clearance line 78

Source documentation

Physical clearance on every interval away from zero gives the compact parameter confinement required to identify the inverse-guide limit.

theorem compact_parameter_family_of_clearance
    (g : ℕ → ℂ → ℂ) (D : ℕ → Set ℂ) (αₙ βₙ : ℕ → ℝ → ℂ)
    {T tw s : ℝ} (C : ℝ≥0) (htw : 0 < tw) (htwT : tw ≤ T) (hs : 0 < s)
    (hαL : ∀ n, LipschitzOnWith C (αₙ n) (Icc 0 T))
    (hg : ∀ n, DifferentiableOn ℂ (g n) (D n)) (hig : ∀ n, InjOn (g n) (D n))
    (hgH : ∀ n, MapsTo (g n) (D n) upperHalfPlane)
    (hway : ∀ n, ‖βₙ n tw‖ = 1 ∧ s ≤ (βₙ n tw).im)
    (hβeq : ∀ n t, t ∈ Ioc 0 T → βₙ n t = g n (αₙ n t))
    (hclear : ∀ δ : ℝ, 0 < δ → δ ≤ T → ∃ r : ℝ, 0 < r ∧
      ∀ n t, t ∈ Icc δ T → ball (αₙ n t) r ⊆ D n) :
    ∀ δ : ℝ, 0 < δ → δ ≤ T →
      ∃ Q : Set ℂ, IsCompact Q ∧ Q ⊆ upperHalfPlane ∧
…

Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.GuideCompactness.exists_joint_guide_limit line 115

Source documentation

Actual inverse charts with a common physical clearance at the waypoint, bi-Lipschitz physical guides, and compact parameter confinement have one joint subsequential limit. The inverse guide remains continuous and simple through its initial boundary point.

theorem exists_joint_guide_limit
    {Ω : Type} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (hpublished : PublishedHalfPlaneUnivalentCompactness)
    (Fₙ g : ℕ → ℂ → ℂ) (D : ℕ → Set ℂ) (Fbar : ℕ → ℂ → OnePoint ℂ)
    (αₙ βₙ : ℕ → ℝ → ℂ) (aₙ : ℕ → ℂ)
    {T tw s ρ A c : ℝ} (C : ℝ≥0)
    (hT : 0 < T) (htw : 0 < tw) (htwT : tw ≤ T)
    (hs : 0 < s) (hρ : 0 < ρ) (hc : 0 < c) (hC : 0 < (C : ℝ))
    (hD : ∀ n, IsOpen (D n))
    (hFn : ∀ n, DifferentiableOn ℂ (Fₙ n) upperHalfPlane)
…

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

theorem OAI.SLEExactGauge.GuideCompactness.exists_joint_guide_limit_of_clearance line 210

Source documentation

Joint guide compactness with compact containment discharged by the actual inverse charts and positive physical clearance away from the tip.

theorem exists_joint_guide_limit_of_clearance
    {Ω : Type} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (hpublished : PublishedHalfPlaneUnivalentCompactness)
    (Fₙ g : ℕ → ℂ → ℂ) (D : ℕ → Set ℂ) (Fbar : ℕ → ℂ → OnePoint ℂ)
    (αₙ βₙ : ℕ → ℝ → ℂ) (aₙ : ℕ → ℂ)
    {T tw s ρ A c : ℝ} (C : ℝ≥0)
    (hT : 0 < T) (htw : 0 < tw) (htwT : tw ≤ T)
    (hs : 0 < s) (hρ : 0 < ρ) (hc : 0 < c) (hC : 0 < (C : ℝ))
    (hD : ∀ n, IsOpen (D n))
    (hFn : ∀ n, DifferentiableOn ℂ (Fₙ n) upperHalfPlane)
…

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