rw [Finset.sum_smul]
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
R : Type u_3
inst✝¹ : OrderedAddCommMonoid R
inst✝ : OrderedSMul ℕ R
n : ℕ
f : ℕ → R
B : R
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ i in range (n + 1), Nat.choose n i • f i ≤ (∑ m in range (n + 1), Nat.choose n m) • B
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
R : Type u_3
inst✝¹ : OrderedAddCommMonoid R
inst✝ : OrderedSMul ℕ R
n : ℕ
f : ℕ → R
B : R
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ i in range (n + 1), Nat.choose n i • f i ≤ ∑ i in range (n + 1), Nat.choose n i • B