PlanarCoordinatePassage.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Passage along an actual convergent family of normalized charts and ribbon coordinate maps. Every continuation tube, early-containment event, and moving mass region is derived from the limiting coordinate guide.

theorem OAI.SLEExactGauge.SequencePassage.planar_coordinate_limit_passage line 21

Source documentation

A convergent recentered admissible family has a positive one-step passage-and-mass probability at every sufficiently small mesh in a prescribed vanishing sequence. The mass lies in the actual moving coordinate middle strip.

theorem planar_coordinate_limit_passage
    {Ω : 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 γ)
    (hplanar : PublishedPlanarDiskOpenness)
    (Qₙ : ℕ → ℂ → ℂ) (Q : ℂ → ℂ) (K : Set ℂ) (C Lq : ℝ≥0)
…

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