WaypointDerivativeBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Nondegenerate waypoint normalization from actual inverse charts and physical clearance. The existing weak omitted-value estimate is enough; no sharp conformal-radius comparison is required.

theorem OAI.SLEExactGauge.waypoint_derivative_bounds_of_clearance line 16

theorem OAI.SLEExactGauge.waypoint_family_normalization_of_clearance line 71

Source documentation

Bounded physical tips, a common clearance ball, and an interior waypoint angle supply exactly the normal-family normalization constants.

theorem waypoint_family_normalization_of_clearance
    (F g : ℕ → ℂ → ℂ) (D : ℕ → Set ℂ) (hD : ∀ n, IsOpen (D n))
    (hF : ∀ n, DifferentiableOn ℂ (F n) upperHalfPlane)
    (hiF : ∀ n, InjOn (F n) upperHalfPlane)
    (hg : ∀ n, DifferentiableOn ℂ (g n) (D n))
    (hig : ∀ n, InjOn (g n) (D n))
    (hFD : ∀ n, MapsTo (F n) upperHalfPlane (D n))
    (hgH : ∀ n, MapsTo (g n) (D n) upperHalfPlane)
    (hgf : ∀ n z, z ∈ upperHalfPlane → g n (F n z) = z)
    (z a : ℕ → ℂ) (s ρ R A : ℝ) (hs : 0 < s) (hρ : 0 < ρ)
    (hz : ∀ n, ‖z n‖ = 1 ∧ s ≤ (z n).im)
    (hclear : ∀ n, ball (F n (z n)) ρ ⊆ D n)
…

Mentions: OAI.SLEExactGauge.upperHalfPlane