NormalizedConformalBounds.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Interior derivative bounds for the normalized inverse maps used to transport the dense experiment. The only input is the existing published compactness consequence for the schlicht class.

def OAI.SLEExactGauge.normalizedInteriorCompact line 16
lemma OAI.SLEExactGauge.normalizedInteriorCompact_isCompact line 19
lemma OAI.SLEExactGauge.normalizedInteriorCompact_nonempty line 30
lemma OAI.SLEExactGauge.normalizedInteriorCompact_subset_halfPlane line 37
structure OAI.SLEExactGauge.IsNormalizedHalfPlaneMap line 45
Source documentation
The interior normalization fixes the value and the derivative norm at a unit semicircle waypoint.
```
structure IsNormalizedHalfPlaneMap (s : ℝ) (F : ℂ → ℂ) (w : ℂ) : Prop where
…
```
theorem OAI.SLEExactGauge.uniform_normalized_derivative_bounds line 53

theorem OAI.SLEExactGauge.uniform_normalized_derivative_bounds_explicit line 95

Source documentation

The same bounds with the normalization hypotheses exposed individually.

theorem uniform_normalized_derivative_bounds_explicit
    (hcompact : PublishedHalfPlaneUnivalentCompactness)
    {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) :
    ∃ c C : ℝ, 0 < c ∧ 0 < C ∧
      ∀ (F : ℂ → ℂ) (w : ℂ), DifferentiableOn ℂ F upperHalfPlane →
        InjOn F upperHalfPlane → ‖w‖ = 1 → s ≤ w.im → F w = 0 →
        ‖deriv F w‖ = 1 → ∀ z : ℂ, ‖z‖ ≤ 2 → s / 2 ≤ z.im →
          c ≤ ‖deriv F z‖ ∧ ‖deriv F z‖ ≤ C := by
…

Mentions: OAI.SLEExactGauge.PublishedHalfPlaneUnivalentCompactness, OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.uniform_waypoint_derivative_ratios line 110

Source documentation

Centering and dividing by the waypoint derivative gives the relative bounds used for an arbitrary inverse chart.

theorem uniform_waypoint_derivative_ratios
    (hcompact : PublishedHalfPlaneUnivalentCompactness)
    {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) :
    ∃ c C : ℝ, 0 < c ∧ 0 < C ∧
      ∀ (F : ℂ → ℂ) (w : ℂ), DifferentiableOn ℂ F upperHalfPlane →
        InjOn F upperHalfPlane → ‖w‖ = 1 → s ≤ w.im → deriv F w ≠ 0 →
        ∀ z : ℂ, ‖z‖ ≤ 2 → s / 2 ≤ z.im →
          c * ‖deriv F w‖ ≤ ‖deriv F z‖ ∧ ‖deriv F z‖ ≤ C * ‖deriv F w‖ := by
…

Mentions: OAI.SLEExactGauge.PublishedHalfPlaneUnivalentCompactness, OAI.SLEExactGauge.upperHalfPlane