calc
  f (a • x + b • y) + g (a • x + b • y) ≤ a • f x + b • f y + (a • g x + b • g y) :=
    add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)
  _ = a • (f x + g x) + b • (f y + g y) := by rw [smul_add, smul_add, add_add_add_comm]
case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.692
α : Type ?u.695
β : Type u_3
ι : Type ?u.701
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y
no goals