ConformalSausageTransfer.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Deterministic conformal area and sausage transfer in rc:compact-sausage-transfer of An explicit exact Hausdorff gauge for SLE. The local patches below may depend on the sausage point; their union need not be convex.

lemma OAI.SLEExactGauge.complex_derivative_real_det line 17

theorem OAI.SLEExactGauge.conformal_area_image_lower line 24

Source documentation

An injective complex differentiable map with derivative bounded below expands area by at least the square of that lower bound.

theorem conformal_area_image_lower
    {F F' : ℂ → ℂ} {S : Set ℂ} (hS : MeasurableSet S)
    (hinj : InjOn F S) (hF : ∀ z ∈ S, HasDerivAt F (F' z) z)
    {c : ℝ} (hc : 0 ≤ c) (hbound : ∀ z ∈ S, c ≤ ‖F' z‖) :
    ENNReal.ofReal (c ^ 2) * volume S ≤ volume (F '' S) := by
…

theorem OAI.SLEExactGauge.sourceSausage_image_subset_of_lipschitz_patches line 39

Source documentation

A point in a small sausage and its witnessing trace point only need to lie in one common Lipschitz patch. No global convexity is assumed.

theorem sourceSausage_image_subset_of_lipschitz_patches
    (F : ℂ → ℂ) (γ : ℝ≥0 → ℂ) (s t : ℝ≥0)
    {v ell : ℝ} (hv : 0 < v) (C : ℝ≥0) (hscale : (C : ℝ) * ell ≤ 1)
    (hpatch : ∀ z ∈ sourceSausageSet γ s t (ell * v),
      ∃ u ∈ Icc s t, dist z (γ u) < ell * v ∧
        ∃ K : Set ℂ, z ∈ K ∧ γ u ∈ K ∧ LipschitzOnWith C F K) :
    F '' sourceSausageSet γ s t (ell * v) ⊆
      sourceSausageSet (fun u => F (γ u)) s t v := by
…

Mentions: OAI.SLEExactGauge.sourceSausageSet

theorem OAI.SLEExactGauge.sourceSausage_image_subset_of_derivative_patches line 60

Source documentation

Complex derivative bounds on convex patches give the local Lipschitz comparison required to send the small sausage into the physical sausage.

theorem sourceSausage_image_subset_of_derivative_patches
    (F F' : ℂ → ℂ) (γ : ℝ≥0 → ℂ) (s t : ℝ≥0)
    {v ell : ℝ} (hv : 0 < v) (C : ℝ≥0) (hscale : (C : ℝ) * ell ≤ 1)
    (hpatch : ∀ z ∈ sourceSausageSet γ s t (ell * v),
      ∃ u ∈ Icc s t, dist z (γ u) < ell * v ∧
        ∃ K : Set ℂ, Convex ℝ K ∧ z ∈ K ∧ γ u ∈ K ∧
          (∀ w ∈ K, HasDerivWithinAt F (F' w) K w) ∧
          (∀ w ∈ K, ‖F' w‖₊ ≤ C)) :
    F '' sourceSausageSet γ s t (ell * v) ⊆
      sourceSausageSet (fun u => F (γ u)) s t v := by
…

Mentions: OAI.SLEExactGauge.sourceSausageSet

theorem OAI.SLEExactGauge.normalized_conformal_area_lower line 78

Source documentation

Normalize the area inequality at physical mesh v, expressing the small-mesh mass at ell * v. This is the exact factor in the manuscript.

theorem normalized_conformal_area_lower
    {F F' : ℂ → ℂ} {S A : Set ℂ} (hS : MeasurableSet S)
    (hinj : InjOn F S) (hF : ∀ z ∈ S, HasDerivAt F (F' z) z)
    {c v ell p : ℝ} (hc : 0 ≤ c) (hv : 0 < v) (hell : 0 < ell)
    (hbound : ∀ z ∈ S, c ≤ ‖F' z‖) (himage : F '' S ⊆ A) :
    ENNReal.ofReal (c ^ 2 * ell ^ p) *
        (ENNReal.ofReal ((ell * v) ^ (-p)) * volume S) ≤
      ENNReal.ofReal (v ^ (-p)) * volume A := by
…

theorem OAI.SLEExactGauge.sourceSausageMass_conformal_transfer line 102

Source documentation

The physical sausage inside the retained middle region receives at least c² ell^p times the small-mesh normalized mass.

theorem sourceSausageMass_conformal_transfer
    (κ : ℝ) (F F' : ℂ → ℂ) (γ : ℝ≥0 → ℂ) (s t : ℝ≥0)
    (R : Set ℂ) {c v ell : ℝ} (hc : 0 ≤ c) (hv : 0 < v) (hell : 0 < ell)
    (hinj : InjOn F (sourceSausageSet γ s t (ell * v)))
    (hF : ∀ z ∈ sourceSausageSet γ s t (ell * v), HasDerivAt F (F' z) z)
    (hbound : ∀ z ∈ sourceSausageSet γ s t (ell * v), c ≤ ‖F' z‖)
    (C : ℝ≥0) (hscale : (C : ℝ) * ell ≤ 1)
    (hregion : F '' sourceSausageSet γ s t (ell * v) ⊆ R)
    (hpatch : ∀ z ∈ sourceSausageSet γ s t (ell * v),
      ∃ u ∈ Icc s t, dist z (γ u) < ell * v ∧
        ∃ K : Set ℂ, Convex ℝ K ∧ z ∈ K ∧ γ u ∈ K ∧
          (∀ w ∈ K, HasDerivWithinAt F (F' w) K w) ∧
…

Mentions: OAI.SLEExactGauge.sourceSausageSet