Theorem: Finset.sum_range_choose_mul_le_pow_two_mul_real (ForML/HasTemperateGrowth.lean)

State before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : ℕ → ℝ
B : ℝ
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ i in range (n + 1), ↑(Nat.choose n i) * f i ≤ ↑(2 ^ n) * B
Tactic:
simp only [← nsmul_eq_mul]
State after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : ℕ → ℝ
B : ℝ
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ x in range (n + 1), Nat.choose n x • f x ≤ 2 ^ n • B

State before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : ℕ → ℝ
B : ℝ
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ x in range (n + 1), Nat.choose n x • f x ≤ 2 ^ n • B
Tactic:
exact Finset.sum_range_choose_smul_le_pow_two_smul h
State after:
no goals