RibbonSequenceCompactness.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Joint extraction of normalized Loewner charts, physical and parameter guides, and local ribbon coordinate maps under a raw waypoint-angle bound.

theorem OAI.SLEExactGauge.uniform_subsequence line 15
theorem OAI.SLEExactGauge.locally_uniform_subsequence line 22

theorem OAI.SLEExactGauge.coordinate_guide_limit_identity line 33

Source documentation

The physical guide in the joint limit is the guide drawn in the limiting coordinate chart. This uses uniform chart convergence, rather than assuming the guide identity survives moving evaluation points.

theorem coordinate_guide_limit_identity
    (Qₙ : ℕ → ℂ → ℂ) (Q : ℂ → ℂ) (K : Set ℂ) (hK : IsClosed K)
    (hQ : ContinuousOn Q K) (hQconv : TendstoUniformlyOn Qₙ Q atTop K)
    (xₙ : ℕ → ℝ) (x : ℝ) (hx : Tendsto xₙ atTop (𝓝 x))
    (αₙ : ℕ → ℝ → ℂ) (α : ℝ → ℂ)
    (hαconv : TendstoUniformlyOn αₙ α atTop (Icc 0 2))
    (hmem : ∀ n t, t ∈ Icc (0 : ℝ) 2 →
      RibbonCoordinates.guideCoordinate 0 (xₙ n) t ∈ K)
    (hshape : ∀ n t, t ∈ Icc (0 : ℝ) 2 →
      αₙ n t = Qₙ n (RibbonCoordinates.guideCoordinate 0 (xₙ n) t)) :
    EqOn α (fun t => Q (RibbonCoordinates.guideCoordinate 0 x t)) (Icc 0 2) := by
…

Mentions: OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate

theorem OAI.SLEExactGauge.actual_ribbon_joint_compactness line 64

Source documentation

The normalized Loewner charts and coordinate charts admit one common subsequence under the raw waypoint-angle normalization hypothesis.

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