English
Gauge is subadditive: gauge s (x + y) ≤ gauge s x + gauge s y.
Русский
Гейдж-функция субаддитивна: gauge s (x + y) ≤ gauge s x + gauge s y.
LaTeX
$$$$\\mathrm{gauge}(s,x+y) \\le \\mathrm{gauge}(s,x) + \\mathrm{gauge}(s,y).$$$$
Lean4
/-- Gauge is subadditive. -/
theorem gauge_add_le (hs : Convex ℝ s) (absorbs : Absorbent ℝ s) (x y : E) : gauge s (x + y) ≤ gauge s x + gauge s y :=
by
refine le_of_forall_pos_lt_add fun ε hε => ?_
obtain ⟨a, ha, ha', x, hx, rfl⟩ := exists_lt_of_gauge_lt absorbs (lt_add_of_pos_right (gauge s x) (half_pos hε))
obtain ⟨b, hb, hb', y, hy, rfl⟩ := exists_lt_of_gauge_lt absorbs (lt_add_of_pos_right (gauge s y) (half_pos hε))
calc
gauge s (a • x + b • y) ≤ a + b :=
gauge_le_of_mem (by positivity) <| by
rw [hs.add_smul ha.le hb.le]
exact add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hy)
_ < gauge s (a • x) + gauge s (b • y) + ε := by linarith
