Fractional moments from a linear summatory bound

theorem NairTenenbaum.arithmeticSummatory_rpow_le {a : ℕ → ℝ} (ha0 : a 0 = 0) (ha : ∀ (n : ℕ), 0 ≤ a n) {C θ x : ℝ} (hC : 0 ≤ C) (hbound : ∀ (t : ℝ), 1 ≤ t → arithmeticSummatory a t ≤ C * t) (hθ : 0 ≤ θ) (hθ1 : θ < 1) (hx : 1 ≤ x) : arithmeticSummatory (fun (n : ℕ) => a n / ↑n ^ θ) x ≤ C / (1 - θ) * x ^ (1 - θ)