OAI/Probability/SLE/Gauge/SerpentineCurve.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Explicit arclength parametrization of the finite serpentine array, continued vertically along its last column.

  1. lemma OAI.SLEExactGauge.Serpentine.columnEntry_succ line 15
  2. def OAI.SLEExactGauge.Serpentine.arraySpine line 20
  3. def OAI.SLEExactGauge.Serpentine.arrayTangent line 27
  4. lemma OAI.SLEExactGauge.Serpentine.arraySpine_tail line 34
  5. lemma OAI.SLEExactGauge.Serpentine.arrayTangent_tail line 52
  6. lemma OAI.SLEExactGauge.Serpentine.arrayTangent_norm line 70
  7. lemma OAI.SLEExactGauge.Serpentine.arraySpine_hasDerivAt line 81
  8. lemma OAI.SLEExactGauge.Serpentine.arrayTangent_lipschitz line 116
  9. theorem OAI.SLEExactGauge.Serpentine.array_normal_patch_bounds line 141

    Source documentation

    Every length-four normal coordinate patch of the explicit array has uniform upper and inverse Lipschitz constants equal to two.

    theorem array_normal_patch_bounds (m j : ℕ) (k : ℝ) :
    LipschitzOnWith 2 (normalRibbon (arraySpine m j) (arrayTangent m j))
      (RibbonCoordinates.ribbonStepPatch k) ∧
    ∀ z ∈ RibbonCoordinates.ribbonStepPatch k,
      ∀ w ∈ RibbonCoordinates.ribbonStepPatch k,
        dist z w ≤ 2 * dist (normalRibbon (arraySpine m j) (arrayTangent m j) z)
          (normalRibbon (arraySpine m j) (arrayTangent m j) w) := by
…

    Mentions: OAI.SLEExactGauge.Serpentine.normalRibbon, OAI.SLEExactGauge.Serpentine.arraySpine, OAI.SLEExactGauge.Serpentine.arrayTangent, OAI.SLEExactGauge.RibbonCoordinates.ribbonStepPatch