HyperbolicGuideCompactness.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The hyperbolic confinement step in es:guide-compactness. A bound on the actual velocity divided by height controls the logarithm of height. A single normalized waypoint then gives compact containment and a common Euclidean Lipschitz bound on each fixed interval away from the tip.

theorem OAI.SLEExactGauge.HyperbolicGuideCompactness.log_height_lipschitz line 19
lemma OAI.SLEExactGauge.HyperbolicGuideCompactness.interval_dist_le_width line 38

theorem OAI.SLEExactGauge.HyperbolicGuideCompactness.height_bounds_from_waypoint line 47

Source documentation

Exponential upper and lower height bounds follow directly from the log-height derivative estimate, without assuming a geometric confinement result.

theorem height_bounds_from_waypoint
    {β : ℝ → ℂ} {δ T tw K s : ℝ} (hK : 0 ≤ K) (hs : 0 < s)
    (htw : tw ∈ Icc δ T)
    (hD : ∀ t ∈ Icc δ T, DifferentiableAt ℝ β t)
    (hH : ∀ t ∈ Icc δ T, 0 < (β t).im)
    (hv : ∀ t ∈ Icc δ T, ‖deriv β t‖ ≤ K * (β t).im)
    (hway : ‖β tw‖ = 1) (hangle : s ≤ (β tw).im) :
    ∀ t ∈ Icc δ T,
      s * Real.exp (-K * (T - δ)) ≤ (β t).im ∧
      (β t).im ≤ Real.exp (K * (T - δ)) := by
…

def OAI.SLEExactGauge.HyperbolicGuideCompactness.speedBound line 81
def OAI.SLEExactGauge.HyperbolicGuideCompactness.radiusBound line 83
theorem OAI.SLEExactGauge.HyperbolicGuideCompactness.euclidean_lipschitz_from_waypoint line 85
theorem OAI.SLEExactGauge.HyperbolicGuideCompactness.norm_bound_from_waypoint line 100
def OAI.SLEExactGauge.HyperbolicGuideCompactness.confinementSet line 120
Source documentation
The common compact set obtained from the actual derivative estimates.
```
def confinementSet (K s δ T : ℝ) : Set ℂ :=
…
```
theorem OAI.SLEExactGauge.HyperbolicGuideCompactness.confinementSet_compact line 123
theorem OAI.SLEExactGauge.HyperbolicGuideCompactness.confinementSet_subset_halfPlane line 126

theorem OAI.SLEExactGauge.HyperbolicGuideCompactness.family_compact_containment_equicontinuity line 133

Source documentation

A normalized family with a common hyperbolic-speed bound is uniformly equicontinuous and remains in one compact subset of the upper half-plane.

theorem family_compact_containment_equicontinuity
    (β : ℕ → ℝ → ℂ) {δ T tw K s : ℝ} (hK : 0 ≤ K) (hs : 0 < s)
    (htw : tw ∈ Icc δ T)
    (hD : ∀ n t, t ∈ Icc δ T → DifferentiableAt ℝ (β n) t)
    (hH : ∀ n t, t ∈ Icc δ T → 0 < (β n t).im)
    (hv : ∀ n t, t ∈ Icc δ T → ‖deriv (β n) t‖ ≤ K * (β n t).im)
    (hway : ∀ n, ‖β n tw‖ = 1) (hangle : ∀ n, s ≤ (β n tw).im) :
    IsCompact (confinementSet K s δ T) ∧
    confinementSet K s δ T ⊆ {z : ℂ | 0 < z.im} ∧
    (∀ n, MapsTo (β n) (Icc δ T) (confinementSet K s δ T)) ∧
    UniformEquicontinuousOn β (Icc δ T) := by
…

Mentions: OAI.SLEExactGauge.HyperbolicGuideCompactness.confinementSet

theorem OAI.SLEExactGauge.HyperbolicGuideCompactness.inverse_chart_derivative_bound line 156

Source documentation

A univalent inverse chart on a physical clearance ball has derivative bounded by its height. The omitted point is the real part of its center value.

theorem inverse_chart_derivative_bound
    {g : ℂ → ℂ} {z : ℂ} {r : ℝ} (hr : 0 < r)
    (hd : DifferentiableOn ℂ g (ball z r)) (hi : InjOn g (ball z r))
    (hH : MapsTo g (ball z r) {w : ℂ | 0 < w.im}) :
    ‖deriv g z‖ ≤ ((128 * Real.pi) / r) * (g z).im := by
…

theorem OAI.SLEExactGauge.HyperbolicGuideCompactness.inverse_guide_composition_bound line 181

Source documentation

Actual composition with a physical guide converts clearance and bounded physical speed into the hyperbolic-speed estimate used above.

theorem inverse_guide_composition_bound
    {g : ℂ → ℂ} {α : ℝ → ℂ} {t r V : ℝ} (hr : 0 < r)
    (hg : DifferentiableOn ℂ g (ball (α t) r)) (hgi : InjOn g (ball (α t) r))
    (hgH : MapsTo g (ball (α t) r) {w : ℂ | 0 < w.im})
    (hα : DifferentiableAt ℝ α t) (hv : ‖deriv α t‖ ≤ V) :
    DifferentiableAt ℝ (g ∘ α) t ∧
      ‖deriv (g ∘ α) t‖ ≤ ((128 * Real.pi * V) / r) * (g (α t)).im := by
…

theorem OAI.SLEExactGauge.HyperbolicGuideCompactness.inverse_guide_family_compactness line 209

Source documentation

The family compactness conclusion with its hyperbolic-speed hypothesis fully discharged by actual inverse charts and physical clearance balls.

theorem inverse_guide_family_compactness
    (g : ℕ → ℂ → ℂ) (α : ℕ → ℝ → ℂ) {δ T tw r V s : ℝ}
    (hr : 0 < r) (hV : 0 ≤ V) (hs : 0 < s) (htw : tw ∈ Icc δ T)
    (hg : ∀ n t, t ∈ Icc δ T → DifferentiableOn ℂ (g n) (ball (α n t) r))
    (hgi : ∀ n t, t ∈ Icc δ T → InjOn (g n) (ball (α n t) r))
    (hgH : ∀ n t, t ∈ Icc δ T → MapsTo (g n) (ball (α n t) r) {w : ℂ | 0 < w.im})
    (hα : ∀ n t, t ∈ Icc δ T → DifferentiableAt ℝ (α n) t)
    (hv : ∀ n t, t ∈ Icc δ T → ‖deriv (α n) t‖ ≤ V)
    (hway : ∀ n, ‖g n (α n tw)‖ = 1)
    (hangle : ∀ n, s ≤ (g n (α n tw)).im) :
    ∃ Q : Set ℂ, IsCompact Q ∧ Q ⊆ {z : ℂ | 0 < z.im} ∧
      (∀ n, MapsTo (g n ∘ α n) (Icc δ T) Q) ∧
…