FreshTipMapOut.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Mapping the actual geometric continuation into the restarted half-plane. At a first height crossing the tip is fresh. The fresh-tip chart limit then maps a simple access path continuously to a simple path starting at the restarted driving point.

theorem OAI.SLEExactGauge.tip_survives_prior_of_strict_height line 16

theorem OAI.SLEExactGauge.map_out_simple_access_path line 37

Source documentation

Extend the map only at the accessible tip. This is sufficient to map the entire simple continuation Path, and does not require a boundary extension of the forward conformal map at other hull points.

theorem map_out_simple_access_path
    (D : Set ℂ) (_hD : IsOpen D) (g : ℂ → ℂ)
    (hg : ContinuousOn g D) (hgi : InjOn g D) (hgH : MapsTo g D upperHalfPlane)
    (ζ w : ℂ) (u : ℝ) (hζ : ζ ∉ D)
    (hlim : Tendsto g (𝓝[D] ζ) (𝓝 (u : ℂ)))
    (p : Path ζ w) (hp : Function.Injective p)
    (hpD : ∀ t, t ≠ 0 → p t ∈ D) :
    ∃ q : Path (0 : ℂ) (g w - (u : ℂ)), Function.Injective q ∧
      (∀ t, t ≠ 0 → q t ∈ upperHalfPlane) ∧
      (∀ t, t ≠ 0 → q t = g (p t) - (u : ℂ)) := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.IsCapacityTwoWitness.map_out_access_at_first_height line 105

Source documentation

Actual capacity charts at a first height crossing map the physical simple continuation to a supported simple path in the restarted half-plane, with the conformal map-back identity at every positive path time.

theorem IsCapacityTwoWitness.map_out_access_at_first_height
    {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness U γ G F) (hU : Continuous U)
    (T : ℝ≥0) (hT : 0 < T) (hheight : 0 < (γ T).im)
    (hfirst : ∀ u : ℝ≥0, u < T → (γ u).im < (γ T).im)
    (w : ℂ) (p : Path (γ T) w) (hp : Function.Injective p)
    (hpD : ∀ t, t ≠ 0 → p t ∈ survivingDomain γ T) :
    ∃ q : Path (0 : ℂ) (G T w - (U T : ℂ)), Function.Injective q ∧
      (∀ t, t ≠ 0 → q t ∈ upperHalfPlane) ∧
      (∀ t, t ≠ 0 → F T (q t + (U T : ℂ)) = p t) := by
…

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