case intro
f : ℕ → ℝ≥0
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (fun i => ↑(f i)) n ≤ (fun i => ↑(f i)) m
⊢ (Summable fun k => 2 ^ ↑k * (fun i => ↑(f i)) (2 ^ k)) ↔ Summable fun i => ↑(f i)
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable fun k => 2 ^ ↑k * f (2 ^ k)) ↔ Summable f
lift f to ℕ → ℝ≥0 using h_nonneg
case intro
f : ℕ → ℝ≥0
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable fun k => 2 ^ ↑k * ↑(f (2 ^ k))) ↔ Summable fun i => ↑(f i)
case intro
f : ℕ → ℝ≥0
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (fun i => ↑(f i)) n ≤ (fun i => ↑(f i)) m
⊢ (Summable fun k => 2 ^ ↑k * (fun i => ↑(f i)) (2 ^ k)) ↔ Summable fun i => ↑(f i)
simp only [NNReal.coe_le_coe] at *
no goals
case intro
f : ℕ → ℝ≥0
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable fun k => 2 ^ ↑k * ↑(f (2 ^ k))) ↔ Summable fun i => ↑(f i)
exact_mod_cast NNReal.summable_condensed_iff h_mono