convexOn — Mathlib

English

Closed balls are convex in seminorms.

Русский

Замкнутые шары выпуклы для семинорм.

LaTeX

$$Convex ℝ (closedBall p x r)$$

Lean4

/-- A seminorm is convex. Also see `convexOn_norm`. -/
protected theorem convexOn : ConvexOn ℝ univ p :=
  by
  refine ⟨convex_univ, fun x _ y _ a b ha hb _ => ?_⟩
  calc
    p (a • x + b • y) ≤ p (a • x) + p (b • y) := map_add_le_add p _ _
    _ = ‖a • (1 : 𝕜)‖ * p x + ‖b • (1 : 𝕜)‖ * p y := by
      rw [← map_smul_eq_mul p, ← map_smul_eq_mul p, smul_one_smul, smul_one_smul]
    _ = a * p x + b * p y := by
      rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]

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