English
If f: E → 𝕜 is subadditive and positively homogeneous, then the sublevel sets {x : f(x) ≤ B} are convex for all B.
Русский
Если f подаддитивна и однородна по знаку, то подуровневые множества {x : f(x) ≤ B} выпуклы для всех B.
LaTeX
$$$$ \\operatorname{Convex}_{\\mathbb{K}}\\bigl( \\{ x \\in E \\mid f(x) \\le B \\} \\bigr) $$$$
Lean4
theorem Convex_subadditive_le [SMul 𝕜 E] {f : E → 𝕜} (hf1 : ∀ x y, f (x + y) ≤ (f x) + (f y))
(hf2 : ∀ ⦃c⦄ x, 0 ≤ c → f (c • x) ≤ c * f x) (B : 𝕜) : Convex 𝕜 {x | f x ≤ B} :=
by
rw [convex_iff_segment_subset]
rintro x hx y hy z ⟨a, b, ha, hb, hs, rfl⟩
calc
_ ≤ a • (f x) + b • (f y) := le_trans (hf1 _ _) (add_le_add (hf2 x ha) (hf2 y hb))
_ ≤ a • B + b • B := by gcongr <;> assumption
_ ≤ B := by rw [← add_smul, hs, one_smul]
