lipschitzWith_circleMap — Mathlib

English

The circle map is Lipschitz with constant |R|, i.e., |circleMap(c,R,θ1) − circleMap(c,R,θ2)| ≤ |R| |θ1 − θ2|.

Русский

Круговая карта липшицева с константой |R|: |circleMap(c,R,θ1) − circleMap(c,R,θ2)| ≤ |R| |θ1 − θ2|.

LaTeX

$$$|circleMap(c,R,\theta_1) - circleMap(c,R,\theta_2)| \le |R|\,|\theta_1 - \theta_2|.$$$

Lean4

theorem lipschitzWith_circleMap (c : ℂ) (R : ℝ) : LipschitzWith (Real.nnabs R) (circleMap c R) :=
  lipschitzWith_of_nnnorm_deriv_le (differentiable_circleMap _ _) fun θ => NNReal.coe_le_coe.1 <| by simp

Похожие утверждения