convexOn_norm — Mathlib

English

The real-norm is convex on any convex set.

Русский

Норма на вещественном нормированном пространстве выпукла на любой выпуклой части пространства.

LaTeX

$$$\text{ConvexOn}_{\mathbb{R}}(s)\,\Rightarrow\, \text{ConvexOn}_{\mathbb{R}}(s)\,\norm$$$

Lean4

/-- The norm on a real normed space is convex on any convex set. See also `Seminorm.convexOn`
and `convexOn_univ_norm`. -/
theorem convexOn_norm (hs : Convex ℝ s) : ConvexOn ℝ s norm :=
  ⟨hs, fun x _ y _ a b ha hb _ =>
    calc
      ‖a • x + b • y‖ ≤ ‖a • x‖ + ‖b • y‖ := norm_add_le _ _
      _ = a * ‖x‖ + b * ‖y‖ := by rw [norm_smul, norm_smul, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]⟩

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