ActualMarkedStraightening.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Straighten the actual complete marked access guide. The local chart's zero set is identified with the explicit physical guide, including the exclusion of every nonlocal guide piece.

theorem OAI.SLEExactGauge.actual_marked_access_straightening line 17

Source documentation

An actual fresh-tip guide and its local marked-point chart give a straightening with an exact physical zero set.

theorem actual_marked_access_straightening
    (hpublished : PublishedHalfPlaneCrosscutStraightening)
    {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness U γ G F) (hU : Continuous U)
    (T : ℝ≥0) (hT : 0 < T)
    (hfresh : ∀ s : ℝ≥0, s < T → γ T ∈ survivingDomain γ s)
    (α : ℝ≥0 → ℂ) (hα : Continuous α) (hiα : Function.Injective α)
    (hα0 : α 0 = γ T) (hαD : ∀ t : ℝ≥0, 0 < t → α t ∈ survivingDomain γ T)
    (hescape : Tendsto α atTop (cocompact ℂ))
    (Q : ℂ ≃ₜ ℂ) (r : ℝ)
    (hQD : MapsTo Q (ball 0 r) (survivingDomain γ T))
    (hlocus : ∀ z ∈ ball (0 : ℂ) r,
…

Mentions: OAI.SLEExactGauge.PublishedHalfPlaneCrosscutStraightening, OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.survivingDomain