ConformalCompactSausage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform sausage transport on retained compact parameter sets. Local uniform convergence supplies derivative bounds and a common positive mesh; the actual Jacobian and convex local patches supply the area comparison.

theorem OAI.SLEExactGauge.eventually_derivative_norm_bounds_on_compact line 16
theorem OAI.SLEExactGauge.eventually_image_compact_subset_open line 52

theorem OAI.SLEExactGauge.eventually_compact_sausage_transfer line 74

Source documentation

All sufficiently late conformal maps transport every interval retained in K, at every sufficiently small deterministic mesh, with common constants. The compact set itself need not be convex.

theorem eventually_compact_sausage_transfer
    (κ : ℝ) (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ)
    (hFn : ∀ n, DifferentiableOn ℂ (Fₙ n) upperHalfPlane)
    (hinj : ∀ n, InjOn (Fₙ n) upperHalfPlane)
    (hF : DifferentiableOn ℂ F upperHalfPlane)
    (hne : ∀ z ∈ upperHalfPlane, deriv F z ≠ 0)
    (hconv : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
    (K : Set ℂ) (hK : IsCompact K) (hKn : K.Nonempty) (hKH : K ⊆ upperHalfPlane)
    (R : Set ℂ) (hR : IsOpen R) (himage : F '' K ⊆ R) :
    ∃ c ell v₀ : ℝ, 0 < c ∧ 0 < ell ∧ 0 < v₀ ∧
      ∀ᶠ n in atTop, ∀ (γ : ℝ≥0 → ℂ) (s t : ℝ≥0), γ '' Icc s t ⊆ K →
        ∀ v : ℝ, 0 < v → v < v₀ →
…

Mentions: OAI.SLEExactGauge.upperHalfPlane