f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
⊢ (⨆ (i : ℕ), ∑ a in Finset.range (Nat.succ i), 2 ^ a * f (2 ^ a)) ≤ f 1 + 2 • ∑' (k : ℕ), f k
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
⊢ (∑' (k : ℕ), 2 ^ k * f (2 ^ k)) ≤ f 1 + 2 * ∑' (k : ℕ), f k
rw [ENNReal.tsum_eq_iSup_nat' (tendsto_atTop_mono Nat.le_succ tendsto_id), two_mul, ← two_nsmul]
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ a in Finset.range (Nat.succ n), 2 ^ a * f (2 ^ a) ≤ f 1 + 2 • ∑ x in Finset.Ico 2 (2 ^ n + 1), f x
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
⊢ (⨆ (i : ℕ), ∑ a in Finset.range (Nat.succ i), 2 ^ a * f (2 ^ a)) ≤ f 1 + 2 • ∑' (k : ℕ), f k
refine'
  iSup_le fun n =>
    le_trans _
      (add_le_add_left
        (nsmul_le_nsmul_of_le_right (ENNReal.sum_le_tsum <| Finset.Ico 2 (2 ^ n + 1)) _) _)
no goals
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ a in Finset.range (Nat.succ n), 2 ^ a * f (2 ^ a) ≤ f 1 + 2 • ∑ x in Finset.Ico 2 (2 ^ n + 1), f x
simpa using Finset.sum_condensed_le hf n