ActualWaypointStraightening.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The local straightening hypotheses at the actual ribbon waypoint. The complete access guide and the inverse identities exclude nonlocal pieces of the guide from the waypoint disk.

theorem OAI.SLEExactGauge.RibbonCoordinates.waypoint_ball_coordinates line 16
theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_mem_future line 27

theorem OAI.SLEExactGauge.RibbonCoordinates.actual_straightened_zero_lies_on_guide line 34

Source documentation

The complete straightening detects the whole physical access guide, including points far outside the local coordinate disk.

theorem actual_straightened_zero_lies_on_guide
    {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness U γ G F) (T : ℝ≥0)
    (P : ℂ → ℂ) {k x : ℝ} (hx : |x| ≤ 1 / 4)
    (hfuture : P '' futureRibbon k ⊆ survivingDomain γ T)
    (β : ℝ≥0 → ℂ)
    (hβ : ∀ t : ℝ≥0, 0 < t →
      β t = G T (P (guideCoordinate k x t)) - (U T : ℂ))
    (h : ℂ ≃ₜ ℂ) (hH : MapsTo h upperHalfPlane upperHalfPlane)
    (hstraight : ∀ t : ℝ≥0, h (β t) = (t : ℂ) * Complex.I)
    {z : ℂ} (hz : z ∈ survivingDomain γ T)
    (hzero : (h (G T z - (U T : ℂ))).re = 0) :
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.RibbonCoordinates.futureRibbon, OAI.SLEExactGauge.survivingDomain, OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate, OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.RibbonCoordinates.actual_waypoint_chart line 63

theorem OAI.SLEExactGauge.RibbonCoordinates.actual_ribbon_complete_guide line 138

Source documentation

The actual complete physical guide is proper because its tail is the centerline; no compactness or properness of a parameter guide is assumed.

theorem actual_ribbon_complete_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)
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon) (hiP : InjOn P closedRibbon)
    {k x : ℝ} (hk : 0 ≤ k) (hx : |x| ≤ 1 / 4)
    (htip : P ((k : ℂ) + (x : ℂ) * Complex.I) = γ T)
    (hfuture : P '' futureRibbon k ⊆ survivingDomain γ T)
    (hescape : Tendsto (fun s : ℝ => ‖P (s : ℂ)‖) atTop atTop) :
    ∃ β : ℝ≥0 → ℂ, Continuous β ∧ Function.Injective β ∧ β 0 = 0 ∧
      (∀ t : ℝ≥0, 0 < t → β t ∈ upperHalfPlane) ∧
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.survivingDomain, OAI.SLEExactGauge.RibbonCoordinates.closedRibbon, OAI.SLEExactGauge.RibbonCoordinates.futureRibbon, OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.RibbonCoordinates.actual_ribbon_waypoint_straightening line 186

theorem OAI.SLEExactGauge.RibbonCoordinates.actual_physical_waypoint_tubes_opposite_sides line 218

Source documentation

Actual physical waypoint neighborhoods lie on opposite sides of the complete stopped access guide. The orientation is selected by the local chart and is shared by the whole pair of neighborhoods.

theorem actual_physical_waypoint_tubes_opposite_sides
    (hpublished : PublishedHalfPlaneCrosscutStraightening)
    (hopen : PublishedPlanarDiskOpenness)
    {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)
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon) (hiP : InjOn P closedRibbon)
    {k x : ℝ} (hk : 1 ≤ k) (hx : |x| ≤ 1 / 4)
    (htip : P ((k : ℂ) + (x : ℂ) * Complex.I) = γ T)
    (hfuture : P '' futureRibbon k ⊆ survivingDomain γ T)
    (hescape : Tendsto (fun s : ℝ => ‖P (s : ℂ)‖) atTop atTop)
…

Mentions: OAI.SLEExactGauge.PublishedHalfPlaneCrosscutStraightening, OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.survivingDomain, OAI.SLEExactGauge.RibbonCoordinates.closedRibbon, OAI.SLEExactGauge.RibbonCoordinates.futureRibbon