Theorem: Finset.sum_range_choose_smul_le_pow_two_smul (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
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 ≤ 2 ^ n • B
Tactic:
rw [← Nat.sum_range_choose]
State after:
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

State before:
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
Tactic:
rw [Finset.sum_smul]
State after:
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

State before:
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
Tactic:
refine Finset.sum_le_sum ?_
State after:
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 ∈ range (n + 1), Nat.choose n i • f i ≤ Nat.choose n i • B

State before:
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 ∈ range (n + 1), Nat.choose n i • f i ≤ Nat.choose n i • B
Tactic:
intro i hi
State after:
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 : ℕ
hi : i ∈ range (n + 1)
⊢ Nat.choose n i • f i ≤ Nat.choose n i • B

State before:
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 : ℕ
hi : i ∈ range (n + 1)
⊢ Nat.choose n i • f i ≤ Nat.choose n i • B
Tactic:
exact smul_le_smul_of_nonneg_left (h i hi) (Nat.zero_le _)
State after:
no goals