lipschitzWith_gauge — Mathlib

English

If s is convex and there exists r > 0 with B(0,r) ⊆ s, then gauge s is Lipschitz with constant 1/r (in particular, LipschitzWith(1/r) gauge s).

Русский

Если s выпуклоe и существует r > 0 с B(0,r) ⊆ s, то gauge s является липшицевой с константой 1/r.

LaTeX

$$$$\exists K>0\;\text{ such that }\mathrm{LipschitzWith}(K)\bigl(\mathrm{gauge}(s)\bigr), \quad K = r^{-1} \;\text{ при } B(0,r)\subseteq s,$$$

Lean4

theorem lipschitzWith_gauge {r : ℝ≥0} (hc : Convex ℝ s) (hr : 0 < r) (hs : Metric.ball (0 : E) r ⊆ s) :
    LipschitzWith r⁻¹ (gauge s) :=
  have : Absorbent ℝ (Metric.ball (0 : E) r) := absorbent_ball_zero hr
  LipschitzWith.of_le_add_mul _ fun x y =>
    calc
      gauge s x = gauge s (y + (x - y)) := by simp
      _ ≤ gauge s y + gauge s (x - y) := (gauge_add_le hc (this.mono hs) _ _)
      _ ≤ gauge s y + ‖x - y‖ / r := (add_le_add_left ((gauge_mono this hs (x - y)).trans_eq (gauge_ball hr.le _)) _)
      _ = gauge s y + r⁻¹ * dist x y := by rw [dist_eq_norm, div_eq_inv_mul, NNReal.coe_inv]

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