CompleteAccessGuide.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The complete physical access guide maps to a proper half-plane crosscut based at the actual driving prime end. Properness at infinity is proved from the hydrodynamic normalization in the capacity witness.

theorem OAI.SLEExactGauge.IsCapacityTwoWitness.centered_chart_escapes line 16

theorem OAI.SLEExactGauge.actual_complete_access_guide line 65

Source documentation

The continuous complete parameter guide has the exact capacity-map formula at every positive time, including its asymptotic endpoint.

theorem actual_complete_access_guide
    {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 ℂ)) :
    ∃ β : ℝ≥0 → ℂ, Continuous β ∧ Function.Injective β ∧ β 0 = 0 ∧
      (∀ t : ℝ≥0, 0 < t → β t ∈ upperHalfPlane) ∧
      Tendsto β atTop (cocompact ℂ) ∧
      ∀ t : ℝ≥0, 0 < t → β t = G T (α t) - (U T : ℂ) := by
…

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