OAI/Probability/SLE/Gauge/NormalRibbonPatch.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Fixed bi-Lipschitz constants for the normal ribbon of a unit-speed curve whose tangent changes at rate at most 1/50. This is the local analytic estimate for the explicit serpentine's straight and circular pieces.

  1. def OAI.SLEExactGauge.Serpentine.normalRibbon line 15
  2. lemma OAI.SLEExactGauge.Serpentine.curve_linear_error line 18
  3. theorem OAI.SLEExactGauge.Serpentine.normalRibbon_patch_bounds line 48

    Source documentation

    A length-four patch has fixed constants 2 in both directions.

    theorem normalRibbon_patch_bounds
    (σ tangent : ℝ → ℂ) (a b : ℝ) (hab : b - a ≤ 4)
    (hd : ∀ t ∈ Icc a b, HasDerivWithinAt σ (tangent t) (Icc a b) t)
    (hunit : ∀ t ∈ Icc a b, ‖tangent t‖ = 1)
    (hL : LipschitzOnWith (1 / 50) tangent (Icc a b))
    (z w : ℂ) (hz : z.re ∈ Icc a b ∧ |z.im| ≤ 1)
    (hw : w.re ∈ Icc a b ∧ |w.im| ≤ 1) :
    dist (normalRibbon σ tangent z) (normalRibbon σ tangent w) ≤ 2 * dist z w ∧
      dist z w ≤ 2 * dist (normalRibbon σ tangent z) (normalRibbon σ tangent w) := by
…

    Mentions: OAI.SLEExactGauge.Serpentine.normalRibbon