ActualSequencePassageRegions.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual convergent guide families imply sequence passage using only compact-dependent middle-strip margins.

theorem OAI.SLEExactGauge.SequencePassage.localized_sequence_success_of_uniform_guide_limit_middle_regions line 19

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_middle_regions
    {Ω : 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