LipschitzGuideConfinement.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Compact confinement for the actual Lipschitz access guides. Local conformal derivative bounds are integrated by continuous induction, so no differentiability of the physical guide is required.

theorem OAI.SLEExactGauge.LipschitzGuideConfinement.lipschitzOn_of_local_bound line 17

Source documentation

A common local distance bound on a real interval is a global bound. The proof uses continuous induction and applies to arbitrary metric targets.

theorem lipschitzOn_of_local_bound
    {E : Type*} [PseudoMetricSpace E] {f : ℝ → E} {a b K : ℝ}
    (hK : 0 ≤ K) (hf : ContinuousOn f (Icc a b))
    (hloc : ∀ t ∈ Icc a b, ∃ ε : ℝ, 0 < ε ∧
      ∀ u ∈ Icc a b, dist u t < ε → dist (f u) (f t) ≤ K * dist u t) :
    LipschitzOnWith ⟨K, hK⟩ f (Icc a b) := by
…

theorem OAI.SLEExactGauge.LipschitzGuideConfinement.log_im_fderiv_bound line 64

theorem OAI.SLEExactGauge.LipschitzGuideConfinement.log_im_lipschitz_on_half_ball line 94

Source documentation

The logarithm of the inverse-map height has bounded gradient on each physical clearance ball.

theorem log_im_lipschitz_on_half_ball
    {g : ℂ → ℂ} {z : ℂ} {r : ℝ} (hr : 0 < r)
    (hg : DifferentiableOn ℂ g (ball z r)) (hi : InjOn g (ball z r))
    (hH : MapsTo g (ball z r) upperHalfPlane) :
    LipschitzOnWith ⟨(256 * Real.pi) / r, by positivity⟩
      (fun w => Real.log (g w).im) (ball z (r / 2)) := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.LipschitzGuideConfinement.log_height_lipschitz line 120

Source documentation

Lipschitz guides have a uniformly Lipschitz logarithmic inverse height, even at their corners.

theorem log_height_lipschitz
    {g : ℂ → ℂ} {α : ℝ → ℂ} {δ T r : ℝ} (hr : 0 < r) (C : ℝ≥0)
    (hL : LipschitzOnWith C α (Icc δ T))
    (hg : ∀ t ∈ Icc δ T, DifferentiableOn ℂ g (ball (α t) r))
    (hi : ∀ t ∈ Icc δ T, InjOn g (ball (α t) r))
    (hH : ∀ t ∈ Icc δ T, MapsTo g (ball (α t) r) upperHalfPlane) :
    LipschitzOnWith ⟨(256 * Real.pi * C) / r, by positivity⟩
      (fun t => Real.log (g (α t)).im) (Icc δ T) := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.LipschitzGuideConfinement.holomorphic_local_distance_bound line 155
Source documentation
A holomorphic derivative bounds the distance quotient from its center in some neighborhood; no regularity of a curve composed with it is needed.
```
theorem holomorphic_local_distance_bound
    {g : ℂ → ℂ} {z : ℂ} (hg : DifferentiableAt ℂ g z) :
    ∃ ε : ℝ, 0 < ε ∧ ∀ w, dist w z < ε →
      dist (g w) (g z) ≤ (‖deriv g z‖ + 1) * dist w z := by
…
```
theorem OAI.SLEExactGauge.LipschitzGuideConfinement.height_bounds_from_waypoint line 177
def OAI.SLEExactGauge.LipschitzGuideConfinement.euclideanSpeed line 214

theorem OAI.SLEExactGauge.LipschitzGuideConfinement.inverse_guide_lipschitz line 219

Source documentation

Common clearance and a waypoint control the full inverse guide's speed for Lipschitz physical guides, including guides with corners.

theorem inverse_guide_lipschitz
    {g : ℂ → ℂ} {α : ℝ → ℂ} {δ T tw r s : ℝ}
    (hr : 0 < r) (C : ℝ≥0) (hs : 0 < s) (htw : tw ∈ Icc δ T)
    (hL : LipschitzOnWith C α (Icc δ T))
    (hg : ∀ t ∈ Icc δ T, DifferentiableOn ℂ g (ball (α t) r))
    (hi : ∀ t ∈ Icc δ T, InjOn g (ball (α t) r))
    (hH : ∀ t ∈ Icc δ T, MapsTo g (ball (α t) r) upperHalfPlane)
    (hway : ‖g (α tw)‖ = 1) (hangle : s ≤ (g (α tw)).im) :
    LipschitzOnWith ⟨euclideanSpeed C r δ T, by dsimp [euclideanSpeed]; positivity⟩
      (g ∘ α) (Icc δ T) := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.LipschitzGuideConfinement.euclideanSpeed

def OAI.SLEExactGauge.LipschitzGuideConfinement.confinementSet line 258
theorem OAI.SLEExactGauge.LipschitzGuideConfinement.family_compact_containment line 262