RibbonCoordinateGeometry.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

Coordinate balls in an embedded ribbon. These deterministic lemmas turn the local lower Lipschitz bound into physical clearance, and identify the future ribbon with part of the actual unbounded surviving component.

theorem OAI.SLEExactGauge.RibbonCoordinates.ball_subset_image_ball line 20

Source documentation

An open coordinate disk whose inverse has Lipschitz constant K contains the physical disk of radius r / K. Compactness of the closed coordinate disk prevents an interior physical point from escaping its image.

theorem ball_subset_image_ball
    (P : ℂ → ℂ) (x : ℂ) {r K : ℝ} (hr : 0 < r) (hK : 0 < K)
    (hP : ContinuousOn P (closedBall x r))
    (hopen : IsOpen (P '' ball x r))
    (hlower : ∀ y ∈ closedBall x r, dist y x ≤ K * dist (P y) (P x)) :
    ball (P x) (r / K) ⊆ P '' ball x r := by
…

def OAI.SLEExactGauge.RibbonCoordinates.closedRibbon line 45
def OAI.SLEExactGauge.RibbonCoordinates.futureRibbon line 46
theorem OAI.SLEExactGauge.RibbonCoordinates.futureRibbon_subset_closedRibbon line 48
theorem OAI.SLEExactGauge.RibbonCoordinates.futureRibbon_convex line 53
theorem OAI.SLEExactGauge.RibbonCoordinates.free_preconnected_subset_surviving line 62
Source documentation
Any unbounded connected free set belongs to the unbounded component used in the actual Loewner surviving domain.
```
theorem free_preconnected_subset_surviving
    (γ : ℝ≥0 → ℂ) (T : ℝ≥0) (S : Set ℂ)
    (hS : IsPreconnected S) (hfree : S ⊆ upperHalfPlane \ (γ '' Icc 0 T))
    (hunbounded : ¬ Bornology.IsBounded S) : S ⊆ survivingDomain γ T := by
…
```
Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.survivingDomain
theorem OAI.SLEExactGauge.RibbonCoordinates.futureRibbon_survives line 74
Source documentation
Embedding excludes all nonlocal pieces of the stopped past from the future ribbon. Escape to infinity places the whole future ribbon in the surviving component, without assuming a filled-hull containment.
```
theorem futureRibbon_survives
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon)
    (hi : InjOn P closedRibbon) {k : ℝ} (hk : 0 ≤ k)
    (hH : ∀ z ∈ closedRibbon, 0 < z.re → P z ∈ upperHalfPlane)
    (γ : ℝ≥0 → ℂ) (T : ℝ≥0)
    (hpast : γ '' Icc 0 T ⊆ P '' {z ∈ closedRibbon | z.re ≤ k})
    (hunbounded : ¬ Bornology.IsBounded (P '' futureRibbon k)) :
    P '' futureRibbon k ⊆ survivingDomain γ T := by
…
```
Mentions: OAI.SLEExactGauge.RibbonCoordinates.closedRibbon, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.RibbonCoordinates.futureRibbon, OAI.SLEExactGauge.survivingDomain

theorem OAI.SLEExactGauge.RibbonCoordinates.coordinate_ball_clearance line 94

Source documentation

A coordinate disk strictly ahead of the front and away from the two ribbon edges gives a physical disk in the actual surviving domain.

theorem coordinate_ball_clearance
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon)
    (hi : InjOn P closedRibbon) {k : ℝ} (hk : 0 ≤ k)
    (hH : ∀ z ∈ closedRibbon, 0 < z.re → P z ∈ upperHalfPlane)
    (γ : ℝ≥0 → ℂ) (T : ℝ≥0)
    (hpast : γ '' Icc 0 T ⊆ P '' {z ∈ closedRibbon | z.re ≤ k})
    (hunbounded : ¬ Bornology.IsBounded (P '' futureRibbon k))
    (x : ℂ) {r K : ℝ} (hr : 0 < r) (hK : 0 < K)
    (hfront : k + r < x.re) (hedge : |x.im| + r < 1)
    (hopen : IsOpen (P '' ball x r))
    (hlower : ∀ y ∈ closedBall x r, dist y x ≤ K * dist (P y) (P x)) :
    ball (P x) (r / K) ⊆ survivingDomain γ T := by
…

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

def OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate line 122
Source documentation
The paper's access guide, before applying the ribbon coordinate map.
```
def guideCoordinate (k x t : ℝ) : ℂ :=
…
```
theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_re line 125
theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_im line 128
theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_continuous line 131
theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_im_bound line 135
theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_lower_chord line 141
Source documentation
The longitudinal coordinate gives the lower chord bound directly.
```
theorem guideCoordinate_lower_chord (k x u v : ℝ) :
    |u - v| ≤ dist (guideCoordinate k x u) (guideCoordinate k x v) := by
…
```
Mentions: OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate
theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_upper_chord line 147
def OAI.SLEExactGauge.RibbonCoordinates.guideRadius line 165
theorem OAI.SLEExactGauge.RibbonCoordinates.guideRadius_pos line 167
theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_disk_margins line 172
Source documentation
The guide is at most a quarter of the ribbon half-width from the centerline; its coordinate disks have radius proportional to min(t,1).
```
theorem guideCoordinate_disk_margins
    {k x t : ℝ} (hx : |x| ≤ 1 / 4) (ht : 0 < t) :
    k + guideRadius t < (guideCoordinate k x t).re ∧
      |(guideCoordinate k x t).im| + guideRadius t < 1 := by
…
```
Mentions: OAI.SLEExactGauge.RibbonCoordinates.guideRadius, OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate

theorem OAI.SLEExactGauge.RibbonCoordinates.physical_guide_clearance line 184

Source documentation

Applying the coordinate disk lemma proves the paper's guide clearance for every positive guide time, with the actual surviving domain.

theorem physical_guide_clearance
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon)
    (hi : InjOn P closedRibbon) {k x K : ℝ} (hk : 0 ≤ k)
    (hx : |x| ≤ 1 / 4) (hK : 0 < K)
    (hH : ∀ z ∈ closedRibbon, 0 < z.re → P z ∈ upperHalfPlane)
    (γ : ℝ≥0 → ℂ) (T : ℝ≥0)
    (hpast : γ '' Icc 0 T ⊆ P '' {z ∈ closedRibbon | z.re ≤ k})
    (hunbounded : ¬ Bornology.IsBounded (P '' futureRibbon k))
    (hopen : ∀ t ∈ Ioc (0 : ℝ) 2,
      IsOpen (P '' ball (guideCoordinate k x t) (guideRadius t)))
    (hlower : ∀ t ∈ Ioc (0 : ℝ) 2,
      ∀ y ∈ closedBall (guideCoordinate k x t) (guideRadius t),
…

Mentions: OAI.SLEExactGauge.RibbonCoordinates.closedRibbon, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.RibbonCoordinates.futureRibbon, OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate, OAI.SLEExactGauge.RibbonCoordinates.guideRadius

def OAI.SLEExactGauge.RibbonCoordinates.guidePatch line 206
Source documentation
The fixed length-four patch appearing in the admissible ribbon class.
```
def guidePatch (k : ℝ) : Set ℂ := {z | k ≤ z.re ∧ z.re ≤ k + 3 ∧ |z.im| ≤ 1}
```
theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_disk_subset_patch line 208
theorem OAI.SLEExactGauge.RibbonCoordinates.guidePatch_subset_closedRibbon line 231

theorem OAI.SLEExactGauge.RibbonCoordinates.physical_guide_clearance_of_patch line 238

Source documentation

The actual fixed patch inverse-Lipschitz bound suffices for all guide disks. The only topological parameter is the cited planar disk theorem.

theorem physical_guide_clearance_of_patch
    (hpublished : PublishedPlanarDiskOpenness)
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon)
    (hi : InjOn P closedRibbon) {k x K : ℝ} (hk : 0 ≤ k)
    (hx : |x| ≤ 1 / 4) (hK : 0 < K)
    (hH : ∀ z ∈ closedRibbon, 0 < z.re → P z ∈ upperHalfPlane)
    (γ : ℝ≥0 → ℂ) (T : ℝ≥0)
    (hpast : γ '' Icc 0 T ⊆ P '' {z ∈ closedRibbon | z.re ≤ k})
    (hunbounded : ¬ Bornology.IsBounded (P '' futureRibbon k))
    (hlower : ∀ u ∈ guidePatch k, ∀ v ∈ guidePatch k,
      dist u v ≤ K * dist (P u) (P v)) :
    ∀ t ∈ Ioc (0 : ℝ) 2,
…

Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.RibbonCoordinates.closedRibbon, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.RibbonCoordinates.futureRibbon, OAI.SLEExactGauge.RibbonCoordinates.guidePatch

theorem OAI.SLEExactGauge.RibbonCoordinates.physical_guide_clearance_away line 262

Source documentation

Uniform clearance on every closed interval away from the tip is the form used by joint physical/conformal guide compactness.

theorem physical_guide_clearance_away
    (hpublished : PublishedPlanarDiskOpenness)
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon)
    (hi : InjOn P closedRibbon) {k x K : ℝ} (hk : 0 ≤ k)
    (hx : |x| ≤ 1 / 4) (hK : 0 < K)
    (hH : ∀ z ∈ closedRibbon, 0 < z.re → P z ∈ upperHalfPlane)
    (γ : ℝ≥0 → ℂ) (T : ℝ≥0)
    (hpast : γ '' Icc 0 T ⊆ P '' {z ∈ closedRibbon | z.re ≤ k})
    (hunbounded : ¬ Bornology.IsBounded (P '' futureRibbon k))
    (hlower : ∀ u ∈ guidePatch k, ∀ v ∈ guidePatch k,
      dist u v ≤ K * dist (P u) (P v))
    {δ : ℝ} (hδ : 0 < δ) (_hδ2 : δ ≤ 2) :
…

theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_mem_patch line 282
theorem OAI.SLEExactGauge.RibbonCoordinates.physical_guide_lipschitz line 293
Source documentation
The fixed coordinate patch speed bound gives the physical guide speed bound required by the compactness and access-localization arguments.
```
theorem physical_guide_lipschitz
    (P : ℂ → ℂ) (C : ℝ≥0) {k x : ℝ} (hx : |x| ≤ 1 / 4)
    (hL : LipschitzOnWith C P (guidePatch k)) :
    LipschitzOnWith (2 * C) (fun t => P (guideCoordinate k x t)) (Icc (0 : ℝ) 2) := by
…
```
Mentions: OAI.SLEExactGauge.RibbonCoordinates.guidePatch, OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate

theorem OAI.SLEExactGauge.RibbonCoordinates.physical_guide_lower_chord line 310

Source documentation

The lower patch Lipschitz bound makes the physical guide uniformly simple, including its initial boundary point.

theorem physical_guide_lower_chord
    (P : ℂ → ℂ) {k x K : ℝ} (hx : |x| ≤ 1 / 4) (hK : 0 < K)
    (hlower : ∀ u ∈ guidePatch k, ∀ v ∈ guidePatch k,
      dist u v ≤ K * dist (P u) (P v)) :
    ∀ u ∈ Icc (0 : ℝ) 2, ∀ v ∈ Icc (0 : ℝ) 2,
      (1 / K) * |u - v| ≤ dist (P (guideCoordinate k x u)) (P (guideCoordinate k x v)) := by
…

Mentions: OAI.SLEExactGauge.RibbonCoordinates.guidePatch, OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate

theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_zero line 322
theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_waypoint line 325
theorem OAI.SLEExactGauge.RibbonCoordinates.futureRibbon_unbounded_of_centerline_escape line 331
Source documentation
The paper's escape condition on the centerline supplies the unboundedness used to select the actual surviving component.
```
theorem futureRibbon_unbounded_of_centerline_escape
    (P : ℂ → ℂ) (k : ℝ)
    (hescape : Tendsto (fun s : ℝ => ‖P (s : ℂ)‖) atTop atTop) :
    ¬ Bornology.IsBounded (P '' futureRibbon k) := by
…
```
Mentions: OAI.SLEExactGauge.RibbonCoordinates.futureRibbon