ActualGuideCompactness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Joint compactness for stopped capacity charts. Freshness, physical clearance and a waypoint angle bound give parameter-guide compactness and nondegenerate limits of the normalized analytic charts.

theorem OAI.SLEExactGauge.actual_guide_joint_compactness line 17

theorem OAI.SLEExactGauge.actual_guide_joint_compactness_with_family line 105

Source documentation

The same actual compactness extraction, retaining the chosen normalized boundary charts and parameter-guide family. Uniform convergence of that family supplies the fixed positive guide-time convergence needed by early trace localization.

theorem actual_guide_joint_compactness_with_family
    {Ω : Type} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (hcompact : PublishedHalfPlaneUnivalentCompactness)
    (hboundary : PublishedLoewnerBoundaryExtension)
    (U : ℕ → ℝ≥0 → ℝ) (γₙ : ℕ → ℝ≥0 → ℂ)
    (G F₀ : ℕ → ℝ≥0 → ℂ → ℂ)
    (hU : ∀ n, Continuous (U n))
    (hw : ∀ n, IsCapacityTwoWitness (U n) (γₙ n) (G n) (F₀ n))
    (T : ℕ → ℝ≥0) (hT : ∀ n, 0 < T n)
    (hfresh : ∀ n s, s < T n → γₙ n (T n) ∈ survivingDomain (γₙ n) s)
…

Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.PublishedHalfPlaneUnivalentCompactness, OAI.SLEExactGauge.PublishedLoewnerBoundaryExtension, OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.survivingDomain