f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (⨆ (i : ℕ), ∑ a in Finset.range (2 ^ i), f a) ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (∑' (k : ℕ), f k) ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
rw [ENNReal.tsum_eq_iSup_nat' (Nat.tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)]
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k in Finset.range n, 2 ^ k • f (2 ^ k) ≤ ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (⨆ (i : ℕ), ∑ a in Finset.range (2 ^ i), f a) ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
refine' iSup_le fun n => (Finset.le_sum_condensed hf n).trans (add_le_add_left _ _)
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ x in Finset.range n, 2 ^ x * f (2 ^ x) ≤ ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k in Finset.range n, 2 ^ k • f (2 ^ k) ≤ ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
simp only [nsmul_eq_mul, Nat.cast_pow, Nat.cast_two]
no goals
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ x in Finset.range n, 2 ^ x * f (2 ^ x) ≤ ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
apply ENNReal.sum_le_tsum